From cd7963badd18b8baff6a811bcf04658d848f771e Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Sat, 28 Dec 2024 14:34:44 +0000
Subject: [PATCH] =?UTF-8?q?[=20add=20]=20`concat=20[=20xs=20]=20=E2=89=A1?=
 =?UTF-8?q?=20=20xs`=20(#2530)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* add: `concat-[_]`

* refactor: rename+deprecate

* refactor: knock-on viscosity

* `List` instead of `Vec`!

* deprecate old name!
---
 CHANGELOG.md                      |  6 ++++++
 src/Data/List/Properties.agda     | 19 +++++++++++++++----
 src/Data/List/Sort/MergeSort.agda |  4 ++--
 3 files changed, 23 insertions(+), 6 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 5c3dfd2747..d21215e9f6 100644
--- a/CHANGELOG.md
+++ b/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?
 
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index cb67ad4ce1..c6d9faea11 100644
--- a/src/Data/List/Properties.agda
+++ b/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."
+#-}
diff --git a/src/Data/List/Sort/MergeSort.agda b/src/Data/List/Sort/MergeSort.agda
index 529d8623d3..0e59de8b94 100644
--- a/src/Data/List/Sort/MergeSort.agda
+++ b/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                      ∎
 
 ------------------------------------------------------------------------