diff options
Diffstat (limited to 'contrib/correctness/examples/fact.v')
-rw-r--r-- | contrib/correctness/examples/fact.v | 69 |
1 files changed, 69 insertions, 0 deletions
diff --git a/contrib/correctness/examples/fact.v b/contrib/correctness/examples/fact.v new file mode 100644 index 00000000..e480c806 --- /dev/null +++ b/contrib/correctness/examples/fact.v @@ -0,0 +1,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,v 1.3 2001/04/11 07:56:19 filliatr Exp $ *) + +(* 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. |