From e83a3b6cce71c20ffb83475c2660e9500d18798e Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Sun, 31 Mar 2019 21:56:30 +0200 Subject: FinMap.lemma-lookupM-delete is another variant of Data.Vec.Properties.lookup∘update′ MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- FinMap.agda | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) (limited to 'FinMap.agda') 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 -- cgit v1.2.3