From da038b29cf37da5f323fb089d14bee97bef60517 Mon Sep 17 00:00:00 2001 From: William Ball Date: Sun, 11 Aug 2024 14:54:43 -0700 Subject: [PATCH] good start --- .gitignore | 3 + .../wball/proof-checker/FORMULA.sig | 17 ++ .../wball/proof-checker/Formula.sml | 35 +++ .../wball/proof-checker/PROOF.sig | 28 +++ .../wball/proof-checker/Proof.sml | 225 ++++++++++++++++++ .../wball/proof-checker/TERM.sig | 10 + .../wball/proof-checker/Term.sml | 16 ++ .../wball/proof-checker/proof-checker.mlb | 9 + sml.pkg | 5 + 9 files changed, 348 insertions(+) create mode 100644 .gitignore create mode 100644 lib/forgejo.ballcloud.cc/wball/proof-checker/FORMULA.sig create mode 100644 lib/forgejo.ballcloud.cc/wball/proof-checker/Formula.sml create mode 100644 lib/forgejo.ballcloud.cc/wball/proof-checker/PROOF.sig create mode 100644 lib/forgejo.ballcloud.cc/wball/proof-checker/Proof.sml create mode 100644 lib/forgejo.ballcloud.cc/wball/proof-checker/TERM.sig create mode 100644 lib/forgejo.ballcloud.cc/wball/proof-checker/Term.sml create mode 100644 lib/forgejo.ballcloud.cc/wball/proof-checker/proof-checker.mlb create mode 100644 sml.pkg diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..2d1e3a2 --- /dev/null +++ b/.gitignore @@ -0,0 +1,3 @@ +**/*.du +**/*.ud +lib/github.com/* diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/FORMULA.sig b/lib/forgejo.ballcloud.cc/wball/proof-checker/FORMULA.sig new file mode 100644 index 0000000..3a74788 --- /dev/null +++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/FORMULA.sig @@ -0,0 +1,17 @@ +signature FORMULA = +sig + datatype t = + Named of string + | Relation of string * Term.t list + | Equal of Term.t * Term.t + | Bottom + | Neg of t + | Conj of t * t + | Disj of t * t + | Impl of t * t + | Iff of t * t + | Forall of t + | Exists of t + + val eq: t * t -> bool +end diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/Formula.sml b/lib/forgejo.ballcloud.cc/wball/proof-checker/Formula.sml new file mode 100644 index 0000000..e2bd3b1 --- /dev/null +++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/Formula.sml @@ -0,0 +1,35 @@ +structure Formula: FORMULA = +struct + datatype t = + Named of string + | Relation of string * Term.t list + | Equal of Term.t * Term.t + | Bottom + | Neg of t + | Conj of t * t + | Disj of t * t + | Impl of t * t + | Iff of t * t + | Forall of t + | Exists of t + + fun eq (Named s1, Named s2) = s1 = s2 + | eq (Relation (r, ts), Relation (p, ss)) = + (r = p andalso List.all Term.eq (ListPair.zip (ts, ss)) + handle unequalLengths => false) + | eq (Equal (t, s), Equal (t', s')) = + Term.eq (t, t') andalso Term.eq (s, s') + | eq (Bottom, Bottom) = true + | eq (Neg phi, Neg psi) = eq (phi, psi) + | eq (Conj (phi, psi), Conj (phi', psi')) = + eq (phi, phi') andalso eq (psi, psi') + | eq (Disj (phi, psi), Disj (phi', psi')) = + eq (phi, phi') andalso eq (psi, psi') + | eq (Impl (phi, psi), Impl (phi', psi')) = + eq (phi, phi') andalso eq (psi, psi') + | eq (Iff (phi, psi), Iff (phi', psi')) = + eq (phi, phi') andalso eq (psi, psi') + | eq (Forall phi, Forall psi) = eq (phi, psi) + | eq (Exists phi, Exists psi) = eq (phi, psi) + | eq _ = false +end diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/PROOF.sig b/lib/forgejo.ballcloud.cc/wball/proof-checker/PROOF.sig new file mode 100644 index 0000000..3a776de --- /dev/null +++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/PROOF.sig @@ -0,0 +1,28 @@ +signature PROOF = +sig + datatype label = + Axiom + | AndI + | AndE + | OrI + | OrE + | ArrI + | ArrE + | NegI + | NegE + | RAA + | IffI + | IffE + | EqI + | EqE + | ForAllI + | ForAllE + | ExistsI + | ExistsE + + exception ProofError of int + + datatype t = Proof of {children: t list, label: label, formula: Formula.t} + + val valid: t * Formula.t list -> bool +end diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/Proof.sml b/lib/forgejo.ballcloud.cc/wball/proof-checker/Proof.sml new file mode 100644 index 0000000..a824fe0 --- /dev/null +++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/Proof.sml @@ -0,0 +1,225 @@ +structure Proof: PROOF = +struct + datatype label = + Axiom + | AndI + | AndE + | OrI + | OrE + | ArrI + | ArrE + | NegI + | NegE + | RAA + | IffI + | IffE + | EqI + | EqE + | ForAllI + | ForAllE + | ExistsI + | ExistsE + + exception ProofError of int + + datatype t = Proof of {children: t list, label: label, formula: Formula.t} + + local open Formula + in + infix eq + fun valid + ( Proof + { children = + kids as + [Proof {formula = phi, ...}, Proof {formula = psi, ...}] + , label = AndI + , formula = Conj (phi', psi') + } + , a + ) = + phi eq phi' andalso psi eq psi' + andalso List.all (fn k => valid (k, a)) kids + | valid + ( Proof + { children = [kid as Proof {formula = Conj (phi, psi), ...}] + , label = AndE + , formula = chi + } + , a + ) = + chi eq phi orelse chi eq psi andalso valid (kid, a) + | valid (Proof {children = [], label = Axiom, formula = phi}, a) = + let + fun mem (phi, []) = false + | mem (phi, x :: xs) = + phi eq x orelse mem (phi, xs) + in + mem (phi, a) + end + | valid + ( Proof + { children = [kid as Proof {formula = phi, ...}] + , label = OrI + , formula = Disj (psi, chi) + } + , a + ) = + (phi eq psi orelse phi eq chi) andalso valid (kid, a) + | valid + ( Proof + { children = + [ left as Proof {formula = Disj (phi, psi), ...} + , mid as Proof {formula = chi, ...} + , right as Proof {formula = chi', ...} + ] + , label = OrE + , formula = chi'' + } + , a + ) = + chi eq chi' andalso chi' eq chi'' andalso valid (left, a) + andalso valid (mid, phi :: a) andalso valid (right, psi :: a) + | valid + ( Proof + { children = [kid as Proof {formula = psi, ...}] + , label = ArrI + , formula = Impl (phi, psi') + } + , a + ) = + psi eq psi' andalso valid (kid, phi :: a) + | valid + ( Proof + { children = + [ left as Proof {formula = Impl (phi, psi), ...} + , right as Proof {formula = phi', ...} + ] + , label = ArrE + , formula = psi' + } + , a + ) = + phi eq phi' andalso psi eq psi' andalso valid (left, a) + andalso valid (right, a) + | valid + ( Proof + { children = [kid as Proof {formula = Bottom, ...}] + , label = NegI + , formula = Neg phi + } + , a + ) = + valid (kid, phi :: a) + | valid + ( Proof + { children = + [ left as Proof {formula = Neg phi, ...} + , right as Proof {formula = phi', ...} + ] + , label = NegE + , formula = Bottom + } + , a + ) = + phi eq phi' andalso valid (left, a) andalso valid (right, a) + | valid + ( Proof + { children = [kid as Proof {formula = Bottom, ...}] + , label = RAA + , formula = phi + } + , a + ) = + valid (kid, Neg phi :: a) + | valid + ( Proof + { children = + [ left as Proof {formula = Impl (phi, psi), ...} + , right as Proof {formula = Impl (psi', phi'), ...} + ] + , label = IffI + , formula = Iff (phi'', psi'') + } + , a + ) = + phi eq phi' andalso phi' eq phi'' andalso psi eq psi' + andalso psi' eq psi'' andalso valid (left, a) andalso valid (right, a) + | valid + ( Proof + { children = [kid as Proof {formula = Iff (phi, psi), ...}] + , label = IffE + , formula = Impl (p, q) + } + , a + ) = + ((phi eq p andalso psi eq q) orelse (phi eq q andalso psi eq p)) + andalso valid (kid, a) + | valid (Proof {children = [], label = EqI, formula = Equal (t, t')}, a) = + Term.eq (t, t') + (* | valid *) + (* ( Proof *) + (* { children = *) + (* [ left as Proof {formula = Equal (t, s), ...} *) + (* , right as Proof {formula = phi, ...} *) + (* ] *) + (* , label = EqE *) + (* , formula = psi *) + (* } *) + (* , a *) + (* ) = *) + (* valid (left, a) andalso valid (right, a) *) + (* andalso Formula.checkSubst (t, s) (phi, psi) *) + (* | valid *) + (* ( Proof *) + (* { children = [kid as Proof {formula = Forall (x, phi), ...}] *) + (* , label = ForAllE *) + (* , formula = psi *) + (* } *) + (* , a *) + (* ) = *) + (* valid (kid, a) *) + (* andalso *) + (* (case Formula.matchVariable x (phi, psi) of *) + (* _ => true handle MatchFailure => false) *) + (* | valid *) + (* ( Proof *) + (* { children = [kid as Proof {formula = phi, ...}] *) + (* , label = ExistsI *) + (* , formula = Exist (x, psi) *) + (* } *) + (* , a *) + (* ) = *) + (* valid (kid, a) *) + (* andalso *) + (* (case Formula.matchVariable x (psi, phi) of *) + (* _ => true handle MatchFailure => false) *) + (* | valid *) + (* ( Proof *) + (* { children = [kid as Proof {formula = phi, ...}] *) + (* , label = ForAllI *) + (* , formula = Forall (x, psi) *) + (* } *) + (* , a *) + (* ) = *) + (* valid (kid, a) *) + (* andalso *) + (* (case Formula.matchVariable x (psi, phi) of *) + (* SOME (t as Term.Var x') => *) + (* Var.eq (x, x') andalso not (List.exists (Formula.occurs t) a) *) + (* | _ => false handle MatchFailure => false) *) + (* | valid *) + (* ( Proof *) + (* { children = *) + (* [ left as Proof {formula = Exist (x, phi), ...} *) + (* , right as Proof {formula = chi, ...} *) + (* ] *) + (* , label = ExistsE *) + (* , formula = chi' *) + (* } *) + (* , a *) + (* ) = *) + (* valid (left, a) andalso valid (right, phi :: a) *) + (* andalso not (List.exists (Formula.occurs (Term.Var x)) a) *) + (* | valid _ = false *) + end +end diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/TERM.sig b/lib/forgejo.ballcloud.cc/wball/proof-checker/TERM.sig new file mode 100644 index 0000000..78d2d07 --- /dev/null +++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/TERM.sig @@ -0,0 +1,10 @@ +signature TERM = +sig + datatype t = + Var of int (* de Bruijn index *) + | Const of string + | Free of string + | Function of string * t list + + val eq: t * t -> bool +end diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/Term.sml b/lib/forgejo.ballcloud.cc/wball/proof-checker/Term.sml new file mode 100644 index 0000000..c22165c --- /dev/null +++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/Term.sml @@ -0,0 +1,16 @@ +structure Term: TERM = +struct + datatype t = + Var of int + | Const of string + | Free of string + | Function of string * t list + + fun eq (Var x1, Var x2) = x1 = x2 + | eq (Const s1, Const s2) = s1 = s2 + | eq (Free s1, Free s2) = s1 = s2 + | eq (Function (f1, args1), Function (f2, args2)) = + (f1 = f2 andalso List.all eq (ListPair.zip (args1, args2)) + handle unequalLengths => false) + | eq _ = false +end diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/proof-checker.mlb b/lib/forgejo.ballcloud.cc/wball/proof-checker/proof-checker.mlb new file mode 100644 index 0000000..d0b4bbf --- /dev/null +++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/proof-checker.mlb @@ -0,0 +1,9 @@ +$(SML_LIB)/basis/basis.mlb +../../../github.com/diku-dk/sml-parse/parse.mlb +../../../github.com/diku-dk/sml-parse/simple_token.mlb +TERM.sig +Term.sml +FORMULA.sig +Formula.sml +PROOF.sig +Proof.sml diff --git a/sml.pkg b/sml.pkg new file mode 100644 index 0000000..b3e735f --- /dev/null +++ b/sml.pkg @@ -0,0 +1,5 @@ +package forgejo.ballcloud.cc/wball/proof-checker + +require { + github.com/diku-dk/sml-parse 0.1.5 #5693148ec0e4cbba1a1664170d9814f3b63267d9 +}