1
(***********************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
4
(* \VV/ *************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(***********************************************************************)
9
(* Certification of Imperative Programs / Jean-Christophe Filli�tre *)
11
(* $Id: exp_int.v 1577 2001-04-11 07:56:19Z filliatr $ *)
13
(* Efficient computation of X^n using
16
* X^(2n+1) = X . (X^n) ^ 2
18
* Proofs of both fonctional and imperative programs.
28
Definition Zdouble := [n:Z]`2*n`.
30
Definition Zsquare := [n:Z](Zmult n n).
32
(* Some auxiliary lemmas about Zdiv2 are necessary *)
34
Lemma Zdiv2_ge_0 : (x:Z) `x >= 0` -> `(Zdiv2 x) >= 0`.
36
Destruct x; Auto with zarith.
37
Destruct p; Auto with zarith.
39
Intros. (Absurd `(NEG p) >= 0`; Red; Auto with zarith).
42
Lemma Zdiv2_lt : (x:Z) `x > 0` -> `(Zdiv2 x) < x`.
45
Intro. Absurd `0 > 0`; [ Omega | Assumption ].
46
Destruct p; Auto with zarith.
50
Replace (POS (xI p0)) with `2*(POS p0)+1`.
52
Simpl. Auto with zarith.
56
Replace (POS (xO p0)) with `2*(POS p0)`.
58
Simpl. Auto with zarith.
63
Absurd `(NEG p) > 0`; Red; Auto with zarith.
64
Elim p; Auto with zarith.
68
(* A property of Zpower: x^(2*n) = (x^2)^n *)
71
(x,n:Z)`n >= 0` -> (Zpower x (Zdouble n))=(Zpower (Zsquare x) n).
75
Replace `2*n` with `n+n`.
80
Simpl. Auto with zarith.
86
Replace (Zpower x `1`) with x.
87
Replace (Zpower (Zsquare x) `1`) with (Zsquare x).
92
Unfold Zpower; Unfold Zpower_pos; Simpl. Omega.
94
Unfold Zpower; Unfold Zpower_pos; Simpl. Omega.
117
{ invariant (Zpower x n)=(Zmult y (Zpower m e)) /\ `e>=0` as Inv
119
(if not (Zeven_odd_bool !e) then y := (Zmult !y !m))
120
{ (Zpower x n) = (Zmult y (Zpower m (Zdouble (Zdiv2 e)))) as Q };
126
{ result=(Zpower x n) }
131
Rewrite (Zodd_div2 e0 H0 Test1) in H. Rewrite H.
134
Replace (Zpower m0 `1`) with m0.
136
Unfold Zpower; Unfold Zpower_pos; Simpl; Ring.
137
Generalize (Zdiv2_ge_0 e0); Omega.
141
Rewrite (Zeven_div2 e0 Test1) in H. Rewrite H.
147
Generalize (Zdiv2_ge_0 e0); Omega.
149
Exact (Zdiv2_lt e0 Test2).
152
Rewrite Q. Unfold Zdouble. Unfold Zsquare.
155
Generalize (Zdiv2_ge_0 e0); Omega.
156
Generalize (Zdiv2_ge_0 e0); Omega.
157
Split; [ Ring | Assumption ].
161
Rewrite H1. Rewrite H.
167
(* Recursive version. *)
170
let rec exp (x:Z) (n:Z) : Z { variant n } =
175
let y = (exp x (Zdiv2 n)) in
176
(if (Zeven_odd_bool n) then
179
(Zmult x (Zmult y y))) { result=(Zpower x n) as Q }
181
{ result=(Zpower x n) }
184
Rewrite Test2. Auto with zarith.
188
Generalize (Zdiv2_ge_0 n0) ; Omega.
190
Generalize (Zdiv2_lt n0) ; Omega.
192
Generalize (Zdiv2_ge_0 n0) ; Omega.
193
(* invariant: case even *)
194
Generalize (Zeven_div2 n0 Test1).
195
Intro Heq. Rewrite Heq.
197
Replace `2*(Zdiv2 n0)` with `(Zdiv2 n0)+(Zdiv2 n0)`.
200
Generalize (Zdiv2_ge_0 n0) ; Omega.
201
Generalize (Zdiv2_ge_0 n0) ; Omega.
203
(* invariant: cas odd *)
204
Generalize (Zodd_div2 n0 Pre1 Test1).
205
Intro Heq. Rewrite Heq.
208
Replace `2*(Zdiv2 n0)` with `(Zdiv2 n0)+(Zdiv2 n0)`.
210
Replace `(Zpower x0 1)` with x0.
212
Unfold Zpower; Unfold Zpower_pos; Simpl. Omega.
213
Generalize (Zdiv2_ge_0 n0) ; Omega.
214
Generalize (Zdiv2_ge_0 n0) ; Omega.
216
Generalize (Zdiv2_ge_0 n0) ; Omega.