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
(*i $Id: exp.v 1577 2001-04-11 07:56:19Z filliatr $ i*)
13
(* Efficient computation of X^n using
16
* X^(2n+1) = X . (X^n) ^ 2
18
* Proofs of both fonctional and imperative programs.
27
(* The specification uses the traditional definition of X^n *)
29
Fixpoint power [x,n:nat] : nat :=
32
| (S n') => (mult x (power x n'))
35
Definition square := [n:nat](mult n n).
38
(* Three lemmas are necessary to establish the forthcoming proof obligations *)
40
(* n = 2*(n/2) => (x^(n/2))^2 = x^n *)
42
Lemma exp_div2_0 : (x,n:nat)
44
-> (square (power x (div2 n)))=(power x n).
47
Intros x n. Pattern n. Apply ind_0_1_SS.
50
Intro. (Absurd (1)=(double (0)); Auto).
53
Cut n0=(double (div2 n0)).
54
Intro. Rewrite <- (H H1).
60
Rewrite <- (plus_n_Sm (div2 n0) (div2 n0)) in H0.
64
(* n = 2*(n/2)+1 => x*(x^(n/2))^2 = x^n *)
66
Lemma exp_div2_1 : (x,n:nat)
67
n=(S (double (div2 n)))
68
-> (mult x (square (power x (div2 n))))=(power x n).
71
Intros x n. Pattern n. Apply ind_0_1_SS.
73
Intro. (Absurd (0)=(S (double (0))); Auto).
78
Cut n0=(S (double (div2 n0))).
79
Intro. Rewrite <- (H H1).
85
Rewrite <- (plus_n_Sm (div2 n0) (div2 n0)) in H0.
89
(* x^(2*n) = (x^2)^n *)
91
Lemma power_2n : (x,n:nat)(power x (double n))=(power (square x) n).
93
Unfold double. Unfold square.
100
Rewrite <- (plus_n_Sm n0 n0).
105
Hints Resolve exp_div2_0 exp_div2_1.
108
(* Functional version.
110
* Here we give the functional program as an incomplete CIC term,
111
* using the tactic Refine.
113
* On this example, it really behaves as the tactic Program.
117
Lemma f_exp : (x,n:nat) { y:nat | y=(power x n) }.
120
(well_founded_induction nat lt lt_wf
121
[n:nat]{y:nat | y=(power x n) }
123
[f:(p:nat)(lt p n)->{y:nat | y=(power x p) }]
125
(left _) => (exist ? ? (S O) ?)
127
let (y,H) = (f (div2 n) ?) in
128
Cases (even_odd_dec n) of
129
(left _) => (exist ? ? (mult y y) ?)
130
| (right _) => (exist ? ? (mult x (mult y y)) ?)
136
Change (square y)=(power x n). Rewrite H. Auto with arith.
137
Change (mult x (square y))=(power x n). Rewrite H. Auto with arith.
141
(* Imperative version. *)
143
Definition even_odd_bool := [x:nat](bool_of_sumbool ? ? (even_odd_dec x)).
146
fun (x:nat)(n:nat) ->
151
while (notzerop_bool !e) do
152
{ invariant (power x n)=(mult y (power m e)) as Inv
154
(if not (even_odd_bool !e) then y := (mult !y !m))
155
{ (power x n) = (mult y (power m (double (div2 e)))) as Q };
161
{ result=(power x n) }
164
Rewrite (odd_double e0 Test1) in Inv. Rewrite Inv. Simpl. Auto with arith.
166
Rewrite (even_double e0 Test1) in Inv. Rewrite Inv. Reflexivity.
169
Exact (lt_div2 e0 Test2).
171
Rewrite Q. Unfold double. Unfold square.
173
Change (mult y1 (power m0 (double (div2 e0))))
174
= (mult y1 (power (square m0) (div2 e0))).
175
Rewrite (power_2n m0 (div2 e0)). Reflexivity.
180
Rewrite H. Rewrite H0.
185
(* Recursive version. *)
188
let rec exp (x:nat) (n:nat) : nat { variant n for lt} =
189
(if (zerop_bool n) then
192
let y = (exp x (div2 n)) in
193
if (even_odd_bool n) then
197
) { result=(power x n) }
201
Exact (lt_div2 n0 Test2).
202
Change (square y)=(power x0 n0). Rewrite Post7. Auto with arith.
203
Change (mult x0 (square y))=(power x0 n0). Rewrite Post7. Auto with arith.