From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001
From: Samuel Mimram <samuel.mimram@ens-lyon.org>
Date: Wed, 28 Jul 2004 21:54:47 +0000
Subject: Imported Upstream version 8.0pl1

---
 contrib/correctness/examples/exp_int.v | 218 +++++++++++++++++++++++++++++++++
 1 file changed, 218 insertions(+)
 create mode 100644 contrib/correctness/examples/exp_int.v

(limited to 'contrib/correctness/examples/exp_int.v')

diff --git a/contrib/correctness/examples/exp_int.v b/contrib/correctness/examples/exp_int.v
new file mode 100644
index 00000000..accd60c2
--- /dev/null
+++ b/contrib/correctness/examples/exp_int.v
@@ -0,0 +1,218 @@
+(***********************************************************************)
+(*  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 *)
+
+(* $Id: exp_int.v,v 1.4 2001/04/11 07:56:19 filliatr Exp $ *)
+
+(* 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 Correctness.
+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 p0.
+Replace (POS (xI p0)) with `2*(POS p0)+1`.
+Omega.
+Simpl. Auto with zarith.
+
+Intro p0.
+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 Inv
+          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] Inv.
+Rewrite (Zodd_div2 e0 H0 Test1) in H. Rewrite H.
+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] Inv.
+Rewrite (Zeven_div2 e0 Test1) in H. Rewrite H.
+Auto with zarith.
+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] Inv.
+Cut `e0 = 0`. Intro.
+Rewrite H1. Rewrite H.
+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.
-- 
cgit v1.2.3