exemples Correctness

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1562 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 993 insertions, 0 deletions

diff --git a/contrib/correctness/examples/Handbook.v b/contrib/correctness/examples/Handbook.v
new file mode 100644
index 000000000..dae287399
--- /dev/null
+++ b/contrib/correctness/examples/Handbook.v
@@ -0,0 +1,238 @@
+(****************************************************************************)
+(*                 The Calculus of Inductive Constructions                  *)
+(*                                                                          *)
+(*                                Projet Coq                                *)
+(*                                                                          *)
+(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
+(*              Rocquencourt         Orsay          Lyon                    *)
+(*                                                                          *)
+(*                                 Coq V6.3                                 *)
+(*                               July 1st 1999                              *)
+(*                                                                          *)
+(****************************************************************************)
+(* Certification of Imperative Programs                                     *)
+(* Jean-Christophe Filliātre                                                *)
+(****************************************************************************)
+(*                                 Handbook.v                               *)
+(****************************************************************************)
+
+(* This file contains proofs of programs taken from the
+ * "Handbook of Theoretical Computer Science", volume B,
+ * chapter "Methods and Logics for Proving Programs", by P. Cousot,
+ * pp 841--993, Edited by J. van Leeuwen (c) Elsevier Science Publishers B.V.
+ * 1990.
+ * 
+ * Programs are refered to by numbers and pages.
+ *)
+
+Require Programs.
+
+Require Sumbool.
+Require Omega.
+Require Zcomplements.
+Require Zpower.
+
+(****************************************************************************)
+
+(* program (2) page 853 to compute x^y (annotated version is (25) page 860) *)
+
+(* en attendant... *)
+Parameter Zdiv2  : Z->Z.
+
+Parameter Zeven_odd_dec : (x:Z){`x=2*(Zdiv2 x)`}+{`x=2*(Zdiv2 x)+1`}.
+Definition Zodd_dec := [z:Z](sumbool_not ? ? (Zeven_odd_dec z)).
+Definition Zodd_bool := [z:Z](bool_of_sumbool ? ? (Zodd_dec z)).
+
+Axiom axiom1 : (x,y:Z) `y>0` -> `x*(Zpower x (Zpred y)) = (Zpower x y)`.
+Axiom axiom2 : (x:Z)`x>0` -> `(Zdiv2 x)<x`.
+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.
+
+Correctness pgm25
+  { `Y >= 0` }
+  begin
+    Z := 1;
+    while !Y <> 0 do
+      { 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)
+      end else begin
+      	Y := (Zdiv2 !Y);	
+	X := (Zmult !X !X)
+      end
+    done
+  end
+  { 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).
+Apply axiom1.
+Omega.
+
+Auto.
+Symmetry.
+Apply Zmult_assoc_r.
+
+Split.
+Unfold Zwf.
+Repeat (Apply conj).
+Omega.
+
+Omega.
+
+Apply axiom2. Omega.
+
+Split.
+Omega.
+
+Decompose [and] Pre2.
+Rewrite <- H1.
+Apply f_equal with f:=(Zmult Z1).
+Apply axiom3. Omega.
+
+Omega.
+
+Decompose [and] Post6.
+Rewrite <- H2.
+Rewrite H1.
+Simpl.
+Omega.
+
+Save.
+
+
+(****************************************************************************)
+
+(* program (178) page 934 to compute the factorial using global variables
+ * annotated version is (185) page 939
+ *)
+
+Parameter Zfact : Z -> Z.
+
+Axiom axiom4 : `(Zfact 0) = 1`.
+Axiom axiom5 : (x:Z) `x>0` -> `(Zfact (x-1))*x=(Zfact x)`.
+
+Correctness pgm178
+let rec F (u:unit) : unit { variant X } =
+  { `X>=0` }
+  (if !X = 0 then
+    Y := 1
+  else begin
+    label L;
+    X := (Zpred !X);
+    (F tt);
+    X := (Zs !X);
+    Y := (Zmult !Y !X)
+  end)
+  { `X=X@` /\ `Y=(Zfact X@)` }.
+Proof.
+Rewrite Test1. Rewrite axiom4. Auto.
+Unfold Zwf. Unfold Zpred. Omega.
+Unfold Zpred. Omega.
+Unfold Zs. Unfold Zpred in Post3. Split.
+Omega.
+Decompose [and] Post3.
+Rewrite H0.
+Replace `X0+(-1)+1` with X0.
+Rewrite H1.
+Replace `X0+(-1)` with `X0-1`.
+Apply axiom5.
+Omega.
+Omega.
+Omega.
+Save.
+
+
+(****************************************************************************)
+
+(* program (186) page 939 "showing the usefulness of auxiliary variables" ! *)
+
+Global Variable N : Z ref.
+Global Variable S : Z ref.
+
+Correctness pgm186
+let rec F (u:unit) : unit { variant N } =
+  { `N>=0` }
+  (if !N > 0 then begin
+    label L;
+    N := (Zpred !N);
+    (F tt);
+    S := (Zs !S);
+    (F tt);
+    N := (Zs !N)
+  end)
+  { `N=N@` /\ `S=S@+(Zpower 2 N@)-1` }.
+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.
+Split.
+Unfold Zpred in Post5. Omega.
+Decompose [and] Post4. Rewrite H1. 
+Decompose [and] Post5. Rewrite H3. Rewrite H2. 
+Replace `(Zpower 2 N0)` with `2*(Zpower 2 (Zpred N0))`. Omega.
+Symmetry.
+Replace `(Zpower 2 N0)` with `(Zpower 2 (1+(Zpred N0)))`.
+Replace `2*(Zpower 2 (Zpred N0))` with `(Zpower 2 1)*(Zpower 2 (Zpred N0))`.
+Apply Zpower_exp.
+Omega.
+Unfold Zpred. Omega.
+Auto.
+Replace `(1+(Zpred N0))` with N0; [ Auto | Unfold Zpred; Omega ].
+Split.
+Auto.
+Replace N0 with `0`; Simpl; Omega.
+Save.
+
+
+(****************************************************************************)
+
+(* program (196) page 944 (recursive factorial procedure with value-result
+ * parameters)
+ *)
+
+Correctness pgm196
+let rec F (U:Z) (V:Z ref) : unit { variant U } =
+  { `U >= 0` }
+  (if U = 0 then
+    V := 1
+  else begin
+    (F (Zpred U) V);	
+    V := (Zmult !V U)
+  end)
+  { `V = (Zfact U)` }.
+Proof.
+Symmetry. Rewrite Test1. Apply axiom4.
+Unfold Zwf. Unfold Zpred. Omega.
+Unfold Zpred. Omega.
+Rewrite Post3. 
+Unfold Zpred. Replace `U0+(-1)` with `U0-1`. Apply axiom5.
+Omega.
+Omega.
+Save.
+
+(****************************************************************************)
+
+(* program (197) page 945 (L_4 subset of Pascal) *)
+
+(*
+procedure P(X:Z; procedure Q(Z:Z));
+  procedure L(X:Z); begin Q(X-1) end;
+  begin if X>0 then P(X-1,L) else Q(X) end;
+
+procedure M(N:Z);
+  procedure R(X:Z); begin writeln(X) (* => RES := !X *) end;
+  begin P(N,R) end.
+*)
diff --git a/contrib/correctness/examples/exp.v b/contrib/correctness/examples/exp.v
new file mode 100644
index 000000000..1b6bc0b38
--- /dev/null
+++ b/contrib/correctness/examples/exp.v
@@ -0,0 +1,205 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* Certification of Imperative Programs / Jean-Christophe Filliātre *)
+
+(*i $Id$ i*)
+
+(* Efficient computation of X^n using
+ * 
+ *    X^(2n)   =     (X^n) ^ 2
+ *    X^(2n+1) = X . (X^n) ^ 2
+ *
+ * Proofs of both fonctional and imperative programs.
+ *)
+
+Require Even.
+Require Div2.
+Require Correctness.
+Require ArithRing.
+Require ZArithRing.
+
+(* The specification uses the traditional definition of X^n *)
+
+Fixpoint power [x,n:nat] : nat :=
+  Cases n of
+    O      => (S O)
+  | (S n') => (mult x (power x n'))
+  end.
+
+Definition square := [n:nat](mult n n).
+
+
+(* Three lemmas are necessary to establish the forthcoming proof obligations *)
+
+(* n = 2*(n/2) => (x^(n/2))^2 = x^n *)
+
+Lemma exp_div2_0 : (x,n:nat)
+     n=(double (div2 n)) 
+  -> (square (power x (div2 n)))=(power x n).
+Proof.
+Unfold square.
+Intros x n. Pattern n. Apply ind_0_1_SS.
+Auto.
+
+Intro. (Absurd (1)=(double (0)); Auto).
+
+Intros. Simpl.
+Cut n0=(double (div2 n0)).
+Intro. Rewrite <- (H H1).
+Ring.
+
+Simpl in H0.
+Unfold double in H0.
+Simpl in H0.
+Rewrite <- (plus_n_Sm (div2 n0) (div2 n0)) in H0.
+(Injection H0; Auto).
+Save.
+
+(* n = 2*(n/2)+1 => x*(x^(n/2))^2 = x^n *)
+
+Lemma exp_div2_1 : (x,n:nat) 
+     n=(S (double (div2 n)))
+  -> (mult x (square (power x (div2 n))))=(power x n).
+Proof.
+Unfold square.
+Intros x n. Pattern n. Apply ind_0_1_SS.
+
+Intro. (Absurd (0)=(S (double (0))); Auto).
+
+Auto.
+
+Intros. Simpl.
+Cut n0=(S (double (div2 n0))).
+Intro. Rewrite <- (H H1).
+Ring.
+
+Simpl in H0.
+Unfold double in H0.
+Simpl in H0.
+Rewrite <- (plus_n_Sm (div2 n0) (div2 n0)) in H0.
+(Injection H0; Auto).
+Save.
+
+(* x^(2*n) = (x^2)^n *)
+
+Lemma power_2n : (x,n:nat)(power x (double n))=(power (square x) n).
+Proof.
+Unfold double. Unfold square.
+Induction n.
+Auto.
+
+Intros.
+Simpl.
+Rewrite <- H.
+Rewrite <- (plus_n_Sm n0 n0).
+Simpl.
+Auto with arith.
+Save.
+
+Hints Resolve exp_div2_0 exp_div2_1.
+
+
+(* Functional version.
+ * 
+ * Here we give the functional program as an incomplete CIC term,
+ * using the tactic Refine.
+ *
+ * On this example, it really behaves as the tactic Program.
+ *)
+
+(*
+Lemma f_exp : (x,n:nat) { y:nat | y=(power x n) }.
+Proof.
+Refine [x:nat]
+  (well_founded_induction nat lt lt_wf
+    [n:nat]{y:nat | y=(power x n) }
+    [n:nat]
+    [f:(p:nat)(lt p n)->{y:nat | y=(power x p) }]
+      	     Cases (zerop n) of 
+               (left _) => (exist ? ? (S O) ?)
+      	     | (right _) => 
+      	       	  let (y,H) = (f (div2 n) ?) in 
+      	       	  Cases (even_odd_dec n) of
+      	       	    (left _) => (exist ? ? (mult y y) ?)
+                  | (right _) => (exist ? ? (mult x (mult y y)) ?)
+		  end
+	     end).
+Proof.
+Rewrite a. Auto.
+Exact (lt_div2 n a).
+Change (square y)=(power x n). Rewrite H. Auto with arith.
+Change (mult x (square y))=(power x n). Rewrite H. Auto with arith.
+Save.
+*)
+
+(* Imperative version. *)
+
+Definition even_odd_bool := [x:nat](bool_of_sumbool ? ? (even_odd_dec x)).
+
+Correctness i_exp
+  fun (x:nat)(n:nat) ->
+    let y = ref (S O) in
+    let m = ref x in
+    let e = ref n in
+    begin
+      while (notzerop_bool !e) do
+        { invariant (power x n)=(mult y (power m e)) as I
+          variant e for lt }
+        (if not (even_odd_bool !e) then y := (mult !y !m))
+          { (power x n) = (mult y (power m (double (div2 e)))) as Q };
+        m := (square !m);
+        e := (div2 !e)
+      done;
+      !y
+    end
+    { result=(power x n) }
+.
+Proof.
+Rewrite (odd_double e0 Test1) in I. Rewrite I. Simpl. Auto with arith.
+
+Rewrite (even_double e0 Test1) in I. Rewrite I. Reflexivity.
+
+Split.
+
+Exact (lt_div2 e0 Test2).
+
+Rewrite Q. Unfold double. Unfold square.
+Simpl. 
+Change (mult y1 (power m0 (double (div2 e0))))
+     = (mult y1 (power (square m0) (div2 e0))).
+Rewrite (power_2n m0 (div2 e0)). Reflexivity.
+
+Auto with arith.
+
+Decompose [and] I.
+Rewrite H0. Rewrite H1.
+Auto with arith.
+Save.
+
+
+(* Recursive version. *)
+
+Correctness r_exp
+  let rec exp (x:nat) (n:nat) : nat { variant n for lt} =
+    (if (zerop_bool n) then
+       (S O)
+     else
+       let y = (exp x (div2 n)) in
+       if (even_odd_bool n) then
+         (mult y y)
+       else
+         (mult x (mult y y))
+    ) { result=(power x n) }
+.
+Proof.
+Rewrite Test2. Auto.
+Exact (lt_div2 n0 Test2).
+Change (square y)=(power x0 n0). Rewrite Post7. Auto with arith.
+Change (mult x0 (square y))=(power x0 n0). Rewrite Post7. Auto with arith.
+Save.
diff --git a/contrib/correctness/examples/exp_int.v b/contrib/correctness/examples/exp_int.v
new file mode 100644
index 000000000..dc55eafa1
--- /dev/null
+++ b/contrib/correctness/examples/exp_int.v
@@ -0,0 +1,225 @@
+(****************************************************************************)
+(*                 The Calculus of Inductive Constructions                  *)
+(*                                                                          *)
+(*                                Projet Coq                                *)
+(*                                                                          *)
+(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
+(*              Rocquencourt         Orsay          Lyon                    *)
+(*                                                                          *)
+(*                                 Coq V6.3                                 *)
+(*                               July 1st 1999                              *)
+(*                                                                          *)
+(****************************************************************************)
+(* Certification of Imperative Programs                                     *)
+(* Jean-Christophe Filliātre                                                *)
+(****************************************************************************)
+(*                                  exp_int.v                               *)
+(****************************************************************************)
+
+(* Efficient computation of X^n using
+ * 
+ *    X^(2n)   =     (X^n) ^ 2
+ *    X^(2n+1) = X . (X^n) ^ 2
+ *
+ * Proofs of both fonctional and imperative programs.
+ *)
+
+Require Zpower.
+Require Zcomplements.
+
+Require Programs.
+Require ZArithRing.
+Require Omega.
+
+Definition Zdouble := [n:Z]`2*n`.
+
+Definition Zsquare := [n:Z](Zmult n n).
+
+(* Some auxiliary lemmas about Zdiv2 are necessary *)
+
+Lemma Zdiv2_ge_0 : (x:Z) `x >= 0` -> `(Zdiv2 x) >= 0`.
+Proof.
+Destruct x; Auto with zarith.
+Destruct p; Auto with zarith.
+Simpl. Omega.
+Intros. (Absurd `(NEG p) >= 0`; Red; Auto with zarith).
+Save.
+
+Lemma Zdiv2_lt : (x:Z) `x > 0` -> `(Zdiv2 x) < x`.
+Proof.
+Destruct x.
+Intro. Absurd `0 > 0`; [ Omega | Assumption ].
+Destruct p; Auto with zarith.
+
+Simpl.
+Intro p.
+Replace (POS (xI p0)) with `2*(POS p0)+1`.
+Omega.
+Simpl. Auto with zarith.
+
+Intro p.
+Simpl.
+Replace (POS (xO p0)) with `2*(POS p0)`.
+Omega.
+Simpl. Auto with zarith.
+
+Simpl. Omega.
+
+Intros. 
+Absurd `(NEG p) > 0`; Red; Auto with zarith.
+Elim p; Auto with zarith.
+Omega.
+Save.
+
+(* A property of Zpower:  x^(2*n) = (x^2)^n *)
+
+Lemma Zpower_2n : 
+  (x,n:Z)`n >= 0` -> (Zpower x (Zdouble n))=(Zpower (Zsquare x) n).
+Proof.
+Unfold Zdouble.
+Intros x n Hn.
+Replace `2*n` with `n+n`.
+Rewrite Zpower_exp.
+Pattern n.
+Apply natlike_ind.
+
+Simpl. Auto with zarith.
+
+Intros.
+Unfold Zs.
+Rewrite Zpower_exp.
+Rewrite Zpower_exp.
+Replace (Zpower x `1`) with x.
+Replace (Zpower (Zsquare x) `1`) with (Zsquare x).
+Rewrite <- H0.
+Unfold Zsquare.
+Ring.
+
+Unfold Zpower; Unfold Zpower_pos; Simpl. Omega.
+
+Unfold Zpower; Unfold Zpower_pos; Simpl. Omega.
+
+Omega.
+Omega.
+Omega.
+Omega.
+Omega.
+Assumption.
+Assumption.
+Omega.
+Save.
+
+
+(* The program *)
+
+Correctness i_exp
+  fun (x:Z)(n:Z) ->
+    { `n >= 0` }
+   (let y = ref 1 in
+    let m = ref x in
+    let e = ref n in
+    begin
+      while !e > 0 do
+        { invariant (Zpower x n)=(Zmult y (Zpower m e)) /\ `e>=0` as I
+          variant e }
+        (if not (Zeven_odd_bool !e) then y := (Zmult !y !m))
+          { (Zpower x n) = (Zmult y (Zpower m (Zdouble (Zdiv2 e)))) as Q };
+        m := (Zsquare !m);
+        e := (Zdiv2 !e)
+      done;
+      !y
+    end)
+    { result=(Zpower x n) }
+.
+Proof.
+(* Zodd *)
+Decompose [and] I.
+Rewrite (Zodd_div2 e0 H1 Test1) in H0. Rewrite H0.
+Rewrite Zpower_exp.
+Unfold Zdouble.
+Replace (Zpower m0 `1`) with m0.
+Ring.
+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.
+Auto with zarith.
+(* Zwf /\ I *)
+Split.
+(* Zwf *)
+Unfold Zwf.
+Repeat Split.
+Generalize (Zdiv2_ge_0 e0); Omega.
+Omega.
+Exact (Zdiv2_lt e0 Test2).
+(* invariant *)
+Split.
+Rewrite Q. Unfold Zdouble. Unfold Zsquare.
+Rewrite (Zpower_2n).
+Trivial.
+Generalize (Zdiv2_ge_0 e0); Omega.
+Generalize (Zdiv2_ge_0 e0); Omega.
+Split; [ Ring | Assumption ].
+(* exit fo loop *)
+Decompose [and] I.
+Cut `e0 = 0`. Intro.
+Rewrite H. Rewrite H0.
+Simpl; Ring.
+Omega.
+Save.
+
+
+(* Recursive version. *)
+
+Correctness r_exp
+  let rec exp (x:Z) (n:Z) : Z { variant n } =
+    { `n >= 0` }
+    (if n = 0 then
+       1
+     else
+       let y = (exp x (Zdiv2 n)) in
+       (if (Zeven_odd_bool n) then
+       	  (Zmult y y)
+        else
+          (Zmult x (Zmult y y))) { result=(Zpower x n) as Q }
+    ) 
+    { result=(Zpower x n) }
+.
+Proof.
+Rewrite Test2. Auto with zarith.
+(* w.f. *)
+Unfold Zwf.
+Repeat Split.
+Generalize (Zdiv2_ge_0 n0) ; Omega.
+Omega.
+Generalize (Zdiv2_lt n0) ; Omega.
+(* rec. call *)
+Generalize (Zdiv2_ge_0 n0) ; Omega.
+(* invariant: case even *)
+Generalize (Zeven_div2 n0 Test1).
+Intro Heq. Rewrite Heq.
+Rewrite Post4.
+Replace `2*(Zdiv2 n0)` with `(Zdiv2 n0)+(Zdiv2 n0)`.
+Rewrite Zpower_exp.
+Auto with zarith.
+Generalize (Zdiv2_ge_0 n0) ; Omega.
+Generalize (Zdiv2_ge_0 n0) ; Omega.
+Omega.
+(* invariant: cas odd *)
+Generalize (Zodd_div2 n0 Pre1 Test1).
+Intro Heq. Rewrite Heq.
+Rewrite Post4.
+Rewrite Zpower_exp.
+Replace `2*(Zdiv2 n0)` with `(Zdiv2 n0)+(Zdiv2 n0)`.
+Rewrite Zpower_exp.
+Replace `(Zpower x0 1)` with x0.
+Ring.
+Unfold Zpower; Unfold Zpower_pos; Simpl. Omega.
+Generalize (Zdiv2_ge_0 n0) ; Omega.
+Generalize (Zdiv2_ge_0 n0) ; Omega.
+Omega.
+Generalize (Zdiv2_ge_0 n0) ; Omega.
+Omega.
+Save.
diff --git a/contrib/correctness/examples/extract.v b/contrib/correctness/examples/extract.v
new file mode 100644
index 000000000..e225ba187
--- /dev/null
+++ b/contrib/correctness/examples/extract.v
@@ -0,0 +1,43 @@
+
+(* Tests d'extraction *)
+
+Require ProgramsExtraction.
+Save State Ici "test extraction".
+
+(* exp *)
+
+Require exp.
+Write Caml File "exp" [ i_exp r_exp ].
+
+(* exp_int *)
+
+Restore State Ici.
+Require exp_int.
+Write Caml File "exp_int" [ i_exp r_exp ].
+
+(* fact *)
+
+Restore State Ici.
+Require fact.
+Initialize x with (S (S (S O))).
+Initialize y with O.
+Write Caml File "fact" [ factorielle ].
+
+(* fact_int *)
+
+Restore State Ici.
+Require fact_int.
+Initialize x with `3`.
+Initialize y with `0`.
+Write Caml File "fact_int" [ factorielle ].
+
+(* Handbook *)
+
+Restore State Ici.
+Require Handbook.
+Initialize X with `3`.
+Initialize Y with `3`.
+Initialize Z with `3`.
+Initialize N with `3`.
+Initialize S with `3`.
+Write Caml File "Handbook" [ pgm178 pgm186 pgm196 ].
diff --git a/contrib/correctness/examples/fact.v b/contrib/correctness/examples/fact.v
new file mode 100644
index 000000000..8c694d132
--- /dev/null
+++ b/contrib/correctness/examples/fact.v
@@ -0,0 +1,78 @@
+(****************************************************************************)
+(*                 The Calculus of Inductive Constructions                  *)
+(*                                                                          *)
+(*                                Projet Coq                                *)
+(*                                                                          *)
+(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
+(*              Rocquencourt         Orsay          Lyon                    *)
+(*                                                                          *)
+(*                                 Coq V6.3                                 *)
+(*                               July 1st 1999                              *)
+(*                                                                          *)
+(****************************************************************************)
+(* Certification of Imperative Programs                                     *)
+(* Jean-Christophe Filliātre                                                *)
+(****************************************************************************)
+(*                                   fact.v                                 *)
+(****************************************************************************)
+
+(* Proof of an imperative program computing the factorial (over type nat) *)
+
+Require Programs.
+Require Omega.
+Require Arith.
+
+Fixpoint fact [n:nat] : nat :=
+  Cases n of
+    O     => (S O)
+  | (S p) => (mult n (fact p))
+  end.
+
+(* (x * y) * (x-1)! = y * x!  *)
+
+Lemma fact_rec : (x,y:nat)(lt O x) ->
+  (mult (mult x y) (fact (pred x))) = (mult y (fact x)).
+Proof.
+Intros x y H.
+Generalize (mult_sym x y). Intro H1. Rewrite H1.
+Generalize (mult_assoc_r y x (fact (pred x))). Intro H2. Rewrite H2.
+Apply (f_equal nat nat [x:nat](mult y x)).
+Generalize H. Elim x; Auto with arith.
+Save.
+
+
+(* we declare two variables x and y *)
+
+Global Variable x : nat ref.
+Global Variable y : nat ref.
+
+(* we give the annotated program *)
+
+Correctness factorielle 
+  begin
+    y := (S O);
+    while (notzerop_bool !x) do
+      { invariant (mult y (fact x)) = (fact x@0) as I
+        variant x for lt }
+      y := (mult !x !y);
+      x := (pred !x)
+    done
+  end
+  { y = (fact x@0) }.
+Proof.
+Split.
+(* decreasing of the variant *)
+Omega.
+(* preservation of the invariant *)
+Rewrite <- I. Exact (fact_rec x0 y1 Test1).
+(* entrance of loop *)
+Auto with arith.
+(* exit of loop *)
+Elim I. Intros H1 H2.
+Rewrite H2 in H1.
+Rewrite <- H1.
+Auto with arith.
+Save.
+
+
+(* $Id$ *)
diff --git a/contrib/correctness/examples/fact_int.v b/contrib/correctness/examples/fact_int.v
new file mode 100644
index 000000000..99e79f7ac
--- /dev/null
+++ b/contrib/correctness/examples/fact_int.v
@@ -0,0 +1,204 @@
+(****************************************************************************)
+(*                 The Calculus of Inductive Constructions                  *)
+(*                                                                          *)
+(*                                Projet Coq                                *)
+(*                                                                          *)
+(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
+(*              Rocquencourt         Orsay          Lyon                    *)
+(*                                                                          *)
+(*                                 Coq V6.3                                 *)
+(*                               July 1st 1999                              *)
+(*                                                                          *)
+(****************************************************************************)
+(* Certification of Imperative Programs                                     *)
+(* Jean-Christophe Filliātre                                                *)
+(****************************************************************************)
+(*                                fact_int.v                                *)
+(****************************************************************************)
+
+(* Proof of an imperative program computing the factorial (over type Z) *)
+
+Require Programs.
+Require Omega.
+Require ZArithRing.
+
+(* We define the factorial as a relation... *)
+
+Inductive fact : Z -> Z -> Prop :=
+    fact_0 : (fact `0` `1`)
+  | fact_S : (z,f:Z) (fact z f) -> (fact (Zs z) (Zmult (Zs z) f)).
+
+(* ...and then we prove that it contains a function *)
+
+Lemma fact_function : (z:Z) `0 <= z` -> (EX f:Z | (fact z f)).
+Proof.
+Intros.
+Apply natlike_ind with P:=[z:Z](EX f:Z | (fact z f)).
+Split with `1`.
+Exact fact_0.
+
+Intros.
+Elim H1.
+Intros.
+Split with `(Zs x)*x0`.
+Exact (fact_S x x0 H2).
+
+Assumption.
+Save.
+
+(* This lemma should belong to the ZArith library *)
+
+Lemma Z_mult_1 : (x,y:Z)`x>=1`->`y>=1`->`x*y>=1`.
+Proof.
+Intros.
+Generalize H.
+Apply natlike_ind with P:=[x:Z]`x >= 1`->`x*y >= 1`.
+Omega.
+
+Intros.
+Simpl.
+Elim (Z_le_lt_eq_dec `0` x0 H1).
+Simpl.
+Unfold Zs.
+Replace `(x0+1)*y` with `x0*y+y`.
+Generalize H2.
+Generalize `x0*y`.
+Intro.
+Intros.
+Omega.
+
+Ring.
+
+Intros.
+Rewrite <- y0.
+Omega.
+
+Omega.
+Save.
+
+(* (fact x f) implies x>=0 and f>=1 *)
+
+Lemma fact_pos : (x,f:Z)(fact x f)-> `x>=0` /\ `f>=1`.
+Proof.
+Intros.
+(Elim H; Auto).
+Omega.
+
+Intros.
+(Split; Try Omega).
+(Apply Z_mult_1; Try Omega).
+Save.
+
+(* (fact 0 x) implies x=1 *)
+
+Lemma fact_0_1 : (x:Z)(fact `0` x) -> `x=1`.
+Proof.
+Intros.
+Inversion H.
+Reflexivity.
+
+Elim (fact_pos z f H1).
+Intros.
+(Absurd `z >= 0`; Omega).
+Save.
+
+
+(* We define the loop invariant : y * x! = x0! *)
+
+Inductive invariant [y,x,x0:Z] : Prop :=
+  c_inv : (f,f0:Z)(fact x f)->(fact x0 f0)->(Zmult y f)=f0
+       -> (invariant y x x0).
+
+(* The following lemma is used to prove the preservation of the invariant *)
+
+Lemma fact_rec : (x0,x,y:Z)`0 < x` ->
+    (invariant y x x0) 
+ -> (invariant `x*y` (Zpred x) x0).
+Proof.
+Intros x0 x y H H0.
+Elim H0.
+Intros.
+Generalize H H0 H3.
+Elim H1.
+Intros.
+Absurd `0 < 0`; Omega.
+
+Intros.
+Apply c_inv with f:=f1 f0:=f0.
+Cut `z+1+-1 = z`. Intro eq_z. Rewrite <- eq_z in H4.
+Assumption.
+
+Omega.
+
+Assumption.
+
+Rewrite (Zmult_sym (Zs z) y).                     
+Rewrite (Zmult_assoc_r y (Zs z) f1).
+Auto.
+Save.
+
+
+(* This one is used to prove the proof obligation at the exit of the loop *)
+
+Lemma invariant_0 : (x,y:Z)(invariant y `0` x)->(fact x y).
+Proof.
+Intros.
+Elim H.
+Intros.
+Generalize (fact_0_1 f H0).
+Intro.
+Rewrite H3 in H2.
+Simpl in H2.
+Replace y with `y*1`.
+Rewrite H2.
+Assumption.
+
+Omega.
+Save.
+
+
+(* At last we come to the proof itself *************************************)
+
+(* we declare two variable x and y *)
+
+Global Variable x : Z ref.
+Global Variable y : Z ref.
+
+(* and we give the annotated program *)
+
+Correctness factorielle 
+  { `0 <= x` }
+  begin
+    y := 1;
+    while !x <> 0 do
+      { invariant `0 <= x` /\ (invariant y x x@0) as I
+        variant x for (Zwf ZERO) }
+      y := (Zmult !x !y);
+      x := (Zpred !x)
+    done
+  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).
+  Omega.
+(* entrance of the loop *)
+Split; Auto.
+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.
+Exact (invariant_0 x y1 H2).
+Save.
+
+
+(* $Id$ *)