basic proof checking completed?

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

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
+  fun eq (Relation (r, ts), Relation (p, ss)) =
-    | 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

lib/forgejo.ballcloud.cc/wball/proof-checker/PROOF.sig

@@ -15,12 +15,12 @@ sig
   | IffE
   | EqI
   | EqE
-  | ForAllI
+  | ForallI
-  | ForAllE
+  | ForallE
   | ExistsI
   | ExistsE
 
-  exception ProofError of int
+  exception ProofError of string
 
   datatype t = Proof of {children: t list, label: label, formula: Formula.t}
 

lib/forgejo.ballcloud.cc/wball/proof-checker/Proof.sml

@@ -15,8 +15,8 @@ struct
   | IffE
   | EqI
   | EqE
-  | ForAllI
+  | ForallI
-  | ForAllE
+  | ForallE
   | ExistsI
   | ExistsE
 
@@ -30,15 +30,16 @@ struct
     fun valid
           ( Proof
               { children =
-                  kids as
+                  [ left as Proof {formula = phi, ...}
-                    [Proof {formula = phi, ...}, Proof {formula = psi, ...}]
+                  , right as Proof {formula = psi, ...}
+                  ]
               , label = AndI
               , formula = Conj (phi', psi')
               }
           , a
           ) =
-          phi eq phi' andalso psi eq psi'
+          phi eq phi' andalso psi eq psi' andalso valid (left, a)
-          andalso List.all (fn k => valid (k, a)) kids
+          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 *)
+      | valid
-      (*     ( Proof *)
+          ( Proof
-      (*         { children = *)
+              { children =
-      (*             [ left as Proof {formula = Equal (t, s), ...} *)
+                  [ left as Proof {formula = Equal (t, s), ...}
-      (*             , right as Proof {formula = phi, ...} *)
+                  , right as Proof {formula = phi, ...}
-      (*             ] *)
+                  ]
-      (*         , label = EqE *)
+              , label = EqE
-      (*         , formula = psi *)
+              , formula = psi
-      (*         } *)
+              }
-      (*     , a *)
+          , a
-      (*     ) = *)
+          ) =
-      (*     valid (left, a) andalso valid (right, a) *)
+          valid (left, a) andalso valid (right, a)
-      (*     andalso Formula.checkSubst (t, s) (phi, psi) *)
+          andalso Formula.checkSubst (t, s) (phi, psi)
-      (* | valid *)
+  | valid
-      (*     ( Proof *)
+      ( Proof
-      (*         { children = [kid as Proof {formula = Forall (x, phi), ...}] *)
+          { children = [kid as Proof {formula = Forall phi, ...}]
-      (*         , label = ForAllE *)
+          , label = ForallE
-      (*         , formula = psi *)
+          , formula = psi
-      (*         } *)
+          }
-      (*     , a *)
+      , a
-      (*     ) = *)
+      ) =
-      (*     valid (kid, a) *)
+      valid (kid, a)
-      (*     andalso *)
+      andalso
-      (*     (case Formula.matchVariable x (phi, psi) of *)
+      (case Formula.matchVariable 0 (phi, psi) of
-      (*        _ => true handle MatchFailure => false) *)
+         _ => true handle MatchFailure => false)
-      (* | valid *)
+  | valid
-      (*     ( Proof *)
+      ( Proof
-      (*         { children = [kid as Proof {formula = phi, ...}] *)
+          { children = [kid as Proof {formula = phi, ...}]
-      (*         , label = ExistsI *)
+          , label = ExistsI
-      (*         , formula = Exist (x, psi) *)
+          , formula = Exists psi
-      (*         } *)
+          }
-      (*     , a *)
+      , a
-      (*     ) = *)
+      ) =
-      (*     valid (kid, a) *)
+      valid (kid, a)
-      (*     andalso *)
+      andalso
-      (*     (case Formula.matchVariable x (psi, phi) of *)
+      (case Formula.matchVariable 0 (psi, phi) of
-      (*        _ => true handle MatchFailure => false) *)
+         _ => true handle MatchFailure => false)
-      (* | valid *)
+  | valid
-      (*     ( Proof *)
+      ( Proof
-      (*         { children = [kid as Proof {formula = phi, ...}] *)
+          { children = [kid as Proof {formula = phi, ...}]
-      (*         , label = ForAllI *)
+          , label = ForallI
-      (*         , formula = Forall (x, psi) *)
+          , formula = Forall psi
-      (*         } *)
+          }
-      (*     , a *)
+      , a
-      (*     ) = *)
+      ) =
-      (*     valid (kid, a) *)
+      valid (kid, a)
-      (*     andalso *)
+      andalso
-      (*     (case Formula.matchVariable x (psi, phi) of *)
+      (case Formula.matchVariable 0 (psi, phi) of
-      (*        SOME (t as Term.Var x') => *)
+         SOME (t as Term.Free _) => not (List.exists (Formula.occurs t) a)
-      (*          Var.eq (x, x') andalso not (List.exists (Formula.occurs t) a) *)
+       | _ => false handle MatchFailure => false)
-      (*      | _ => false handle MatchFailure => false) *)
+  | valid
-      (* | valid *)
+      ( Proof
-      (*     ( Proof *)
+          { children =
-      (*         { children = *)
+              [ kid as Proof {formula = Exists phi, ...} ]
-      (*             [ left as Proof {formula = Exist (x, phi), ...} *)
+          , label = ExistsE
-      (*             , right as Proof {formula = chi, ...} *)
+          , formula = psi
-      (*             ] *)
+          }
-      (*         , label = ExistsE *)
+      , a
-      (*         , formula = chi' *)
+      ) =
-      (*         } *)
+      valid (kid, a)
-      (*     , a *)
+      andalso
-      (*     ) = *)
+      (case Formula.matchVariable 0 (phi, psi) of
-      (*     valid (left, a) andalso valid (right, phi :: a) *)
+            SOME (t as Term.Free _) => not (List.exists (Formula.occurs t) a)
-      (*     andalso not (List.exists (Formula.occurs (Term.Var x)) a) *)
+          | _ => false handle MatchFailure => false)
-      (* | valid _ = false *)
+  | valid _ = false
   end
 end

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

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