From acd483029407c8a6386c6a4da70e110e172011e6 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 23 May 2024 13:22:06 +0100
Subject: [PATCH 01/16] refactor `scanr` etc.

---
 CHANGELOG.md                  |  19 +++++
 src/Data/List.agda            |   4 +
 src/Data/List/Base.agda       |  56 +++++++++-----
 src/Data/List/Properties.agda |  61 ++++++++-------
 src/Data/List/Scans.agda      | 142 ++++++++++++++++++++++++++++++++++
 5 files changed, 234 insertions(+), 48 deletions(-)
 create mode 100644 src/Data/List/Scans.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 29839632c7..d28213eabb 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -65,6 +65,20 @@ Deprecated names
   isRing*  ↦  Algebra.Structures.isRing
   ```
 
+* In `Data.List.Base`:
+  ```agda
+  inits  ↦  Data.List.Scans.inits
+  tails  ↦  Data.List.Scans.tails
+  scanr  ↦  Data.List.Scans.scanr
+  scanl  ↦  Data.List.Scans.scanl
+  ```
+
+* In `Data.List.Properties`:
+  ```agda
+  scanr-defn  ↦  Data.List.Scans.scanr-defn
+  scanl-defn  ↦  Data.List.Scans.scanl-defn
+  ```
+
 * In `Data.Nat.Divisibility.Core`:
   ```agda
   *-pres-∣  ↦  Data.Nat.Divisibility.*-pres-∣
@@ -89,6 +103,11 @@ New modules
   Algebra.Module.Bundles.Raw
   ```
 
+* Refactoring of `Data.List.Base.{inits|tails|scanr|scanl}`:
+  ```
+  Data.List.Scans
+  ```
+
 * Prime factorisation of natural numbers.
   ```
   Data.Nat.Primality.Factorisation
diff --git a/src/Data/List.agda b/src/Data/List.agda
index 7747cbbd74..b5d5cf1f8f 100644
--- a/src/Data/List.agda
+++ b/src/Data/List.agda
@@ -8,6 +8,7 @@
 -- lists.
 
 {-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --warn=noUserWarning #-} -- for deprecated scans etc.
 
 module Data.List where
 
@@ -15,3 +16,6 @@ module Data.List where
 -- Types and basic operations
 
 open import Data.List.Base public
+  hiding (inits; tails; scanr; scanl)
+open import Data.List.Scans public
+  using (inits; tails; scanr; scanl)
diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index c3c894cf65..d9ed566b28 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -189,14 +189,6 @@ iterate : (A → A) → A → ℕ → List A
 iterate f e zero    = []
 iterate f e (suc n) = e ∷ iterate f (f e) n
 
-inits : List A → List (List A)
-inits []       = [] ∷ []
-inits (x ∷ xs) = [] ∷ map (x ∷_) (inits xs)
-
-tails : List A → List (List A)
-tails []       = [] ∷ []
-tails (x ∷ xs) = (x ∷ xs) ∷ tails xs
-
 insertAt : (xs : List A) → Fin (suc (length xs)) → A → List A
 insertAt xs       zero    v = v ∷ xs
 insertAt (x ∷ xs) (suc i) v = x ∷ insertAt xs i v
@@ -205,18 +197,6 @@ updateAt : (xs : List A) → Fin (length xs) → (A → A) → List A
 updateAt (x ∷ xs) zero    f = f x ∷ xs
 updateAt (x ∷ xs) (suc i) f = x ∷ updateAt xs i f
 
--- Scans
-
-scanr : (A → B → B) → B → List A → List B
-scanr f e []       = e ∷ []
-scanr f e (x ∷ xs) with scanr f e xs
-... | []     = []                -- dead branch
-... | y ∷ ys = f x y ∷ y ∷ ys
-
-scanl : (A → B → A) → A → List B → List A
-scanl f e []       = e ∷ []
-scanl f e (x ∷ xs) = e ∷ scanl f (f e x) xs
-
 -- Tabulation
 
 applyUpTo : (ℕ → A) → ℕ → List A
@@ -571,3 +551,39 @@ _─_ = removeAt
 "Warning: _─_ was deprecated in v2.0.
 Please use removeAt instead."
 #-}
+
+-- Version 2.1
+
+inits : List A → List (List A)
+inits []       = [] ∷ []
+inits (x ∷ xs) = [] ∷ map (x ∷_) (inits xs)
+{-# WARNING_ON_USAGE inits
+"Warning: inits was deprecated in v2.1.
+Please use Data.List.Scans.inits instead."
+#-}
+
+tails : List A → List (List A)
+tails []       = [] ∷ []
+tails (x ∷ xs) = (x ∷ xs) ∷ tails xs
+{-# WARNING_ON_USAGE tails
+"Warning: tails was deprecated in v2.1.
+Please use Data.List.Scans.tails instead."
+#-}
+
+scanr : (A → B → B) → B → List A → List B
+scanr f e []       = e ∷ []
+scanr f e (x ∷ xs) with scanr f e xs
+... | []         = []                -- dead branch
+... | ys@(y ∷ _) = f x y ∷ ys
+{-# WARNING_ON_USAGE scanr
+"Warning: scanr was deprecated in v2.1.
+Please use Data.List.Scans.scanr instead."
+#-}
+
+scanl : (A → B → A) → A → List B → List A
+scanl f e []       = e ∷ []
+scanl f e (x ∷ xs) = e ∷ scanl f (f e x) xs
+{-# WARNING_ON_USAGE scanl
+"Warning: scanl was deprecated in v2.1.
+Please use Data.List.Scans.scanl instead."
+#-}
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index ab9b0241e1..f639a9cbd1 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -8,6 +8,7 @@
 -- equalities than _≡_.
 
 {-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --warn=noUserWarning #-} -- for deprecated scans etc.
 
 module Data.List.Properties where
 
@@ -809,34 +810,6 @@ sum-++ (x ∷ xs) ys = begin
 ∈⇒∣product {n} {n ∷ ns} (here  refl) = divides (product ns) (*-comm n (product ns))
 ∈⇒∣product {n} {m ∷ ns} (there n∈ns) = ∣n⇒∣m*n m (∈⇒∣product n∈ns)
 
-------------------------------------------------------------------------
--- scanr
-
-scanr-defn : ∀ (f : A → B → B) (e : B) →
-             scanr f e ≗ map (foldr f e) ∘ tails
-scanr-defn f e []             = refl
-scanr-defn f e (x ∷ [])       = refl
-scanr-defn f e (x ∷ y∷xs@(_ ∷ _))
-  with eq ← scanr-defn f e y∷xs
-  with z ∷ zs ← scanr f e y∷xs
-  = let z≡fy⦇f⦈xs , _ = ∷-injective eq in cong₂ (λ z → f x z ∷_) z≡fy⦇f⦈xs eq
-
-------------------------------------------------------------------------
--- scanl
-
-scanl-defn : ∀ (f : A → B → A) (e : A) →
-             scanl f e ≗ map (foldl f e) ∘ inits
-scanl-defn f e []       = refl
-scanl-defn f e (x ∷ xs) = cong (e ∷_) (begin
-   scanl f (f e x) xs
- ≡⟨ scanl-defn f (f e x) xs ⟩
-   map (foldl f (f e x)) (inits xs)
- ≡⟨ refl ⟩
-   map (foldl f e ∘ (x ∷_)) (inits xs)
- ≡⟨ map-∘ (inits xs) ⟩
-   map (foldl f e) (map (x ∷_) (inits xs))
- ∎)
-
 ------------------------------------------------------------------------
 -- applyUpTo
 
@@ -1582,3 +1555,35 @@ map-─ = map-removeAt
 "Warning: map-─ was deprecated in v2.0.
 Please use map-removeAt instead."
 #-}
+
+-- Version 2.1
+
+scanr-defn : ∀ (f : A → B → B) (e : B) →
+             scanr f e ≗ map (foldr f e) ∘ tails
+scanr-defn f e []             = refl
+scanr-defn f e (x ∷ [])       = refl
+scanr-defn f e (x ∷ xs@(_ ∷ _))
+  with eq ← scanr-defn f e xs
+  with ys@(_ ∷ _) ← scanr f e xs
+  = cong₂ (λ z → f x z ∷_) (∷-injectiveˡ eq) eq
+{-# WARNING_ON_USAGE scanr-defn
+"Warning: scanr-defn was deprecated in v2.1.
+Please use Data.List.Scans.scanr-defn instead."
+#-}
+
+scanl-defn : ∀ (f : A → B → A) (e : A) →
+             scanl f e ≗ map (foldl f e) ∘ inits
+scanl-defn f e []       = refl
+scanl-defn f e (x ∷ xs) = cong (e ∷_) (begin
+   scanl f (f e x) xs
+ ≡⟨ scanl-defn f (f e x) xs ⟩
+   map (foldl f (f e x)) (inits xs)
+ ≡⟨ refl ⟩
+   map (foldl f e ∘ (x ∷_)) (inits xs)
+ ≡⟨ map-∘ (inits xs) ⟩
+   map (foldl f e) (map (x ∷_) (inits xs))
+ ∎)
+{-# WARNING_ON_USAGE scanl-defn
+"Warning: scanl-defn was deprecated in v2.1.
+Please use Data.List.Scans.scanl-defn instead."
+#-}
diff --git a/src/Data/List/Scans.agda b/src/Data/List/Scans.agda
new file mode 100644
index 0000000000..2a3bdd3f03
--- /dev/null
+++ b/src/Data/List/Scans.agda
@@ -0,0 +1,142 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- List scans: definition and properties
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.List.Scans where
+
+open import Data.List.Base as List using (List; []; _∷_)
+open import Data.List.NonEmpty.Base as List⁺ using (List⁺; _∷_; toList)
+import Data.List.Properties as List
+import Data.List.NonEmpty.Properties as List⁺
+open import Function.Base using (_∘_; _$_)
+open import Level using (Level)
+open import Relation.Binary.PropositionalEquality.Core
+  using (_≡_; _≗_; refl; trans; cong; cong₂)
+open import Relation.Binary.PropositionalEquality.Properties using (module ≡-Reasoning)
+
+private
+  variable
+    a b : Level
+    A : Set a
+    B : Set b
+
+
+------------------------------------------------------------------------
+-- Definitions
+
+-- Inits
+
+inits⁺ : List A → List⁺ (List A)
+inits⁺ xs = [] ∷ go xs
+  where
+  go : List A → List (List A)
+  go []       = []
+  go (x ∷ xs) = List.[ x ] ∷ List.map (x ∷_) (go xs)
+
+inits : List A → List (List A)
+inits = toList ∘ inits⁺
+
+-- Tails
+
+tails⁺ : List A → List⁺ (List A)
+tails⁺ xs = xs ∷ go xs
+  where
+  go : List A → List (List A)
+  go []       = []
+  go (x ∷ xs) = xs ∷ go xs
+
+tails : List A → List (List A)
+tails = toList ∘ tails⁺
+
+-- Scanr
+
+module _ (f : A → B → B) where
+
+  scanr⁺ : (e : B) → List A → List⁺ B
+  scanr⁺ e []       = e ∷ []
+  scanr⁺ e (x ∷ xs) = let y ∷ ys = scanr⁺ e xs in f x y ∷ y ∷ ys
+
+  scanr : (e : B) → List A → List B
+  scanr e = toList ∘ scanr⁺ e
+
+-- Scanl
+
+module _ (f : A → B → A) where
+
+  scanl⁺ : A → List B → List⁺ A
+  scanl⁺ e xs = e ∷ go e xs
+    where
+    go : A → List B → List A
+    go _ []       = []
+    go e (x ∷ xs) = let fex = f e x in fex ∷ go fex xs
+
+  scanl : A → List B → List A
+  scanl e = toList ∘ scanl⁺ e
+
+------------------------------------------------------------------------
+-- Properties
+
+-- inits
+
+toList-inits⁺ : toList ∘ inits⁺ ≗ inits {A = A}
+toList-inits⁺ []       = refl
+toList-inits⁺ (x ∷ xs) = cong (([] ∷_) ∘ List.map (x ∷_)) (toList-inits⁺ xs)
+
+-- tails
+
+toList-tails⁺ : toList ∘ tails⁺ ≗ tails {A = A}
+toList-tails⁺ []          = refl
+toList-tails⁺ ys@(_ ∷ xs) = cong (ys ∷_) (toList-tails⁺ xs)
+
+-- scanr⁺ and scanr
+
+module _ (f : A → B → B) (e : B) where
+
+  private
+    h = List.foldr f e
+
+  scanr⁺-defn : scanr⁺ f e ≗ List⁺.map h ∘ tails⁺
+  scanr⁺-defn []       = refl
+  scanr⁺-defn (x ∷ xs) = let eq = scanr⁺-defn xs
+    in cong₂ (λ z → f x z ∷_) (cong List⁺.head eq) (cong toList eq)
+
+  scanr-defn : scanr f e ≗ List.map h ∘ tails
+  scanr-defn xs = begin
+    scanr f e xs
+      ≡⟨ cong toList (scanr⁺-defn xs) ⟩
+    toList (List⁺.map h (tails⁺ xs))
+      ≡⟨⟩
+    List.map h (toList (tails⁺ xs))
+      ≡⟨⟩
+    List.map h (tails xs)
+      ∎
+    where open ≡-Reasoning
+
+-- scanl⁺ and scanl
+
+module _ (f : A → B → A) where
+
+  private
+    h = List.foldl f
+
+  scanl⁺-defn : ∀ e → scanl⁺ f e ≗ List⁺.map (h e) ∘ inits⁺
+  scanl⁺-defn e []       = refl
+  scanl⁺-defn e (x ∷ xs) = let eq = scanl⁺-defn (f e x) xs in
+    cong (e ∷_) $ cong (f e x ∷_) $ trans (cong List⁺.tail eq) (List.map-∘ _)
+
+  scanl-defn : ∀ e → scanl f e ≗ List.map (h e) ∘ inits
+  scanl-defn e []       = refl
+  scanl-defn e (x ∷ xs) = cong (e ∷_) $ begin
+    scanl f (f e x) xs
+      ≡⟨ scanl-defn (f e x) xs ⟩
+    List.map (h (f e x)) (inits xs)
+      ≡⟨⟩
+    List.map (h e ∘ (x ∷_)) (inits xs)
+      ≡⟨ List.map-∘ (inits xs) ⟩
+    List.map (h e) (List.map (x ∷_) (inits xs))
+     ∎
+    where open ≡-Reasoning

From 2426a968bd1e27a94d389402cecec63c017a5cd1 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 23 May 2024 13:50:07 +0100
Subject: [PATCH 02/16] restore `inits` etc. but lazier; plus knock-on
 consequences

---
 CHANGELOG.md                                  |  4 +--
 src/Data/List.agda                            |  4 +--
 src/Data/List/Base.agda                       | 30 +++++++++----------
 .../Membership/Propositional/Properties.agda  |  3 +-
 src/Data/List/Scans.agda                      | 26 +++++++---------
 src/Tactic/RingSolver/Core/NatSet.agda        |  2 +-
 6 files changed, 29 insertions(+), 40 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d28213eabb..26eb09daa0 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -67,8 +67,6 @@ Deprecated names
 
 * In `Data.List.Base`:
   ```agda
-  inits  ↦  Data.List.Scans.inits
-  tails  ↦  Data.List.Scans.tails
   scanr  ↦  Data.List.Scans.scanr
   scanl  ↦  Data.List.Scans.scanl
   ```
@@ -103,7 +101,7 @@ New modules
   Algebra.Module.Bundles.Raw
   ```
 
-* Refactoring of `Data.List.Base.{inits|tails|scanr|scanl}`:
+* Refactoring of `Data.List.Base.{scanr|scanl}` and their properties:
   ```
   Data.List.Scans
   ```
diff --git a/src/Data/List.agda b/src/Data/List.agda
index b5d5cf1f8f..b400dbf16f 100644
--- a/src/Data/List.agda
+++ b/src/Data/List.agda
@@ -16,6 +16,6 @@ module Data.List where
 -- Types and basic operations
 
 open import Data.List.Base public
-  hiding (inits; tails; scanr; scanl)
+  hiding (scanr; scanl)
 open import Data.List.Scans public
-  using (inits; tails; scanr; scanl)
+  using (scanr; scanl)
diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index d9ed566b28..e129dc9989 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -189,6 +189,20 @@ iterate : (A → A) → A → ℕ → List A
 iterate f e zero    = []
 iterate f e (suc n) = e ∷ iterate f (f e) n
 
+inits : List A → List (List A)
+inits {A = A} xs = [] ∷ go xs
+  where
+  go : List A → List (List A)
+  go []       = []
+  go (x ∷ xs) = [ x ] ∷ map (x ∷_) (go xs)
+
+tails : List A → List (List A)
+tails {A = A} xs = xs ∷ go xs
+  where
+  go : List A → List (List A)
+  go []       = []
+  go (_ ∷ xs) = xs ∷ go xs
+
 insertAt : (xs : List A) → Fin (suc (length xs)) → A → List A
 insertAt xs       zero    v = v ∷ xs
 insertAt (x ∷ xs) (suc i) v = x ∷ insertAt xs i v
@@ -554,22 +568,6 @@ Please use removeAt instead."
 
 -- Version 2.1
 
-inits : List A → List (List A)
-inits []       = [] ∷ []
-inits (x ∷ xs) = [] ∷ map (x ∷_) (inits xs)
-{-# WARNING_ON_USAGE inits
-"Warning: inits was deprecated in v2.1.
-Please use Data.List.Scans.inits instead."
-#-}
-
-tails : List A → List (List A)
-tails []       = [] ∷ []
-tails (x ∷ xs) = (x ∷ xs) ∷ tails xs
-{-# WARNING_ON_USAGE tails
-"Warning: tails was deprecated in v2.1.
-Please use Data.List.Scans.tails instead."
-#-}
-
 scanr : (A → B → B) → B → List A → List B
 scanr f e []       = e ∷ []
 scanr f e (x ∷ xs) with scanr f e xs
diff --git a/src/Data/List/Membership/Propositional/Properties.agda b/src/Data/List/Membership/Propositional/Properties.agda
index 47ee739817..f93bf81f4a 100644
--- a/src/Data/List/Membership/Propositional/Properties.agda
+++ b/src/Data/List/Membership/Propositional/Properties.agda
@@ -338,8 +338,7 @@ module _ {_•_ : Op₂ A} where
 -- inits
 
 []∈inits : ∀ {a} {A : Set a} (as : List A) → [] ∈ inits as
-[]∈inits []       = here refl
-[]∈inits (a ∷ as) = here refl
+[]∈inits _ = here refl
 
 ------------------------------------------------------------------------
 -- Other properties
diff --git a/src/Data/List/Scans.agda b/src/Data/List/Scans.agda
index 2a3bdd3f03..bd005df783 100644
--- a/src/Data/List/Scans.agda
+++ b/src/Data/List/Scans.agda
@@ -37,9 +37,6 @@ inits⁺ xs = [] ∷ go xs
   go []       = []
   go (x ∷ xs) = List.[ x ] ∷ List.map (x ∷_) (go xs)
 
-inits : List A → List (List A)
-inits = toList ∘ inits⁺
-
 -- Tails
 
 tails⁺ : List A → List⁺ (List A)
@@ -49,9 +46,6 @@ tails⁺ xs = xs ∷ go xs
   go []       = []
   go (x ∷ xs) = xs ∷ go xs
 
-tails : List A → List (List A)
-tails = toList ∘ tails⁺
-
 -- Scanr
 
 module _ (f : A → B → B) where
@@ -82,13 +76,13 @@ module _ (f : A → B → A) where
 
 -- inits
 
-toList-inits⁺ : toList ∘ inits⁺ ≗ inits {A = A}
+toList-inits⁺ : toList ∘ inits⁺ ≗ List.inits {A = A}
 toList-inits⁺ []       = refl
 toList-inits⁺ (x ∷ xs) = cong (([] ∷_) ∘ List.map (x ∷_)) (toList-inits⁺ xs)
 
 -- tails
 
-toList-tails⁺ : toList ∘ tails⁺ ≗ tails {A = A}
+toList-tails⁺ : toList ∘ tails⁺ ≗ List.tails {A = A}
 toList-tails⁺ []          = refl
 toList-tails⁺ ys@(_ ∷ xs) = cong (ys ∷_) (toList-tails⁺ xs)
 
@@ -104,15 +98,15 @@ module _ (f : A → B → B) (e : B) where
   scanr⁺-defn (x ∷ xs) = let eq = scanr⁺-defn xs
     in cong₂ (λ z → f x z ∷_) (cong List⁺.head eq) (cong toList eq)
 
-  scanr-defn : scanr f e ≗ List.map h ∘ tails
+  scanr-defn : scanr f e ≗ List.map h ∘ List.tails
   scanr-defn xs = begin
     scanr f e xs
       ≡⟨ cong toList (scanr⁺-defn xs) ⟩
     toList (List⁺.map h (tails⁺ xs))
       ≡⟨⟩
     List.map h (toList (tails⁺ xs))
-      ≡⟨⟩
-    List.map h (tails xs)
+      ≡⟨ cong (List.map h) (toList-tails⁺ xs) ⟩
+    List.map h (List.tails xs)
       ∎
     where open ≡-Reasoning
 
@@ -128,15 +122,15 @@ module _ (f : A → B → A) where
   scanl⁺-defn e (x ∷ xs) = let eq = scanl⁺-defn (f e x) xs in
     cong (e ∷_) $ cong (f e x ∷_) $ trans (cong List⁺.tail eq) (List.map-∘ _)
 
-  scanl-defn : ∀ e → scanl f e ≗ List.map (h e) ∘ inits
+  scanl-defn : ∀ e → scanl f e ≗ List.map (h e) ∘ List.inits
   scanl-defn e []       = refl
   scanl-defn e (x ∷ xs) = cong (e ∷_) $ begin
     scanl f (f e x) xs
       ≡⟨ scanl-defn (f e x) xs ⟩
-    List.map (h (f e x)) (inits xs)
+    List.map (h (f e x)) (List.inits xs)
       ≡⟨⟩
-    List.map (h e ∘ (x ∷_)) (inits xs)
-      ≡⟨ List.map-∘ (inits xs) ⟩
-    List.map (h e) (List.map (x ∷_) (inits xs))
+    List.map (h e ∘ (x ∷_)) (List.inits xs)
+      ≡⟨ List.map-∘ (List.inits xs) ⟩
+    List.map (h e) (List.map (x ∷_) (List.inits xs))
      ∎
     where open ≡-Reasoning
diff --git a/src/Tactic/RingSolver/Core/NatSet.agda b/src/Tactic/RingSolver/Core/NatSet.agda
index 1b27fae60a..626c49dae9 100644
--- a/src/Tactic/RingSolver/Core/NatSet.agda
+++ b/src/Tactic/RingSolver/Core/NatSet.agda
@@ -37,7 +37,7 @@
 module Tactic.RingSolver.Core.NatSet where
 
 open import Data.Nat.Base   as ℕ     using (ℕ; suc; zero)
-open import Data.List.Base  as List  using (List; _∷_; [])
+open import Data.List       as List  using (List; _∷_; [])
 open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
 open import Data.Bool.Base  as Bool  using (Bool)
 open import Function.Base            using (const; _∘_)

From 833d9c1735a68977b7c2c6010f8de18e20248aa1 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 23 May 2024 14:40:02 +0100
Subject: [PATCH 03/16] more refactoring; plus knock-on consequences

---
 CHANGELOG.md                            | 12 +++++++
 src/Codata/Sized/Colist/Properties.agda |  3 +-
 src/Data/List/NonEmpty/Base.agda        | 18 +++++++++++
 src/Data/List/NonEmpty/Properties.agda  | 16 +++++++++-
 src/Data/List/Scans.agda                | 42 ++++---------------------
 src/Tactic/RingSolver/Core/NatSet.agda  |  5 +--
 6 files changed, 56 insertions(+), 40 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 26eb09daa0..f5058ee9a2 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -77,6 +77,18 @@ Deprecated names
   scanl-defn  ↦  Data.List.Scans.scanl-defn
   ```
 
+* In `Data.List.NonEmpty.Base`:
+  ```agda
+  inits : List A → List⁺ (List A)
+  tails : List A → List⁺ (List A)
+  ```
+
+* In `Data.List.NonEmpty.Properties`:
+  ```agda
+  toList-inits : toList ∘ List⁺.inits ≗ List.inits
+  toList-tails : toList ∘ List⁺.tails ≗ List.tails
+  ```
+
 * In `Data.Nat.Divisibility.Core`:
   ```agda
   *-pres-∣  ↦  Data.Nat.Divisibility.*-pres-∣
diff --git a/src/Codata/Sized/Colist/Properties.agda b/src/Codata/Sized/Colist/Properties.agda
index c03b3c2096..39d798686f 100644
--- a/src/Codata/Sized/Colist/Properties.agda
+++ b/src/Codata/Sized/Colist/Properties.agda
@@ -22,6 +22,7 @@ open import Codata.Sized.Stream as Stream using (Stream; _∷_)
 open import Data.Vec.Bounded as Vec≤ using (Vec≤)
 open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_)
+import Data.List.Scans as Scans
 open import Data.List.Relation.Binary.Equality.Propositional using (≋-refl)
 open import Data.Maybe.Base as Maybe using (Maybe; nothing; just)
 import Data.Maybe.Properties as Maybe
@@ -283,7 +284,7 @@ fromList-++ []       bs = refl
 fromList-++ (a ∷ as) bs = ≡.refl ∷ λ where .force → fromList-++ as bs
 
 fromList-scanl : ∀ (c : B → A → B) n as →
-                 i ⊢ fromList (List.scanl c n as) ≈ scanl c n (fromList as)
+                 i ⊢ fromList (Scans.scanl c n as) ≈ scanl c n (fromList as)
 fromList-scanl c n []       = ≡.refl ∷ λ where .force → refl
 fromList-scanl c n (a ∷ as) =
   ≡.refl ∷ λ where .force → fromList-scanl c (c n a) as
diff --git a/src/Data/List/NonEmpty/Base.agda b/src/Data/List/NonEmpty/Base.agda
index 0b1793eaf7..2c5ff8c943 100644
--- a/src/Data/List/NonEmpty/Base.agda
+++ b/src/Data/List/NonEmpty/Base.agda
@@ -143,6 +143,24 @@ concatMap f = concat ∘′ map f
 ap : List⁺ (A → B) → List⁺ A → List⁺ B
 ap fs as = concatMap (λ f → map f as) fs
 
+-- Inits
+
+inits : List A → List⁺ (List A)
+inits xs = [] ∷ go xs
+  where
+  go : List A → List (List A)
+  go []       = []
+  go (x ∷ xs) = List.[ x ] ∷ List.map (x ∷_) (go xs)
+
+-- Tails
+
+tails : List A → List⁺ (List A)
+tails xs = xs ∷ go xs
+  where
+  go : List A → List (List A)
+  go []       = []
+  go (x ∷ xs) = xs ∷ go xs
+
 -- Reverse
 
 reverse : List⁺ A → List⁺ A
diff --git a/src/Data/List/NonEmpty/Properties.agda b/src/Data/List/NonEmpty/Properties.agda
index c20f024c4a..f6d9c521b4 100644
--- a/src/Data/List/NonEmpty/Properties.agda
+++ b/src/Data/List/NonEmpty/Properties.agda
@@ -18,7 +18,7 @@ open import Data.List.Effectful using () renaming (monad to listMonad)
 open import Data.List.NonEmpty.Effectful using () renaming (monad to list⁺Monad)
 open import Data.List.NonEmpty
   using (List⁺; _∷_; tail; head; toList; _⁺++_; _⁺++⁺_; _++⁺_; length; fromList;
-    drop+; map; groupSeqs; ungroupSeqs)
+    drop+; map; inits; tails; groupSeqs; ungroupSeqs)
 open import Data.List.NonEmpty.Relation.Unary.All using (All; toList⁺; _∷_)
 open import Data.List.Relation.Unary.All using ([]; _∷_) renaming (All to ListAll)
 import Data.List.Properties as List
@@ -118,6 +118,20 @@ map-cong f≗g (x ∷ xs) = cong₂ _∷_ (f≗g x) (List.map-cong f≗g xs)
 map-∘ : {g : B → C} {f : A → B} → map (g ∘ f) ≗ map g ∘ map f
 map-∘ (x ∷ xs) = cong (_ ∷_) (List.map-∘ xs)
 
+------------------------------------------------------------------------
+-- inits
+
+toList-inits : toList ∘ inits ≗ List.inits {A = A}
+toList-inits []       = refl
+toList-inits (x ∷ xs) = cong (([] ∷_) ∘ List.map (x ∷_)) (toList-inits xs)
+
+------------------------------------------------------------------------
+-- tails
+
+toList-tails : toList ∘ tails ≗ List.tails {A = A}
+toList-tails []          = refl
+toList-tails ys@(_ ∷ xs) = cong (ys ∷_) (toList-tails xs)
+
 ------------------------------------------------------------------------
 -- groupSeqs
 
diff --git a/src/Data/List/Scans.agda b/src/Data/List/Scans.agda
index bd005df783..7100ab0195 100644
--- a/src/Data/List/Scans.agda
+++ b/src/Data/List/Scans.agda
@@ -28,24 +28,6 @@ private
 ------------------------------------------------------------------------
 -- Definitions
 
--- Inits
-
-inits⁺ : List A → List⁺ (List A)
-inits⁺ xs = [] ∷ go xs
-  where
-  go : List A → List (List A)
-  go []       = []
-  go (x ∷ xs) = List.[ x ] ∷ List.map (x ∷_) (go xs)
-
--- Tails
-
-tails⁺ : List A → List⁺ (List A)
-tails⁺ xs = xs ∷ go xs
-  where
-  go : List A → List (List A)
-  go []       = []
-  go (x ∷ xs) = xs ∷ go xs
-
 -- Scanr
 
 module _ (f : A → B → B) where
@@ -74,18 +56,6 @@ module _ (f : A → B → A) where
 ------------------------------------------------------------------------
 -- Properties
 
--- inits
-
-toList-inits⁺ : toList ∘ inits⁺ ≗ List.inits {A = A}
-toList-inits⁺ []       = refl
-toList-inits⁺ (x ∷ xs) = cong (([] ∷_) ∘ List.map (x ∷_)) (toList-inits⁺ xs)
-
--- tails
-
-toList-tails⁺ : toList ∘ tails⁺ ≗ List.tails {A = A}
-toList-tails⁺ []          = refl
-toList-tails⁺ ys@(_ ∷ xs) = cong (ys ∷_) (toList-tails⁺ xs)
-
 -- scanr⁺ and scanr
 
 module _ (f : A → B → B) (e : B) where
@@ -93,7 +63,7 @@ module _ (f : A → B → B) (e : B) where
   private
     h = List.foldr f e
 
-  scanr⁺-defn : scanr⁺ f e ≗ List⁺.map h ∘ tails⁺
+  scanr⁺-defn : scanr⁺ f e ≗ List⁺.map h ∘ List⁺.tails
   scanr⁺-defn []       = refl
   scanr⁺-defn (x ∷ xs) = let eq = scanr⁺-defn xs
     in cong₂ (λ z → f x z ∷_) (cong List⁺.head eq) (cong toList eq)
@@ -102,10 +72,10 @@ module _ (f : A → B → B) (e : B) where
   scanr-defn xs = begin
     scanr f e xs
       ≡⟨ cong toList (scanr⁺-defn xs) ⟩
-    toList (List⁺.map h (tails⁺ xs))
+    toList (List⁺.map h (List⁺.tails xs))
       ≡⟨⟩
-    List.map h (toList (tails⁺ xs))
-      ≡⟨ cong (List.map h) (toList-tails⁺ xs) ⟩
+    List.map h (toList (List⁺.tails xs))
+      ≡⟨ cong (List.map h) (List⁺.toList-tails xs) ⟩
     List.map h (List.tails xs)
       ∎
     where open ≡-Reasoning
@@ -117,7 +87,7 @@ module _ (f : A → B → A) where
   private
     h = List.foldl f
 
-  scanl⁺-defn : ∀ e → scanl⁺ f e ≗ List⁺.map (h e) ∘ inits⁺
+  scanl⁺-defn : ∀ e → scanl⁺ f e ≗ List⁺.map (h e) ∘ List⁺.inits
   scanl⁺-defn e []       = refl
   scanl⁺-defn e (x ∷ xs) = let eq = scanl⁺-defn (f e x) xs in
     cong (e ∷_) $ cong (f e x ∷_) $ trans (cong List⁺.tail eq) (List.map-∘ _)
@@ -132,5 +102,5 @@ module _ (f : A → B → A) where
     List.map (h e ∘ (x ∷_)) (List.inits xs)
       ≡⟨ List.map-∘ (List.inits xs) ⟩
     List.map (h e) (List.map (x ∷_) (List.inits xs))
-     ∎
+      ∎
     where open ≡-Reasoning
diff --git a/src/Tactic/RingSolver/Core/NatSet.agda b/src/Tactic/RingSolver/Core/NatSet.agda
index 626c49dae9..ddd7d406c2 100644
--- a/src/Tactic/RingSolver/Core/NatSet.agda
+++ b/src/Tactic/RingSolver/Core/NatSet.agda
@@ -37,7 +37,8 @@
 module Tactic.RingSolver.Core.NatSet where
 
 open import Data.Nat.Base   as ℕ     using (ℕ; suc; zero)
-open import Data.List       as List  using (List; _∷_; [])
+open import Data.List.Base  as List  using (List; _∷_; [])
+open import Data.List.Scans as Scans using (scanl)
 open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
 open import Data.Bool.Base  as Bool  using (Bool)
 open import Function.Base            using (const; _∘_)
@@ -98,7 +99,7 @@ fromList : List ℕ → NatSet
 fromList = List.foldr insert []
 
 toList : NatSet → List ℕ
-toList = List.drop 1 ∘ List.map ℕ.pred ∘ List.scanl (λ x y → suc (y ℕ.+ x)) 0
+toList = List.drop 1 ∘ List.map ℕ.pred ∘ Scans.scanl (λ x y → suc (y ℕ.+ x)) 0
 
 ------------------------------------------------------------------------
 -- Tests

From cfded4667d9e6893b94b4bdb297bcbb2408d521d Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 23 May 2024 14:43:18 +0100
Subject: [PATCH 04/16] tidy up

---
 src/Data/List.agda            | 2 +-
 src/Data/List/Properties.agda | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/List.agda b/src/Data/List.agda
index b400dbf16f..cd654881bd 100644
--- a/src/Data/List.agda
+++ b/src/Data/List.agda
@@ -8,7 +8,7 @@
 -- lists.
 
 {-# OPTIONS --cubical-compatible --safe #-}
-{-# OPTIONS --warn=noUserWarning #-} -- for deprecated scans etc.
+{-# OPTIONS --warn=noUserWarning #-} -- for deprecated scans
 
 module Data.List where
 
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index f639a9cbd1..32dc79e184 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -8,7 +8,7 @@
 -- equalities than _≡_.
 
 {-# OPTIONS --cubical-compatible --safe #-}
-{-# OPTIONS --warn=noUserWarning #-} -- for deprecated scans etc.
+{-# OPTIONS --warn=noUserWarning #-} -- for deprecated scans
 
 module Data.List.Properties where
 

From 268fbb7b314cb41ea9ea469b602256270e39c02f Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 27 May 2024 14:18:39 +0100
Subject: [PATCH 05/16] refactored into `Base`

---
 src/Data/List/Scans.agda      | 106 ----------------------------------
 src/Data/List/Scans/Base.agda |  49 ++++++++++++++++
 2 files changed, 49 insertions(+), 106 deletions(-)
 delete mode 100644 src/Data/List/Scans.agda
 create mode 100644 src/Data/List/Scans/Base.agda

diff --git a/src/Data/List/Scans.agda b/src/Data/List/Scans.agda
deleted file mode 100644
index 7100ab0195..0000000000
--- a/src/Data/List/Scans.agda
+++ /dev/null
@@ -1,106 +0,0 @@
-------------------------------------------------------------------------
--- The Agda standard library
---
--- List scans: definition and properties
-------------------------------------------------------------------------
-
-{-# OPTIONS --cubical-compatible --safe #-}
-
-module Data.List.Scans where
-
-open import Data.List.Base as List using (List; []; _∷_)
-open import Data.List.NonEmpty.Base as List⁺ using (List⁺; _∷_; toList)
-import Data.List.Properties as List
-import Data.List.NonEmpty.Properties as List⁺
-open import Function.Base using (_∘_; _$_)
-open import Level using (Level)
-open import Relation.Binary.PropositionalEquality.Core
-  using (_≡_; _≗_; refl; trans; cong; cong₂)
-open import Relation.Binary.PropositionalEquality.Properties using (module ≡-Reasoning)
-
-private
-  variable
-    a b : Level
-    A : Set a
-    B : Set b
-
-
-------------------------------------------------------------------------
--- Definitions
-
--- Scanr
-
-module _ (f : A → B → B) where
-
-  scanr⁺ : (e : B) → List A → List⁺ B
-  scanr⁺ e []       = e ∷ []
-  scanr⁺ e (x ∷ xs) = let y ∷ ys = scanr⁺ e xs in f x y ∷ y ∷ ys
-
-  scanr : (e : B) → List A → List B
-  scanr e = toList ∘ scanr⁺ e
-
--- Scanl
-
-module _ (f : A → B → A) where
-
-  scanl⁺ : A → List B → List⁺ A
-  scanl⁺ e xs = e ∷ go e xs
-    where
-    go : A → List B → List A
-    go _ []       = []
-    go e (x ∷ xs) = let fex = f e x in fex ∷ go fex xs
-
-  scanl : A → List B → List A
-  scanl e = toList ∘ scanl⁺ e
-
-------------------------------------------------------------------------
--- Properties
-
--- scanr⁺ and scanr
-
-module _ (f : A → B → B) (e : B) where
-
-  private
-    h = List.foldr f e
-
-  scanr⁺-defn : scanr⁺ f e ≗ List⁺.map h ∘ List⁺.tails
-  scanr⁺-defn []       = refl
-  scanr⁺-defn (x ∷ xs) = let eq = scanr⁺-defn xs
-    in cong₂ (λ z → f x z ∷_) (cong List⁺.head eq) (cong toList eq)
-
-  scanr-defn : scanr f e ≗ List.map h ∘ List.tails
-  scanr-defn xs = begin
-    scanr f e xs
-      ≡⟨ cong toList (scanr⁺-defn xs) ⟩
-    toList (List⁺.map h (List⁺.tails xs))
-      ≡⟨⟩
-    List.map h (toList (List⁺.tails xs))
-      ≡⟨ cong (List.map h) (List⁺.toList-tails xs) ⟩
-    List.map h (List.tails xs)
-      ∎
-    where open ≡-Reasoning
-
--- scanl⁺ and scanl
-
-module _ (f : A → B → A) where
-
-  private
-    h = List.foldl f
-
-  scanl⁺-defn : ∀ e → scanl⁺ f e ≗ List⁺.map (h e) ∘ List⁺.inits
-  scanl⁺-defn e []       = refl
-  scanl⁺-defn e (x ∷ xs) = let eq = scanl⁺-defn (f e x) xs in
-    cong (e ∷_) $ cong (f e x ∷_) $ trans (cong List⁺.tail eq) (List.map-∘ _)
-
-  scanl-defn : ∀ e → scanl f e ≗ List.map (h e) ∘ List.inits
-  scanl-defn e []       = refl
-  scanl-defn e (x ∷ xs) = cong (e ∷_) $ begin
-    scanl f (f e x) xs
-      ≡⟨ scanl-defn (f e x) xs ⟩
-    List.map (h (f e x)) (List.inits xs)
-      ≡⟨⟩
-    List.map (h e ∘ (x ∷_)) (List.inits xs)
-      ≡⟨ List.map-∘ (List.inits xs) ⟩
-    List.map (h e) (List.map (x ∷_) (List.inits xs))
-      ∎
-    where open ≡-Reasoning
diff --git a/src/Data/List/Scans/Base.agda b/src/Data/List/Scans/Base.agda
new file mode 100644
index 0000000000..73e7d794ad
--- /dev/null
+++ b/src/Data/List/Scans/Base.agda
@@ -0,0 +1,49 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- List scans: definitions
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.List.Scans.Base where
+
+open import Data.List.Base as List using (List; []; _∷_)
+open import Data.List.NonEmpty.Base as List⁺ using (List⁺; _∷_; toList)
+open import Function.Base using (_∘_)
+open import Level using (Level)
+
+private
+  variable
+    a b : Level
+    A : Set a
+    B : Set b
+
+
+------------------------------------------------------------------------
+-- Definitions
+
+-- Scanr
+
+module _ (f : A → B → B) where
+
+  scanr⁺ : (e : B) → List A → List⁺ B
+  scanr⁺ e []       = e ∷ []
+  scanr⁺ e (x ∷ xs) = let y ∷ ys = scanr⁺ e xs in f x y ∷ y ∷ ys
+
+  scanr : (e : B) → List A → List B
+  scanr e = toList ∘ scanr⁺ e
+
+-- Scanl
+
+module _ (f : A → B → A) where
+
+  scanl⁺ : A → List B → List⁺ A
+  scanl⁺ e xs = e ∷ go e xs
+    where
+    go : A → List B → List A
+    go _ []       = []
+    go e (x ∷ xs) = let fex = f e x in fex ∷ go fex xs
+
+  scanl : A → List B → List A
+  scanl e = toList ∘ scanl⁺ e

From a74fba4d4c79631667b92a58aeb8dbb4214edf6a Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 27 May 2024 14:21:10 +0100
Subject: [PATCH 06/16] ... and `Properties`

---
 src/Data/List/Scans/Properties.agda | 80 +++++++++++++++++++++++++++++
 1 file changed, 80 insertions(+)
 create mode 100644 src/Data/List/Scans/Properties.agda

diff --git a/src/Data/List/Scans/Properties.agda b/src/Data/List/Scans/Properties.agda
new file mode 100644
index 0000000000..6ebbf5353f
--- /dev/null
+++ b/src/Data/List/Scans/Properties.agda
@@ -0,0 +1,80 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- List scans: properties
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.List.Scans.Properties where
+
+open import Data.List.Base as List using (List; []; _∷_)
+open import Data.List.NonEmpty.Base as List⁺ using (List⁺; _∷_; toList)
+import Data.List.Properties as List
+import Data.List.NonEmpty.Properties as List⁺
+open import Data.List.Scans.Base
+open import Function.Base using (_∘_; _$_)
+open import Level using (Level)
+open import Relation.Binary.PropositionalEquality.Core
+  using (_≡_; _≗_; refl; trans; cong; cong₂)
+open import Relation.Binary.PropositionalEquality.Properties
+  using (module ≡-Reasoning)
+
+private
+  variable
+    a b : Level
+    A : Set a
+    B : Set b
+
+
+------------------------------------------------------------------------
+-- Properties
+
+-- scanr⁺ and scanr
+
+module _ (f : A → B → B) (e : B) where
+
+  private
+    h = List.foldr f e
+
+  scanr⁺-defn : scanr⁺ f e ≗ List⁺.map h ∘ List⁺.tails
+  scanr⁺-defn []       = refl
+  scanr⁺-defn (x ∷ xs) = let eq = scanr⁺-defn xs
+    in cong₂ (λ z → f x z ∷_) (cong List⁺.head eq) (cong toList eq)
+
+  scanr-defn : scanr f e ≗ List.map h ∘ List.tails
+  scanr-defn xs = begin
+    scanr f e xs
+      ≡⟨ cong toList (scanr⁺-defn xs) ⟩
+    toList (List⁺.map h (List⁺.tails xs))
+      ≡⟨⟩
+    List.map h (toList (List⁺.tails xs))
+      ≡⟨ cong (List.map h) (List⁺.toList-tails xs) ⟩
+    List.map h (List.tails xs)
+      ∎
+    where open ≡-Reasoning
+
+-- scanl⁺ and scanl
+
+module _ (f : A → B → A) where
+
+  private
+    h = List.foldl f
+
+  scanl⁺-defn : ∀ e → scanl⁺ f e ≗ List⁺.map (h e) ∘ List⁺.inits
+  scanl⁺-defn e []       = refl
+  scanl⁺-defn e (x ∷ xs) = let eq = scanl⁺-defn (f e x) xs in
+    cong (e ∷_) $ cong (f e x ∷_) $ trans (cong List⁺.tail eq) (List.map-∘ _)
+
+  scanl-defn : ∀ e → scanl f e ≗ List.map (h e) ∘ List.inits
+  scanl-defn e []       = refl
+  scanl-defn e (x ∷ xs) = cong (e ∷_) $ begin
+    scanl f (f e x) xs
+      ≡⟨ scanl-defn (f e x) xs ⟩
+    List.map (h (f e x)) (List.inits xs)
+      ≡⟨⟩
+    List.map (h e ∘ (x ∷_)) (List.inits xs)
+      ≡⟨ List.map-∘ (List.inits xs) ⟩
+    List.map (h e) (List.map (x ∷_) (List.inits xs))
+      ∎
+    where open ≡-Reasoning

From 1c1e079eca598c5b8ebecb5839b5584be3cf615b Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 27 May 2024 14:39:49 +0100
Subject: [PATCH 07/16] fix-up `inits` and `tails`

---
 CHANGELOG.md                     | 15 ++++++++++++++-
 src/Data/List/Base.agda          | 20 ++++++++++----------
 src/Data/List/NonEmpty/Base.agda | 12 ++----------
 3 files changed, 26 insertions(+), 21 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index f5058ee9a2..1abd89989d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -115,7 +115,8 @@ New modules
 
 * Refactoring of `Data.List.Base.{scanr|scanl}` and their properties:
   ```
-  Data.List.Scans
+  Data.List.Scans.Base
+  Data.List.Scans.Properties
   ```
 
 * Prime factorisation of natural numbers.
@@ -371,12 +372,24 @@ Additions to existing modules
   i*j≢0     : .{{_ : NonZero i}} .{{_ : NonZero j}} → NonZero (i * j)
   ```
 
+* In `Data.List.Base` redefine `inits` and `tails` in terms of:
+  ```agda
+  inits-tail : List A → List (List A)
+  tails-tail : List A → List (List A)
+  ```
+
 * In `Data.List.Membership.Setoid.Properties`:
   ```agda
   reverse⁺ : x ∈ xs → x ∈ reverse xs
   reverse⁻ : x ∈ reverse xs → x ∈ xs
   ```
 
+* In `Data.List.NonEmpty.Base`:
+  ```agda
+  inits : List A → List⁺ (List A)
+  tails : List A → List⁺ (List A)
+  ```
+
 * In `Data.List.Properties`:
   ```agda
   length-catMaybes      : length (catMaybes xs) ≤ length xs
diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index e129dc9989..3df18d99fc 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -189,19 +189,19 @@ iterate : (A → A) → A → ℕ → List A
 iterate f e zero    = []
 iterate f e (suc n) = e ∷ iterate f (f e) n
 
+inits-tail : List A → List (List A)
+inits-tail []       = []
+inits-tail (x ∷ xs) = [ x ] ∷ map (x ∷_) (inits-tail xs)
+
 inits : List A → List (List A)
-inits {A = A} xs = [] ∷ go xs
-  where
-  go : List A → List (List A)
-  go []       = []
-  go (x ∷ xs) = [ x ] ∷ map (x ∷_) (go xs)
+inits xs = [] ∷ inits-tail xs
+
+tails-tail : List A → List (List A)
+tails-tail []       = []
+tails-tail (_ ∷ xs) = xs ∷ tails-tail xs
 
 tails : List A → List (List A)
-tails {A = A} xs = xs ∷ go xs
-  where
-  go : List A → List (List A)
-  go []       = []
-  go (_ ∷ xs) = xs ∷ go xs
+tails xs = xs ∷ tails-tail xs
 
 insertAt : (xs : List A) → Fin (suc (length xs)) → A → List A
 insertAt xs       zero    v = v ∷ xs
diff --git a/src/Data/List/NonEmpty/Base.agda b/src/Data/List/NonEmpty/Base.agda
index 2c5ff8c943..66bab56605 100644
--- a/src/Data/List/NonEmpty/Base.agda
+++ b/src/Data/List/NonEmpty/Base.agda
@@ -146,20 +146,12 @@ ap fs as = concatMap (λ f → map f as) fs
 -- Inits
 
 inits : List A → List⁺ (List A)
-inits xs = [] ∷ go xs
-  where
-  go : List A → List (List A)
-  go []       = []
-  go (x ∷ xs) = List.[ x ] ∷ List.map (x ∷_) (go xs)
+inits xs = [] ∷ List.inits-tail xs
 
 -- Tails
 
 tails : List A → List⁺ (List A)
-tails xs = xs ∷ go xs
-  where
-  go : List A → List (List A)
-  go []       = []
-  go (x ∷ xs) = xs ∷ go xs
+tails xs = xs ∷ List.tails-tail xs
 
 -- Reverse
 

From f2b1d617fbbcc28d6ff1e0807117fe7f397a0f1a Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 27 May 2024 14:40:25 +0100
Subject: [PATCH 08/16] fix up `import`s

---
 src/Data/List.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/List.agda b/src/Data/List.agda
index cd654881bd..70e8519440 100644
--- a/src/Data/List.agda
+++ b/src/Data/List.agda
@@ -17,5 +17,5 @@ module Data.List where
 
 open import Data.List.Base public
   hiding (scanr; scanl)
-open import Data.List.Scans public
+open import Data.List.Scans.Base public
   using (scanr; scanl)

From c7af1ef47d8c07acbb76aaa0148a4812cf4a5079 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 27 May 2024 14:44:08 +0100
Subject: [PATCH 09/16] knock-ons

---
 src/Codata/Sized/Colist/Properties.agda | 2 +-
 src/Tactic/RingSolver/Core/NatSet.agda  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Codata/Sized/Colist/Properties.agda b/src/Codata/Sized/Colist/Properties.agda
index 39d798686f..3a9958b715 100644
--- a/src/Codata/Sized/Colist/Properties.agda
+++ b/src/Codata/Sized/Colist/Properties.agda
@@ -22,7 +22,7 @@ open import Codata.Sized.Stream as Stream using (Stream; _∷_)
 open import Data.Vec.Bounded as Vec≤ using (Vec≤)
 open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_)
-import Data.List.Scans as Scans
+import Data.List.Scans.Base as Scans
 open import Data.List.Relation.Binary.Equality.Propositional using (≋-refl)
 open import Data.Maybe.Base as Maybe using (Maybe; nothing; just)
 import Data.Maybe.Properties as Maybe
diff --git a/src/Tactic/RingSolver/Core/NatSet.agda b/src/Tactic/RingSolver/Core/NatSet.agda
index ddd7d406c2..53af68c511 100644
--- a/src/Tactic/RingSolver/Core/NatSet.agda
+++ b/src/Tactic/RingSolver/Core/NatSet.agda
@@ -38,7 +38,7 @@ module Tactic.RingSolver.Core.NatSet where
 
 open import Data.Nat.Base   as ℕ     using (ℕ; suc; zero)
 open import Data.List.Base  as List  using (List; _∷_; [])
-open import Data.List.Scans as Scans using (scanl)
+open import Data.List.Scans.Base as Scans using (scanl)
 open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
 open import Data.Bool.Base  as Bool  using (Bool)
 open import Function.Base            using (const; _∘_)

From 3cc0b3c22edd4e509e97d58531971af6f4e36285 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 27 May 2024 14:53:06 +0100
Subject: [PATCH 10/16] Andreas's suggestions

---
 CHANGELOG.md                     |  4 ++--
 src/Data/List/Base.agda          | 16 ++++++++--------
 src/Data/List/NonEmpty/Base.agda |  4 ++--
 3 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1abd89989d..0f2070ec03 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -374,8 +374,8 @@ Additions to existing modules
 
 * In `Data.List.Base` redefine `inits` and `tails` in terms of:
   ```agda
-  inits-tail : List A → List (List A)
-  tails-tail : List A → List (List A)
+  tail∘inits : List A → List (List A)
+  tail∘tails : List A → List (List A)
   ```
 
 * In `Data.List.Membership.Setoid.Properties`:
diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index 3df18d99fc..4dea5e5f10 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -189,19 +189,19 @@ iterate : (A → A) → A → ℕ → List A
 iterate f e zero    = []
 iterate f e (suc n) = e ∷ iterate f (f e) n
 
-inits-tail : List A → List (List A)
-inits-tail []       = []
-inits-tail (x ∷ xs) = [ x ] ∷ map (x ∷_) (inits-tail xs)
+tail∘inits : List A → List (List A)
+tail∘inits []       = []
+tail∘inits (x ∷ xs) = [ x ] ∷ map (x ∷_) (tail∘inits xs)
 
 inits : List A → List (List A)
-inits xs = [] ∷ inits-tail xs
+inits xs = [] ∷ tail∘inits xs
 
-tails-tail : List A → List (List A)
-tails-tail []       = []
-tails-tail (_ ∷ xs) = xs ∷ tails-tail xs
+tail∘tails : List A → List (List A)
+tail∘tails []       = []
+tail∘tails (_ ∷ xs) = xs ∷ tail∘tails xs
 
 tails : List A → List (List A)
-tails xs = xs ∷ tails-tail xs
+tails xs = xs ∷ tail∘tails xs
 
 insertAt : (xs : List A) → Fin (suc (length xs)) → A → List A
 insertAt xs       zero    v = v ∷ xs
diff --git a/src/Data/List/NonEmpty/Base.agda b/src/Data/List/NonEmpty/Base.agda
index 66bab56605..f332dcc162 100644
--- a/src/Data/List/NonEmpty/Base.agda
+++ b/src/Data/List/NonEmpty/Base.agda
@@ -146,12 +146,12 @@ ap fs as = concatMap (λ f → map f as) fs
 -- Inits
 
 inits : List A → List⁺ (List A)
-inits xs = [] ∷ List.inits-tail xs
+inits xs = [] ∷ List.tail∘inits xs
 
 -- Tails
 
 tails : List A → List⁺ (List A)
-tails xs = xs ∷ List.tails-tail xs
+tails xs = xs ∷ List.tail∘tails xs
 
 -- Reverse
 

From 9fef63aed1d08539ad48b796ae6881f0864c387c Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Tue, 28 May 2024 10:24:10 +0100
Subject: [PATCH 11/16] further, better, refactoring is possible

---
 src/Data/List/NonEmpty/Properties.agda |  6 ++----
 src/Data/List/Scans/Properties.agda    | 15 +++++----------
 2 files changed, 7 insertions(+), 14 deletions(-)

diff --git a/src/Data/List/NonEmpty/Properties.agda b/src/Data/List/NonEmpty/Properties.agda
index f6d9c521b4..9469cd2b87 100644
--- a/src/Data/List/NonEmpty/Properties.agda
+++ b/src/Data/List/NonEmpty/Properties.agda
@@ -122,15 +122,13 @@ map-∘ (x ∷ xs) = cong (_ ∷_) (List.map-∘ xs)
 -- inits
 
 toList-inits : toList ∘ inits ≗ List.inits {A = A}
-toList-inits []       = refl
-toList-inits (x ∷ xs) = cong (([] ∷_) ∘ List.map (x ∷_)) (toList-inits xs)
+toList-inits _ = refl
 
 ------------------------------------------------------------------------
 -- tails
 
 toList-tails : toList ∘ tails ≗ List.tails {A = A}
-toList-tails []          = refl
-toList-tails ys@(_ ∷ xs) = cong (ys ∷_) (toList-tails xs)
+toList-tails _ = refl
 
 ------------------------------------------------------------------------
 -- groupSeqs
diff --git a/src/Data/List/Scans/Properties.agda b/src/Data/List/Scans/Properties.agda
index 6ebbf5353f..3b240e8a19 100644
--- a/src/Data/List/Scans/Properties.agda
+++ b/src/Data/List/Scans/Properties.agda
@@ -48,8 +48,6 @@ module _ (f : A → B → B) (e : B) where
       ≡⟨ cong toList (scanr⁺-defn xs) ⟩
     toList (List⁺.map h (List⁺.tails xs))
       ≡⟨⟩
-    List.map h (toList (List⁺.tails xs))
-      ≡⟨ cong (List.map h) (List⁺.toList-tails xs) ⟩
     List.map h (List.tails xs)
       ∎
     where open ≡-Reasoning
@@ -67,14 +65,11 @@ module _ (f : A → B → A) where
     cong (e ∷_) $ cong (f e x ∷_) $ trans (cong List⁺.tail eq) (List.map-∘ _)
 
   scanl-defn : ∀ e → scanl f e ≗ List.map (h e) ∘ List.inits
-  scanl-defn e []       = refl
-  scanl-defn e (x ∷ xs) = cong (e ∷_) $ begin
-    scanl f (f e x) xs
-      ≡⟨ scanl-defn (f e x) xs ⟩
-    List.map (h (f e x)) (List.inits xs)
+  scanl-defn e xs = begin
+    scanl f e xs
+      ≡⟨ cong toList (scanl⁺-defn e xs) ⟩
+    toList (List⁺.map (h e) (List⁺.inits xs))
       ≡⟨⟩
-    List.map (h e ∘ (x ∷_)) (List.inits xs)
-      ≡⟨ List.map-∘ (List.inits xs) ⟩
-    List.map (h e) (List.map (x ∷_) (List.inits xs))
+    List.map (h e) (List.inits xs)
       ∎
     where open ≡-Reasoning

From b3d45a78fe9387e1f259edabee3263c33c1e206e Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Tue, 28 May 2024 10:28:38 +0100
Subject: [PATCH 12/16] yet further, better, refactoring is possible: remove
 explicit equational reasoning!

---
 src/Data/List/Scans/Properties.agda | 20 ++------------------
 1 file changed, 2 insertions(+), 18 deletions(-)

diff --git a/src/Data/List/Scans/Properties.agda b/src/Data/List/Scans/Properties.agda
index 3b240e8a19..01b2229684 100644
--- a/src/Data/List/Scans/Properties.agda
+++ b/src/Data/List/Scans/Properties.agda
@@ -17,8 +17,6 @@ open import Function.Base using (_∘_; _$_)
 open import Level using (Level)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; _≗_; refl; trans; cong; cong₂)
-open import Relation.Binary.PropositionalEquality.Properties
-  using (module ≡-Reasoning)
 
 private
   variable
@@ -43,14 +41,7 @@ module _ (f : A → B → B) (e : B) where
     in cong₂ (λ z → f x z ∷_) (cong List⁺.head eq) (cong toList eq)
 
   scanr-defn : scanr f e ≗ List.map h ∘ List.tails
-  scanr-defn xs = begin
-    scanr f e xs
-      ≡⟨ cong toList (scanr⁺-defn xs) ⟩
-    toList (List⁺.map h (List⁺.tails xs))
-      ≡⟨⟩
-    List.map h (List.tails xs)
-      ∎
-    where open ≡-Reasoning
+  scanr-defn xs = cong toList (scanr⁺-defn xs)
 
 -- scanl⁺ and scanl
 
@@ -65,11 +56,4 @@ module _ (f : A → B → A) where
     cong (e ∷_) $ cong (f e x ∷_) $ trans (cong List⁺.tail eq) (List.map-∘ _)
 
   scanl-defn : ∀ e → scanl f e ≗ List.map (h e) ∘ List.inits
-  scanl-defn e xs = begin
-    scanl f e xs
-      ≡⟨ cong toList (scanl⁺-defn e xs) ⟩
-    toList (List⁺.map (h e) (List⁺.inits xs))
-      ≡⟨⟩
-    List.map (h e) (List.inits xs)
-      ∎
-    where open ≡-Reasoning
+  scanl-defn e xs = cong toList (scanl⁺-defn e xs)

From 3f5ad538f2a2a9bcc3736c62cb614bb463dd305f Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Tue, 28 May 2024 14:15:17 +0100
Subject: [PATCH 13/16] Update CHANGELOG.md

Fix deprecated names
---
 CHANGELOG.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 0f2070ec03..0c8852b528 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -67,8 +67,8 @@ Deprecated names
 
 * In `Data.List.Base`:
   ```agda
-  scanr  ↦  Data.List.Scans.scanr
-  scanl  ↦  Data.List.Scans.scanl
+  scanr  ↦  Data.List.Scans.Base.scanr
+  scanl  ↦  Data.List.Scans.Base.scanl
   ```
 
 * In `Data.List.Properties`:

From aa265607ed5fffd4a2b35220eb6aed2ae8eb8df4 Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Tue, 28 May 2024 14:18:13 +0100
Subject: [PATCH 14/16] Update Base.agda

Fix deprecations
---
 src/Data/List/Base.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index 4dea5e5f10..9ea8b551b9 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -575,7 +575,7 @@ scanr f e (x ∷ xs) with scanr f e xs
 ... | ys@(y ∷ _) = f x y ∷ ys
 {-# WARNING_ON_USAGE scanr
 "Warning: scanr was deprecated in v2.1.
-Please use Data.List.Scans.scanr instead."
+Please use Data.List.Scans.Base.scanr instead."
 #-}
 
 scanl : (A → B → A) → A → List B → List A
@@ -583,5 +583,5 @@ scanl f e []       = e ∷ []
 scanl f e (x ∷ xs) = e ∷ scanl f (f e x) xs
 {-# WARNING_ON_USAGE scanl
 "Warning: scanl was deprecated in v2.1.
-Please use Data.List.Scans.scanl instead."
+Please use Data.List.Scans.Base.scanl instead."
 #-}

From f70cf4d1b9661a2088ad71cb878b7eef827d19c8 Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Tue, 28 May 2024 14:20:42 +0100
Subject: [PATCH 15/16] Update Properties.agda

Fix deprecations
---
 src/Data/List/Properties.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 32dc79e184..e280be132b 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -1568,7 +1568,7 @@ scanr-defn f e (x ∷ xs@(_ ∷ _))
   = cong₂ (λ z → f x z ∷_) (∷-injectiveˡ eq) eq
 {-# WARNING_ON_USAGE scanr-defn
 "Warning: scanr-defn was deprecated in v2.1.
-Please use Data.List.Scans.scanr-defn instead."
+Please use Data.List.Scans.Properties.scanr-defn instead."
 #-}
 
 scanl-defn : ∀ (f : A → B → A) (e : A) →
@@ -1585,5 +1585,5 @@ scanl-defn f e (x ∷ xs) = cong (e ∷_) (begin
  ∎)
 {-# WARNING_ON_USAGE scanl-defn
 "Warning: scanl-defn was deprecated in v2.1.
-Please use Data.List.Scans.scanl-defn instead."
+Please use Data.List.Scans.Properties.scanl-defn instead."
 #-}

From 0efdcd09367a64250edd74faa4bb5e257e112772 Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Tue, 28 May 2024 14:24:29 +0100
Subject: [PATCH 16/16] Update CHANGELOG.md

Fix deprecated names
---
 CHANGELOG.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 0c8852b528..88dbe3c075 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -73,8 +73,8 @@ Deprecated names
 
 * In `Data.List.Properties`:
   ```agda
-  scanr-defn  ↦  Data.List.Scans.scanr-defn
-  scanl-defn  ↦  Data.List.Scans.scanl-defn
+  scanr-defn  ↦  Data.List.Scans.Properties.scanr-defn
+  scanl-defn  ↦  Data.List.Scans.Properties.scanl-defn
   ```
 
 * In `Data.List.NonEmpty.Base`: