--
-- **Etog** is a toy LCF-style theorem prover for the
-- equational theory of groups, written in Simple Haskell.
--
-- The "trusted kernel" is in this file and is less than 100
-- lines of code. It does not contain any fancy types, monads,
-- infinite lists, or anything like that.
--
-- Some example proofs can be found in `EtogDemo.hs`, including
-- a proof of the elementary "socks and shoes" theorem:
--
-- (a * b)^-1 = b^-1 * a^-1
--
-- ...first in a very verbose form, and then with variations.
--
-- SPDX-FileCopyrightText: Chris Pressey, the original author of this work, has dedicated it to the public domain.
-- For more information, please refer to <https://unlicense.org/>
-- SPDX-License-Identifier: Unlicense
--
module Etog (
Expr(Ident, Mul, Inv, Var), check,
reflex, symm, trans, subst, leibniz,
assocL, assocR,
identIntroL, identIntroR, identElimL, identElimR,
invIntroL, invIntroR, invElimL, invElimR
) where
--
-- Definitions
--
type VarName = String
data Expr = Ident
| Mul Expr Expr
| Inv Expr
| Var VarName
deriving (Ord, Eq)
instance Show Expr where
show Ident = "e"
show (Mul a b) = "(" ++ (show a) ++ "*" ++ (show b) ++ ")"
show (Inv a) = "~" ++ (show a)
show (Var n) = n
data Theorem = Thm Expr Expr
deriving (Ord, Eq)
instance Show Theorem where
show (Thm a b) = (show a) ++ "=" ++ (show b)
--
-- Primitive operations
--
substExpr :: Expr -> VarName -> Expr -> Expr
substExpr Ident _ _ = Ident
substExpr (Mul e1 e2) v ex = Mul (substExpr e1 v ex) (substExpr e2 v ex)
substExpr (Inv e1) v ex = Inv (substExpr e1 v ex)
substExpr e1@(Var s) v ex = if s == v then ex else e1
update :: (Expr -> Expr) -> [Int] -> Theorem -> Theorem
update f (1:index) (Thm lhs rhs) = Thm (updateExpr f index lhs) rhs
update f (2:index) (Thm lhs rhs) = Thm lhs (updateExpr f index rhs)
updateExpr f [] t = f t
updateExpr f (1:index) (Mul x y) = Mul (updateExpr f index x) y
updateExpr f (2:index) (Mul x y) = Mul x (updateExpr f index y)
updateExpr f (1:index) (Inv x) = Inv (updateExpr f index x)
--
-- Axioms and Rules of Inference of Equational Logic
--
reflex :: Expr -> Theorem
reflex e = Thm e e
symm :: Theorem -> Theorem
symm (Thm a b) = Thm b a
trans :: Theorem -> Theorem -> Theorem
trans (Thm p q1) (Thm q2 r) = if q1 == q2 then (Thm p r) else error "not transitive"
subst :: Expr -> VarName -> Theorem -> Theorem
subst e v (Thm p q) = Thm (substExpr p v e) (substExpr q v e)
leibniz :: Expr -> VarName -> Theorem -> Theorem
leibniz e v (Thm p q) = Thm (substExpr e v p) (substExpr e v q)
--
-- Axioms of Group Theory
--
assocL = update $ \(Mul (Mul x y) z) -> Mul x (Mul y z)
assocR = update $ \(Mul x (Mul y z)) -> Mul (Mul x y) z
identIntroL = update $ \x -> Mul Ident x
identIntroR = update $ \x -> Mul x Ident
identElimL = update $ \(Mul Ident x) -> x
identElimR = update $ \(Mul x Ident) -> x
invIntroL n = update $ \Ident -> Mul (Inv (Var n)) (Var n)
invIntroR n = update $ \Ident -> Mul (Var n) (Inv (Var n))
invElimL = update $ \(Mul (Inv x1) x2) -> if x1 == x2 then Ident else error "not inverse"
invElimR = update $ \(Mul x1 (Inv x2)) -> if x1 == x2 then Ident else error "not inverse"
--
-- Helpers
--
check thm expected =
let
errMsg = "expected '" ++ expected ++ "' but derived '" ++ (show thm) ++ "'"
in
if (show thm) == expected then thm else error errMsg