diff options
Diffstat (limited to 'FinMap.agda')
| -rw-r--r-- | FinMap.agda | 24 |
1 files changed, 22 insertions, 2 deletions
diff --git a/FinMap.agda b/FinMap.agda index 9b7da07..a515a2f 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -4,11 +4,11 @@ open import Data.Nat using (ℕ ; zero ; suc) open import Data.Maybe using (Maybe ; just ; nothing ; maybe′) open import Data.Fin using (Fin ; zero ; suc) open import Data.Fin.Props using (_≟_) -open import Data.Vec using (Vec ; [] ; _∷_ ; _[_]≔_ ; replicate ; tabulate) renaming (lookup to lookupVec) +open import Data.Vec using (Vec ; [] ; _∷_ ; _[_]≔_ ; replicate ; tabulate ; foldr) renaming (lookup to lookupVec ; map to mapV) open import Data.Vec.Properties using (lookup∘tabulate) open import Data.List using (List ; [] ; _∷_ ; map ; zip) open import Data.Product using (_×_ ; _,_) -open import Function using (id ; _∘_ ; flip) +open import Function using (id ; _∘_ ; flip ; const) open import Relation.Nullary using (yes ; no) open import Relation.Nullary.Negation using (contradiction) open import Relation.Binary.Core using (_≡_ ; refl ; _≢_) @@ -46,6 +46,15 @@ union m1 m2 = fromFunc (λ f → maybe′ id (lookup f m2) (lookupM f m1)) restrict : {A : Set} {n : ℕ} → (Fin n → A) → List (Fin n) → FinMapMaybe n A restrict f is = fromAscList (zip is (map f is)) +delete : {A : Set} {n : ℕ} → Fin n → FinMapMaybe n A → FinMapMaybe n A +delete i m = m [ i ]≔ nothing + +delete-many : {A : Set} {n m : ℕ} → Vec (Fin n) m → FinMapMaybe n A → FinMapMaybe n A +delete-many = flip (foldr (const _) delete) + +partialize : {A : Set} {n : ℕ} → FinMap n A → FinMapMaybe n A +partialize = mapV just + lemma-just≢nothing : {A Whatever : Set} {a : A} {ma : Maybe A} → ma ≡ just a → ma ≡ nothing → Whatever lemma-just≢nothing refl () @@ -91,6 +100,17 @@ lemma-tabulate-∘ : {n : ℕ} {A : Set} → {f g : Fin n → A} → f ≗ g → lemma-tabulate-∘ {zero} {_} {f} {g} f≗g = refl lemma-tabulate-∘ {suc n} {_} {f} {g} f≗g = cong₂ _∷_ (f≗g zero) (lemma-tabulate-∘ (f≗g ∘ suc)) +lemma-partialize-fromFunc : {n : ℕ} {A : Set} → (f : Fin n → A) → partialize (fromFunc f) ≡ fromFunc (just ∘ f) +lemma-partialize-fromFunc {zero} f = refl +lemma-partialize-fromFunc {suc _} f = cong (_∷_ (just (f zero))) (lemma-partialize-fromFunc (f ∘ suc)) + +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 with p refl +... | () +lemma-lookupM-delete {i = zero} {j = suc j} (_ ∷ _) p = refl +lemma-lookupM-delete {i = suc i} {j = zero} (x ∷ xs) p = refl +lemma-lookupM-delete {i = suc i} {j = suc j} (x ∷ xs) p = lemma-lookupM-delete xs (p ∘ cong suc) + lemma-union-restrict : {n : ℕ} {A : Set} → (f : Fin n → A) → (is : List (Fin n)) → union (restrict f is) (fromFunc f) ≡ fromFunc f lemma-union-restrict {n} f is = lemma-tabulate-∘ (lemma-inner is) where lemma-inner : (is : List (Fin n)) → (j : Fin n) → maybe′ id (lookup j (fromFunc f)) (lookupM j (restrict f is)) ≡ f j |