content: = Hilbert Systems =
  
  (link:index.html?a=1&p=hilbert[Try this prover online]!)
  
  Most
  https://en.wikipedia.org/wiki/Computer-assisted_proof#Philosophical_objections[objections
  to computer-assisted proofs] are themselves objectionable. However, one
  concern is valid: how can a program prove a theorem correctly if its source
  code is complex and therefore likely riddled with bugs?
  
  Take the first proof of https://en.wikipedia.org/wiki/Four_color_theorem[the
  four colour map theorem], which relied upon a one-off program written in IBM
  370 assembly to tediously check numerous cases. Do we believe it did its job
  perfectly? Could there be, say, an off-by-one bug in some loop that causes it
  to skip a case that actually requires 5 colours?
  
  How about our link:fol.html[MESON prover for first-order logic]? Are there
  really no bugs in our code?
  
  https://en.wikipedia.org/wiki/Logic_for_Computable_Functions[The LCF theorem
  prover] pioneered a solution to this problem: develop a core module that
  exports a few functions which provide the only ways to create theorems. These
  functions correspond to the laws of logic.
  
  If this core module is correctly implemented, the rest of our program can be
  buggy, yet still produce only correct theorems because ultimately it is forced
  to obey the core's rules of inference.
  
  This is a proven approach in software engineering. For instance, a red-black
  tree module typically exports functions that maintain particular invariants,
  such as ensuring a tree is always approximately balanced and is a binary search
  tree. No matter how we call the exported functions, these invariants always hold.
  
  == Prelude ==
  
  We write a theorem prover that our bootstrapped compiler can build.
  
  We start with definitions that are normally at our fingertips thanks to `Prelude`:
  
  ++++++++++
  <script>
  function hideshow(s) {
    var x = document.getElementById(s);
    if (x.style.display === "none") {
      x.style.display = "block";
    } else {
      x.style.display = "none";
    }
  }
  </script>
  <p><a onclick='hideshow("prelude");'>&#9654; Toggle prelude</a></p>
  <div id='prelude' style='display:none'>
  ++++++++++
  
  \begin{code}
  infixr 9 .
  infixl 7 *
  infixl 6 + , -
  infixr 5 ++
  infixl 4 <*>
  infix 4 == , <=
  infixl 3 &&
  infixl 2 ||
  infixl 1 >> , >>=
  infixr 0 $
  
  foreign import ccall "putchar" putChar :: Int -> IO Int
  
  class Functor f where fmap :: (a -> b) -> f a -> f b
  class Applicative f where
    pure :: a -> f a
    (<*>) :: f (a -> b) -> f a -> f b
  class Monad m where
    return :: a -> m a
    (>>=) :: m a -> (a -> m b) -> m b
  instance Applicative IO where
    pure = ioPure
    f <*> x = ioBind f \g -> ioBind x \y -> ioPure (g y)
  instance Monad IO where return = ioPure ; (>>=) = ioBind
  instance Functor IO where fmap f x = ioPure f <*> x
  f >> g = f >>= \_ -> g
  f $ x = f x
  f || g = if f then True else g
  f && g = if f then g else False
  flst xs n c = case xs of [] -> n; (:) h t -> c h t
  foldr c n l = flst l n (\h t -> c h(foldr c n t))
  zipWith f xs ys = flst xs [] $ \x xt -> flst ys [] $ \y yt -> f x y : zipWith f xt yt
  any f xs = foldr (\x a -> f x || a) False xs
  not a = case a of True -> False; False -> True
  f . g = \x -> f (g x)
  id x = x
  flip f x y = f y x
  (++) = flip (foldr (:))
  concat = foldr (++) []
  map = flip (foldr . ((:) .)) []
  mapM_ f = foldr ((>>) . f) (pure ())
  putStr = mapM_ $ putChar . ord
  error s = unsafePerformIO $ putStr s >> putChar (ord '\n') >> exitSuccess
  undefined = error "undefined"
  intersperse x as = flst as [] \a at -> a : foldr (\h t -> [x, h] ++ t) [] at
  null [] = True
  null _  = False
  
  class Eq a where (==) :: a -> a -> Bool
  instance Eq Int where (==) = intEq
  instance Eq Char where (==) = charEq
  instance Eq a => Eq [a] where
    xs == ys = case xs of
      [] -> case ys of
        [] -> True
        (:) _ _ -> False
      x:xt -> case ys of
        [] -> False
        y:yt -> x == y && xt == yt
  
  class Show a where
    showsPrec :: Int -> a -> String -> String
    showsPrec _ x = (show x++)
    show :: a -> String
    show x = shows x ""
  
  shows = showsPrec 0
  showParen b f = if b then ('(':) . f . (')':) else f
  
  (<=) = intLE
  x > y = y <= x && not (y == x)
  \end{code}
  
  ++++++++++
  </div>
  ++++++++++
  
  == Terms, Formulas, Theorems ==
  
  We define data types for terms and first-order formulas. This time, we
  avoid recursion schemes: our compiler can handle them, but lacks support for
  pattern synonyms and deriving `Functor`.
  
  \begin{code}
  data Term = Var String | Fun String [Term] deriving Eq
  
  data FO = Top | Bot | Atom String [Term]
    | Not FO | FO :/\ FO | FO :\/ FO | FO :==> FO | FO :<=> FO
    | Forall String FO | Exists String FO
    deriving Eq
  \end{code}
  
  A value of type `Theorem` should only exist if it contains a valid formula.
  Only functions corresponding to the rules of inference or axiom schema should
  be able to create `Theorem` values.
  
  \begin{code}
  data Theorem = Theorem FO
  \end{code}
  
  Functions for pretty-printing:
  
  \begin{code}
  instance Show Term where
    showsPrec _ = \case
      Var s -> (s ++)
      Fun s ts -> (s ++) . showParen (not $ null ts)
        (foldr (.) id $ intersperse (", "++) $ map shows ts)
  
  instance Show FO where
    showsPrec p = \case
      Top -> ('1':)
      Bot -> ('0':)
      Atom s ts -> shows $ Fun s ts
      Not x -> ('~':) . showsPrec 4 x
      x :/\ y -> showParen (p > 3) $ showsPrec 3 x . (" /\\ " ++) . showsPrec 3 y
      x :\/ y -> showParen (p > 2) $ showsPrec 2 x . (" \\/ " ++) . showsPrec 2 y
      x :==> y -> showParen (p > 1) $ showsPrec 2 x . (" ==> " ++) . showsPrec 1 y
      x :<=> y -> showParen (p > 1) $ showsPrec 2 x . (" <=> " ++) . showsPrec 1 y
      Forall s x -> showParen (p > 0) $ ("forall " ++) . (s++) . (". "++) . showsPrec 0 x
      Exists s x -> showParen (p > 0) $ ("exists " ++) . (s++) . (". "++) . showsPrec 0 x
  \end{code}
  
  == Rules and Axioms ==
  
  We follow along chapter 6 of John Harrison's 'Handbook of Practical Logic and
  Automated Reasoning'.
  
  We need a helper function to determine if a given variable appears in a term:
  
  \begin{code}
  occurs s t = s == t || case t of
    Var _ -> False
    Fun _ args -> any (occurs s) args
  \end{code}
  
  And another to determine if a given variable is free in a formula:
  
  \begin{code}
  isFree t = \case
    Top -> False
    Bot -> False
    Atom _ ts -> any (occurs t) ts
    Not x -> isFree t x
    x :/\ y -> isFree t x || isFree t y
    x :\/ y -> isFree t x || isFree t y
    x :==> y -> isFree t x || isFree t y
    x :<=> y -> isFree t x || isFree t y
    Forall v x -> not (occurs (Var v) t) && isFree t x
    Exists v x -> not (occurs (Var v) t) && isFree t x
  \end{code}
  
  A dash of syntax sugar to make constructing equalities prettier in our code:
  
  \begin{code}
  s =: t = Atom "=" [s, t]
  \end{code}
  
  The two rules of inference are modus ponens and generalization:
  
  \begin{code}
  ponens (Theorem (p :==> q)) (Theorem p') | p == p' = Theorem q
  gen x (Theorem t) = Theorem $ Forall x t
  \end{code}
  
  Now for the axioms (cf.
  https://en.wikipedia.org/wiki/Hilbert_system#Logical_axioms[Wikipedia's article
  on Hilbert systems]). Our propositional fragment is built from implication and
  falsehood, so we start with the S and K combinators, and the law of the
  excluded middle (LEM). Then we add a few rules for quantified variables and a
  few for equality.
  
  \begin{code}
  axiomK p q        = Theorem $ p :==> (q :==> p)
  axiomS p q r      = Theorem $ (p :==> (q :==> r)) :==> ((p :==> q) :==> (p :==> r))
  axiomLEM p        = Theorem $ ((p :==> Bot) :==> Bot) :==> p
  axiomAllImp x p q = Theorem $ Forall x (p :==> q) :==> (Forall x p :==> Forall x q)
  axiomImpAll x p | isFree (Var x) p = Theorem $ p :==> Forall x p
  axiomExEq x t | occurs (Var x) t = Theorem $ Exists x $ Var x =: t
  axiomRefl t       = Theorem $ t =: t
  axiomFunCong  f ls rs = Theorem $ foldr (:==>) (Fun f ls =: Fun f rs) $ zipWith (=:) ls rs
  axiomPredCong p ls rs = Theorem $ foldr (:==>) (Atom p ls :==> Atom p rs) $ zipWith (=:) ls rs
  \end{code}
  
  In theory, we could write all our formulas with just implication, falsehood and
  the universal quantifier, but for our sanity's sake we support all the popular
  connectives:
  
  \begin{code}
  axiomIffImp1 p q = Theorem $ (p :<=> q) :==> (p :==> q)
  axiomIffImp2 p q = Theorem $ (p :<=> q) :==> (q :==> p)
  axiomImpIff p q  = Theorem $ (p :==> q) :==> ((q :==> p) :==> (p :<=> q))
  axiomTrue        = Theorem $ Top :<=> (Bot :==> Bot)
  axiomNot p       = Theorem $ Not p :<=> (p :==> Bot)
  axiomAnd p q     = Theorem $ (p :/\ q) :<=> ((p :==> (q :==> Bot)) :==> Bot)
  axiomOr p q      = Theorem $ (p :\/ q) :<=> Not (Not p :/\ Not q)
  axiomExists x p  = Theorem $ Exists x p :<=> Not (Forall x $ Not p)
  \end{code}
  
  We're done! We have built an interactive theorem prover.
  
  Well, we would have if we had a REPL (though edit-compile-run is tolerable) and
  if our compiler supported modules: the `Theorem` data constructor should never
  be used again, and modules would enforce this. (Ideally we'd also provide a
  unidirectional pattern synonym for matching purposes.)
  
  Instead, we must rely on the honour system: from now on, `Theorem` may only
  appear when pattern matching.
  
  == Calculemus! ==
  
  We prove theorems and derive rules:
  
  \begin{code}
  -- |-  p ==> p
  impRefl p = ponens (ponens
    (axiomS p (p :==> p) p)
    (axiomK p $ p :==> p))
    (axiomK p p)
  
  -- |- p ==> p ==> q  /  |- p ==> q
  impDedup th@(Theorem (p :==> (_ :==> q))) = ponens (ponens (axiomS p p q) th) (impRefl p)
  
  -- |- q  /  |- p ==> q
  addAssum p th@(Theorem f) = ponens (axiomK f p) th
  
  -- |- q ==> r  /  |- (p ==> q) ==> (p ==> r)
  impAddAssum p th@(Theorem (q :==> r)) = ponens (axiomS p q r) (addAssum p th)
  
  -- |- p ==> q  |- q ==> r  /  |- p ==> r
  impTrans th1@(Theorem (p :==> _)) th2 = ponens (impAddAssum p th2) th1
  
  -- |- p ==> r  /  |- p ==> q ==> r
  impInsert q th@(Theorem (p :==> r)) = impTrans th (axiomK r q)
  
  -- |- p ==> q ==> r  /  |- q ==> p ==> r
  impSwap th@(Theorem (p :==> (q :==> r))) = impTrans (axiomK q p) $ ponens (axiomS p q r) th
  
  -- |- (q ==> r) ==> (p ==> q) ==> (p ==> r)
  impTransTh p q r = impTrans (axiomK (q :==> r) p) (axiomS p q r)
  
  -- |- p ==> q  /  |- (p ==> r) ==> (q ==> r)
  impAddConcl r th@(Theorem (p :==> q)) = ponens (impSwap (impTransTh p q r)) th
  
  -- |- (p ==> q ==> r) ==> (q ==> p ==> r)
  impSwapTh p q r = impTrans (axiomS p q r) $ impAddConcl (p :==> r) $ axiomK q p
  
  -- |- (p ==> q ==> r) ==> (s ==> t ==> u)  /  |- (q ==> p ==> r) ==> (t ==> s ==> u)
  impSwap2 th@(Theorem ((p :==> (q :==> r)) :==> (s :==> (t :==> u))))
    = impTrans (impSwapTh q p r) (impTrans th (impSwapTh s t u))
  
  -- |- p ==> q ==> r  |- p ==> q  /  |- p ==> r
  rightMP ith th = impDedup (impTrans th (impSwap ith))
  
  -- |- p <=> q  /  |- p ==> q
  iffImp1 th@(Theorem (p :<=> q)) = ponens (axiomIffImp1 p q) th
  
  -- |- p <=> q  /  |- q ==> p
  iffImp2 th@(Theorem (p :<=> q)) = ponens (axiomIffImp2 p q) th
  
  -- |- p ==> q  |- q ==> p  /  |- p <=> q
  impAntisym th1@(Theorem (p :==> q)) th2 = ponens (ponens (axiomImpIff p q) th1) th2
  
  -- |- p ==> (q ==> 0) ==> 0  /  |- p ==> q
  rightDoubleNeg th@(Theorem (p :==> ((_ :==> Bot) :==> Bot))) = impTrans th $ axiomLEM p
  
  -- |- 0 ==> p
  exFalso p = rightDoubleNeg $ axiomK Bot (p :==> Bot)
  
  -- |- 1
  truth = ponens (iffImp2 axiomTrue) (impRefl Bot)
  
  -- |- s = t ==> t = s
  eqSym s t = let
    rth = axiomRefl s
    f th = ponens (impSwap th) rth
    in f $ f $ axiomPredCong "=" [s, s] [t, s]
  
  -- |- s = t ==> t = u ==> s = u
  eqTrans s t u = let
    th1 = axiomPredCong "=" [t, u] [s, u]
    th2 = ponens (impSwap th1) (axiomRefl u)
    in impTrans (eqSym s t) th2
  
  examples =
    [ axiomOr (Atom "x" []) (Atom "y" [])
    , impTransTh (Atom "Foo" []) (Atom "Bar" []) (Atom "Baz" [])
    , eqSym (Var "a") (Var "b")
    , eqTrans (Var "x") (Var "y") (Var "z")
    ]
  
  concl (Theorem t) = t
  main = mapM_ (putStr . flip shows "\n" . concl) examples
  \end{code}
  