...

Commits (65)
 ... ... @@ -9,8 +9,8 @@ function morph Z.t : C.t axiom morph_zero: morph Z.zero = C.zero axiom morph_one: morph Z.one = C.one axiom morph_add: forall z1 z2:Z.t. morph (Z.(+) z1 z2) = C.(+) (morph z1) (morph z2) axiom morph_mul: forall z1 z2:Z.t. morph (Z.(*) z1 z2) = C.(*) (morph z1) (morph z2) axiom morph_mul: forall z1 z2:Z.t. morph (Z.( * ) z1 z2) = C.( * ) (morph z1) (morph z2) axiom morph_inv: forall z:Z.t. morph (Z.(-_) z) = C.(-_) (morph z) val predicate eq0 (x:Z.t) ensures { result <-> x = Z.zero } ... ... @@ -26,7 +26,7 @@ function interp (x:t) (y:vars) : C.t = match x with | Var n -> y n | Add x1 x2 -> C.(+) (interp x1 y) (interp x2 y) | Mul x1 x2 -> C.(*) (interp x1 y) (interp x2 y) | Mul x1 x2 -> C.( * ) (interp x1 y) (interp x2 y) | Cst c -> morph c end predicate eq (x1 x2:t) = forall y: vars. interp x1 y = interp x2 y ... ... @@ -39,12 +39,12 @@ type t' = list m (* sum of monomials *) function mon (x:list int) (y:vars) : C.t = match x with | Nil -> C.one | Cons x r -> C.(*) (y x) (mon r y) end | Cons x r -> C.( * ) (y x) (mon r y) end function interp' (x:t') (y:vars) : C.t = match x with | Nil -> C.zero | Cons (M a m) r -> C.(+) (C.(*) (morph a) (mon m y)) (interp' r y) end | Cons (M a m) r -> C.(+) (C.( * ) (morph a) (mon m y)) (interp' r y) end predicate eq_mon (m1 m2: list int) = forall y: vars. mon m1 y = mon m2 y predicate eq' (x1 x2: t') = forall y: vars. interp' x1 y = interp' x2 y ... ... @@ -53,7 +53,7 @@ use list.Append use list.Length let rec lemma mon_append (x1 x2: list int) (y:vars) ensures { mon (x1 ++ x2) y = C.(*) (mon x1 y) (mon x2 y) } ensures { mon (x1 ++ x2) y = C.( * ) (mon x1 y) (mon x2 y) } variant { x1 } = match x1 with Nil -> () | Cons _ x -> mon_append x x2 y end ... ... @@ -72,12 +72,12 @@ let rec lemma interp_sum (x1 x2:t') (y:vars) let ghost function append_mon (m1 m2:m) ensures { forall y. interp' (Cons result Nil) y = C.(*) (interp' (Cons m1 Nil) y) (interp' (Cons m2 Nil) y) } = match m1,m2 with M a1 l1, M a2 l2 -> M (Z.(*) a1 a2) (l1 ++ l2) end = C.( * ) (interp' (Cons m1 Nil) y) (interp' (Cons m2 Nil) y) } = match m1,m2 with M a1 l1, M a2 l2 -> M (Z.( * ) a1 a2) (l1 ++ l2) end let rec ghost function mul_mon (x:t') (mon:m) : t' ensures { forall y. interp' result y = C.(*) (interp' x y) (interp' (Cons mon Nil) y) } interp' result y = C.( * ) (interp' x y) (interp' (Cons mon Nil) y) } = match x with | Nil -> Nil | Cons m r -> ... ... @@ -87,7 +87,7 @@ let rec ghost function mul_mon (x:t') (mon:m) : t' end let rec ghost function mul_devel (x1 x2:t') : t' ensures { forall y. interp' result y = C.(*) (interp' x1 y) (interp' x2 y) } = ensures { forall y. interp' result y = C.( * ) (interp' x1 y) (interp' x2 y) } = match x1 with | Nil -> Nil | Cons (M a m) r -> (mul_mon x2 (M a m)) ++ (mul_devel r x2) ... ... @@ -211,7 +211,7 @@ function id (x:int) : int = x let predicate eq0_int (x:int) = x = 0 clone export UnitaryCommutativeRingDecision with type C.t = int, constant C.zero = zero, constant C.one = one, function C.(-_) = (-_), function C.(+) = (+), function C.(*) = (*), type Z.t = int, constant Z.zero = zero, constant Z.one = one, function Z.(-_) = (-_), function Z.(+) = (+), function Z.(*) = (*), function morph = id, goal morph_zero, goal morph_one, goal morph_add, goal morph_mul, goal morph_inv, val eq0 = eq0_int, clone export UnitaryCommutativeRingDecision with type C.t = int, constant C.zero = zero, constant C.one = one, function C.(-_) = (-_), function C.(+) = (+), function C.( * ) = ( * ), type Z.t = int, constant Z.zero = zero, constant Z.one = one, function Z.(-_) = (-_), function Z.(+) = (+), function Z.( * ) = ( * ), function morph = id, goal morph_zero, goal morph_one, goal morph_add, goal morph_mul, goal morph_inv, val eq0 = eq0_int, axiom . (* FIXME: replace with "goal" and prove *) meta "compute_max_steps" 0x10000000 ... ... @@ -227,10 +227,10 @@ type r type a function (+) a a : a function (*) a a : a function ( * ) a a : a clone algebra.UnitaryCommutativeRing as R with type t = r, axiom . clone algebra.Ring as A with type t = a, function (+) = (+), function (*) = (*), axiom . clone algebra.Ring as A with type t = a, function (+) = (+), function ( * ) = ( * ), axiom . constant one : a constant zero : a = A.zero axiom AUnitary : forall x:a. one * x = x * one = x ... ... @@ -243,7 +243,7 @@ val function (\$) r a : a axiom ExtDistSumA : forall r: r, x y: a. r \$ (x + y) = r \$ x + r \$ y axiom ExtDistSumR : forall r s: r, x: a. (R.(+) r s)\$x = r\$x + s\$x axiom AssocMulExt : forall r s: r, x: a. (R.(*) r s)\$x = r\$(s\$x) axiom AssocMulExt : forall r s: r, x: a. (R.( * ) r s)\$x = r\$(s\$x) axiom UnitExt : forall x: a. R.one \$ x = x axiom CommMulExt : forall r: r, x y: a. r\$(x*y) = (r\$x)*y = x*(r\$y) ... ... @@ -273,7 +273,7 @@ val function aplus a a : a val function atimes a a : a val function aopp a : a clone export AssocAlgebra with type r = r, type a = a, constant one = aone, constant A.zero = azero, constant R.zero = rzero, constant R.one = rone, function R.(+) = rplus, function R.(*) = rtimes, function R.(-_) = ropp, function (+) = aplus, function (*) = atimes, function A.(-_) = aopp, axiom . clone export AssocAlgebra with type r = r, type a = a, constant one = aone, constant A.zero = azero, constant R.zero = rzero, constant R.one = rone, function R.(+) = rplus, function R.( * ) = rtimes, function R.(-_) = ropp, function (+) = aplus, function ( * ) = atimes, function A.(-_) = aopp, axiom . (*axiom azero_def: azero = A.zero*) (* FIXME *) ... ... @@ -465,7 +465,7 @@ let predicate eq0_int (x:int) = x=0 let function (\$\$) (x y:int) :int = x * y clone export AssocAlgebraDecision with type r = int, type a = int, val rzero = Int.zero, val rone = Int.one, val rplus = (+), val ropp = (-_), val rtimes = (*), val azero = Int.zero, val aone = Int.one, val aplus = (+), val aopp = (-_), val atimes = (*), val (\$) = (\$\$), goal AUnitary, goal ANonTrivial, goal ExtDistSumA, goal ExtDistSumR, goal AssocMulExt, goal UnitExt, goal CommMulExt, val eq0 = eq0_int, goal A.MulAssoc.Assoc, goal A.Unit_def_l, goal A.Unit_def_r, goal A.Comm, goal A.Assoc, clone export AssocAlgebraDecision with type r = int, type a = int, val rzero = Int.zero, val rone = Int.one, val rplus = (+), val ropp = (-_), val rtimes = ( * ), val azero = Int.zero, val aone = Int.one, val aplus = (+), val aopp = (-_), val atimes = ( * ), val (\$) = (\$\$), goal AUnitary, goal ANonTrivial, goal ExtDistSumA, goal ExtDistSumR, goal AssocMulExt, goal UnitExt, goal CommMulExt, val eq0 = eq0_int, goal A.MulAssoc.Assoc, goal A.Unit_def_l, goal A.Unit_def_r, goal A.Comm, goal A.Assoc, axiom . (* FIXME: replace with "goal" and prove *) ... ...
 open Why3 open Cert_syntax open Cert_transformations open Cert_verif (** Certified transformations *) let checker_ctrans = checker_ctrans check_certif ctask_equal let assumption_trans = checker_ctrans assumption let trivial_trans = checker_ctrans trivial let exfalso_trans = checker_ctrans exfalso let intros_trans = checker_ctrans intros let intuition_trans = checker_ctrans intuition let swap_trans where = checker_ctrans (swap where) let revert_trans ls = checker_ctrans (revert ls) let intro_trans where = checker_ctrans (intro where) let left_trans where = checker_ctrans (dir Left where) let right_trans where = checker_ctrans (dir Right where) let split_trans where = checker_ctrans (split_logic where) let instantiate_trans t what = checker_ctrans (inst t what) let assert_trans t = checker_ctrans (cut t) let case_trans t = checker_ctrans (case t) let rewrite_trans g rev where = checker_ctrans (rewrite g rev where) let clear_trans l = checker_ctrans (clear l) let pose_trans name t = checker_ctrans (pose name t) (** Register certified transformations *) let () = let open Args_wrapper in let open Trans in register_transform_l "assumption_cert" (store assumption_trans) ~desc:"A certified version of coq tactic [assumption]"; register_transform_l "trivial_cert" (store trivial_trans) ~desc:"A certified version of (simplified) coq tactic [trivial]"; register_transform_l "exfalso_cert" (store exfalso_trans) ~desc:"A certified version of coq tactic [exfalso]"; register_transform_l "intros_cert" (store intros_trans) ~desc:"A certified version of coq tactic [intros]"; register_transform_l "intuition_cert" (store intuition_trans) ~desc:"A certified version of (simplified) coq tactic [intuition]"; wrap_and_register ~desc:"A certified transformation that negates \ and swaps an hypothesis from the context to the goal]" "swap_cert" (Topt ("in", Tprsymbol (Ttrans_l))) (fun where -> store (swap_trans where)); wrap_and_register ~desc:"A certified transformation that generalizes a variable in the goal" "revert_cert" (Tlsymbol (Ttrans_l)) (fun ls -> store (revert_trans ls)); wrap_and_register ~desc:"A certified version of (simplified) coq tactic [intro]" "intro_cert" (Topt ("in", Tprsymbol (Ttrans_l))) (fun where -> store (intro_trans where)); wrap_and_register ~desc:"A certified version of coq tactic [left]" "left_cert" (Topt ("in", Tprsymbol (Ttrans_l))) (fun where -> store (left_trans where)); wrap_and_register ~desc:"A certified version of coq tactic [right]" "right_cert" (Topt ("in", Tprsymbol (Ttrans_l))) (fun where -> store (right_trans where)); wrap_and_register ~desc:"A certified version of (simplified) coq tactic [split]" "split_cert" (Topt ("in", Tprsymbol (Ttrans_l))) (fun where -> store (split_trans where)); wrap_and_register ~desc:"A certified version of transformation instantiate" "instantiate_cert" (Tterm (Topt ("in", Tprsymbol Ttrans_l))) (fun t_inst where -> store (instantiate_trans t_inst where)); wrap_and_register ~desc:"A certified version of transformation rewrite" "rewrite_cert" (Toptbool ("<-", (Tprsymbol (Topt ("in", Tprsymbol (Ttrans_l)))))) (fun rev g where -> store (rewrite_trans g rev where)); wrap_and_register ~desc:"A certified version of transformation assert" "assert_cert" (Tformula Ttrans_l) (fun t -> store (assert_trans t)); wrap_and_register ~desc:"A certified version of transformation case" "case_cert" (Tformula Ttrans_l) (fun t -> store (case_trans t)); wrap_and_register ~desc:"A certified version of (simplified) coq tactic [clear]" "clear_cert" (Tprlist Ttrans_l) (fun l -> store (clear_trans l)); wrap_and_register ~desc:"A certified version of (simplified) coq tactic [pose]" "pose_cert" (Tstring (Tformula Ttrans_l)) (fun name t -> store (pose_trans name t))
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
 predicate a predicate b predicate c predicate d predicate e predicate f axiom A : a axiom B : b predicate p (x : bool) goal G1 : a /\ b goal G2 : (a /\ b) /\ (a /\ a /\ a /\ b) goal G3 : (b /\ a) /\ ( (a /\ a) /\ c) goal G4 : a /\ (b \/ d) goal G5 : (a \/ c) /\ (d \/ b) goal G6 : a /\ (c \/ d) goal G7 : (a /\ (d \/ c) ) \/ ( ((a /\ b) /\ ((b /\ (d \/ e \/ a)) \/d)) \/ (a /\ c) ) goal G8 : ((((a /\ a) /\ (a /\ a)) /\ ((a /\ a) /\ (a /\ a))) /\ (((a /\ a) /\ (a /\ a)) /\ ((a /\ a) /\ (a /\ a)))) /\ ((((a /\ a) /\ (a /\ a)) /\ ((a /\ a) /\ (a /\ a))) /\ (((a /\ a) /\ (a /\ a)) /\ ((a /\ a) /\ (a /\ a)))) goal G9 : c /\ (d \/ f) <-> (c /\ d) \/ (c /\ f) goal G10 : c -> d goal G11 : a /\ (d -> d) goal G12 : (c <-> a) -> (d \/ c) goal G13 : (c <-> d) -> c -> d goal G14 : (d <-> c) -> c -> d goal G15 : (a -> b -> d <-> c) -> c -> d goal G16 : d \/ c -> c goal G17 : (d <-> a) -> d goal G18 : a -> d -> b -> c -> a -> d goal G19 : forall x. (forall u. u <-> a) -> (x <-> x) goal G20 : exists x : bool. p x -> (forall y. p y) goal G21 : true