1 files changed, 94 insertions, 0 deletions
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.