Add some properties relating to List.concat (#1317)

Author: Taneb

CHANGELOG.md

@@ -40,6 +40,13 @@ Other minor additions
 
 * Added `Reflection.TypeChecking.Format.errorPartFmt`.
 
+* Added new properties to `Data.List.Properties`:
+  ```agda
+  concat-++ : concat xss ++ concat yss ≡ concat (xss ++ yss)
+  concat-concat : concat ∘ map concat ≗ concat ∘ concat
+  concat-[-] : concat ∘ map [_] ≗ id
+  ```
+
 * Added new records to `Algebra.Bundles`:
   ```agda
   RawNearSemiring c ℓ : Set (suc (c ⊔ ℓ))

src/Data/List/Properties.agda

@@ -496,6 +496,22 @@ concat-map {f = f} xss = begin
   foldr (λ ys → map f ys ++_) [] xss         ≡⟨ sym (foldr-fusion (map f) [] (map-++-commute f) xss) ⟩
   map f (concat xss)                         ∎
 
+concat-++ : (xss yss : List (List A)) → concat xss ++ concat yss ≡ concat (xss ++ yss)
+concat-++ [] yss = refl
+concat-++ ([] ∷ xss) yss = concat-++ xss yss
+concat-++ ((x ∷ xs) ∷ xss) yss = cong (x ∷_) (concat-++ (xs ∷ xss) yss)
+
+concat-concat : concat {A = A} ∘ map concat ≗ concat ∘ concat
+concat-concat [] = refl
+concat-concat (xss ∷ xsss) = begin
+  concat (map concat (xss ∷ xsss))   ≡⟨ cong (concat xss ++_) (concat-concat xsss) ⟩
+  concat xss ++ concat (concat xsss) ≡⟨ concat-++ xss (concat xsss) ⟩
+  concat (concat (xss ∷ xsss))       ∎
+
+concat-[-] : concat {A = A} ∘ map [_] ≗ id
+concat-[-] [] = refl
+concat-[-] (x ∷ xs) = cong (x ∷_) (concat-[-] xs)
+
 ------------------------------------------------------------------------
 -- sum