From c1c25e643b16aa03e74bf695095a7ad5aca76ff5 Mon Sep 17 00:00:00 2001 From: William Ball Date: Sun, 11 Aug 2024 16:41:51 -0700 Subject: [PATCH] basic proof checking completed? --- .../wball/proof-checker/FORMULA.sig | 10 +- .../wball/proof-checker/Formula.sml | 65 +++++++- .../wball/proof-checker/PROOF.sig | 6 +- .../wball/proof-checker/Proof.sml | 143 +++++++++--------- .../wball/proof-checker/TERM.sig | 11 ++ .../wball/proof-checker/Term.sml | 45 ++++++ 6 files changed, 200 insertions(+), 80 deletions(-) diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/FORMULA.sig b/lib/forgejo.ballcloud.cc/wball/proof-checker/FORMULA.sig index 3a74788..c79c6a2 100644 --- a/lib/forgejo.ballcloud.cc/wball/proof-checker/FORMULA.sig +++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/FORMULA.sig @@ -1,8 +1,7 @@ signature FORMULA = sig datatype t = - Named of string - | Relation of string * Term.t list + Relation of string * Term.t list | Equal of Term.t * Term.t | Bottom | Neg of t @@ -14,4 +13,11 @@ sig | Exists of t val eq: t * t -> bool + + val checkSubst: Term.t * Term.t -> t * t -> bool + + exception MatchFailure + val matchVariable: int -> t * t -> Term.t option + + val occurs: Term.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 index e2bd3b1..8671b21 100644 --- a/lib/forgejo.ballcloud.cc/wball/proof-checker/Formula.sml +++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/Formula.sml @@ -1,8 +1,7 @@ structure Formula: FORMULA = struct datatype t = - Named of string - | Relation of string * Term.t list + Relation of string * Term.t list | Equal of Term.t * Term.t | Bottom | Neg of t @@ -13,8 +12,7 @@ struct | Forall of t | Exists of t - fun eq (Named s1, Named s2) = s1 = s2 - | eq (Relation (r, ts), Relation (p, ss)) = + fun 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')) = @@ -32,4 +30,63 @@ struct | eq (Forall phi, Forall psi) = eq (phi, psi) | eq (Exists phi, Exists psi) = eq (phi, psi) | eq _ = false + + fun checkSubst sub (Relation (r, ts), Relation (p, ss)) = + r = p + andalso + List.all (fn x => x) (map (Term.checkSubst sub) (ListPair.zip (ts, ss))) + | checkSubst sub (Equal (t, s), Equal (t', s')) = + Term.checkSubst sub (t, t') andalso Term.checkSubst sub (s, s') + | checkSubst sub (Bottom, Bottom) = true + | checkSubst sub (Neg phi, Neg psi) = checkSubst sub (phi, psi) + | checkSubst sub (Conj (phi, psi), Conj (phi', psi')) = + checkSubst sub (phi, phi') andalso checkSubst sub (psi, psi') + | checkSubst sub (Disj (phi, psi), Disj (phi', psi')) = + checkSubst sub (phi, phi') andalso checkSubst sub (psi, psi') + | checkSubst sub (Impl (phi, psi), Impl (phi', psi')) = + checkSubst sub (phi, phi') andalso checkSubst sub (psi, psi') + | checkSubst sub (Iff (phi, psi), Iff (phi', psi')) = + checkSubst sub (phi, phi') andalso checkSubst sub (psi, psi') + | checkSubst sub (Forall phi, Forall psi) = checkSubst sub (phi, psi) + | checkSubst sub (Exists phi, Exists psi) = checkSubst sub (phi, psi) + | checkSubst _ _ = false + + exception MatchFailure + fun matchVariable x (Relation (r, ts), Relation (p, ss)) = + if r = p then + foldl Term.mergeOption NONE (map (Term.matchVariable x) + (ListPair.zipEq (ts, ss) handle UnequalLengths => raise MatchFailure)) + else + raise MatchFailure + | matchVariable x (Equal (t, s), Equal (t', s')) = + Term.mergeOption + (Term.matchVariable x (t, t'), Term.matchVariable x (s, s')) + | matchVariable x (Bottom, Bottom) = NONE + | matchVariable x (Neg phi, Neg psi) = matchVariable x (phi, psi) + | matchVariable x (Conj (phi, psi), Conj (phi', psi')) = + Term.mergeOption + (matchVariable x (phi, phi'), matchVariable x (psi, psi')) + | matchVariable x (Disj (phi, psi), Disj (phi', psi')) = + Term.mergeOption + (matchVariable x (phi, phi'), matchVariable x (psi, psi')) + | matchVariable x (Impl (phi, psi), Impl (phi', psi')) = + Term.mergeOption + (matchVariable x (phi, phi'), matchVariable x (psi, psi')) + | matchVariable x (Iff (phi, psi), Iff (phi', psi')) = + Term.mergeOption + (matchVariable x (phi, phi'), matchVariable x (psi, psi')) + | matchVariable x (Exists phi, Exists psi) = matchVariable (x + 1) (phi, psi) + | matchVariable x (Forall phi, Forall psi) = matchVariable (x + 1) (phi, psi) + | matchVariable _ _ = raise MatchFailure + + fun occurs t (Relation (_, ts)) = List.exists (Term.occurs t) ts + | occurs t (Equal (p, q)) = Term.occurs t p orelse Term.occurs t q + | occurs t Bottom = false + | occurs t (Neg phi) = occurs t phi + | occurs t (Conj (phi, psi)) = occurs t phi orelse occurs t psi + | occurs t (Disj (phi, psi)) = occurs t phi orelse occurs t psi + | occurs t (Impl (phi, psi)) = occurs t phi orelse occurs t psi + | occurs t (Iff (phi, psi)) = occurs t phi orelse occurs t psi + | occurs t (Exists phi) = occurs (Term.incVars t) phi + | occurs t (Forall phi) = occurs (Term.incVars t) phi end diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/PROOF.sig b/lib/forgejo.ballcloud.cc/wball/proof-checker/PROOF.sig index 3a776de..12fa6ba 100644 --- a/lib/forgejo.ballcloud.cc/wball/proof-checker/PROOF.sig +++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/PROOF.sig @@ -15,12 +15,12 @@ sig | IffE | EqI | EqE - | ForAllI - | ForAllE + | ForallI + | ForallE | ExistsI | ExistsE - exception ProofError of int + exception ProofError of string datatype t = Proof of {children: t list, label: label, formula: Formula.t} diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/Proof.sml b/lib/forgejo.ballcloud.cc/wball/proof-checker/Proof.sml index a824fe0..c95b9bd 100644 --- a/lib/forgejo.ballcloud.cc/wball/proof-checker/Proof.sml +++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/Proof.sml @@ -15,8 +15,8 @@ struct | IffE | EqI | EqE - | ForAllI - | ForAllE + | ForallI + | ForallE | ExistsI | ExistsE @@ -30,15 +30,16 @@ struct fun valid ( Proof { children = - kids as - [Proof {formula = phi, ...}, Proof {formula = psi, ...}] + [ left as Proof {formula = phi, ...} + , right as 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 + phi eq phi' andalso psi eq psi' andalso valid (left, a) + andalso valid (right, a) | valid ( Proof { children = [kid as Proof {formula = Conj (phi, psi), ...}] @@ -156,70 +157,70 @@ struct 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 *) + | 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 phi, ...}] + , label = ForallE + , formula = psi + } + , a + ) = + valid (kid, a) + andalso + (case Formula.matchVariable 0 (phi, psi) of + _ => true handle MatchFailure => false) + | valid + ( Proof + { children = [kid as Proof {formula = phi, ...}] + , label = ExistsI + , formula = Exists psi + } + , a + ) = + valid (kid, a) + andalso + (case Formula.matchVariable 0 (psi, phi) of + _ => true handle MatchFailure => false) + | valid + ( Proof + { children = [kid as Proof {formula = phi, ...}] + , label = ForallI + , formula = Forall psi + } + , a + ) = + valid (kid, a) + andalso + (case Formula.matchVariable 0 (psi, phi) of + SOME (t as Term.Free _) => not (List.exists (Formula.occurs t) a) + | _ => false handle MatchFailure => false) + | valid + ( Proof + { children = + [ kid as Proof {formula = Exists phi, ...} ] + , label = ExistsE + , formula = psi + } + , a + ) = + valid (kid, a) + andalso + (case Formula.matchVariable 0 (phi, psi) of + SOME (t as Term.Free _) => not (List.exists (Formula.occurs t) a) + | _ => false handle MatchFailure => false) + | 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 index 78d2d07..ff22eb2 100644 --- a/lib/forgejo.ballcloud.cc/wball/proof-checker/TERM.sig +++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/TERM.sig @@ -7,4 +7,15 @@ sig | Function of string * t list val eq: t * t -> bool + + val checkSubst: t * t -> t * t -> bool + + exception MatchFailure + val matchVariable: int -> t * t -> t option + + val mergeOption: t option * t option -> t option + + val incVars : t -> t + + val occurs : 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 index c22165c..e0c62a1 100644 --- a/lib/forgejo.ballcloud.cc/wball/proof-checker/Term.sml +++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/Term.sml @@ -13,4 +13,49 @@ struct (f1 = f2 andalso List.all eq (ListPair.zip (args1, args2)) handle unequalLengths => false) | eq _ = false + + infix eq + + fun checkSubst (t, s) (t', s') = + t eq t' andalso s eq s' orelse t' eq s' + orelse + case (t', s') of + (Function (f, args1), Function (g, args2)) => + (f = g + andalso + (List.all (checkSubst (t, s)) (ListPair.zipEq (args1, args2)) + handle UnequalLengths => false)) + | _ => false + + exception MatchFailure + + fun mergeOption (SOME t, SOME s) = + if t eq s then SOME t else raise MatchFailure + | mergeOption (NONE, b) = b + | mergeOption (a, NONE) = a + + fun matchVariable _ (Const s1, Const s2) = + if s1 = s2 then NONE else raise MatchFailure + | matchVariable y (Var x, t) = + if x = y then + SOME t + else + (case t of + Var x' => if x = x' then NONE else raise MatchFailure + | _ => raise MatchFailure) + | matchVariable x (Function (f, ts), Function (g, ss)) = + foldl mergeOption NONE (map (matchVariable x) + (ListPair.zipEq (ts, ss) handle UnequalLengths => raise MatchFailure)) + | matchVariable _ (Free s1, Free s2) = if s1 = s2 then NONE else raise MatchFailure + | matchVariable _ _ = raise MatchFailure + + fun incVars (Var x) = Var (x + 1) + | incVars (Function (f, args)) = Function (f, map incVars args) + | incVars t = t + + fun occurs (Const s1) (Const s2) = s1 = s2 + | occurs (Var x1) (Var x2) = x1 = x2 + | occurs t (Function (_, ts)) = List.exists (occurs t) ts + | occurs (Free s1) (Free s2) = s1 = s2 + | occurs _ _ = false end