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, 0 insertions, 961 deletions
diff --git a/contrib/correctness/examples/Handbook.v b/contrib/correctness/examples/Handbook.v deleted file mode 100644 index abb1cc76..00000000 --- a/contrib/correctness/examples/Handbook.v +++ /dev/null @@ -1,232 +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: Handbook.v 1577 2001-04-11 07:56:19Z filliatr $ *) - -(* 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 deleted file mode 100644 index 3142e906..00000000 --- a/contrib/correctness/examples/exp.v +++ /dev/null @@ -1,204 +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 *) - -(*i $Id: exp.v 1577 2001-04-11 07:56:19Z filliatr $ 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 deleted file mode 100644 index 044263ca..00000000 --- a/contrib/correctness/examples/exp_int.v +++ /dev/null @@ -1,218 +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: exp_int.v 1577 2001-04-11 07:56:19Z filliatr $ *) - -(* 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 deleted file mode 100644 index e225ba18..00000000 --- a/contrib/correctness/examples/extract.v +++ /dev/null @@ -1,43 +0,0 @@ - -(* 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 deleted file mode 100644 index 07e77140..00000000 --- a/contrib/correctness/examples/fact.v +++ /dev/null @@ -1,69 +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.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. 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. |