diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-10-16 10:57:31 +0200 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-10-16 10:57:31 +0200 |
| commit | 71c4040262bd1c0ac5962425ee4b3bb3b51cc93b (patch) | |
| tree | 796d7fa99a2f20bdbac3e4cfcb400083d733dc93 /CheckInsert.agda | |
| parent | d2548922c7abb20fee5633be6e654430517555af (diff) | |
| download | bidiragda-71c4040262bd1c0ac5962425ee4b3bb3b51cc93b.tar.gz | |
sym result of lemma-lookupM-{i,checkI}nsert-other
Typically we have the complex term on the LHS and the simplified term on
the RHS. These lemmata did it otherwise and by symming them, we save two
syms.
Diffstat (limited to 'CheckInsert.agda')
| -rw-r--r-- | CheckInsert.agda | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/CheckInsert.agda b/CheckInsert.agda index 9dc8a60..52dffc4 100644 --- a/CheckInsert.agda +++ b/CheckInsert.agda @@ -70,7 +70,7 @@ lemma-lookupM-checkInsert i j x y h h' pl ph' | ._ | new _ with i ≟ j lemma-lookupM-checkInsert i .i x y h h' pl ph' | ._ | new pl' | yes refl = contradiction (trans (sym pl) pl') (λ ()) lemma-lookupM-checkInsert i j x y h .(insert j y h) pl refl | ._ | new _ | no i≢j = begin lookupM i (insert j y h) - ≡⟨ sym (lemma-lookupM-insert-other i j y h i≢j) ⟩ + ≡⟨ lemma-lookupM-insert-other i j y h i≢j ⟩ lookupM i h ≡⟨ pl ⟩ just x ∎ @@ -78,7 +78,7 @@ lemma-lookupM-checkInsert i j x y h .(insert j y h) pl refl | ._ | new _ | no iâ lemma-lookupM-checkInsert i j x y h h' pl () | ._ | wrong _ _ _ -lemma-lookupM-checkInsert-other : {n : â„•} → (i j : Fin n) → i ≢ j → (x : Carrier) → (h h' : FinMapMaybe n Carrier) → checkInsert j x h ≡ just h' → lookupM i h ≡ lookupM i h' +lemma-lookupM-checkInsert-other : {n : â„•} → (i j : Fin n) → i ≢ j → (x : Carrier) → (h h' : FinMapMaybe n Carrier) → checkInsert j x h ≡ just h' → lookupM i h' ≡ lookupM i h lemma-lookupM-checkInsert-other i j i≢j x h h' ph' with lookupM j h lemma-lookupM-checkInsert-other i j i≢j x h h' ph' | just y with deq x y lemma-lookupM-checkInsert-other i j i≢j x h .h refl | just y | yes x≈y = refl |