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, 953 insertions, 0 deletions
diff --git a/contrib7/correctness/ArrayPermut.v b/contrib7/correctness/ArrayPermut.v new file mode 100644 index 00000000..4a0025ca --- /dev/null +++ b/contrib7/correctness/ArrayPermut.v @@ -0,0 +1,183 @@ +(************************************************************************) +(* 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 new file mode 100644 index 00000000..3fdc78c1 --- /dev/null +++ b/contrib7/correctness/Arrays.v @@ -0,0 +1,75 @@ +(************************************************************************) +(* 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 new file mode 100644 index 00000000..448b0ab6 --- /dev/null +++ b/contrib7/correctness/Arrays_stuff.v @@ -0,0 +1,16 @@ +(************************************************************************) +(* 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 new file mode 100644 index 00000000..b0fde165 --- /dev/null +++ b/contrib7/correctness/Correctness.v @@ -0,0 +1,25 @@ +(************************************************************************) +(* 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 new file mode 100644 index 00000000..12c8c9de --- /dev/null +++ b/contrib7/correctness/Exchange.v @@ -0,0 +1,94 @@ +(************************************************************************) +(* 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 new file mode 100644 index 00000000..c7a7687d --- /dev/null +++ b/contrib7/correctness/ProgBool.v @@ -0,0 +1,66 @@ +(************************************************************************) +(* 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 new file mode 100644 index 00000000..0ca830c2 --- /dev/null +++ b/contrib7/correctness/ProgInt.v @@ -0,0 +1,19 @@ +(************************************************************************) +(* 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 new file mode 100644 index 00000000..20f82ce4 --- /dev/null +++ b/contrib7/correctness/ProgramsExtraction.v @@ -0,0 +1,30 @@ +(************************************************************************) +(* 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 new file mode 100644 index 00000000..00beeaeb --- /dev/null +++ b/contrib7/correctness/Programs_stuff.v @@ -0,0 +1,13 @@ +(************************************************************************) +(* 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 new file mode 100644 index 00000000..f476142e --- /dev/null +++ b/contrib7/correctness/Sorted.v @@ -0,0 +1,198 @@ +(************************************************************************) +(* 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 new file mode 100644 index 00000000..6e1eb03a --- /dev/null +++ b/contrib7/correctness/Tuples.v @@ -0,0 +1,106 @@ +(************************************************************************) +(* 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 new file mode 100644 index 00000000..33659b43 --- /dev/null +++ b/contrib7/correctness/preuves.v @@ -0,0 +1,128 @@ + +(* 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. + + + |