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

5 files changed, 34 insertions, 37 deletions

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")