From 3ab245029ac43720a71dfd9c9a15e91f2312f069 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <helmut@subdivi.de>
Date: Tue, 2 Jan 2018 05:01:56 +0100
Subject: remove lemma-lookupM-insert in favour of lookup∘update
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 FinMap.agda | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

(limited to 'FinMap.agda')

diff --git a/FinMap.agda b/FinMap.agda
index 3786b97..2a17519 100644
--- 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)
-- 
cgit v1.2.3