Simple prover based on the approach used in the B-Book by J.R. Abrial

b-book-theorems.sml

(*
Simple prover based on the approach used in the B-Book by J.R. Abrial
Copyright (C) 2024  Cole Blakley

This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program.  If not, see <https://www.gnu.org/licenses/>.
*)
val p = Placeholder "p";
val q = Placeholder "q";
val r = Placeholder "r";

(* Precedence sanity checks*)
val impl_equiv_check = (p == q --> q == p) = Equiv (Equiv (p, Implies (q, q)), p);
val impl_and_check = (p && q --> q && p) = Implies (And (p, q), And (q, p));
val equiv_and_check = (p && q == q && p) = Equiv (And (p, q), And (q, p));
val ex_check = (p && Not q --> Not q && p) = Implies (And (p, Not q), And (Not q, p));
val multi_impl_check = (p --> q --> q) = (Implies (Implies (p, q), q));
val impl_122 = (p --> Not q --> Not (p && q)) = (Implies (Implies (p, Not q), Not (And (p, q))));

(* Theorems from the B Book *)
val theorem_1_2_1 = all_true (simple_prove ( p --> Not (Not p) ));
val theorem_1_2_2 = all_true (simple_prove ( p && Not q --> Not (p --> q) ));
val theorem_1_2_3 = all_true (simple_prove ( p --> Not q --> Not (p && q) ));
val theorem_1_2_4 = all_true (simple_prove ( p --> r --> (Not (Not p) --> r) ));
val theorem_1_2_5 = all_true (simple_prove ( (p --> (Not q --> r)) --> (Not (p --> q) --> r) ));
val theorem_1_2_6 = all_true (simple_prove ( ((Not p --> r) && (Not q --> r)) --> (Not (p && q) --> r) ));
val theorem_1_2_7 = all_true (simple_prove ( (Not p --> r) && (q --> r) --> (p --> q --> r) ));
val theorem_1_2_8  = all_true (simple_prove ( (p --> (q --> r)) --> (p && q --> r) ));
val theorem_1_2_9 = all_true (simple_prove ( (Not p --> q) && r --> (Not (p && r) --> q && r) ));
val theorem_1_2_10 = all_true (simple_prove ( (p --> r) && (q --> r) && (p || q) --> r ));

(* Basic properties *)
val commutative_1 = all_true (simple_prove ( p || q == q || p ));
val commutative_2 = all_true (simple_prove ( p && q == q && p ));
val commutative_3 = all_true (simple_prove ( (p == q) == (q == p) ));

val associative_1 = all_true (simple_prove ( p || q || r == p || (q || r) ));
val associative_2 = all_true (simple_prove ( p && q && r == p && (q && r) ));
val associative_3 = all_true (simple_prove ( (p == q == r) == (p == (q == r)) ));

val distributive_1 = all_true (simple_prove ( r && (p || q) == (r && p) || (r && q) ));
val distributive_2 = all_true (simple_prove ( r || (p && q) == (r || p) && (r || q) ));
val distributive_3 = all_true (simple_prove ( r --> (p && q) == (r --> p) && (r --> q) ));

val excluded_middle = all_true (simple_prove ( p || Not p ));

val idempotence_1 = all_true (simple_prove ( p || p == p) );
val idempotence_2 = all_true (simple_prove ( p && p == p) );

val absorption_1 = all_true (simple_prove ( (p || q) && p == p ));
val absorption_2 = all_true (simple_prove ( (p && q) || p == p ));

val de_morgan_1 = all_true (simple_prove ( Not (p || q) == Not p && Not q ));
val de_morgan_2 = all_true (simple_prove ( Not (p && q) == Not p || Not q ));
val de_morgan_3 = all_true (simple_prove ( Not (p && q) == p --> Not q ));
val de_morgan_4 = all_true (simple_prove ( Not (p --> q) == p && Not q ));

val double_negation = all_true (simple_prove ( Not (Not p) == p ));

val transitivity = all_true (simple_prove ( ((p --> q) && (q --> r)) --> (p --> r) ));

predicates.sml

(*
Simple prover based on the approach used in the B-Book by J.R. Abrial
Copyright (C) 2024  Cole Blakley

This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program.  If not, see <https://www.gnu.org/licenses/>.
*)
datatype variable = Var of int;
datatype expression = VarExpr of variable
                    | SubstExpr of variable * expression * expression;
datatype predicate = Bool of bool
                   | Placeholder of string
                   | Not of predicate
                   | And of predicate * predicate
                   | Implies of predicate * predicate
                   | Or of predicate * predicate
                   | Equiv of predicate * predicate
                   | Forall of variable * predicate
                   | SubstPred of variable * expression * predicate;

val == = fn (a, b) => Equiv (a, b);
infix 4 ==;

val --> = fn (a, b) => Implies (a, b);
infix 5 -->;

val && = fn (a, b) => And (a, b);
infix 6 &&;

val || = fn (a, b) => Or (a, b);
infix 6 ||;

(*
Rule 1 (CNJ or and-introduction):
   HYP :- P
   HYP :- Q
   --------------
   HYP :- P and Q

Rule 2 and 2' (and-elimination):
   HYP :- P and Q
   --------------
   HYP :- P
   HYP :- Q
*)
fun cnj (And (p, q)) = [p, q]
  | cnj pred = [];

(*
Rule 3 (DED):
   HYP, P :- Q
   -------------
   HYP :- P -> Q

Rule 4:
   HYP :- P -> Q
   -------------
   HYP, P :- Q
*)
fun ded context (Implies (p, q)) = (p::context, [q])
  | ded context _ = (context, []);

(* Dummy function used as a type-compatible label with the inference_rules set.
   This allows us to record fn ded as a proof step in the same way we record other rules
   as proof steps *)
fun ded_lbl (pl:predicate list) (p:predicate) = [] : predicate list;

(*
DR 1:
   HYP :- P
   ----------
   HYP :- !!P
*)
fun dr1 (Not (Not p)) = [p]
  | dr1 pred = [];

(*
DR 2:
   HYP :- P
   HYP :- !Q
   ----------------
   HYP :- !(P -> Q)
*)
fun dr2 (Not (Implies (p, q))) = [p, Not q]
  | dr2 pred = [];

(*
DR 3:
   HYP :- P -> !Q
   --------------
   HYP :- !(P and Q)
*)
fun dr3 (Not (And (p, q))) = [Implies (p, Not q)]
  | dr3 pred = [];

(*
DR 4:
   HYP :- P -> R
   ---------------
   HYP :- !!P -> R
*)
fun dr4 (Implies (Not (Not p), r)) = [Implies (p, r)]
  | dr4 pred = [];

(*
DR 5:
   HYP :- P -> (!Q -> R)
   ---------------------
   HYP :- !(P -> Q) -> R
*)
fun dr5 (Implies (Not (Implies (p, q)), r)) = [Implies (p, Implies (Not q, r))]
  | dr5 pred = [];

(*
DR 6:
   HYP :- !P -> R
   HYP :- !Q -> R
   ----------------------
   HYP :- !(P and Q) -> R
*)
fun dr6 (Implies ((Not (And (p, q))), r)) = [Implies (Not p, r), Implies (Not q, r)]
  | dr6 pred = [];

(*
DR 7:
   HYP :- !P -> R
   HYP :- Q -> R
   --------------------
   HYP :- (P -> Q) -> R
*)
fun dr7 (Implies (Implies (p, q), r)) = [Implies (Not p, r), Implies (q, r)]
  | dr7 pred = [];

(*
DR 8:
   HYP :- P -> (Q -> R)
   --------------------
   P and Q -> R
*)
fun dr8 (Implies (And (p, q), r)) = [Implies (p, Implies (q, r))]
  | dr8 pred = [];

(*
DB 1:
   P occurs in HYP
   ---------------
   HYP :- !P -> R
*)
fun db1 context (Implies (Not p, r)) = if List.exists (fn x => x = p) context then [Bool true]
                                       else []
  | db1 context pred = [];

(*
DB 2:
   !P occurs in HYP
   ----------------
   HYP :- P -> R
*)
fun db2 context (Implies (p, r)) = if List.exists (fn x => x = (Not p)) context then [Bool true]
                                   else []
  | db2 context pred = [];

(*
BS 1:
   R occurs in HYP
   ---------------
   HYP :- P -> R
*)
fun bs1 context (Implies (p, r)) = if List.exists (fn x => x = r) context then [Bool true]
                                   else []
  | bs1 context pred = [];

(*
BS 2:
   P occurs in HYP
   ---------------
   HYP :- P
*)
fun bs2 context (p:predicate) = if List.exists (fn x => x = p) context then [Bool true]
                                else [];

(*
DR 9:
   HYP :- !P -> R
   ---------------------------
   HYP :- !(forall x : P) -> R
*)
fun dr9 (Implies (Not (Forall (x, p)), r)) = [Not p --> r]
  | dr9 pred = [];

(*
DR 10: (Note: requires manual effort to pick E)
   HYP :- [x := E]!P
   ----------------------
   HYP :- !(forall x : P)
*)
fun dr10 e (Not (Forall (x, p))) = [SubstPred (x, e, Not p)]
  | dr10 e pred = [];

(*
DR 11: (Note: requires manual effort to pick E and P)
   (forall x : P) occurs in HYP
   HYP :- [x := E]P -> R
   ----------------------------
   HYP :- R

   - Assumes (forall x : P) is known to be in context
   - x should be a fresh new variable
*)
fun dr11 x e p r = [SubstPred (x, e, p) --> r];

(*
SUB 1:
   [x := E]x
   ---------
   E

SUB 2:
   [x := E]y
   ---------
   y          (if y is a variable that is not x)
*)
fun sub1 (SubstExpr (x, e, VarExpr y)) = if x = y then [e] else [VarExpr y]
  | sub1 expr = [];

(*
SUB 3:
   [x := E](P and Q)
   -----------------------
   [x := E]P and [x := E]Q
*)
fun sub3 (SubstPred (x, e, And (p, q))) = [SubstPred (x, e, p) && SubstPred (x, e, q)]
  | sub3 pred = [];

(*
SUB 4:
   [x := E](P -> Q)
   ----------------------
   [x := E]P -> [x := E]Q
*)
fun sub4 (SubstPred (x, e, Implies (p, q))) = [SubstPred (x, e, p) --> SubstPred (x, e, q)]
  | sub4 pred = [];

(*
SUB 5:
   [x := E]!P
   ----------
   ![x := E]P
*)
fun sub5 (SubstPred (x, e, Not p)) = [Not (SubstPred (x, e, p))]
  | sub5 pred = [];

(*
SUB 6:
   [x := E](forall x : P)
   ----------------------
   forall x : P

SUB 7:
   [x := E](forall y : P)
   ----------------------
   forall y : [x := E]P
*)
fun sub6 (SubstPred (x, e, Forall (y, p))) =
      if x = y then [Forall (y, p)]
      else [Forall (y, SubstPred (x, e, p))]
  | sub6 pred = [];

(*
SUB 8:
   [x := x]F
   ---------
   F
*)
fun sub8 (SubstPred (x, VarExpr y, f)) = if x = y then [f] else []
  | sub8 pred = [];

(*
SUB 9:
   [x := E]F
   ---------
   F
   SKIPPED: It is inefficient to check if x is non-free in F. Instead, in the final step of formula simplification,
   we will rewrite all substitutions [x := E]F into F' such that all occurrences of x in F' have been
   replaced by E. If x is not found anywhere within F, this rule will have effectively been applied since F'
   will equal F after the rewrite process.

SUB 10:
   [y := E][x := y]F
   -----------------
   [x := E]F        if y \ F
   SKIPPED: It is inefficient to check if y is non-free in F. Instead, it is easier to rewrite [x := y]F, resulting
   in expanded formula F', then rewrite [y := E]F'. If y ends up being non-free in F, the result will be the same
   since all occurrences of x in F will be replaced by y, which will then be replaced by E.

SUB 11:
   SKIPPED: Same reasons as SUB 9 and SUB 10.
*)

(* TODO: Have the prover build a proof tree at each step *)
(* TODO: Add the new rules to the proof procedure *)
(* TODO: Add way to pause execution when needing to apply DR10 or DR11
    so user can manually pick values, then continue proving *)

(*
Rewrite all occurrences of Or and Equiv using simpler operations
*)
fun op_rewrite (Or (p, q)) = Not (op_rewrite p) --> op_rewrite q
  | op_rewrite (Equiv (p, q)) = (op_rewrite p --> op_rewrite q) && (op_rewrite q --> op_rewrite p)
  | op_rewrite (Not p) = Not (op_rewrite p)
  | op_rewrite (And (p, q)) = op_rewrite p && op_rewrite q
  | op_rewrite (Implies (p, q)) = op_rewrite p --> op_rewrite q
  | op_rewrite (Bool v) = Bool v
  | op_rewrite (Placeholder v) = Placeholder v
  | op_rewrite (Forall (v, p)) = Forall (v, op_rewrite p)
  | op_rewrite (SubstPred (v, e, p)) = SubstPred (v, e, op_rewrite p);

fun rule_wrapper rule context p = rule p;
val inference_rules = bs1::bs2::db1::db2::(map (fn r => rule_wrapper r) [dr1, dr2, dr3, dr4, dr5, dr6, dr7, dr8, cnj]);

(*
Generates new goal(s) such that proving all of the new goals is sufficient
to prove the original goal. Returns (new_context, new_goals, rule_used). If
new_goals = [], then the original goal failed to be proved.
*)
fun prove_step context goal (rule::rules) =
      (* Try each inference rule in order *)
      (case (rule context goal) of
         []    => prove_step context goal rules
      | goals' => (context, goals', SOME rule))
  | prove_step context goal [] =
      (* Only try to use the deduction rule when no other rules are applicable *)
      (case (ded context goal) of
         (_, [])           => (context, [], NONE)
      | (context', goals') => (context', goals', SOME ded_lbl));

(* Prove the given goal. Returns a list of proof results.
   If a proof result is Bool true, then that proof was discharged; otherwise,
   that proof failed to discharge. *)
fun prove context main_goal = let
   fun prove' context goal =
      (case (prove_step context goal inference_rules) of
         (_, [], _)                    => [goal] (* Can't reduce any further *)
       | (context', goals', rule_used) => List.concat (map (fn g => prove' context' g) goals'));
in
   prove' context (op_rewrite main_goal)
end;

(* Prove goal with no initial hypotheses *)
fun simple_prove goal = prove [] goal;

fun all_true discharges = List.all (fn x => x = Bool true) discharges;