Refactor Data.List.Base.scan* and their properties

CHANGELOG.md

@@ -65,6 +65,30 @@ Deprecated names
   isRing*  ↦  Algebra.Structures.isRing
   ```
 
+* In `Data.List.Base`:
+  ```agda
+  scanr  ↦  Data.List.Scans.Base.scanr
+  scanl  ↦  Data.List.Scans.Base.scanl
+  ```
+
+* In `Data.List.Properties`:
+  ```agda
+  scanr-defn  ↦  Data.List.Scans.Properties.scanr-defn
+  scanl-defn  ↦  Data.List.Scans.Properties.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-∣
@@ -89,6 +113,12 @@ New modules
   Algebra.Module.Bundles.Raw
   ```
 
+* Refactoring of `Data.List.Base.{scanr|scanl}` and their properties:
+  ```
+  Data.List.Scans.Base
+  Data.List.Scans.Properties
+  ```
+
 * Prime factorisation of natural numbers.
   ```
   Data.Nat.Primality.Factorisation
@@ -342,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
+  tail∘inits : List A → List (List A)
+  tail∘tails : 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

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.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
@@ -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

src/Data/List.agda

@@ -8,10 +8,14 @@
 -- lists.
 
 {-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --warn=noUserWarning #-} -- for deprecated scans
 
 module Data.List where
 
 ------------------------------------------------------------------------
 -- Types and basic operations
 
 open import Data.List.Base public
+  hiding (scanr; scanl)
+open import Data.List.Scans.Base public
+  using (scanr; scanl)

src/Data/List/Base.agda

@@ -189,13 +189,19 @@ iterate : (A → A) → A → ℕ → List A
 iterate f e zero    = []
 iterate f e (suc n) = e ∷ iterate f (f e) n
 
+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 []       = [] ∷ []
-inits (x ∷ xs) = [] ∷ map (x ∷_) (inits xs)
+inits xs = [] ∷ tail∘inits xs
+
+tail∘tails : List A → List (List A)
+tail∘tails []       = []
+tail∘tails (_ ∷ xs) = xs ∷ tail∘tails xs
 
 tails : List A → List (List A)
-tails []       = [] ∷ []
-tails (x ∷ xs) = (x ∷ xs) ∷ tails xs
+tails xs = xs ∷ tail∘tails xs
 
 insertAt : (xs : List A) → Fin (suc (length xs)) → A → List A
 insertAt xs       zero    v = v ∷ xs
@@ -205,18 +211,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 +565,23 @@ _─_ = removeAt
 "Warning: _─_ was deprecated in v2.0.
 Please use removeAt instead."
 #-}
+
+-- Version 2.1
+
+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.Base.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.Base.scanl instead."
+#-}

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

src/Data/List/NonEmpty/Base.agda

@@ -143,6 +143,16 @@ 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 = [] ∷ List.tail∘inits xs
+
+-- Tails
+
+tails : List A → List⁺ (List A)
+tails xs = xs ∷ List.tail∘tails xs
+
 -- Reverse
 
 reverse : List⁺ A → List⁺ A

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,18 @@ 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
+
+------------------------------------------------------------------------
+-- tails
+
+toList-tails : toList ∘ tails ≗ List.tails {A = A}
+toList-tails _ = refl
+
 ------------------------------------------------------------------------
 -- groupSeqs
 

src/Data/List/Properties.agda

@@ -8,6 +8,7 @@
 -- equalities than _≡_.
 
 {-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --warn=noUserWarning #-} -- for deprecated scans
 
 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.Properties.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.Properties.scanl-defn instead."
+#-}

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

src/Data/List/Scans/Properties.agda

@@ -0,0 +1,59 @@
+------------------------------------------------------------------------
+-- 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₂)
+
+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 = cong toList (scanr⁺-defn xs)
+
+-- 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 xs = cong toList (scanl⁺-defn e xs)

src/Tactic/RingSolver/Core/NatSet.agda

@@ -38,6 +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.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; _∘_)
@@ -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