diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /contrib/correctness/Exchange.v | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'contrib/correctness/Exchange.v')
-rw-r--r-- | contrib/correctness/Exchange.v | 95 |
1 files changed, 0 insertions, 95 deletions
diff --git a/contrib/correctness/Exchange.v b/contrib/correctness/Exchange.v deleted file mode 100644 index 035a98f2..00000000 --- a/contrib/correctness/Exchange.v +++ /dev/null @@ -1,95 +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 5920 2004-07-16 20:01:26Z herbelin $ *) - -(****************************************************************************) -(* Exchange of two elements in an array *) -(* Definition and properties *) -(****************************************************************************) - -Require Import ProgInt. -Require Import 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)%Z -> - (0 <= j < n)%Z -> - #t [i] = #t' [j] -> - #t [j] = #t' [i] -> - (forall k:Z, (0 <= k < n)%Z -> k <> i -> k <> j -> #t [k] = #t' [k]) -> - exchange t t' i j. - -(* Properties about exchanges *) - -Lemma exchange_1 : - forall (n:Z) (A:Set) (t:array n A) (i j:Z), - (0 <= i < n)%Z -> - (0 <= j < n)%Z -> #(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. -Qed. - -Hint Resolve exchange_1: v62 datatypes. - - -Lemma exchange_proof : - forall (n:Z) (A:Set) (t:array n A) (i j:Z), - (0 <= i < n)%Z -> - (0 <= j < n)%Z -> exchange (store (store t i #t [j]) j #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 #t [j]) #t [i] H_j H_k not_j_k). -auto with datatypes. -Qed. - -Hint Resolve exchange_proof: v62 datatypes. - - -Lemma exchange_sym : - forall (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. -Qed. - -Hint Resolve exchange_sym: v62 datatypes. - - -Lemma exchange_id : - forall (n:Z) (A:Set) (t t':array n A) (i j:Z), - exchange t t' i j -> - i = j -> forall k:Z, (0 <= k < n)%Z -> #t [k] = #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. -Qed. - -Hint Resolve exchange_id: v62 datatypes.
\ No newline at end of file |