remove lemma-lookupM-insert-other in favour of lookup∘update′
[~helmut/bidiragda.git] / CheckInsert.agda
index e0e35ec..316d8b1 100644 (file)
@@ -9,6 +9,7 @@ open import Data.Fin.Properties using (_≟_)
 open import Data.Maybe using (Maybe ; nothing ; just) renaming (setoid to MaybeSetoid ; Eq to MaybeEq)
 open import Data.Vec using (Vec) renaming (_∷_ to _∷V_)
 open import Data.Vec.Equality using () renaming (module Equality to VecEq)
+open import Data.Vec.Properties using (lookup∘update′)
 open import Relation.Nullary using (Dec ; yes ; no ; _)
 open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Binary using (Setoid ; module DecSetoid)
@@ -69,7 +70,7 @@ lemma-lookupM-checkInsert i j h pl y ph'  | ._ | new _ with i ≟ j
 lemma-lookupM-checkInsert i .i h pl y ph' | ._ | new pl' | yes refl = contradiction (trans (sym pl) pl') (λ ())
 lemma-lookupM-checkInsert i j h {x} pl y refl | ._ | new _ | no i≢j = begin
   lookupM i (insert j y h)
-    ≡⟨ lemma-lookupM-insert-other i j y h i≢j ⟩
+    ≡⟨ lookup∘update′ i≢j h (just y) ⟩
   lookupM i h
     ≡⟨ pl ⟩
   just x ∎
@@ -82,4 +83,4 @@ lemma-lookupM-checkInsert-other i j i≢j x h ph' with lookupM j h
 lemma-lookupM-checkInsert-other i j i≢j x h ph' | just y with deq x y
 lemma-lookupM-checkInsert-other i j i≢j x h refl | just y | yes x≈y = refl
 lemma-lookupM-checkInsert-other i j i≢j x h () | just y | no x≉y
-lemma-lookupM-checkInsert-other i j i≢j x h refl | nothing = lemma-lookupM-insert-other i j x h i≢j
+lemma-lookupM-checkInsert-other i j i≢j x h refl | nothing = lookup∘update′ i≢j h (just x)