From 7fe97cf3e53fe94c6a6bdd2a0a5c869d9bf7092e Mon Sep 17 00:00:00 2001 From: filliatr Date: Tue, 10 Apr 2001 14:45:40 +0000 Subject: portage exemples Correctness; changement du nom de pred_of_minus dans coq_omega git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1573 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/correctness/examples/Handbook.v | 36 ++++++++++++++++----------------- contrib/correctness/examples/exp_int.v | 14 ++++++------- contrib/correctness/examples/fact.v | 3 +-- contrib/correctness/examples/fact_int.v | 15 +++++++------- contrib/omega/coq_omega.ml | 3 ++- 5 files changed, 34 insertions(+), 37 deletions(-) (limited to 'contrib') diff --git a/contrib/correctness/examples/Handbook.v b/contrib/correctness/examples/Handbook.v index dae287399..26b2af4cf 100644 --- a/contrib/correctness/examples/Handbook.v +++ b/contrib/correctness/examples/Handbook.v @@ -25,7 +25,7 @@ * Programs are refered to by numbers and pages. *) -Require Programs. +Require Correctness. Require Sumbool. Require Omega. @@ -49,34 +49,34 @@ Axiom axiom3 : (x,y:Z) `y>=0` -> `(Zpower (x*x) (Zdiv2 y)) = (Zpower x y)`. Global Variable X : Z ref. Global Variable Y : Z ref. -Global Variable Z : Z ref. +Global Variable Z_ : Z ref. Correctness pgm25 { `Y >= 0` } begin - Z := 1; + Z_ := 1; while !Y <> 0 do - { invariant `Y >= 0` /\ `Z * (Zpower X Y) = (Zpower X@0 Y@0)` + { invariant `Y >= 0` /\ `Z_ * (Zpower X Y) = (Zpower X@0 Y@0)` variant Y } if (Zodd_bool !Y) then begin Y := (Zpred !Y); - Z := (Zmult !Z !X) + Z_ := (Zmult !Z_ !X) end else begin Y := (Zdiv2 !Y); X := (Zmult !X !X) end done end - { Z = (Zpower X@ Y@) }. + { Z_ = (Zpower X@ Y@) }. Proof. Split. Unfold Zpred; Unfold Zwf; Omega. Split. Unfold Zpred; Omega. Decompose [and] Pre2. -Rewrite <- H1. -Replace `Z1*X0*(Zpower X0 (Zpred Y0))` with `Z1*(X0*(Zpower X0 (Zpred Y0)))`. -Apply f_equal with f := (Zmult Z1). +Rewrite <- H0. +Replace `Z_1*X0*(Zpower X0 (Zpred Y0))` with `Z_1*(X0*(Zpower X0 (Zpred Y0)))`. +Apply f_equal with f := (Zmult Z_1). Apply axiom1. Omega. @@ -97,15 +97,15 @@ Split. Omega. Decompose [and] Pre2. -Rewrite <- H1. -Apply f_equal with f:=(Zmult Z1). +Rewrite <- H0. +Apply f_equal with f:=(Zmult Z_1). Apply axiom3. Omega. Omega. Decompose [and] Post6. Rewrite <- H2. -Rewrite H1. +Rewrite H0. Simpl. Omega. @@ -143,9 +143,9 @@ Unfold Zpred. Omega. Unfold Zs. Unfold Zpred in Post3. Split. Omega. Decompose [and] Post3. -Rewrite H0. +Rewrite H. Replace `X0+(-1)+1` with X0. -Rewrite H1. +Rewrite H0. Replace `X0+(-1)` with `X0-1`. Apply axiom5. Omega. @@ -176,12 +176,12 @@ let rec F (u:unit) : unit { variant N } = Proof. Unfold Zwf. Unfold Zpred. Omega. Unfold Zpred. Omega. -Decompose [and] Post5. Rewrite H0. Unfold Zwf. Unfold Zpred. Omega. -Decompose [and] Post5. Rewrite H0. Unfold Zpred. Omega. +Decompose [and] Post5. Rewrite H. Unfold Zwf. Unfold Zpred. Omega. +Decompose [and] Post5. Rewrite H. Unfold Zpred. Omega. Split. Unfold Zpred in Post5. Omega. -Decompose [and] Post4. Rewrite H1. -Decompose [and] Post5. Rewrite H3. Rewrite H2. +Decompose [and] Post4. Rewrite H0. +Decompose [and] Post5. Rewrite H2. Rewrite H1. Replace `(Zpower 2 N0)` with `2*(Zpower 2 (Zpred N0))`. Omega. Symmetry. Replace `(Zpower 2 N0)` with `(Zpower 2 (1+(Zpred N0)))`. diff --git a/contrib/correctness/examples/exp_int.v b/contrib/correctness/examples/exp_int.v index e6beecccf..d0c77e980 100644 --- a/contrib/correctness/examples/exp_int.v +++ b/contrib/correctness/examples/exp_int.v @@ -133,8 +133,8 @@ Correctness i_exp . Proof. (* Zodd *) -Decompose [and] I. -Rewrite (Zodd_div2 e0 H1 Test1) in H0. Rewrite H0. +Decompose [and] Inv. +Rewrite (Zodd_div2 e0 H0 Test1) in H. Rewrite H. Rewrite Zpower_exp. Unfold Zdouble. Replace (Zpower m0 `1`) with m0. @@ -143,11 +143,9 @@ Unfold Zpower; Unfold Zpower_pos; Simpl; Ring. Generalize (Zdiv2_ge_0 e0); Omega. Omega. (* Zeven *) -Decompose [and] I. -Rewrite (Zeven_div2 e0 Test1) in H0. Rewrite H0. +Decompose [and] Inv. +Rewrite (Zeven_div2 e0 Test1) in H. Rewrite H. Auto with zarith. -(* Zwf /\ I *) -Split. (* Zwf *) Unfold Zwf. Repeat Split. @@ -163,9 +161,9 @@ Generalize (Zdiv2_ge_0 e0); Omega. Generalize (Zdiv2_ge_0 e0); Omega. Split; [ Ring | Assumption ]. (* exit fo loop *) -Decompose [and] I. +Decompose [and] Inv. Cut `e0 = 0`. Intro. -Rewrite H. Rewrite H0. +Rewrite H1. Rewrite H. Simpl; Ring. Omega. Save. diff --git a/contrib/correctness/examples/fact.v b/contrib/correctness/examples/fact.v index 8c694d132..a6c443807 100644 --- a/contrib/correctness/examples/fact.v +++ b/contrib/correctness/examples/fact.v @@ -18,7 +18,7 @@ (* Proof of an imperative program computing the factorial (over type nat) *) -Require Programs. +Require Correctness. Require Omega. Require Arith. @@ -60,7 +60,6 @@ Correctness factorielle end { y = (fact x@0) }. Proof. -Split. (* decreasing of the variant *) Omega. (* preservation of the invariant *) diff --git a/contrib/correctness/examples/fact_int.v b/contrib/correctness/examples/fact_int.v index 99e79f7ac..f510fe32b 100644 --- a/contrib/correctness/examples/fact_int.v +++ b/contrib/correctness/examples/fact_int.v @@ -18,7 +18,7 @@ (* Proof of an imperative program computing the factorial (over type Z) *) -Require Programs. +Require Correctness. Require Omega. Require ZArithRing. @@ -70,7 +70,7 @@ Omega. Ring. Intros. -Rewrite <- y0. +Rewrite <- b. Omega. Omega. @@ -171,7 +171,7 @@ Correctness factorielle begin y := 1; while !x <> 0 do - { invariant `0 <= x` /\ (invariant y x x@0) as I + { invariant `0 <= x` /\ (invariant y x x@0) as Inv variant x for (Zwf ZERO) } y := (Zmult !x !y); x := (Zpred !x) @@ -179,15 +179,14 @@ Correctness factorielle end { (fact x@0 y) }. Proof. -Split. (* decreasing *) Unfold Zwf. Unfold Zpred. Omega. (* preservation of the invariant *) Split. Unfold Zpred; Omega. Cut `0 < x0`. Intro Hx0. - Decompose [and] I. - Exact (fact_rec x x0 y1 Hx0 H1). + Decompose [and] Inv. + Exact (fact_rec x x0 y1 Hx0 H0). Omega. (* entrance of the loop *) Split; Auto. @@ -195,8 +194,8 @@ Elim (fact_function x Pre1). Intros. Apply c_inv with f:=x0 f0:=x0; Auto. Omega. (* exit of the loop *) -Decompose [and] I. -Rewrite H1 in H2. +Decompose [and] Inv. +Rewrite H0 in H2. Exact (invariant_0 x y1 H2). Save. diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index 15022750a..16bbd614f 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -228,6 +228,7 @@ let constant dir s = anomaly ("Coq_omega: cannot find "^ (Nametab.string_of_qualid (Nametab.make_qualid dir id))) +let arith_constant dir = constant ("Arith"::dir) let zarith_constant dir = constant ("Zarith"::dir) let logic_constant dir = constant ("Logic"::dir) @@ -266,7 +267,7 @@ let coq_inj_ge = lazy (zarith_constant ["auxiliary"] "inj_ge") let coq_inj_gt = lazy (zarith_constant ["auxiliary"] "inj_gt") let coq_inj_neq = lazy (zarith_constant ["auxiliary"] "inj_neq") let coq_inj_eq = lazy (zarith_constant ["auxiliary"] "inj_eq") -let coq_pred_of_minus = lazy (zarith_constant ["auxiliary"] "pred_of_minus") +let coq_pred_of_minus = lazy (arith_constant ["Minus"] "pred_of_minus") let coq_fast_Zplus_assoc_r = lazy (zarith_constant ["auxiliary"] "fast_Zplus_assoc_r") let coq_fast_Zplus_assoc_l = lazy (zarith_constant ["auxiliary"] "fast_Zplus_assoc_l") let coq_fast_Zmult_assoc_r = lazy (zarith_constant ["auxiliary"] "fast_Zmult_assoc_r") -- cgit v1.2.3