infixr 9 . infixl 7 * infixl 6 + , - infixr 5 ++ infixl 4 <*> infix 4 == , <= infixl 3 && infixl 2 || infixl 1 >> , >>= infixr 0 $ ffi "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)
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.
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.
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