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

1 files changed, 18 insertions, 18 deletions

diff --git a/contrib/correctness/examples/Handbook.v b/contrib/correctness/examples/Handbook.v
index dae2873996..26b2af4cfd 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)))`.