blob: 07e771401b436d5835c84b199adb1b5cae9e1a18 (
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
|
(***********************************************************************)
(* 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: fact.v 1577 2001-04-11 07:56:19Z filliatr $ *)
(* Proof of an imperative program computing the factorial (over type nat) *)
Require Correctness.
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.
|
