diff options
Diffstat (limited to 'contrib7/correctness')
-rw-r--r-- | contrib7/correctness/ArrayPermut.v | 183 | ||||
-rw-r--r-- | contrib7/correctness/Arrays.v | 75 | ||||
-rw-r--r-- | contrib7/correctness/Arrays_stuff.v | 16 | ||||
-rw-r--r-- | contrib7/correctness/Correctness.v | 25 | ||||
-rw-r--r-- | contrib7/correctness/Exchange.v | 94 | ||||
-rw-r--r-- | contrib7/correctness/ProgBool.v | 66 | ||||
-rw-r--r-- | contrib7/correctness/ProgInt.v | 19 | ||||
-rw-r--r-- | contrib7/correctness/ProgramsExtraction.v | 30 | ||||
-rw-r--r-- | contrib7/correctness/Programs_stuff.v | 13 | ||||
-rw-r--r-- | contrib7/correctness/Sorted.v | 198 | ||||
-rw-r--r-- | contrib7/correctness/Tuples.v | 106 | ||||
-rw-r--r-- | contrib7/correctness/preuves.v | 128 |
12 files changed, 0 insertions, 953 deletions
diff --git a/contrib7/correctness/ArrayPermut.v b/contrib7/correctness/ArrayPermut.v deleted file mode 100644 index 4a0025ca..00000000 --- a/contrib7/correctness/ArrayPermut.v +++ /dev/null @@ -1,183 +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: ArrayPermut.v,v 1.1.2.1 2004/07/16 19:30:16 herbelin Exp $ *) - -(****************************************************************************) -(* Permutations of elements in arrays *) -(* Definition and properties *) -(****************************************************************************) - -Require ProgInt. -Require Arrays. -Require Export Exchange. - -Require 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 : - (t,t':(array n A))(i,j:Z)(exchange t t' i j) -> (permut t t') - | permut_refl : - (t:(array n A))(permut t t) - | permut_sym : - (t,t':(array n A))(permut t t') -> (permut t' t) - | permut_trans : - (t,t',t'':(array n A)) - (permut t t') -> (permut t' t'') -> (permut t t''). - -Hints 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 : - (t,t':(array n A))(i,j:Z)`g <= i <= d` -> `g <= j <= d` - -> (exchange t t' i j) -> (sub_permut g d t t') - | sub_permut_refl : - (t:(array n A))(sub_permut g d t t) - | sub_permut_sym : - (t,t':(array n A))(sub_permut g d t t') -> (sub_permut g d t' t) - | sub_permut_trans : - (t,t',t'':(array n A)) - (sub_permut g d t t') -> (sub_permut g d t' t'') - -> (sub_permut g d t t''). - -Hints 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] - (i:Z) `g <= i <= d` -> #t[i] = #t'[i]. - -(* array_id is an equivalence relation *) - -Lemma array_id_refl : - (n:Z)(A:Set)(t:(array n A))(g,d:Z) - (array_id t t g d). -Proof. -Unfold array_id. -Auto with datatypes. -Save. - -Hints Resolve array_id_refl : v62 datatypes. - -Lemma array_id_sym : - (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. Intros. -Symmetry; Auto with datatypes. -Save. - -Hints Resolve array_id_sym : v62 datatypes. - -Lemma array_id_trans : - (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. Intros. -Apply trans_eq with y:=#t'[i]; Auto with datatypes. -Save. - -Hints Resolve array_id_trans: v62 datatypes. - -(* Outside the segment [g,d] the elements are equal *) - -Lemma sub_permut_id : - (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. Induction 1; Intros. -Elim H2; Intros. -Unfold array_id; 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. -Save. - -Hints Resolve sub_permut_id. - -Lemma sub_permut_eq : - (n:Z)(A:Set)(t,t':(array n A))(g,d:Z) - (sub_permut g d t t') -> - (i:Z) (`0<=i<g` \/ `d<i<n`) -> #t[i]=#t'[i]. -Proof. -Intros n A t t' g d Htt' i Hi. -Elim (sub_permut_id Htt'). Unfold array_id. -Intros. -Elim Hi; [ Intro; Apply H; Omega | Intro; Apply H0; Omega ]. -Save. - -(* sub_permut is a particular case of permutation *) - -Lemma sub_permut_is_permut : - (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. Induction 1; Intros; EAuto with datatypes. -Save. - -Hints 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 : - (N:Z)(A:Set)(t,t':(array N A)) - (g,g',d,d':Z) `d < g` - -> (sub_permut g d t t') -> (sub_permut g' d' t t'). -Proof. -Intros N A t t' g g' d d' Hdg. -(Induction 1; Intros). -(Absurd `g <= d`; Omega). -Auto with datatypes. -Auto with datatypes. -EAuto with datatypes. -Save. - -(* A sub-permutation on a segment may be extended to any segment that - * contains the first one. - *) - -Lemma sub_permut_extension : - (N:Z)(A:Set)(t,t':(array N A)) - (g,g',d,d':Z) `g' <= g` -> `d <= d'` - -> (sub_permut g d t t') -> (sub_permut g' d' t t'). -Proof. -Intros N A t t' g g' d d' Hgg' Hdd'. -(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. -Save. diff --git a/contrib7/correctness/Arrays.v b/contrib7/correctness/Arrays.v deleted file mode 100644 index 3fdc78c1..00000000 --- a/contrib7/correctness/Arrays.v +++ /dev/null @@ -1,75 +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: Arrays.v,v 1.1.2.1 2004/07/16 19:30:16 herbelin Exp $ *) - -(**********************************************) -(* 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 : (n:Z)(T:Set) T -> (array n T). - -Parameter access : (n:Z)(T:Set) (array n T) -> Z -> T. - -Parameter store : (n:Z)(T:Set) (array n T) -> Z -> T -> (array n T). - - -(* Axioms *) - -Axiom new_def : (n:Z)(T:Set)(v0:T) - (i:Z) `0<=i<n` -> (access (new n v0) i) = v0. - -Axiom store_def_1 : (n:Z)(T:Set)(t:(array n T))(v:T) - (i:Z) `0<=i<n` -> - (access (store t i v) i) = v. - -Axiom store_def_2 : (n:Z)(T:Set)(t:(array n T))(v:T) - (i:Z)(j:Z) `0<=i<n` -> `0<=j<n` -> - `i <> j` -> - (access (store t i v) j) = (access t j). - -Hints Resolve new_def store_def_1 store_def_2 : datatypes v62. - -(* A tactic to simplify access in arrays *) - -Tactic Definition ArrayAccess 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 ident) - V8only (at level 0, t at level 0). diff --git a/contrib7/correctness/Arrays_stuff.v b/contrib7/correctness/Arrays_stuff.v deleted file mode 100644 index 448b0ab6..00000000 --- a/contrib7/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: Arrays_stuff.v,v 1.1.2.1 2004/07/16 19:30:16 herbelin Exp $ *) - -Require Export Exchange. -Require Export ArrayPermut. -Require Export Sorted. - diff --git a/contrib7/correctness/Correctness.v b/contrib7/correctness/Correctness.v deleted file mode 100644 index b0fde165..00000000 --- a/contrib7/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.v,v 1.1.2.1 2004/07/16 19:30:16 herbelin Exp $ *) - -(* 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 "'". -*) diff --git a/contrib7/correctness/Exchange.v b/contrib7/correctness/Exchange.v deleted file mode 100644 index 12c8c9de..00000000 --- a/contrib7/correctness/Exchange.v +++ /dev/null @@ -1,94 +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.v,v 1.1.2.1 2004/07/16 19:30:16 herbelin Exp $ *) - -(****************************************************************************) -(* Exchange of two elements in an array *) -(* Definition and properties *) -(****************************************************************************) - -Require ProgInt. -Require 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` -> `0<=j<n` -> - (#t[i] = #t'[j]) -> - (#t[j] = #t'[i]) -> - ((k:Z)`0<=k<n` -> `k<>i` -> `k<>j` -> #t[k] = #t'[k]) -> - (exchange t t' i j). - -(* Properties about exchanges *) - -Lemma exchange_1 : (n:Z)(A:Set)(t:(array n A)) - (i,j:Z) `0<=i<n` -> `0<=j<n` -> - (access (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. -Save. - -Hints Resolve exchange_1 : v62 datatypes. - - -Lemma exchange_proof : - (n:Z)(A:Set)(t:(array n A)) - (i,j:Z) `0<=i<n` -> `0<=j<n` -> - (exchange (store (store t i (access t j)) j (access 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 (access t j)) (access t i) H_j H_k not_j_k). -Auto with datatypes. -Save. - -Hints Resolve exchange_proof : v62 datatypes. - - -Lemma exchange_sym : - (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. -Save. - -Hints Resolve exchange_sym : v62 datatypes. - - -Lemma exchange_id : - (n:Z)(A:Set)(t,t':(array n A))(i,j:Z) - (exchange t t' i j) -> - i=j -> - (k:Z) `0 <= k < n` -> (access t k)=(access 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. -Save. - -Hints Resolve exchange_id : v62 datatypes. diff --git a/contrib7/correctness/ProgBool.v b/contrib7/correctness/ProgBool.v deleted file mode 100644 index c7a7687d..00000000 --- a/contrib7/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: ProgBool.v,v 1.1.2.1 2004/07/16 19:30:16 herbelin Exp $ *) - -Require ZArith. -Require Export Bool_nat. -Require Export Sumbool. - -Definition annot_bool : - (b:bool) { b':bool | if b' then b=true else b=false }. -Proof. -Intro b. -Exists b. Case b; Trivial. -Save. - - -(* Logical connectives *) - -Definition spec_and := [A,B,C,D:Prop][b:bool]if b then A /\ C else B \/ D. - -Definition prog_bool_and : - (Q1,Q2:bool->Prop) (sig bool Q1) -> (sig bool 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. -Save. - -Definition spec_or := [A,B,C,D:Prop][b:bool]if b then A \/ C else B /\ D. - -Definition prog_bool_or : - (Q1,Q2:bool->Prop) (sig bool Q1) -> (sig bool 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. -Save. - -Definition spec_not:= [A,B:Prop][b:bool]if b then B else A. - -Definition prog_bool_not : - (Q:bool->Prop) (sig bool 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. -Save. - diff --git a/contrib7/correctness/ProgInt.v b/contrib7/correctness/ProgInt.v deleted file mode 100644 index 0ca830c2..00000000 --- a/contrib7/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: ProgInt.v,v 1.1.2.1 2004/07/16 19:30:16 herbelin Exp $ *) - -Require Export ZArith. -Require Export ZArith_dec. - -Theorem Znotzero : (x:Z){`x<>0`}+{`x=0`}. -Proof. -Intro x. Elim (Z_eq_dec x `0`) ; Auto. -Save. diff --git a/contrib7/correctness/ProgramsExtraction.v b/contrib7/correctness/ProgramsExtraction.v deleted file mode 100644 index 20f82ce4..00000000 --- a/contrib7/correctness/ProgramsExtraction.v +++ /dev/null @@ -1,30 +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: ProgramsExtraction.v,v 1.1.2.1 2004/07/16 19:30:16 herbelin Exp $ *) - -Require Export Extraction. - -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/contrib7/correctness/Programs_stuff.v b/contrib7/correctness/Programs_stuff.v deleted file mode 100644 index 00beeaeb..00000000 --- a/contrib7/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: Programs_stuff.v,v 1.1.2.1 2004/07/16 19:30:16 herbelin Exp $ *) - -Require Export Arrays_stuff. diff --git a/contrib7/correctness/Sorted.v b/contrib7/correctness/Sorted.v deleted file mode 100644 index f476142e..00000000 --- a/contrib7/correctness/Sorted.v +++ /dev/null @@ -1,198 +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: Sorted.v,v 1.1.2.1 2004/07/16 19:30:16 herbelin Exp $ *) - -Require Export Arrays. -Require ArrayPermut. - -Require ZArithRing. -Require Omega. -V7only [Import Z_scope.]. -Open Local Scope Z_scope. - -Set Implicit Arguments. - -(* Definition *) - -Definition sorted_array := - [N:Z][A:(array N Z)][deb:Z][fin:Z] - `deb<=fin` -> (x:Z) `x>=deb` -> `x<fin` -> (Zle #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 : - (N:Z)(A:(array N Z))(n:Z)(m:Z) - (sorted_array A n m) - -> (k:Z)`k>=n` - -> (i:Z) `0<=i` -> `k+i<=m` - -> (Zle (access A k) (access A `k+i`)). -Proof. -Intros N A n m H_sorted k H_k i H_i. -Pattern i. Apply natlike_ind. -Intro. -Replace `k+0` with k; Omega. (*** Ring `k+0` => BUG ***) - -Intros. -Apply Zle_trans with m:=(access A `k+x`). -Apply H0 ; Omega. - -Unfold Zs. -Replace `k+(x+1)` with `(k+x)+1`. -Unfold sorted_array in H_sorted. -Apply H_sorted ; Omega. - -Omega. - -Assumption. -Save. - -(* one element and any of the following *) - -Lemma sorted_elements : - (N:Z)(A:(array N Z))(n:Z)(m:Z)(k:Z)(l:Z) - (sorted_array A n m) - -> `k>=n` -> `l<N` -> `k<=l` -> `l<=m` - -> (Zle (access A k) (access A l)). -Proof. -Intros. -Replace l with `k+(l-k)`. -Apply sorted_elements_1 with n:=n m:=m; [Assumption | Omega | Omega | Omega]. -Omega. -Save. - -Hints Resolve sorted_elements : datatypes v62. - -(* A sub-array of a sorted array is sorted *) - -Lemma sub_sorted_array : (N:Z)(A:(array N Z))(deb:Z)(fin:Z)(i:Z)(j:Z) - (sorted_array A deb fin) -> - (`i>=deb` -> `j<=fin` -> `i<=j` -> (sorted_array A i j)). -Proof. -Unfold sorted_array. -Intros. -Apply H ; Omega. -Save. - -Hints Resolve sub_sorted_array : datatypes v62. - -(* Extension on the left of the property of being sorted *) - -Lemma left_extension : (N:Z)(A:(array N Z))(i:Z)(j:Z) - `i>0` -> `j<N` -> (sorted_array A i j) - -> (Zle #A[`i-1`] #A[i]) -> (sorted_array A `i-1` j). -Proof. -(Intros; Unfold sorted_array ; 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. -Save. - -(* Extension on the right *) - -Lemma right_extension : (N:Z)(A:(array N Z))(i:Z)(j:Z) - `i>=0` -> `j<N-1` -> (sorted_array A i j) - -> (Zle #A[j] #A[`j+1`]) -> (sorted_array A i `j+1`). -Proof. -(Intros; Unfold sorted_array ; Intros). -Elim (Z_lt_ge_dec x j). -Intro Hcut. -Apply H1 ; Omega. - -Intro HCut. -Replace x with j ; [Assumption | Omega]. -Save. - -(* Substitution of the leftmost value by a smaller value *) - -Lemma left_substitution : - (N:Z)(A:(array N Z))(i:Z)(j:Z)(v:Z) - `i>=0` -> `j<N` -> (sorted_array A i j) - -> (Zle 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 ; 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:=(access A i) ; [Assumption | Apply H_sorted ; Omega]. - -(Rewrite store_def_2; Try Omega). -(Rewrite store_def_2; Try Omega). -Apply H_sorted ; Omega. -Omega. -Save. - -(* Substitution of the rightmost value by a larger value *) - -Lemma right_substitution : - (N:Z)(A:(array N Z))(i:Z)(j:Z)(v:Z) - `i>=0` -> `j<N` -> (sorted_array A i j) - -> (Zle #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 ; 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:=(access 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. -Save. - -(* Affectation outside of the sorted region *) - -Lemma no_effect : - (N:Z)(A:(array N Z))(i:Z)(j:Z)(k:Z)(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 ; Intros. -Rewrite store_def_2 ; Try Omega. -Rewrite store_def_2 ; Try Omega. -Apply H1 ; Assumption. -Save. - -Lemma sorted_array_id : (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. -Intros Hgd x H1x H2x. -Rewrite <- (Hid x); [ Idtac | Omega ]. -Rewrite <- (Hid `x+1`); [ Idtac | Omega ]. -Apply Hsorted; Assumption. -Save. diff --git a/contrib7/correctness/Tuples.v b/contrib7/correctness/Tuples.v deleted file mode 100644 index 6e1eb03a..00000000 --- a/contrib7/correctness/Tuples.v +++ /dev/null @@ -1,106 +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.v,v 1.1.2.1 2004/07/16 19:30:16 herbelin Exp $ *) - -(* 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 : (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 : (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 : (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 : (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 : (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 : (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 : (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 : (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 : (x1:T1)(x2:T2)(x3:T3)(P x1 x2 x3) - -> (dep_tuple_3 T1 T2 T3 P). - - diff --git a/contrib7/correctness/preuves.v b/contrib7/correctness/preuves.v deleted file mode 100644 index 33659b43..00000000 --- a/contrib7/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. - - - |