remove lemma-lookupM-insert-other in favour of lookup∘update′

2 files changed, 7 insertions, 12 deletions

diff --git a/CheckInsert.agda b/CheckInsert.agda
index e0e35ec..316d8b1 100644
--- a/CheckInsert.agda
+++ b/CheckInsert.agda
@@ -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)
diff --git a/FinMap.agda b/FinMap.agda
index 2a17519..8322b79 100644
--- a/FinMap.agda
+++ b/FinMap.agda
@@ -7,7 +7,7 @@ open import Data.Fin using (Fin ; zero ; suc)
 open import Data.Fin.Properties using (_≟_)
 open import Data.Vec using (Vec ; [] ; _∷_ ; _[_]≔_ ; replicate ; tabulate ; foldr ; zip ; toList) renaming (lookup to lookupVec ; map to mapV)
 open import Data.Vec.Equality using ()
-open import Data.Vec.Properties using (lookup∘update)
+open import Data.Vec.Properties using (lookup∘update ; lookup∘update′)
 open import Data.Product using (_×_ ; _,_)
 open import Data.List.All as All using (All)
 import Data.List.All.Properties as AllP
@@ -84,12 +84,6 @@ lemma-lookupM-empty : {A : Set} {n : ℕ} → (i : Fin n) → lookupM {A} i empt
 lemma-lookupM-empty zero    = refl
 lemma-lookupM-empty (suc i) = lemma-lookupM-empty i
 
-lemma-lookupM-insert-other : {A : Set} {n : ℕ} → (i j : Fin n) → (a : A) → (m : FinMapMaybe n A) → i ≢ j → lookupM i (insert j a m) ≡ lookupM i m
-lemma-lookupM-insert-other zero    zero    a m        p = contradiction refl p
-lemma-lookupM-insert-other zero    (suc j) a (x ∷ xs) p = refl
-lemma-lookupM-insert-other (suc i) zero    a (x ∷ xs) p = refl
-lemma-lookupM-insert-other (suc i) (suc j) a (x ∷ xs) p = lemma-lookupM-insert-other i j a xs (p ∘ cong suc)
-
 lemma-lookupM-restrict : {A : Set} {n m : ℕ} → (i : Fin n) → (f : Fin n → A) → (is : Vec (Fin n) m) → {a : A} → lookupM i (restrict f is) ≡ just a → f i ≡ a
 lemma-lookupM-restrict i f []            p = contradiction (trans (sym p) (lemma-lookupM-empty i)) (λ ())
 lemma-lookupM-restrict i f (i' ∷ is)     p with i ≟ i'
@@ -101,7 +95,7 @@ lemma-lookupM-restrict i f (.i ∷ is) {a} p | yes refl = just-injective (begin
    just a ∎)
 lemma-lookupM-restrict i f (i' ∷ is) {a} p | no i≢i' = lemma-lookupM-restrict i f is (begin
   lookupM i (restrict f is)
-    ≡⟨ sym (lemma-lookupM-insert-other i i' (f i') (restrict f is) i≢i') ⟩
+    ≡⟨ sym (lookup∘update′ i≢i' (restrict f is) (just (f i'))) ⟩
   lookupM i (insert i' (f i') (restrict f is))
     ≡⟨ p ⟩
   just a ∎)
@@ -111,13 +105,13 @@ lemma-lookupM-restrict-∈ i f (j ∷ js)  p             with i ≟ j
 lemma-lookupM-restrict-∈ i f (.i ∷ js) p             | yes refl = lookup∘update i (restrict f js) (just (f i))
 lemma-lookupM-restrict-∈ i f (j ∷ js) (Any.here i≡j) | no i≢j = contradiction i≡j i≢j
 lemma-lookupM-restrict-∈ i f (j ∷ js) (Any.there p)  | no i≢j =
-  trans (lemma-lookupM-insert-other i j (f j) (restrict f js) i≢j)
+  trans (lookup∘update′ i≢j (restrict f js) (just (f j)))
         (lemma-lookupM-restrict-∈ i f js p)
 
 lemma-lookupM-restrict-∉ : {A : Set} {n m : ℕ} → (i : Fin n) → (f : Fin n → A) → (js : Vec (Fin n) m) → i ∉ js → lookupM i (restrict f js) ≡ nothing
 lemma-lookupM-restrict-∉ i f []       i∉[]  = lemma-lookupM-empty i
 lemma-lookupM-restrict-∉ i f (j ∷ js) i∉jjs =
-  trans (lemma-lookupM-insert-other i j (f j) (restrict f js) (All.head i∉jjs))
+  trans (lookup∘update′ (All.head i∉jjs) (restrict f js) (just (f j)))
         (lemma-lookupM-restrict-∉ i f js (All.tail i∉jjs))
 
 lemma-tabulate-∘ : {n : ℕ} {A : Set} → {f g : Fin n → A} → f ≗ g → tabulate f ≡ tabulate g