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