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

diff --git a/Bidir.agda b/Bidir.agda
index 1022fab..ce88f1e 100644 (file)
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -15,7 +15,7 @@ open import Data.List using (List)
 open import Data.List.All using (All)
 open import Data.Vec using (Vec ; [] ; _∷_ ; toList ; map ; allFin) renaming (lookup to lookupVec)
 open import Data.Vec.Equality using () renaming (module Equality to VecEq)
-open import Data.Vec.Properties using (lookup∘tabulate ; map-cong ; map-∘ ; map-lookup-allFin)
+open import Data.Vec.Properties using (lookup∘tabulate ; lookup∘update ; map-cong ; map-∘ ; map-lookup-allFin)
 open import Data.Product using (∃ ; _×_ ; _,_ ; proj₁ ; proj₂)
 open import Function using (id ; _∘_ ; flip)
 open import Relation.Binary.Core using (refl ; _≡_)
@@ -56,7 +56,7 @@ lemma-lookupM-checkInserted i x h refl | ._ | same x' x≈x' pl = begin
     ≈⟨ MaybeEq.just (Setoid.sym A.setoid x≈x') ⟩
   just x ∎
   where open EqR (MaybeSetoid A.setoid)
-lemma-lookupM-checkInserted i x h refl | ._ | new _ = Setoid.reflexive (MaybeSetoid A.setoid) (lemma-lookupM-insert i x h)
+lemma-lookupM-checkInserted i x h refl | ._ | new _ = Setoid.reflexive (MaybeSetoid A.setoid) (lookup∘update i h (just x))
 lemma-lookupM-checkInserted i x h () | ._ | wrong _ _ _
 
 _in-domain-of_ : {m n : ℕ} {A : Set} → (is : Vec (Fin m) n) → (FinMapMaybe m A) → Set
@@ -69,7 +69,7 @@ lemma-assoc-domain (i' ∷ is') (x' ∷ xs') () | nothing | [ ph' ]
 lemma-assoc-domain (i' ∷ is') (x' ∷ xs') ph | just h' | [ ph' ] with checkInsert i' x' h' | inspect (checkInsert i' x') h' | insertionresult i' x' h'
 lemma-assoc-domain (i' ∷ is') (x' ∷ xs') refl | just h | [ ph' ] | ._ | _ | same x _ pl = All._∷_ (x , pl) (lemma-assoc-domain is' xs' ph')
 lemma-assoc-domain (i' ∷ is') (x' ∷ xs') refl | just h' | [ ph' ] | ._ | [ cI≡ ] | new _ = All._∷_
-  (x' , lemma-lookupM-insert i' x' h')
+  (x' , lookup∘update i' h' (just x'))
   (Data.List.All.map
     (λ {i} p → proj₁ p , lemma-lookupM-checkInsert i i' h' (proj₂ p) x' cI≡)
     (lemma-assoc-domain is' xs' ph'))

diff --git a/FinMap.agda b/FinMap.agda
index 3786b97..2a17519 100644 (file)
--- a/FinMap.agda
+++ b/FinMap.agda
@@ -7,6 +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.Product using (_�_ ; _,_)
 open import Data.List.All as All using (All)
 import Data.List.All.Properties as AllP
@@ -83,10 +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 : {A : Set} {n : ℕ} → (i : Fin n) → (a : A) → (m : FinMapMaybe n A) → lookupM i (insert i a m) ≡ just a
-lemma-lookupM-insert zero    a (x ∷ xs) = refl
-lemma-lookupM-insert (suc i) a (x ∷ xs) = lemma-lookupM-insert i a xs
-
 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
@@ -98,7 +95,7 @@ lemma-lookupM-restrict i f []            p = contradiction (trans (sym p) (lemma
 lemma-lookupM-restrict i f (i' ∷ is)     p with i ≟ i'
 lemma-lookupM-restrict i f (.i ∷ is) {a} p | yes refl = just-injective (begin
    just (f i)
-     ≡⟨ sym (lemma-lookupM-insert i (f i) (restrict f is)) ⟩
+     ≡⟨ sym (lookup∘update i (restrict f is) (just (f i))) ⟩
    lookupM i (insert i (f i) (restrict f is))
      ≡⟨ p ⟩
    just a ∎)
@@ -111,7 +108,7 @@ lemma-lookupM-restrict i f (i' ∷ is) {a} p | no i≢i' = lemma-lookupM-restric
 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) ≡ just (f i)
 lemma-lookupM-restrict-∈ i f [] ()
 lemma-lookupM-restrict-∈ i f (j ∷ js)  p             with i ≟ j
-lemma-lookupM-restrict-∈ i f (.i ∷ js) p             | yes refl = lemma-lookupM-insert i (f i) (restrict f js)
+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)