From 71c4040262bd1c0ac5962425ee4b3bb3b51cc93b Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Thu, 16 Oct 2014 10:57:31 +0200 Subject: 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. --- CheckInsert.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'CheckInsert.agda') 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 -- cgit v1.2.3