diff options
Diffstat (limited to 'contrib/correctness/Exchange.v')
| -rw-r--r-- | contrib/correctness/Exchange.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/contrib/correctness/Exchange.v b/contrib/correctness/Exchange.v index 2a449ba25..ddad80b35 100644 --- a/contrib/correctness/Exchange.v +++ b/contrib/correctness/Exchange.v @@ -25,23 +25,23 @@ Implicit Arguments On. 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]) -> + (#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]. + (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). +Rewrite (store_def_2 (store t i #t[j]) #t[i] H_j H_i not_j_i). Auto with datatypes. Save. |