[ add ] concat [ xs ] ≡ xs (#2530)

* add: `concat-[_]`

* refactor: rename+deprecate

* refactor: knock-on viscosity

* `List` instead of `Vec`!

* deprecate old name!

CHANGELOG.md

@@ -76,6 +76,11 @@ Deprecated names
   normalise-correct  ↦  Algebra.Solver.Monoid.Normal.correct
   ```
 
+* In `Data.List.Properties`:
+  ```agda
+  concat-[-]   ↦  concat-map-[_]
+  ```
+
 * In `Data.List.Relation.Binary.Permutation.Setoid.Properties`:
   ```agda
   split  ↦  ↭-split
@@ -318,6 +323,7 @@ Additions to existing modules
   ```agda
   product≢0    : All NonZero ns → NonZero (product ns)
   ∈⇒≤product   : All NonZero ns → n ∈ ns → n ≤ product ns
+  concat-[_]   : concat ∘ [_] ≗ id
   concatMap-++ : concatMap f (xs ++ ys) ≡ concatMap f xs ++ concatMap f ys
   filter-≐     : P ≐ Q → filter P? ≗ filter Q?
 

src/Data/List/Properties.agda

@@ -677,9 +677,12 @@ concat-concat (xss ∷ xsss) = begin
   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)
+concat-map-[_] : concat {A = A} ∘ map [_] ≗ id
+concat-map-[ [] ]     = refl
+concat-map-[ x ∷ xs ] = cong (x ∷_) (concat-map-[ xs ])
+
+concat-[_] : concat {A = A} ∘ [_] ≗ id
+concat-[ xs ] = ++-identityʳ xs
 
 ------------------------------------------------------------------------
 -- concatMap
@@ -688,7 +691,7 @@ concatMap-cong : ∀ {f g : A → List B} → f ≗ g → concatMap f ≗ concat
 concatMap-cong eq = cong concat ∘ map-cong eq
 
 concatMap-pure : concatMap {A = A} [_] ≗ id
-concatMap-pure = concat-[-]
+concatMap-pure = concat-map-[_]
 
 concatMap-map : (g : B → List C) → (f : A → B) →
                 concatMap g ∘′ (map f) ≗ concatMap (g ∘′ f)
@@ -1647,3 +1650,11 @@ scanl-defn f e (x ∷ xs) = cong (e ∷_) (begin
 "Warning: scanl-defn was deprecated in v2.1.
 Please use Data.List.Scans.Properties.scanl-defn instead."
 #-}
+
+-- Version 2.2
+
+concat-[-] = concat-map-[_]
+{-# WARNING_ON_USAGE concat-[-]
+"Warning: concat-[-] was deprecated in v2.2.
+Please use concat-map-[_] instead."
+#-}

src/Data/List/Sort/MergeSort.agda

@@ -17,7 +17,7 @@ module Data.List.Sort.MergeSort
 open import Data.Bool.Base using (true; false)
 open import Data.List.Base
   using (List; []; _∷_; merge; length; map; [_]; concat; _++_)
-open import Data.List.Properties using (length-partition; ++-assoc; concat-[-])
+open import Data.List.Properties using (length-partition; ++-assoc; concat-map-[_])
 open import Data.List.Relation.Unary.Linked using ([]; [-])
 import Data.List.Relation.Unary.Sorted.TotalOrder.Properties as Sorted
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
@@ -86,7 +86,7 @@ mergeAll-↭ (xs ∷ ys ∷ xss) (acc rec) = begin
 sort-↭ : ∀ xs → sort xs ↭ xs
 sort-↭ xs = begin
   mergeAll (map [_] xs) _ ↭⟨ mergeAll-↭ (map [_] xs) _ ⟩
-  concat (map [_] xs)     ≡⟨ concat-[-] xs ⟩
+  concat (map [_] xs)     ≡⟨ concat-map-[ xs ] ⟩
   xs                      ∎
 
 ------------------------------------------------------------------------