diff options
Diffstat (limited to 'contrib/correctness/Exchange.v')
| -rw-r--r-- | contrib/correctness/Exchange.v | 107 |
1 files changed, 54 insertions, 53 deletions
diff --git a/contrib/correctness/Exchange.v b/contrib/correctness/Exchange.v index 85c19b48bc..8016a29271 100644 --- a/contrib/correctness/Exchange.v +++ b/contrib/correctness/Exchange.v @@ -15,80 +15,81 @@ (* Definition and properties *) (****************************************************************************) -Require ProgInt. -Require Arrays. +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` -> `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). +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 : (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]. +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. -Save. +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. -Hints Resolve exchange_1 : v62 datatypes. +Hint 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). + 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 (access t j)) (access t i) H_j H_k not_j_k). -Auto with datatypes. -Save. +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. -Hints Resolve exchange_proof : v62 datatypes. +Hint 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). + 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. -Save. +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. -Hints Resolve exchange_sym : v62 datatypes. +Hint 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). + 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. -Save. - -Hints Resolve exchange_id : v62 datatypes. +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 |