1 files changed, 183 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.