diff options
Diffstat (limited to 'FinMap.agda')
| -rw-r--r-- | FinMap.agda | 66 |
1 files changed, 29 insertions, 37 deletions
diff --git a/FinMap.agda b/FinMap.agda index 1fc2d16..c04c510 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -5,7 +5,7 @@ open import Data.Nat using (ℕ ; zero ; suc) open import Data.Maybe using (Maybe ; just ; nothing ; maybe′) renaming (setoid to MaybeEq) open import Data.Fin using (Fin ; zero ; suc) open import Data.Fin.Props using (_≟_) -open import Data.Vec using (Vec ; [] ; _∷_ ; _[_]≔_ ; replicate ; tabulate ; foldr) renaming (lookup to lookupVec ; map to mapV) +open import Data.Vec using (Vec ; [] ; _∷_ ; _[_]≔_ ; replicate ; tabulate ; foldr ; toList) renaming (lookup to lookupVec ; map to mapV) open import Data.Vec.Equality using () open Data.Vec.Equality.Equality using (_∷-cong_) open import Data.Vec.Properties using (lookup∘tabulate) @@ -37,17 +37,11 @@ fromAscList : {A : Set} {n : ℕ} → List (Fin n × A) → FinMapMaybe n A fromAscList [] = empty fromAscList ((f , a) ∷ xs) = insert f a (fromAscList xs) -FinMap : ℕ → Set → Set -FinMap n A = Vec A n +fromFunc : {A : Set} {n : ℕ} → (Fin n → A) → FinMapMaybe n A +fromFunc = mapV just ∘ tabulate -lookup : {A : Set} {n : ℕ} → Fin n → FinMap n A → A -lookup = lookupVec - -fromFunc : {A : Set} {n : ℕ} → (Fin n → A) → FinMap n A -fromFunc = tabulate - -union : {A : Set} {n : ℕ} → FinMapMaybe n A → FinMap n A → FinMap n A -union m1 m2 = fromFunc (λ f → maybe′ id (lookup f m2) (lookupM f m1)) +union : {A : Set} {n : ℕ} → FinMapMaybe n A → FinMapMaybe n A → FinMapMaybe n A +union m1 m2 = tabulate (λ f → maybe′ just (lookupM 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)) @@ -58,9 +52,6 @@ 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 () @@ -103,9 +94,9 @@ 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-fromFunc-tabulate : {n : ℕ} {A : Set} → (f : Fin n → A) → fromFunc f ≡ tabulate (just ∘ f) +lemma-fromFunc-tabulate {zero} f = refl +lemma-fromFunc-tabulate {suc _} f = cong (_∷_ (just (f zero))) (lemma-fromFunc-tabulate (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 @@ -114,23 +105,24 @@ 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 - lemma-inner [] j = begin - maybe′ id (lookup j (fromFunc f)) (lookupM j empty) - ≡⟨ cong (maybe′ id (lookup j (fromFunc f))) (lemma-lookupM-empty j) ⟩ - maybe′ id (lookup j (fromFunc f)) nothing - ≡⟨ refl ⟩ - lookup j (fromFunc f) - ≡⟨ lookup∘tabulate f j ⟩ - f j ∎ - lemma-inner (i ∷ is) j with j ≟ i - lemma-inner (.j ∷ is) j | yes refl = cong (maybe′ id (lookup j (fromFunc f))) - (lemma-lookupM-insert j (f j) (restrict f is)) - lemma-inner (i ∷ is) j | no j≢i = begin - maybe′ id (lookup j (fromFunc f)) (lookupM j (insert i (f i) (restrict f is))) - ≡⟨ cong (maybe′ id (lookup j (fromFunc f))) (sym (lemma-lookupM-insert-other j i (f i) (restrict f is) j≢i)) ⟩ - maybe′ id (lookup j (fromFunc f)) (lookupM j (restrict f is)) - ≡⟨ lemma-inner is j ⟩ - f j ∎ +lemma-disjoint-union : {n m : ℕ} {A : Set} → (f : Fin n → A) → (t : Vec (Fin n) m) → union (restrict f (toList t)) (delete-many t (fromFunc f)) ≡ fromFunc f +lemma-disjoint-union {n} {m} f t = trans (lemma-tabulate-∘ (lemma-inner t)) (sym (lemma-fromFunc-tabulate f)) + where lemma-inner : {m : ℕ} → (t : Vec (Fin n) m) → (x : Fin n) → maybe′ just (lookupM x (delete-many t (fromFunc f))) (lookupM x (restrict f (toList t))) ≡ just (f x) + lemma-inner [] x = begin + maybe′ just (lookupM x (fromFunc f)) (lookupM x empty) + ≡⟨ cong (maybe′ just (lookupM x (fromFunc f))) (lemma-lookupM-empty x) ⟩ + lookupM x (fromFunc f) + ≡⟨ cong (lookupM x) (lemma-fromFunc-tabulate f) ⟩ + lookupM x (tabulate (just ∘ f)) + ≡⟨ lookup∘tabulate (just ∘ f) x ⟩ + just (f x) ∎ + lemma-inner (t ∷ ts) x with x ≟ t + lemma-inner (.x ∷ ts) x | yes refl = cong (maybe′ just (lookupM x (delete-many (x ∷ ts) (fromFunc f)))) (lemma-lookupM-insert x (f x) (restrict f (toList ts))) + lemma-inner (t ∷ ts) x | no ¬p = begin + maybe′ just (lookupM x (delete-many (t ∷ ts) (fromFunc f))) (lookupM x (restrict f (toList (t ∷ ts)))) + ≡⟨ cong (maybe′ just (lookupM x (delete-many (t ∷ ts) (fromFunc f)))) (sym (lemma-lookupM-insert-other x t (f t) (restrict f (toList ts)) ¬p)) ⟩ + maybe′ just (lookupM x (delete-many (t ∷ ts) (fromFunc f))) (lookupM x (restrict f (toList ts))) + ≡⟨ cong (flip (maybe′ just) (lookupM x (restrict f (toList ts)))) (lemma-lookupM-delete (delete-many ts (fromFunc f)) ¬p) ⟩ + maybe′ just (lookupM x (delete-many ts (fromFunc f))) (lookupM x (restrict f (toList ts))) + ≡⟨ lemma-inner ts x ⟩ + just (f x) ∎ |