```
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)
```

# Hilbert Systems

Most 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 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 MESON prover for first-order logic? Are there really no bugs in our code?

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`

:

## 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`

.

```
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
```

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.

`data Theorem = Theorem FO`

Functions for pretty-printing:

```
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
```

## 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:

```
occurs s t = s == t || case t of
Var _ -> False
Fun _ args -> any (occurs s) args
```

And another to determine if a given variable is free in a formula:

```
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
```

A dash of syntax sugar to make constructing equalities prettier in our code:

`s =: t = Atom "=" [s, t]`

The two rules of inference are modus ponens and generalization:

```
ponens (Theorem (p :==> q)) (Theorem p') | p == p' = Theorem q
gen x (Theorem t) = Theorem $ Forall x t
```

Now for the axioms (cf. 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.

```
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
```

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:

```
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)
```

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:

```
-- |- 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
```

*blynn@cs.stanford.edu*💡