diff options
Diffstat (limited to 'FinMap.agda')
| -rw-r--r-- | FinMap.agda | 8 |
1 files changed, 1 insertions, 7 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 |