summaryrefslogtreecommitdiff
path: root/contrib/correctness/examples/fact.v
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.