From dcb452b1d1a3261ebefd7ff6885a4fa07d812e67 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Thu, 1 Aug 2024 09:20:40 +0100 Subject: [PATCH] [ new ] map-concat --- CHANGELOG.md | 5 +++++ src/Data/Vec/Properties.agda | 15 +++++++++++++++ 2 files changed, 20 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 80da9ee48e..69c41b2635 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -26,3 +26,8 @@ New modules Additions to existing modules ----------------------------- + +* New lemma in `Data.Vec.Properties`: + ```agda + map-concat : map f (concat xss) ≡ concat (map (map f) xss) + ``` diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index bea3cfea95..f0b69c3297 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -439,6 +439,21 @@ map-⊛ : ∀ (f : A → B → C) (g : A → B) (xs : Vec A n) → map-⊛ f g [] = refl map-⊛ f g (x ∷ xs) = cong (f x (g x) ∷_) (map-⊛ f g xs) +map-concat : (f : A → B) (xss : Vec (Vec A m) n) → + map f (concat xss) ≡ concat (map (map f) xss) +map-concat f [] = refl +map-concat f (xs ∷ xss) = begin + map f (concat (xs ∷ xss)) + ≡⟨⟩ + map f (xs ++ concat xss) + ≡⟨ map-++ f xs (concat xss) ⟩ + map f xs ++ map f (concat xss) + ≡⟨ cong (map f xs ++_) (map-concat f xss) ⟩ + map f xs ++ concat (map (map f) xss) + ≡⟨⟩ + concat (map (map f) (xs ∷ xss)) + ∎ where open ≡-Reasoning + toList-map : ∀ (f : A → B) (xs : Vec A n) → toList (map f xs) ≡ List.map f (toList xs) toList-map f [] = refl