exemples Correctness

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1562 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 78 insertions, 0 deletions

diff --git a/contrib/correctness/examples/fact.v b/contrib/correctness/examples/fact.v
new file mode 100644
index 0000000000..8c694d132b
--- /dev/null
+++ b/contrib/correctness/examples/fact.v
@@ -0,0 +1,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$ *)