Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
(* ========================================================================= *) (* First order logic with equality. *) (* *) (* Copyright (c) 2003-2007, John Harrison. (See "LICENSE.txt" for details.) *) (* ========================================================================= *) let is_eq = function (Atom(R("=",_))) -> true | _ -> false;; let mk_eq s t = Atom(R("=",[s;t]));; let dest_eq fm = match fm with Atom(R("=",[s;t])) -> s,t | _ -> failwith "dest_eq: not an equation";; let lhs eq = fst(dest_eq eq) and rhs eq = snd(dest_eq eq);; (* ------------------------------------------------------------------------- *) (* The set of predicates in a formula. *) (* ------------------------------------------------------------------------- *) let rec predicates fm = atom_union (fun (R(p,a)) -> [p,length a]) fm;; (* ------------------------------------------------------------------------- *) (* Code to generate equality axioms for functions. *) (* ------------------------------------------------------------------------- *) let function_congruence (f,n) = if n = 0 then [] else let argnames_x = map (fun n -> "x"^(string_of_int n)) (1 -- n) and argnames_y = map (fun n -> "y"^(string_of_int n)) (1 -- n) in let args_x = map (fun x -> Var x) argnames_x and args_y = map (fun x -> Var x) argnames_y in let ant = end_itlist mk_and (map2 mk_eq args_x args_y) and con = mk_eq (Fn(f,args_x)) (Fn(f,args_y)) in [itlist mk_forall (argnames_x @ argnames_y) (Imp(ant,con))];; (* ------------------------------------------------------------------------- *) (* Example. *) (* ------------------------------------------------------------------------- *) START_INTERACTIVE;; function_congruence ("f",3);; function_congruence ("+",2);; END_INTERACTIVE;; (* ------------------------------------------------------------------------- *) (* And for predicates. *) (* ------------------------------------------------------------------------- *) let predicate_congruence (p,n) = if n = 0 then [] else let argnames_x = map (fun n -> "x"^(string_of_int n)) (1 -- n) and argnames_y = map (fun n -> "y"^(string_of_int n)) (1 -- n) in let args_x = map (fun x -> Var x) argnames_x and args_y = map (fun x -> Var x) argnames_y in let ant = end_itlist mk_and (map2 mk_eq args_x args_y) and con = Imp(Atom(R(p,args_x)),Atom(R(p,args_y))) in [itlist mk_forall (argnames_x @ argnames_y) (Imp(ant,con))];; (* ------------------------------------------------------------------------- *) (* Hence implement logic with equality just by adding equality "axioms". *) (* ------------------------------------------------------------------------- *) let equivalence_axioms = [<>; < y = z>>];; let equalitize fm = let allpreds = predicates fm in if not (mem ("=",2) allpreds) then fm else let preds = subtract allpreds ["=",2] and funcs = functions fm in let axioms = itlist (union ** function_congruence) funcs (itlist (union ** predicate_congruence) preds equivalence_axioms) in Imp(end_itlist mk_and axioms,fm);; (* ------------------------------------------------------------------------- *) (* A simple example (see EWD1266a and the application to Morley's theorem). *) (* ------------------------------------------------------------------------- *) START_INTERACTIVE;; let ewd = equalitize <<(forall x. f(x) ==> g(x)) /\ (exists x. f(x)) /\ (forall x y. g(x) /\ g(y) ==> x = y) ==> forall y. g(y) ==> f(y)>>;; meson ewd;; (* ------------------------------------------------------------------------- *) (* Wishnu Prasetya's example (even nicer with an "exists unique" primitive). *) (* ------------------------------------------------------------------------- *) let wishnu = equalitize <<(exists x. x = f(g(x)) /\ forall x'. x' = f(g(x')) ==> x = x') <=> (exists y. y = g(f(y)) /\ forall y'. y' = g(f(y')) ==> y = y')>>;; time meson wishnu;; (* ------------------------------------------------------------------------- *) (* More challenging equational problems. (Size 18, 61814 seconds.) *) (* ------------------------------------------------------------------------- *) (********* (meson ** equalitize) <<(forall x y z. x * (y * z) = (x * y) * z) /\ (forall x. 1 * x = x) /\ (forall x. i(x) * x = 1) ==> forall x. x * i(x) = 1>>;; ********) (* ------------------------------------------------------------------------- *) (* Other variants not mentioned in book. *) (* ------------------------------------------------------------------------- *) (************* (meson ** equalitize) <<(forall x y z. x * (y * z) = (x * y) * z) /\ (forall x. 1 * x = x) /\ (forall x. x * 1 = x) /\ (forall x. x * x = 1) ==> forall x y. x * y = y * x>>;; (* ------------------------------------------------------------------------- *) (* With symmetry at leaves and one-sided congruences (Size = 16, 54659 s). *) (* ------------------------------------------------------------------------- *) let fm = <<(forall x. x = x) /\ (forall x y z. x * (y * z) = (x * y) * z) /\ (forall x y z. =((x * y) * z,x * (y * z))) /\ (forall x. 1 * x = x) /\ (forall x. x = 1 * x) /\ (forall x. i(x) * x = 1) /\ (forall x. 1 = i(x) * x) /\ (forall x y. x = y ==> i(x) = i(y)) /\ (forall x y z. x = y ==> x * z = y * z) /\ (forall x y z. x = y ==> z * x = z * y) /\ (forall x y z. x = y /\ y = z ==> x = z) ==> forall x. x * i(x) = 1>>;; time meson fm;; (* ------------------------------------------------------------------------- *) (* Newer version of stratified equalities. *) (* ------------------------------------------------------------------------- *) let fm = <<(forall x y z. axiom(x * (y * z),(x * y) * z)) /\ (forall x y z. axiom((x * y) * z,x * (y * z)) /\ (forall x. axiom(1 * x,x)) /\ (forall x. axiom(x,1 * x)) /\ (forall x. axiom(i(x) * x,1)) /\ (forall x. axiom(1,i(x) * x)) /\ (forall x x'. x = x' ==> cchain(i(x),i(x'))) /\ (forall x x' y y'. x = x' /\ y = y' ==> cchain(x * y,x' * y'))) /\ (forall s t. axiom(s,t) ==> achain(s,t)) /\ (forall s t u. axiom(s,t) /\ (t = u) ==> achain(s,u)) /\ (forall x x' u. x = x' /\ achain(i(x'),u) ==> cchain(i(x),u)) /\ (forall x x' y y' u. x = x' /\ y = y' /\ achain(x' * y',u) ==> cchain(x * y,u)) /\ (forall s t. cchain(s,t) ==> s = t) /\ (forall s t. achain(s,t) ==> s = t) /\ (forall t. t = t) ==> forall x. x * i(x) = 1>>;; time meson fm;; let fm = <<(forall x y z. axiom(x * (y * z),(x * y) * z)) /\ (forall x y z. axiom((x * y) * z,x * (y * z)) /\ (forall x. axiom(1 * x,x)) /\ (forall x. axiom(x,1 * x)) /\ (forall x. axiom(i(x) * x,1)) /\ (forall x. axiom(1,i(x) * x)) /\ (forall x x'. x = x' ==> cong(i(x),i(x'))) /\ (forall x x' y y'. x = x' /\ y = y' ==> cong(x * y,x' * y'))) /\ (forall s t. axiom(s,t) ==> achain(s,t)) /\ (forall s t. cong(s,t) ==> cchain(s,t)) /\ (forall s t u. axiom(s,t) /\ (t = u) ==> achain(s,u)) /\ (forall s t u. cong(s,t) /\ achain(t,u) ==> cchain(s,u)) /\ (forall s t. cchain(s,t) ==> s = t) /\ (forall s t. achain(s,t) ==> s = t) /\ (forall t. t = t) ==> forall x. x * i(x) = 1>>;; time meson fm;; (* ------------------------------------------------------------------------- *) (* Showing congruence closure. *) (* ------------------------------------------------------------------------- *) let fm = equalitize < f(c) = c>>;; time meson fm;; let fm = < achain(s,t)) /\ (forall s t. cong(s,t) ==> cchain(s,t)) /\ (forall s t u. axiom(s,t) /\ (t = u) ==> achain(s,u)) /\ (forall s t u. cong(s,t) /\ achain(t,u) ==> cchain(s,u)) /\ (forall s t. cchain(s,t) ==> s = t) /\ (forall s t. achain(s,t) ==> s = t) /\ (forall t. t = t) /\ (forall x y. x = y ==> cong(f(x),f(y))) ==> f(c) = c>>;; time meson fm;; (* ------------------------------------------------------------------------- *) (* With stratified equalities. *) (* ------------------------------------------------------------------------- *) let fm = <<(forall x y z. eqA (x * (y * z),(x * y) * z)) /\ (forall x y z. eqA ((x * y) * z)) /\ (forall x. eqA (1 * x,x)) /\ (forall x. eqA (x,1 * x)) /\ (forall x. eqA (i(x) * x,1)) /\ (forall x. eqA (1,i(x) * x)) /\ (forall x. eqA (x,x)) /\ (forall x y. eqA (x,y) ==> eqC (i(x),i(y))) /\ (forall x y. eqC (x,y) ==> eqC (i(x),i(y))) /\ (forall x y. eqT (x,y) ==> eqC (i(x),i(y))) /\ (forall w x y z. eqA (w,x) /\ eqA (y,z) ==> eqC (w * y,x * z)) /\ (forall w x y z. eqA (w,x) /\ eqC (y,z) ==> eqC (w * y,x * z)) /\ (forall w x y z. eqA (w,x) /\ eqT (y,z) ==> eqC (w * y,x * z)) /\ (forall w x y z. eqC (w,x) /\ eqA (y,z) ==> eqC (w * y,x * z)) /\ (forall w x y z. eqC (w,x) /\ eqC (y,z) ==> eqC (w * y,x * z)) /\ (forall w x y z. eqC (w,x) /\ eqT (y,z) ==> eqC (w * y,x * z)) /\ (forall w x y z. eqT (w,x) /\ eqA (y,z) ==> eqC (w * y,x * z)) /\ (forall w x y z. eqT (w,x) /\ eqC (y,z) ==> eqC (w * y,x * z)) /\ (forall w x y z. eqT (w,x) /\ eqT (y,z) ==> eqC (w * y,x * z)) /\ (forall x y z. eqA (x,y) /\ eqA (y,z) ==> eqT (x,z)) /\ (forall x y z. eqC (x,y) /\ eqA (y,z) ==> eqT (x,z)) /\ (forall x y z. eqA (x,y) /\ eqC (y,z) ==> eqT (x,z)) /\ (forall x y z. eqA (x,y) /\ eqT (y,z) ==> eqT (x,z)) /\ (forall x y z. eqC (x,y) /\ eqT (y,z) ==> eqT (x,z)) ==> forall x. eqT (x * i(x),1)>>;; (* ------------------------------------------------------------------------- *) (* With transitivity chains... *) (* ------------------------------------------------------------------------- *) let fm = <<(forall x y z. eqA (x * (y * z),(x * y) * z)) /\ (forall x y z. eqA ((x * y) * z)) /\ (forall x. eqA (1 * x,x)) /\ (forall x. eqA (x,1 * x)) /\ (forall x. eqA (i(x) * x,1)) /\ (forall x. eqA (1,i(x) * x)) /\ (forall x y. eqA (x,y) ==> eqC (i(x),i(y))) /\ (forall x y. eqC (x,y) ==> eqC (i(x),i(y))) /\ (forall w x y. eqA (w,x) ==> eqC (w * y,x * y)) /\ (forall w x y. eqC (w,x) ==> eqC (w * y,x * y)) /\ (forall x y z. eqA (y,z) ==> eqC (x * y,x * z)) /\ (forall x y z. eqC (y,z) ==> eqC (x * y,x * z)) /\ (forall x y z. eqA (x,y) /\ eqA (y,z) ==> eqT (x,z)) /\ (forall x y z. eqC (x,y) /\ eqA (y,z) ==> eqT (x,z)) /\ (forall x y z. eqA (x,y) /\ eqC (y,z) ==> eqT (x,z)) /\ (forall x y z. eqC (x,y) /\ eqC (y,z) ==> eqT (x,z)) /\ (forall x y z. eqA (x,y) /\ eqT (y,z) ==> eqT (x,z)) /\ (forall x y z. eqC (x,y) /\ eqT (y,z) ==> eqT (x,z)) ==> forall x. eqT (x * i(x),1) \/ eqC (x * i(x),1)>>;; time meson fm;; (* ------------------------------------------------------------------------- *) (* Enforce canonicity (proof size = 20). *) (* ------------------------------------------------------------------------- *) let fm = <<(forall x y z. eq1(x * (y * z),(x * y) * z)) /\ (forall x y z. eq1((x * y) * z,x * (y * z))) /\ (forall x. eq1(1 * x,x)) /\ (forall x. eq1(x,1 * x)) /\ (forall x. eq1(i(x) * x,1)) /\ (forall x. eq1(1,i(x) * x)) /\ (forall x y z. eq1(x,y) ==> eq1(x * z,y * z)) /\ (forall x y z. eq1(x,y) ==> eq1(z * x,z * y)) /\ (forall x y z. eq1(x,y) /\ eq2(y,z) ==> eq2(x,z)) /\ (forall x y. eq1(x,y) ==> eq2(x,y)) ==> forall x. eq2(x,i(x))>>;; time meson fm;; ******************) END_INTERACTIVE;;