diff options
| -rwxr-xr-x | configure | 2 | ||||
| -rw-r--r-- | contrib/correctness/ArrayPermut.v | 175 | ||||
| -rw-r--r-- | contrib/correctness/Arrays.v | 78 | ||||
| -rw-r--r-- | contrib/correctness/Arrays_stuff.v | 16 | ||||
| -rw-r--r-- | contrib/correctness/Correctness.v | 25 | ||||
| -rw-r--r-- | contrib/correctness/Exchange.v | 95 | ||||
| -rw-r--r-- | contrib/correctness/ProgBool.v | 66 | ||||
| -rw-r--r-- | contrib/correctness/ProgInt.v | 19 | ||||
| -rw-r--r-- | contrib/correctness/ProgramsExtraction.v | 28 | ||||
| -rw-r--r-- | contrib/correctness/Programs_stuff.v | 13 | ||||
| -rw-r--r-- | contrib/correctness/Sorted.v | 202 | ||||
| -rw-r--r-- | contrib/correctness/Tuples.v | 98 | ||||
| -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 | ||||
| -rw-r--r-- | contrib/correctness/preuves.v | 128 |
19 files changed, 1 insertions, 1905 deletions
@@ -968,7 +968,7 @@ PRINTF=`which printf` # Subdirectories of theories/ added in coq_config.ml subdirs () { - (cd $1; find * \( -name .svn -prune \) -o \( -type d -exec $PRINTF "\"%s\";\n" {} \; \) | grep -v correctness >> "$mlconfig_file") + (cd $1; find * \( -name .svn -prune \) -o \( -type d -exec $PRINTF "\"%s\";\n" {} \; \) >> "$mlconfig_file") } echo "let theories_dirs = [" >> "$mlconfig_file" diff --git a/contrib/correctness/ArrayPermut.v b/contrib/correctness/ArrayPermut.v deleted file mode 100644 index 1c3406fd2..000000000 --- a/contrib/correctness/ArrayPermut.v +++ /dev/null @@ -1,175 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \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$ *) - -(****************************************************************************) -(* Permutations of elements in arrays *) -(* Definition and properties *) -(****************************************************************************) - -Require Import ProgInt. -Require Import Arrays. -Require Export Exchange. - -Require Import Omega. - -Set Implicit Arguments. - -(* We define "permut" as the smallest equivalence relation which contains - * transpositions i.e. exchange of two elements. - *) - -Inductive permut (n:Z) (A:Set) : array n A -> array n A -> Prop := - | exchange_is_permut : - forall (t t':array n A) (i j:Z), exchange t t' i j -> permut t t' - | permut_refl : forall t:array n A, permut t t - | permut_sym : forall t t':array n A, permut t t' -> permut t' t - | permut_trans : - forall t t' t'':array n A, permut t t' -> permut t' t'' -> permut t t''. - -Hint Resolve exchange_is_permut permut_refl permut_sym permut_trans: v62 - datatypes. - -(* We also define the permutation on a segment of an array, "sub_permut", - * the other parts of the array being unchanged - * - * One again we define it as the smallest equivalence relation containing - * transpositions on the given segment. - *) - -Inductive sub_permut (n:Z) (A:Set) (g d:Z) : -array n A -> array n A -> Prop := - | exchange_is_sub_permut : - forall (t t':array n A) (i j:Z), - (g <= i <= d)%Z -> - (g <= j <= d)%Z -> exchange t t' i j -> sub_permut g d t t' - | sub_permut_refl : forall t:array n A, sub_permut g d t t - | sub_permut_sym : - forall t t':array n A, sub_permut g d t t' -> sub_permut g d t' t - | sub_permut_trans : - forall t t' t'':array n A, - sub_permut g d t t' -> sub_permut g d t' t'' -> sub_permut g d t t''. - -Hint Resolve exchange_is_sub_permut sub_permut_refl sub_permut_sym - sub_permut_trans: v62 datatypes. - -(* To express that some parts of arrays are equal we introduce the - * property "array_id" which says that a segment is the same on two - * arrays. - *) - -Definition array_id (n:Z) (A:Set) (t t':array n A) - (g d:Z) := forall i:Z, (g <= i <= d)%Z -> #t [i] = #t' [i]. - -(* array_id is an equivalence relation *) - -Lemma array_id_refl : - forall (n:Z) (A:Set) (t:array n A) (g d:Z), array_id t t g d. -Proof. -unfold array_id in |- *. -auto with datatypes. -Qed. - -Hint Resolve array_id_refl: v62 datatypes. - -Lemma array_id_sym : - forall (n:Z) (A:Set) (t t':array n A) (g d:Z), - array_id t t' g d -> array_id t' t g d. -Proof. -unfold array_id in |- *. intros. -symmetry in |- *; auto with datatypes. -Qed. - -Hint Resolve array_id_sym: v62 datatypes. - -Lemma array_id_trans : - forall (n:Z) (A:Set) (t t' t'':array n A) (g d:Z), - array_id t t' g d -> array_id t' t'' g d -> array_id t t'' g d. -Proof. -unfold array_id in |- *. intros. -apply trans_eq with (y := #t' [i]); auto with datatypes. -Qed. - -Hint Resolve array_id_trans: v62 datatypes. - -(* Outside the segment [g,d] the elements are equal *) - -Lemma sub_permut_id : - forall (n:Z) (A:Set) (t t':array n A) (g d:Z), - sub_permut g d t t' -> - array_id t t' 0 (g - 1) /\ array_id t t' (d + 1) (n - 1). -Proof. -intros n A t t' g d. simple induction 1; intros. -elim H2; intros. -unfold array_id in |- *; split; intros. -apply H7; omega. -apply H7; omega. -auto with datatypes. -decompose [and] H1; auto with datatypes. -decompose [and] H1; decompose [and] H3; eauto with datatypes. -Qed. - -Hint Resolve sub_permut_id. - -Lemma sub_permut_eq : - forall (n:Z) (A:Set) (t t':array n A) (g d:Z), - sub_permut g d t t' -> - forall i:Z, (0 <= i < g)%Z \/ (d < i < n)%Z -> #t [i] = #t' [i]. -Proof. -intros n A t t' g d Htt' i Hi. -elim (sub_permut_id Htt'). unfold array_id in |- *. -intros. -elim Hi; [ intro; apply H; omega | intro; apply H0; omega ]. -Qed. - -(* sub_permut is a particular case of permutation *) - -Lemma sub_permut_is_permut : - forall (n:Z) (A:Set) (t t':array n A) (g d:Z), - sub_permut g d t t' -> permut t t'. -Proof. -intros n A t t' g d. simple induction 1; intros; eauto with datatypes. -Qed. - -Hint Resolve sub_permut_is_permut. - -(* If we have a sub-permutation on an empty segment, then we have a - * sub-permutation on any segment. - *) - -Lemma sub_permut_void : - forall (N:Z) (A:Set) (t t':array N A) (g g' d d':Z), - (d < g)%Z -> sub_permut g d t t' -> sub_permut g' d' t t'. -Proof. -intros N A t t' g g' d d' Hdg. -simple induction 1; intros. -absurd (g <= d)%Z; omega. -auto with datatypes. -auto with datatypes. -eauto with datatypes. -Qed. - -(* A sub-permutation on a segment may be extended to any segment that - * contains the first one. - *) - -Lemma sub_permut_extension : - forall (N:Z) (A:Set) (t t':array N A) (g g' d d':Z), - (g' <= g)%Z -> (d <= d')%Z -> sub_permut g d t t' -> sub_permut g' d' t t'. -Proof. -intros N A t t' g g' d d' Hgg' Hdd'. -simple induction 1; intros. -apply exchange_is_sub_permut with (i := i) (j := j); - [ omega | omega | assumption ]. -auto with datatypes. -auto with datatypes. -eauto with datatypes. -Qed.
\ No newline at end of file diff --git a/contrib/correctness/Arrays.v b/contrib/correctness/Arrays.v deleted file mode 100644 index 28211ff77..000000000 --- a/contrib/correctness/Arrays.v +++ /dev/null @@ -1,78 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \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$ *) - -(**********************************************) -(* Functional arrays, for use in Correctness. *) -(**********************************************) - -(* This is an axiomatization of arrays. - * - * The type (array N T) is the type of arrays ranging from 0 to N-1 - * which elements are of type T. - * - * Arrays are created with new, accessed with access and modified with store. - * - * Operations of accessing and storing are not guarded, but axioms are. - * So these arrays can be viewed as arrays where accessing and storing - * out of the bounds has no effect. - *) - - -Require Export ProgInt. - -Set Implicit Arguments. - - -(* The type of arrays *) - -Parameter array : Z -> Set -> Set. - - -(* Functions to create, access and modify arrays *) - -Parameter new : forall (n:Z) (T:Set), T -> array n T. - -Parameter access : forall (n:Z) (T:Set), array n T -> Z -> T. - -Parameter store : forall (n:Z) (T:Set), array n T -> Z -> T -> array n T. - - -(* Axioms *) - -Axiom - new_def : - forall (n:Z) (T:Set) (v0:T) (i:Z), - (0 <= i < n)%Z -> access (new n v0) i = v0. - -Axiom - store_def_1 : - forall (n:Z) (T:Set) (t:array n T) (v:T) (i:Z), - (0 <= i < n)%Z -> access (store t i v) i = v. - -Axiom - store_def_2 : - forall (n:Z) (T:Set) (t:array n T) (v:T) (i j:Z), - (0 <= i < n)%Z -> - (0 <= j < n)%Z -> i <> j -> access (store t i v) j = access t j. - -Hint Resolve new_def store_def_1 store_def_2: datatypes v62. - -(* A tactic to simplify access in arrays *) - -Ltac array_access i j H := - elim (Z_eq_dec i j); - [ intro H; rewrite H; rewrite store_def_1 - | intro H; rewrite store_def_2; [ idtac | idtac | idtac | exact H ] ]. - -(* Symbolic notation for access *) - -Notation "# t [ c ]" := (access t c) (at level 0, t at level 0).
\ No newline at end of file diff --git a/contrib/correctness/Arrays_stuff.v b/contrib/correctness/Arrays_stuff.v deleted file mode 100644 index 6d381bb22..000000000 --- a/contrib/correctness/Arrays_stuff.v +++ /dev/null @@ -1,16 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \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$ *) - -Require Export Exchange. -Require Export ArrayPermut. -Require Export Sorted. - diff --git a/contrib/correctness/Correctness.v b/contrib/correctness/Correctness.v deleted file mode 100644 index 1cf73f4e0..000000000 --- a/contrib/correctness/Correctness.v +++ /dev/null @@ -1,25 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \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$ *) - -(* Correctness is base on the tactic Refine (developped on purpose) *) - -Require Export Tuples. - -Require Export ProgInt. -Require Export ProgBool. -Require Export Zwf. - -Require Export Arrays. - -(* -Token "'". -*)
\ No newline at end of file diff --git a/contrib/correctness/Exchange.v b/contrib/correctness/Exchange.v deleted file mode 100644 index 0afb60ab2..000000000 --- a/contrib/correctness/Exchange.v +++ /dev/null @@ -1,95 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \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$ *) - -(****************************************************************************) -(* Exchange of two elements in an array *) -(* Definition and properties *) -(****************************************************************************) - -Require Import ProgInt. -Require Import Arrays. - -Set Implicit Arguments. - -(* Definition *) - -Inductive exchange (n:Z) (A:Set) (t t':array n A) (i j:Z) : Prop := - exchange_c : - (0 <= i < n)%Z -> - (0 <= j < n)%Z -> - #t [i] = #t' [j] -> - #t [j] = #t' [i] -> - (forall k:Z, (0 <= k < n)%Z -> k <> i -> k <> j -> #t [k] = #t' [k]) -> - exchange t t' i j. - -(* Properties about exchanges *) - -Lemma exchange_1 : - forall (n:Z) (A:Set) (t:array n A) (i j:Z), - (0 <= i < n)%Z -> - (0 <= j < n)%Z -> #(store (store t i #t [j]) j #t [i]) [i] = #t [j]. -Proof. -intros n A t i j H_i H_j. -case (dec_eq j i). -intro eq_i_j. rewrite eq_i_j. -auto with datatypes. -intro not_j_i. -rewrite (store_def_2 (store t i #t [j]) #t [i] H_j H_i not_j_i). -auto with datatypes. -Qed. - -Hint Resolve exchange_1: v62 datatypes. - - -Lemma exchange_proof : - forall (n:Z) (A:Set) (t:array n A) (i j:Z), - (0 <= i < n)%Z -> - (0 <= j < n)%Z -> exchange (store (store t i #t [j]) j #t [i]) t i j. -Proof. -intros n A t i j H_i H_j. -apply exchange_c; auto with datatypes. -intros k H_k not_k_i not_k_j. -cut (j <> k); auto with datatypes. intro not_j_k. -rewrite (store_def_2 (store t i #t [j]) #t [i] H_j H_k not_j_k). -auto with datatypes. -Qed. - -Hint Resolve exchange_proof: v62 datatypes. - - -Lemma exchange_sym : - forall (n:Z) (A:Set) (t t':array n A) (i j:Z), - exchange t t' i j -> exchange t' t i j. -Proof. -intros n A t t' i j H1. -elim H1. clear H1. intros. -constructor 1; auto with datatypes. -intros. rewrite (H3 k); auto with datatypes. -Qed. - -Hint Resolve exchange_sym: v62 datatypes. - - -Lemma exchange_id : - forall (n:Z) (A:Set) (t t':array n A) (i j:Z), - exchange t t' i j -> - i = j -> forall k:Z, (0 <= k < n)%Z -> #t [k] = #t' [k]. -Proof. -intros n A t t' i j Hex Heq k Hk. -elim Hex. clear Hex. intros. -rewrite Heq in H1. rewrite Heq in H2. -case (Z_eq_dec k j). - intro Heq'. rewrite Heq'. assumption. - intro Hnoteq. apply (H3 k); auto with datatypes. rewrite Heq. assumption. -Qed. - -Hint Resolve exchange_id: v62 datatypes.
\ No newline at end of file diff --git a/contrib/correctness/ProgBool.v b/contrib/correctness/ProgBool.v deleted file mode 100644 index 80c5c2549..000000000 --- a/contrib/correctness/ProgBool.v +++ /dev/null @@ -1,66 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \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$ *) - -Require Import ZArith. -Require Export Bool_nat. -Require Export Sumbool. - -Definition annot_bool : - forall b:bool, {b' : bool | if b' then b = true else b = false}. -Proof. -intro b. -exists b. case b; trivial. -Qed. - - -(* Logical connectives *) - -Definition spec_and (A B C D:Prop) (b:bool) := if b then A /\ C else B \/ D. - -Definition prog_bool_and : - forall Q1 Q2:bool -> Prop, - sig Q1 -> - sig Q2 -> - {b : bool | if b then Q1 true /\ Q2 true else Q1 false \/ Q2 false}. -Proof. -intros Q1 Q2 H1 H2. -elim H1. intro b1. elim H2. intro b2. -case b1; case b2; intros. -exists true; auto. -exists false; auto. exists false; auto. exists false; auto. -Qed. - -Definition spec_or (A B C D:Prop) (b:bool) := if b then A \/ C else B /\ D. - -Definition prog_bool_or : - forall Q1 Q2:bool -> Prop, - sig Q1 -> - sig Q2 -> - {b : bool | if b then Q1 true \/ Q2 true else Q1 false /\ Q2 false}. -Proof. -intros Q1 Q2 H1 H2. -elim H1. intro b1. elim H2. intro b2. -case b1; case b2; intros. -exists true; auto. exists true; auto. exists true; auto. -exists false; auto. -Qed. - -Definition spec_not (A B:Prop) (b:bool) := if b then B else A. - -Definition prog_bool_not : - forall Q:bool -> Prop, sig Q -> {b : bool | if b then Q false else Q true}. -Proof. -intros Q H. -elim H. intro b. -case b; intro. -exists false; auto. exists true; auto. -Qed. diff --git a/contrib/correctness/ProgInt.v b/contrib/correctness/ProgInt.v deleted file mode 100644 index f5a0682f2..000000000 --- a/contrib/correctness/ProgInt.v +++ /dev/null @@ -1,19 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \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$ *) - -Require Export ZArith. -Require Export ZArith_dec. - -Theorem Znotzero : forall x:Z, {x <> 0%Z} + {x = 0%Z}. -Proof. -intro x. elim (Z_eq_dec x 0); auto. -Qed.
\ No newline at end of file diff --git a/contrib/correctness/ProgramsExtraction.v b/contrib/correctness/ProgramsExtraction.v deleted file mode 100644 index ef7960747..000000000 --- a/contrib/correctness/ProgramsExtraction.v +++ /dev/null @@ -1,28 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \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$ *) - -Extract Inductive unit => unit [ "()" ]. -Extract Inductive bool => bool [ true false ]. -Extract Inductive sumbool => bool [ true false ]. - -Require Export Correctness. - -Declare ML Module "pextract". - -Grammar vernac vernac : ast := - imperative_ocaml [ "Write" "Caml" "File" stringarg($file) - "[" ne_identarg_list($idl) "]" "." ] - -> [ (IMPERATIVEEXTRACTION $file (VERNACARGLIST ($LIST $idl))) ] - -| initialize [ "Initialize" identarg($id) "with" comarg($c) "." ] - -> [ (INITIALIZE $id $c) ] -. diff --git a/contrib/correctness/Programs_stuff.v b/contrib/correctness/Programs_stuff.v deleted file mode 100644 index 1b1eb8743..000000000 --- a/contrib/correctness/Programs_stuff.v +++ /dev/null @@ -1,13 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \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$ *) - -Require Export Arrays_stuff. diff --git a/contrib/correctness/Sorted.v b/contrib/correctness/Sorted.v deleted file mode 100644 index 9d9c4c79a..000000000 --- a/contrib/correctness/Sorted.v +++ /dev/null @@ -1,202 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* Library about sorted (sub-)arrays / Nicolas Magaud, July 1998 *) - -(* $Id$ *) - -Require Export Arrays. -Require Import ArrayPermut. - -Require Import ZArithRing. -Require Import Omega. -Open Local Scope Z_scope. - -Set Implicit Arguments. - -(* Definition *) - -Definition sorted_array (N:Z) (A:array N Z) (deb fin:Z) := - deb <= fin -> forall x:Z, x >= deb -> x < fin -> #A [x] <= #A [x + 1]. - -(* Elements of a sorted sub-array are in increasing order *) - -(* one element and the next one *) - -Lemma sorted_elements_1 : - forall (N:Z) (A:array N Z) (n m:Z), - sorted_array A n m -> - forall k:Z, - k >= n -> forall i:Z, 0 <= i -> k + i <= m -> #A [k] <= #A [k + i]. -Proof. -intros N A n m H_sorted k H_k i H_i. -pattern i in |- *. apply natlike_ind. -intro. -replace (k + 0) with k; omega. (*** Ring `k+0` => BUG ***) - -intros. -apply Zle_trans with (m := #A [k + x]). -apply H0; omega. - -unfold Zsucc in |- *. -replace (k + (x + 1)) with (k + x + 1). -unfold sorted_array in H_sorted. -apply H_sorted; omega. - -omega. - -assumption. -Qed. - -(* one element and any of the following *) - -Lemma sorted_elements : - forall (N:Z) (A:array N Z) (n m k l:Z), - sorted_array A n m -> - k >= n -> l < N -> k <= l -> l <= m -> #A [k] <= #A [l]. -Proof. -intros. -replace l with (k + (l - k)). -apply sorted_elements_1 with (n := n) (m := m); - [ assumption | omega | omega | omega ]. -omega. -Qed. - -Hint Resolve sorted_elements: datatypes v62. - -(* A sub-array of a sorted array is sorted *) - -Lemma sub_sorted_array : - forall (N:Z) (A:array N Z) (deb fin i j:Z), - sorted_array A deb fin -> - i >= deb -> j <= fin -> i <= j -> sorted_array A i j. -Proof. -unfold sorted_array in |- *. -intros. -apply H; omega. -Qed. - -Hint Resolve sub_sorted_array: datatypes v62. - -(* Extension on the left of the property of being sorted *) - -Lemma left_extension : - forall (N:Z) (A:array N Z) (i j:Z), - i > 0 -> - j < N -> - sorted_array A i j -> #A [i - 1] <= #A [i] -> sorted_array A (i - 1) j. -Proof. -intros; unfold sorted_array in |- *; intros. -elim (Z_ge_lt_dec x i). (* (`x >= i`) + (`x < i`) *) -intro Hcut. -apply H1; omega. - -intro Hcut. -replace x with (i - 1). -replace (i - 1 + 1) with i; [ assumption | omega ]. - -omega. -Qed. - -(* Extension on the right *) - -Lemma right_extension : - forall (N:Z) (A:array N Z) (i j:Z), - i >= 0 -> - j < N - 1 -> - sorted_array A i j -> #A [j] <= #A [j + 1] -> sorted_array A i (j + 1). -Proof. -intros; unfold sorted_array in |- *; intros. -elim (Z_lt_ge_dec x j). -intro Hcut. -apply H1; omega. - -intro HCut. -replace x with j; [ assumption | omega ]. -Qed. - -(* Substitution of the leftmost value by a smaller value *) - -Lemma left_substitution : - forall (N:Z) (A:array N Z) (i j v:Z), - i >= 0 -> - j < N -> - sorted_array A i j -> v <= #A [i] -> sorted_array (store A i v) i j. -Proof. -intros N A i j v H_i H_j H_sorted H_v. -unfold sorted_array in |- *; intros. - -cut (x = i \/ x > i). -intro Hcut; elim Hcut; clear Hcut; intro. -rewrite H2. -rewrite store_def_1; try omega. -rewrite store_def_2; try omega. -apply Zle_trans with (m := #A [i]); [ assumption | apply H_sorted; omega ]. - -rewrite store_def_2; try omega. -rewrite store_def_2; try omega. -apply H_sorted; omega. -omega. -Qed. - -(* Substitution of the rightmost value by a larger value *) - -Lemma right_substitution : - forall (N:Z) (A:array N Z) (i j v:Z), - i >= 0 -> - j < N -> - sorted_array A i j -> #A [j] <= v -> sorted_array (store A j v) i j. -Proof. -intros N A i j v H_i H_j H_sorted H_v. -unfold sorted_array in |- *; intros. - -cut (x = j - 1 \/ x < j - 1). -intro Hcut; elim Hcut; clear Hcut; intro. -rewrite H2. -replace (j - 1 + 1) with j; [ idtac | omega ]. (*** Ring `j-1+1`. => BUG ***) -rewrite store_def_2; try omega. -rewrite store_def_1; try omega. -apply Zle_trans with (m := #A [j]). -apply sorted_elements with (n := i) (m := j); try omega; assumption. -assumption. - -rewrite store_def_2; try omega. -rewrite store_def_2; try omega. -apply H_sorted; omega. - -omega. -Qed. - -(* Affectation outside of the sorted region *) - -Lemma no_effect : - forall (N:Z) (A:array N Z) (i j k v:Z), - i >= 0 -> - j < N -> - sorted_array A i j -> - 0 <= k < i \/ j < k < N -> sorted_array (store A k v) i j. -Proof. -intros. -unfold sorted_array in |- *; intros. -rewrite store_def_2; try omega. -rewrite store_def_2; try omega. -apply H1; assumption. -Qed. - -Lemma sorted_array_id : - forall (N:Z) (t1 t2:array N Z) (g d:Z), - sorted_array t1 g d -> array_id t1 t2 g d -> sorted_array t2 g d. -Proof. -intros N t1 t2 g d Hsorted Hid. -unfold array_id in Hid. -unfold sorted_array in Hsorted. unfold sorted_array in |- *. -intros Hgd x H1x H2x. -rewrite <- (Hid x); [ idtac | omega ]. -rewrite <- (Hid (x + 1)); [ idtac | omega ]. -apply Hsorted; assumption. -Qed.
\ No newline at end of file diff --git a/contrib/correctness/Tuples.v b/contrib/correctness/Tuples.v deleted file mode 100644 index e7d710f04..000000000 --- a/contrib/correctness/Tuples.v +++ /dev/null @@ -1,98 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \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$ *) - -(* Tuples *) - -Definition tuple_1 (X:Set) := X. -Definition tuple_2 := prod. -Definition Build_tuple_2 := pair. -Definition proj_2_1 := fst. -Definition proj_2_2 := snd. - -Record tuple_3 (T1 T2 T3:Set) : Set := - {proj_3_1 : T1; proj_3_2 : T2; proj_3_3 : T3}. - -Record tuple_4 (T1 T2 T3 T4:Set) : Set := - {proj_4_1 : T1; proj_4_2 : T2; proj_4_3 : T3; proj_4_4 : T4}. - -Record tuple_5 (T1 T2 T3 T4 T5:Set) : Set := - {proj_5_1 : T1; proj_5_2 : T2; proj_5_3 : T3; proj_5_4 : T4; proj_5_5 : T5}. - -Record tuple_6 (T1 T2 T3 T4 T5 T6:Set) : Set := - {proj_6_1 : T1; - proj_6_2 : T2; - proj_6_3 : T3; - proj_6_4 : T4; - proj_6_5 : T5; - proj_6_6 : T6}. - -Record tuple_7 (T1 T2 T3 T4 T5 T6 T7:Set) : Set := - {proj_7_1 : T1; - proj_7_2 : T2; - proj_7_3 : T3; - proj_7_4 : T4; - proj_7_5 : T5; - proj_7_6 : T6; - proj_7_7 : T7}. - - -(* Existentials *) - -Definition sig_1 := sig. -Definition exist_1 := exist. - -Inductive sig_2 (T1 T2:Set) (P:T1 -> T2 -> Prop) : Set := - exist_2 : forall (x1:T1) (x2:T2), P x1 x2 -> sig_2 T1 T2 P. - -Inductive sig_3 (T1 T2 T3:Set) (P:T1 -> T2 -> T3 -> Prop) : Set := - exist_3 : forall (x1:T1) (x2:T2) (x3:T3), P x1 x2 x3 -> sig_3 T1 T2 T3 P. - - -Inductive sig_4 (T1 T2 T3 T4:Set) (P:T1 -> T2 -> T3 -> T4 -> Prop) : Set := - exist_4 : - forall (x1:T1) (x2:T2) (x3:T3) (x4:T4), - P x1 x2 x3 x4 -> sig_4 T1 T2 T3 T4 P. - -Inductive sig_5 (T1 T2 T3 T4 T5:Set) (P:T1 -> T2 -> T3 -> T4 -> T5 -> Prop) : -Set := - exist_5 : - forall (x1:T1) (x2:T2) (x3:T3) (x4:T4) (x5:T5), - P x1 x2 x3 x4 x5 -> sig_5 T1 T2 T3 T4 T5 P. - -Inductive sig_6 (T1 T2 T3 T4 T5 T6:Set) -(P:T1 -> T2 -> T3 -> T4 -> T5 -> T6 -> Prop) : Set := - exist_6 : - forall (x1:T1) (x2:T2) (x3:T3) (x4:T4) (x5:T5) - (x6:T6), P x1 x2 x3 x4 x5 x6 -> sig_6 T1 T2 T3 T4 T5 T6 P. - -Inductive sig_7 (T1 T2 T3 T4 T5 T6 T7:Set) -(P:T1 -> T2 -> T3 -> T4 -> T5 -> T6 -> T7 -> Prop) : Set := - exist_7 : - forall (x1:T1) (x2:T2) (x3:T3) (x4:T4) (x5:T5) - (x6:T6) (x7:T7), - P x1 x2 x3 x4 x5 x6 x7 -> sig_7 T1 T2 T3 T4 T5 T6 T7 P. - -Inductive sig_8 (T1 T2 T3 T4 T5 T6 T7 T8:Set) -(P:T1 -> T2 -> T3 -> T4 -> T5 -> T6 -> T7 -> T8 -> Prop) : Set := - exist_8 : - forall (x1:T1) (x2:T2) (x3:T3) (x4:T4) (x5:T5) - (x6:T6) (x7:T7) (x8:T8), - P x1 x2 x3 x4 x5 x6 x7 x8 -> sig_8 T1 T2 T3 T4 T5 T6 T7 T8 P. - -Inductive dep_tuple_2 (T1 T2:Set) (P:T1 -> T2 -> Set) : Set := - Build_dep_tuple_2 : - forall (x1:T1) (x2:T2), P x1 x2 -> dep_tuple_2 T1 T2 P. - -Inductive dep_tuple_3 (T1 T2 T3:Set) (P:T1 -> T2 -> T3 -> Set) : Set := - Build_dep_tuple_3 : - forall (x1:T1) (x2:T2) (x3:T3), P x1 x2 x3 -> dep_tuple_3 T1 T2 T3 P. - diff --git a/contrib/correctness/examples/Handbook.v b/contrib/correctness/examples/Handbook.v deleted file mode 100644 index 4be00cd15..000000000 --- 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$ *) - -(* 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 2c5a169a5..000000000 --- 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$ 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 0e35f6c51..000000000 --- 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$ *) - -(* 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 e225ba187..000000000 --- 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 fba440bb1..000000000 --- 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$ *) - -(* 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 c234c5ca3..000000000 --- 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$ *) - -(* 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. diff --git a/contrib/correctness/preuves.v b/contrib/correctness/preuves.v deleted file mode 100644 index 33659b436..000000000 --- a/contrib/correctness/preuves.v +++ /dev/null @@ -1,128 +0,0 @@ - -(* Quelques preuves sur des programmes simples, - * juste histoire d'avoir un petit bench. - *) - -Require Correctness. -Require Omega. - -Global Variable x : Z ref. -Global Variable y : Z ref. -Global Variable z : Z ref. -Global Variable i : Z ref. -Global Variable j : Z ref. -Global Variable n : Z ref. -Global Variable m : Z ref. -Variable r : Z. -Variable N : Z. -Global Variable t : array N of Z. - -(**********************************************************************) - -Require Exchange. -Require ArrayPermut. - -Correctness swap - fun (N:Z)(t:array N of Z)(i,j:Z) -> - { `0 <= i < N` /\ `0 <= j < N` } - (let v = t[i] in - begin - t[i] := t[j]; - t[j] := v - end) - { (exchange t t@ i j) }. -Proof. -Auto with datatypes. -Save. - -Correctness downheap - let rec downheap (N:Z)(t:array N of Z) : unit { variant `0` } = - (swap N t 0 0) { True } -. - -(**********************************************************************) - -Global Variable x : Z ref. -Debug on. -Correctness assign0 (x := 0) { `x=0` }. -Save. - -(**********************************************************************) - -Global Variable i : Z ref. -Debug on. -Correctness assign1 { `0 <= i` } (i := !i + 1) { `0 < i` }. -Omega. -Save. - -(**********************************************************************) - -Global Variable i : Z ref. -Debug on. -Correctness if0 { `0 <= i` } (if !i>0 then i:=!i-1 else tt) { `0 <= i` }. -Omega. -Save. - -(**********************************************************************) - -Global Variable i : Z ref. -Debug on. -Correctness assert0 { `0 <= i` } begin assert { `i=2` }; i:=!i-1 end { `i=1` }. - -(**********************************************************************) - -Correctness echange - { `0 <= i < N` /\ `0 <= j < N` } - begin - label B; - x := t[!i]; t[!i] := t[!j]; t[!j] := !x; - assert { #t[i] = #t@B[j] /\ #t[j] = #t@B[i] } - end. -Proof. -Auto with datatypes. -Save. - - -(**********************************************************************) - -(* - * while x <= y do x := x+1 done { y < x } - *) - -Correctness incrementation - while !x < !y do - { invariant True variant `(Zs y)-x` } - x := !x + 1 - done - { `y < x` }. -Proof. -Exact (Zwf_well_founded `0`). -Unfold Zwf. Omega. -Exact I. -Save. - - -(************************************************************************) - -Correctness pivot1 - begin - while (Z_lt_ge_dec !i r) do - { invariant True variant (Zminus (Zs r) i) } i := (Zs !i) - done; - while (Z_lt_ge_dec r !j) do - { invariant True variant (Zminus (Zs j) r) } j := (Zpred !j) - done - end - { `j <= r` /\ `r <= i` }. -Proof. -Exact (Zwf_well_founded `0`). -Unfold Zwf. Omega. -Exact I. -Exact (Zwf_well_founded `0`). -Unfold Zwf. Unfold Zpred. Omega. -Exact I. -Omega. -Save. - - - |