diff options
Diffstat (limited to 'FinMap.agda')
| -rw-r--r-- | FinMap.agda | 22 |
1 files changed, 16 insertions, 6 deletions
diff --git a/FinMap.agda b/FinMap.agda index ea4f49b..240bbe1 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -40,6 +40,11 @@ fromAscList ((f , a) ∷ xs) = insert f a (fromAscList xs) fromFunc : {A : Set} {n : ℕ} → (Fin n → A) → FinMapMaybe n A fromFunc = mapV just ∘ tabulate +reshape : {n : ℕ} {A : Set} → FinMapMaybe n A → (l : ℕ) → FinMapMaybe l A +reshape m zero = [] +reshape [] (suc l) = nothing ∷ (reshape [] l) +reshape (x ∷ xs) (suc l) = x ∷ (reshape xs l) + 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)) @@ -94,17 +99,24 @@ 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-fromFunc-tabulate : {n : ℕ} {A : Set} → (f : Fin n → A) → fromFunc f ≡ tabulate (just ∘ f) +lemma-lookupM-fromFunc : {n : ℕ} {A : Set} → (f : Fin n → A) → flip lookupM (fromFunc f) ≗ just ∘ f +lemma-lookupM-fromFunc f zero = refl +lemma-lookupM-fromFunc f (suc i) = lemma-lookupM-fromFunc (f ∘ suc) i + +lemma-fromFunc-tabulate : {n : ℕ} {A : Set} → (f : Fin n → A) → fromFunc f ≡ tabulate (Maybe.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 -... | () +lemma-lookupM-delete {i = zero} {j = zero} (_ ∷ _) p = contradiction refl p 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-reshape-id : {n : ℕ} {A : Set} → (m : FinMapMaybe n A) → reshape m n ≡ m +lemma-reshape-id [] = refl +lemma-reshape-id (x ∷ xs) = cong (_∷_ x) (lemma-reshape-id xs) + 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) @@ -112,9 +124,7 @@ lemma-disjoint-union {n} {m} f t = trans (lemma-tabulate-∘ (lemma-inner t)) (s 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 ⟩ + ≡⟨ lemma-lookupM-fromFunc 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))) |