diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /contrib/correctness/examples/fact_int.v | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'contrib/correctness/examples/fact_int.v')
-rw-r--r-- | contrib/correctness/examples/fact_int.v | 195 |
1 files changed, 0 insertions, 195 deletions
diff --git a/contrib/correctness/examples/fact_int.v b/contrib/correctness/examples/fact_int.v deleted file mode 100644 index f463ca80..00000000 --- a/contrib/correctness/examples/fact_int.v +++ /dev/null @@ -1,195 +0,0 @@ -(***********************************************************************) -(* 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_int.v 1577 2001-04-11 07:56:19Z filliatr $ *) - -(* Proof of an imperative program computing the factorial (over type Z) *) - -Require Correctness. -Require Omega. -Require ZArithRing. - -(* We define the factorial as a relation... *) - -Inductive fact : Z -> Z -> Prop := - fact_0 : (fact `0` `1`) - | fact_S : (z,f:Z) (fact z f) -> (fact (Zs z) (Zmult (Zs z) f)). - -(* ...and then we prove that it contains a function *) - -Lemma fact_function : (z:Z) `0 <= z` -> (EX f:Z | (fact z f)). -Proof. -Intros. -Apply natlike_ind with P:=[z:Z](EX f:Z | (fact z f)). -Split with `1`. -Exact fact_0. - -Intros. -Elim H1. -Intros. -Split with `(Zs x)*x0`. -Exact (fact_S x x0 H2). - -Assumption. -Save. - -(* This lemma should belong to the ZArith library *) - -Lemma Z_mult_1 : (x,y:Z)`x>=1`->`y>=1`->`x*y>=1`. -Proof. -Intros. -Generalize H. -Apply natlike_ind with P:=[x:Z]`x >= 1`->`x*y >= 1`. -Omega. - -Intros. -Simpl. -Elim (Z_le_lt_eq_dec `0` x0 H1). -Simpl. -Unfold Zs. -Replace `(x0+1)*y` with `x0*y+y`. -Generalize H2. -Generalize `x0*y`. -Intro. -Intros. -Omega. - -Ring. - -Intros. -Rewrite <- b. -Omega. - -Omega. -Save. - -(* (fact x f) implies x>=0 and f>=1 *) - -Lemma fact_pos : (x,f:Z)(fact x f)-> `x>=0` /\ `f>=1`. -Proof. -Intros. -(Elim H; Auto). -Omega. - -Intros. -(Split; Try Omega). -(Apply Z_mult_1; Try Omega). -Save. - -(* (fact 0 x) implies x=1 *) - -Lemma fact_0_1 : (x:Z)(fact `0` x) -> `x=1`. -Proof. -Intros. -Inversion H. -Reflexivity. - -Elim (fact_pos z f H1). -Intros. -(Absurd `z >= 0`; Omega). -Save. - - -(* We define the loop invariant : y * x! = x0! *) - -Inductive invariant [y,x,x0:Z] : Prop := - c_inv : (f,f0:Z)(fact x f)->(fact x0 f0)->(Zmult y f)=f0 - -> (invariant y x x0). - -(* The following lemma is used to prove the preservation of the invariant *) - -Lemma fact_rec : (x0,x,y:Z)`0 < x` -> - (invariant y x x0) - -> (invariant `x*y` (Zpred x) x0). -Proof. -Intros x0 x y H H0. -Elim H0. -Intros. -Generalize H H0 H3. -Elim H1. -Intros. -Absurd `0 < 0`; Omega. - -Intros. -Apply c_inv with f:=f1 f0:=f0. -Cut `z+1+-1 = z`. Intro eq_z. Rewrite <- eq_z in H4. -Assumption. - -Omega. - -Assumption. - -Rewrite (Zmult_sym (Zs z) y). -Rewrite (Zmult_assoc_r y (Zs z) f1). -Auto. -Save. - - -(* This one is used to prove the proof obligation at the exit of the loop *) - -Lemma invariant_0 : (x,y:Z)(invariant y `0` x)->(fact x y). -Proof. -Intros. -Elim H. -Intros. -Generalize (fact_0_1 f H0). -Intro. -Rewrite H3 in H2. -Simpl in H2. -Replace y with `y*1`. -Rewrite H2. -Assumption. - -Omega. -Save. - - -(* At last we come to the proof itself *************************************) - -(* we declare two variable x and y *) - -Global Variable x : Z ref. -Global Variable y : Z ref. - -(* and we give the annotated program *) - -Correctness factorielle - { `0 <= x` } - begin - y := 1; - while !x <> 0 do - { invariant `0 <= x` /\ (invariant y x x@0) as Inv - variant x for (Zwf ZERO) } - y := (Zmult !x !y); - x := (Zpred !x) - done - end - { (fact x@0 y) }. -Proof. -Split. -(* decreasing *) -Unfold Zwf. Unfold Zpred. Omega. -(* preservation of the invariant *) -Split. - Unfold Zpred; Omega. - Cut `0 < x0`. Intro Hx0. - Decompose [and] Inv. - Exact (fact_rec x x0 y1 Hx0 H0). - Omega. -(* entrance of the loop *) -Split; Auto. -Elim (fact_function x Pre1). Intros. -Apply c_inv with f:=x0 f0:=x0; Auto. -Omega. -(* exit of the loop *) -Decompose [and] Inv. -Rewrite H0 in H2. -Exact (invariant_0 x y1 H2). -Save. |