blob: 8c694d132baeb737010ab8d5312c009590952719 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
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$ *)
|
