diff options
Diffstat (limited to 'contrib/correctness/examples')
| -rw-r--r-- | contrib/correctness/examples/Handbook.v | 232 | ||||
| -rw-r--r-- | contrib/correctness/examples/exp.v | 204 | ||||
| -rw-r--r-- | contrib/correctness/examples/exp_int.v | 218 | ||||
| -rw-r--r-- | contrib/correctness/examples/extract.v | 43 | ||||
| -rw-r--r-- | contrib/correctness/examples/fact.v | 69 | ||||
| -rw-r--r-- | contrib/correctness/examples/fact_int.v | 195 |
6 files changed, 961 insertions, 0 deletions
diff --git a/contrib/correctness/examples/Handbook.v b/contrib/correctness/examples/Handbook.v new file mode 100644 index 00000000..8c983a72 --- /dev/null +++ b/contrib/correctness/examples/Handbook.v @@ -0,0 +1,232 @@ +(***********************************************************************) +(* 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: Handbook.v,v 1.3 2001/04/11 07:56:19 filliatr Exp $ *) + +(* This file contains proofs of programs taken from the + * "Handbook of Theoretical Computer Science", volume B, + * chapter "Methods and Logics for Proving Programs", by P. Cousot, + * pp 841--993, Edited by J. van Leeuwen (c) Elsevier Science Publishers B.V. + * 1990. + * + * Programs are refered to by numbers and pages. + *) + +Require Correctness. + +Require Sumbool. +Require Omega. +Require Zcomplements. +Require Zpower. + +(****************************************************************************) + +(* program (2) page 853 to compute x^y (annotated version is (25) page 860) *) + +(* en attendant... *) +Parameter Zdiv2 : Z->Z. + +Parameter Zeven_odd_dec : (x:Z){`x=2*(Zdiv2 x)`}+{`x=2*(Zdiv2 x)+1`}. +Definition Zodd_dec := [z:Z](sumbool_not ? ? (Zeven_odd_dec z)). +Definition Zodd_bool := [z:Z](bool_of_sumbool ? ? (Zodd_dec z)). + +Axiom axiom1 : (x,y:Z) `y>0` -> `x*(Zpower x (Zpred y)) = (Zpower x y)`. +Axiom axiom2 : (x:Z)`x>0` -> `(Zdiv2 x)<x`. +Axiom axiom3 : (x,y:Z) `y>=0` -> `(Zpower (x*x) (Zdiv2 y)) = (Zpower x y)`. + +Global Variable X : Z ref. +Global Variable Y : Z ref. +Global Variable Z_ : Z ref. + +Correctness pgm25 + { `Y >= 0` } + begin + Z_ := 1; + while !Y <> 0 do + { invariant `Y >= 0` /\ `Z_ * (Zpower X Y) = (Zpower X@0 Y@0)` + variant Y } + if (Zodd_bool !Y) then begin + Y := (Zpred !Y); + Z_ := (Zmult !Z_ !X) + end else begin + Y := (Zdiv2 !Y); + X := (Zmult !X !X) + end + done + end + { Z_ = (Zpower X@ Y@) }. +Proof. +Split. +Unfold Zpred; Unfold Zwf; Omega. +Split. +Unfold Zpred; Omega. +Decompose [and] Pre2. +Rewrite <- H0. +Replace `Z_1*X0*(Zpower X0 (Zpred Y0))` with `Z_1*(X0*(Zpower X0 (Zpred Y0)))`. +Apply f_equal with f := (Zmult Z_1). +Apply axiom1. +Omega. + +Auto. +Symmetry. +Apply Zmult_assoc_r. + +Split. +Unfold Zwf. +Repeat (Apply conj). +Omega. + +Omega. + +Apply axiom2. Omega. + +Split. +Omega. + +Decompose [and] Pre2. +Rewrite <- H0. +Apply f_equal with f:=(Zmult Z_1). +Apply axiom3. Omega. + +Omega. + +Decompose [and] Post6. +Rewrite <- H2. +Rewrite H0. +Simpl. +Omega. + +Save. + + +(****************************************************************************) + +(* program (178) page 934 to compute the factorial using global variables + * annotated version is (185) page 939 + *) + +Parameter Zfact : Z -> Z. + +Axiom axiom4 : `(Zfact 0) = 1`. +Axiom axiom5 : (x:Z) `x>0` -> `(Zfact (x-1))*x=(Zfact x)`. + +Correctness pgm178 +let rec F (u:unit) : unit { variant X } = + { `X>=0` } + (if !X = 0 then + Y := 1 + else begin + label L; + X := (Zpred !X); + (F tt); + X := (Zs !X); + Y := (Zmult !Y !X) + end) + { `X=X@` /\ `Y=(Zfact X@)` }. +Proof. +Rewrite Test1. Rewrite axiom4. Auto. +Unfold Zwf. Unfold Zpred. Omega. +Unfold Zpred. Omega. +Unfold Zs. Unfold Zpred in Post3. Split. +Omega. +Decompose [and] Post3. +Rewrite H. +Replace `X0+(-1)+1` with X0. +Rewrite H0. +Replace `X0+(-1)` with `X0-1`. +Apply axiom5. +Omega. +Omega. +Omega. +Save. + + +(****************************************************************************) + +(* program (186) page 939 "showing the usefulness of auxiliary variables" ! *) + +Global Variable N : Z ref. +Global Variable S : Z ref. + +Correctness pgm186 +let rec F (u:unit) : unit { variant N } = + { `N>=0` } + (if !N > 0 then begin + label L; + N := (Zpred !N); + (F tt); + S := (Zs !S); + (F tt); + N := (Zs !N) + end) + { `N=N@` /\ `S=S@+(Zpower 2 N@)-1` }. +Proof. +Unfold Zwf. Unfold Zpred. Omega. +Unfold Zpred. Omega. +Decompose [and] Post5. Rewrite H. Unfold Zwf. Unfold Zpred. Omega. +Decompose [and] Post5. Rewrite H. Unfold Zpred. Omega. +Split. +Unfold Zpred in Post5. Omega. +Decompose [and] Post4. Rewrite H0. +Decompose [and] Post5. Rewrite H2. Rewrite H1. +Replace `(Zpower 2 N0)` with `2*(Zpower 2 (Zpred N0))`. Omega. +Symmetry. +Replace `(Zpower 2 N0)` with `(Zpower 2 (1+(Zpred N0)))`. +Replace `2*(Zpower 2 (Zpred N0))` with `(Zpower 2 1)*(Zpower 2 (Zpred N0))`. +Apply Zpower_exp. +Omega. +Unfold Zpred. Omega. +Auto. +Replace `(1+(Zpred N0))` with N0; [ Auto | Unfold Zpred; Omega ]. +Split. +Auto. +Replace N0 with `0`; Simpl; Omega. +Save. + + +(****************************************************************************) + +(* program (196) page 944 (recursive factorial procedure with value-result + * parameters) + *) + +Correctness pgm196 +let rec F (U:Z) (V:Z ref) : unit { variant U } = + { `U >= 0` } + (if U = 0 then + V := 1 + else begin + (F (Zpred U) V); + V := (Zmult !V U) + end) + { `V = (Zfact U)` }. +Proof. +Symmetry. Rewrite Test1. Apply axiom4. +Unfold Zwf. Unfold Zpred. Omega. +Unfold Zpred. Omega. +Rewrite Post3. +Unfold Zpred. Replace `U0+(-1)` with `U0-1`. Apply axiom5. +Omega. +Omega. +Save. + +(****************************************************************************) + +(* program (197) page 945 (L_4 subset of Pascal) *) + +(* +procedure P(X:Z; procedure Q(Z:Z)); + procedure L(X:Z); begin Q(X-1) end; + begin if X>0 then P(X-1,L) else Q(X) end; + +procedure M(N:Z); + procedure R(X:Z); begin writeln(X) (* => RES := !X *) end; + begin P(N,R) end. +*) diff --git a/contrib/correctness/examples/exp.v b/contrib/correctness/examples/exp.v new file mode 100644 index 00000000..dcfcec87 --- /dev/null +++ b/contrib/correctness/examples/exp.v @@ -0,0 +1,204 @@ +(***********************************************************************) +(* 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 *) + +(*i $Id: exp.v,v 1.3 2001/04/11 07:56:19 filliatr Exp $ i*) + +(* Efficient computation of X^n using + * + * X^(2n) = (X^n) ^ 2 + * X^(2n+1) = X . (X^n) ^ 2 + * + * Proofs of both fonctional and imperative programs. + *) + +Require Even. +Require Div2. +Require Correctness. +Require ArithRing. +Require ZArithRing. + +(* The specification uses the traditional definition of X^n *) + +Fixpoint power [x,n:nat] : nat := + Cases n of + O => (S O) + | (S n') => (mult x (power x n')) + end. + +Definition square := [n:nat](mult n n). + + +(* Three lemmas are necessary to establish the forthcoming proof obligations *) + +(* n = 2*(n/2) => (x^(n/2))^2 = x^n *) + +Lemma exp_div2_0 : (x,n:nat) + n=(double (div2 n)) + -> (square (power x (div2 n)))=(power x n). +Proof. +Unfold square. +Intros x n. Pattern n. Apply ind_0_1_SS. +Auto. + +Intro. (Absurd (1)=(double (0)); Auto). + +Intros. Simpl. +Cut n0=(double (div2 n0)). +Intro. Rewrite <- (H H1). +Ring. + +Simpl in H0. +Unfold double in H0. +Simpl in H0. +Rewrite <- (plus_n_Sm (div2 n0) (div2 n0)) in H0. +(Injection H0; Auto). +Save. + +(* n = 2*(n/2)+1 => x*(x^(n/2))^2 = x^n *) + +Lemma exp_div2_1 : (x,n:nat) + n=(S (double (div2 n))) + -> (mult x (square (power x (div2 n))))=(power x n). +Proof. +Unfold square. +Intros x n. Pattern n. Apply ind_0_1_SS. + +Intro. (Absurd (0)=(S (double (0))); Auto). + +Auto. + +Intros. Simpl. +Cut n0=(S (double (div2 n0))). +Intro. Rewrite <- (H H1). +Ring. + +Simpl in H0. +Unfold double in H0. +Simpl in H0. +Rewrite <- (plus_n_Sm (div2 n0) (div2 n0)) in H0. +(Injection H0; Auto). +Save. + +(* x^(2*n) = (x^2)^n *) + +Lemma power_2n : (x,n:nat)(power x (double n))=(power (square x) n). +Proof. +Unfold double. Unfold square. +Induction n. +Auto. + +Intros. +Simpl. +Rewrite <- H. +Rewrite <- (plus_n_Sm n0 n0). +Simpl. +Auto with arith. +Save. + +Hints Resolve exp_div2_0 exp_div2_1. + + +(* Functional version. + * + * Here we give the functional program as an incomplete CIC term, + * using the tactic Refine. + * + * On this example, it really behaves as the tactic Program. + *) + +(* +Lemma f_exp : (x,n:nat) { y:nat | y=(power x n) }. +Proof. +Refine [x:nat] + (well_founded_induction nat lt lt_wf + [n:nat]{y:nat | y=(power x n) } + [n:nat] + [f:(p:nat)(lt p n)->{y:nat | y=(power x p) }] + Cases (zerop n) of + (left _) => (exist ? ? (S O) ?) + | (right _) => + let (y,H) = (f (div2 n) ?) in + Cases (even_odd_dec n) of + (left _) => (exist ? ? (mult y y) ?) + | (right _) => (exist ? ? (mult x (mult y y)) ?) + end + end). +Proof. +Rewrite a. Auto. +Exact (lt_div2 n a). +Change (square y)=(power x n). Rewrite H. Auto with arith. +Change (mult x (square y))=(power x n). Rewrite H. Auto with arith. +Save. +*) + +(* Imperative version. *) + +Definition even_odd_bool := [x:nat](bool_of_sumbool ? ? (even_odd_dec x)). + +Correctness i_exp + fun (x:nat)(n:nat) -> + let y = ref (S O) in + let m = ref x in + let e = ref n in + begin + while (notzerop_bool !e) do + { invariant (power x n)=(mult y (power m e)) as Inv + variant e for lt } + (if not (even_odd_bool !e) then y := (mult !y !m)) + { (power x n) = (mult y (power m (double (div2 e)))) as Q }; + m := (square !m); + e := (div2 !e) + done; + !y + end + { result=(power x n) } +. +Proof. +Rewrite (odd_double e0 Test1) in Inv. Rewrite Inv. Simpl. Auto with arith. + +Rewrite (even_double e0 Test1) in Inv. Rewrite Inv. Reflexivity. + +Split. +Exact (lt_div2 e0 Test2). + +Rewrite Q. Unfold double. Unfold square. +Simpl. +Change (mult y1 (power m0 (double (div2 e0)))) + = (mult y1 (power (square m0) (div2 e0))). +Rewrite (power_2n m0 (div2 e0)). Reflexivity. + +Auto with arith. + +Decompose [and] Inv. +Rewrite H. Rewrite H0. +Auto with arith. +Save. + + +(* Recursive version. *) + +Correctness r_exp + let rec exp (x:nat) (n:nat) : nat { variant n for lt} = + (if (zerop_bool n) then + (S O) + else + let y = (exp x (div2 n)) in + if (even_odd_bool n) then + (mult y y) + else + (mult x (mult y y)) + ) { result=(power x n) } +. +Proof. +Rewrite Test2. Auto. +Exact (lt_div2 n0 Test2). +Change (square y)=(power x0 n0). Rewrite Post7. Auto with arith. +Change (mult x0 (square y))=(power x0 n0). Rewrite Post7. Auto with arith. +Save. diff --git a/contrib/correctness/examples/exp_int.v b/contrib/correctness/examples/exp_int.v new file mode 100644 index 00000000..accd60c2 --- /dev/null +++ b/contrib/correctness/examples/exp_int.v @@ -0,0 +1,218 @@ +(***********************************************************************) +(* 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: exp_int.v,v 1.4 2001/04/11 07:56:19 filliatr Exp $ *) + +(* Efficient computation of X^n using + * + * X^(2n) = (X^n) ^ 2 + * X^(2n+1) = X . (X^n) ^ 2 + * + * Proofs of both fonctional and imperative programs. + *) + +Require Zpower. +Require Zcomplements. + +Require Correctness. +Require ZArithRing. +Require Omega. + +Definition Zdouble := [n:Z]`2*n`. + +Definition Zsquare := [n:Z](Zmult n n). + +(* Some auxiliary lemmas about Zdiv2 are necessary *) + +Lemma Zdiv2_ge_0 : (x:Z) `x >= 0` -> `(Zdiv2 x) >= 0`. +Proof. +Destruct x; Auto with zarith. +Destruct p; Auto with zarith. +Simpl. Omega. +Intros. (Absurd `(NEG p) >= 0`; Red; Auto with zarith). +Save. + +Lemma Zdiv2_lt : (x:Z) `x > 0` -> `(Zdiv2 x) < x`. +Proof. +Destruct x. +Intro. Absurd `0 > 0`; [ Omega | Assumption ]. +Destruct p; Auto with zarith. + +Simpl. +Intro p0. +Replace (POS (xI p0)) with `2*(POS p0)+1`. +Omega. +Simpl. Auto with zarith. + +Intro p0. +Simpl. +Replace (POS (xO p0)) with `2*(POS p0)`. +Omega. +Simpl. Auto with zarith. + +Simpl. Omega. + +Intros. +Absurd `(NEG p) > 0`; Red; Auto with zarith. +Elim p; Auto with zarith. +Omega. +Save. + +(* A property of Zpower: x^(2*n) = (x^2)^n *) + +Lemma Zpower_2n : + (x,n:Z)`n >= 0` -> (Zpower x (Zdouble n))=(Zpower (Zsquare x) n). +Proof. +Unfold Zdouble. +Intros x n Hn. +Replace `2*n` with `n+n`. +Rewrite Zpower_exp. +Pattern n. +Apply natlike_ind. + +Simpl. Auto with zarith. + +Intros. +Unfold Zs. +Rewrite Zpower_exp. +Rewrite Zpower_exp. +Replace (Zpower x `1`) with x. +Replace (Zpower (Zsquare x) `1`) with (Zsquare x). +Rewrite <- H0. +Unfold Zsquare. +Ring. + +Unfold Zpower; Unfold Zpower_pos; Simpl. Omega. + +Unfold Zpower; Unfold Zpower_pos; Simpl. Omega. + +Omega. +Omega. +Omega. +Omega. +Omega. +Assumption. +Assumption. +Omega. +Save. + + +(* The program *) + +Correctness i_exp + fun (x:Z)(n:Z) -> + { `n >= 0` } + (let y = ref 1 in + let m = ref x in + let e = ref n in + begin + while !e > 0 do + { invariant (Zpower x n)=(Zmult y (Zpower m e)) /\ `e>=0` as Inv + variant e } + (if not (Zeven_odd_bool !e) then y := (Zmult !y !m)) + { (Zpower x n) = (Zmult y (Zpower m (Zdouble (Zdiv2 e)))) as Q }; + m := (Zsquare !m); + e := (Zdiv2 !e) + done; + !y + end) + { result=(Zpower x n) } +. +Proof. +(* Zodd *) +Decompose [and] Inv. +Rewrite (Zodd_div2 e0 H0 Test1) in H. Rewrite H. +Rewrite Zpower_exp. +Unfold Zdouble. +Replace (Zpower m0 `1`) with m0. +Ring. +Unfold Zpower; Unfold Zpower_pos; Simpl; Ring. +Generalize (Zdiv2_ge_0 e0); Omega. +Omega. +(* Zeven *) +Decompose [and] Inv. +Rewrite (Zeven_div2 e0 Test1) in H. Rewrite H. +Auto with zarith. +Split. +(* Zwf *) +Unfold Zwf. +Repeat Split. +Generalize (Zdiv2_ge_0 e0); Omega. +Omega. +Exact (Zdiv2_lt e0 Test2). +(* invariant *) +Split. +Rewrite Q. Unfold Zdouble. Unfold Zsquare. +Rewrite (Zpower_2n). +Trivial. +Generalize (Zdiv2_ge_0 e0); Omega. +Generalize (Zdiv2_ge_0 e0); Omega. +Split; [ Ring | Assumption ]. +(* exit fo loop *) +Decompose [and] Inv. +Cut `e0 = 0`. Intro. +Rewrite H1. Rewrite H. +Simpl; Ring. +Omega. +Save. + + +(* Recursive version. *) + +Correctness r_exp + let rec exp (x:Z) (n:Z) : Z { variant n } = + { `n >= 0` } + (if n = 0 then + 1 + else + let y = (exp x (Zdiv2 n)) in + (if (Zeven_odd_bool n) then + (Zmult y y) + else + (Zmult x (Zmult y y))) { result=(Zpower x n) as Q } + ) + { result=(Zpower x n) } +. +Proof. +Rewrite Test2. Auto with zarith. +(* w.f. *) +Unfold Zwf. +Repeat Split. +Generalize (Zdiv2_ge_0 n0) ; Omega. +Omega. +Generalize (Zdiv2_lt n0) ; Omega. +(* rec. call *) +Generalize (Zdiv2_ge_0 n0) ; Omega. +(* invariant: case even *) +Generalize (Zeven_div2 n0 Test1). +Intro Heq. Rewrite Heq. +Rewrite Post4. +Replace `2*(Zdiv2 n0)` with `(Zdiv2 n0)+(Zdiv2 n0)`. +Rewrite Zpower_exp. +Auto with zarith. +Generalize (Zdiv2_ge_0 n0) ; Omega. +Generalize (Zdiv2_ge_0 n0) ; Omega. +Omega. +(* invariant: cas odd *) +Generalize (Zodd_div2 n0 Pre1 Test1). +Intro Heq. Rewrite Heq. +Rewrite Post4. +Rewrite Zpower_exp. +Replace `2*(Zdiv2 n0)` with `(Zdiv2 n0)+(Zdiv2 n0)`. +Rewrite Zpower_exp. +Replace `(Zpower x0 1)` with x0. +Ring. +Unfold Zpower; Unfold Zpower_pos; Simpl. Omega. +Generalize (Zdiv2_ge_0 n0) ; Omega. +Generalize (Zdiv2_ge_0 n0) ; Omega. +Omega. +Generalize (Zdiv2_ge_0 n0) ; Omega. +Omega. +Save. diff --git a/contrib/correctness/examples/extract.v b/contrib/correctness/examples/extract.v new file mode 100644 index 00000000..e225ba18 --- /dev/null +++ b/contrib/correctness/examples/extract.v @@ -0,0 +1,43 @@ + +(* Tests d'extraction *) + +Require ProgramsExtraction. +Save State Ici "test extraction". + +(* exp *) + +Require exp. +Write Caml File "exp" [ i_exp r_exp ]. + +(* exp_int *) + +Restore State Ici. +Require exp_int. +Write Caml File "exp_int" [ i_exp r_exp ]. + +(* fact *) + +Restore State Ici. +Require fact. +Initialize x with (S (S (S O))). +Initialize y with O. +Write Caml File "fact" [ factorielle ]. + +(* fact_int *) + +Restore State Ici. +Require fact_int. +Initialize x with `3`. +Initialize y with `0`. +Write Caml File "fact_int" [ factorielle ]. + +(* Handbook *) + +Restore State Ici. +Require Handbook. +Initialize X with `3`. +Initialize Y with `3`. +Initialize Z with `3`. +Initialize N with `3`. +Initialize S with `3`. +Write Caml File "Handbook" [ pgm178 pgm186 pgm196 ]. 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. diff --git a/contrib/correctness/examples/fact_int.v b/contrib/correctness/examples/fact_int.v new file mode 100644 index 00000000..cb2b0460 --- /dev/null +++ b/contrib/correctness/examples/fact_int.v @@ -0,0 +1,195 @@ +(***********************************************************************) +(* 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,v 1.3 2001/04/11 07:56:19 filliatr Exp $ *) + +(* 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. |