diff options
Diffstat (limited to 'contrib7/correctness/ArrayPermut.v')
-rw-r--r-- | contrib7/correctness/ArrayPermut.v | 183 |
1 files changed, 0 insertions, 183 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. |