FinMap.lemma-lookupM-delete is another variant of Data.Vec.Properties.lookup∘update′

2 files changed, 4 insertions, 10 deletions

diff --git a/FinMap.agda b/FinMap.agda
index 459ec7e..0df0d6f 100644
--- a/FinMap.agda
+++ b/FinMap.agda
@@ -109,16 +109,10 @@ lemma-lookupM-restrict-∉ i f (j ∷ js) i∉jjs =
   P.trans (lookup∘update′ (All.head i∉jjs) (restrict f js) (just (f j)))
           (lemma-lookupM-restrict-∉ i f js (All.tail i∉jjs))
 
-lemma-lookupM-delete : {n : ℕ} {A : Set} {i j : Fin n} → (f : FinMapMaybe n A) → i ≢ j → lookupM i (delete j f) ≡ lookupM i f
-lemma-lookupM-delete {i = zero}  {j = zero}  (_ ∷ _)  p = contradiction P.refl p
-lemma-lookupM-delete {i = zero}  {j = suc j} (_ ∷ _)  p = P.refl
-lemma-lookupM-delete {i = suc i} {j = zero}  (x ∷ xs) p = P.refl
-lemma-lookupM-delete {i = suc i} {j = suc j} (x ∷ xs) p = lemma-lookupM-delete xs (p ∘ P.cong suc)
-
 lemma-lookupM-delete-many : {n m : ℕ} {A : Set} (h : FinMapMaybe n A) → (i : Fin n) → (js : Vec (Fin n) m) → i ∉ js → lookupM i (delete-many js h) ≡ lookupM i h
 lemma-lookupM-delete-many {n} h i []       i∉[]  = P.refl
 lemma-lookupM-delete-many {n} h i (j ∷ js) i∉jjs =
-  P.trans (lemma-lookupM-delete (delete-many js h) (All.head i∉jjs))
+  P.trans (lookup∘update′ (All.head i∉jjs) (delete-many js h) nothing)
           (lemma-lookupM-delete-many h i js (All.tail i∉jjs))
 
 lemma-reshape-id : {n : ℕ} {A : Set} → (m : FinMapMaybe n A) → reshape m n ≡ m
diff --git a/Precond.agda b/Precond.agda
index 3fccfe8..9b4a66c 100644
--- a/Precond.agda
+++ b/Precond.agda
@@ -15,7 +15,7 @@ import Data.Maybe.Categorical
 open Category.Monad.RawMonad {Level.zero} Data.Maybe.Categorical.monad using (_>>=_)
 open Category.Functor.RawFunctor {Level.zero} Data.Maybe.Categorical.functor using (_<$>_)
 open import Data.Vec using (Vec ; [] ; _∷_ ; map ; lookup ; toList)
-open import Data.Vec.Properties using (map-cong ; map-∘ ; tabulate-∘ ; lookup-replicate ; tabulate-cong ; lookup∘tabulate)
+open import Data.Vec.Properties using (map-cong ; map-∘ ; tabulate-∘ ; lookup-replicate ; tabulate-cong ; lookup∘tabulate ; lookup∘update′)
 import Data.List.All
 open import Data.List.Any using (here ; there)
 open import Data.List.Membership.Setoid using (_∉_)
@@ -28,7 +28,7 @@ open P.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
 open import Relation.Nullary using (yes ; no)
 
 open import Structures using (IsFunctor ; module Shaped ; Shaped)
-open import FinMap using (FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; delete-many ; delete ; lemma-lookupM-delete ; reshape ; lemma-reshape-id)
+open import FinMap using (FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; delete-many ; delete ; reshape ; lemma-reshape-id)
 import CheckInsert
 open CheckInsert (P.decSetoid deq) using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other)
 import BFF
@@ -63,7 +63,7 @@ lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} (Data.List.A
           just x
             ≡⟨ P.cong (maybe′ just _) (P.sym px) ⟩
           maybe′ just (lookupM i (delete-many is (fromFunc g))) (lookup i h) ∎
-        inner f | no f≢i = P.cong (flip (maybe′ just) (lookup f h)) (lemma-lookupM-delete (delete-many is (fromFunc g)) f≢i)
+        inner f | no f≢i = P.cong (flip (maybe′ just) (lookup f h)) (lookup∘update′ f≢i (delete-many is (fromFunc g)) nothing)
 
 module _ (G : Get) where
   open Get G