Revise definitions of Data.List.Base.scanl|inits; add Data.List.NonEmpty.Base.scanl⁺|inits⁺

CHANGELOG.md

@@ -271,6 +271,20 @@ Additions to existing modules
   i*j≢0     : .{{_ : NonZero i}} .{{_ : NonZero j}} → NonZero (i * j)
   ```
 
+* In `Data.List.NonEmpty.Base`:
+  ```agda
+  inits⁺     : List A → List⁺ (List A)
+  scanl⁺     : (A → B → A) → A → List B → List⁺ A
+  ```
+
+* In `Data.List.NonEmpty.Properties`:
+  ```agda
+  toList-map    : (f : A → B) → toList ∘ map f ≗ List.map f ∘ toList
+  toList-inits⁺ : toList ∘ inits⁺ ≗ List.inits
+  scanl⁺-defn   : scanl⁺ f e ≗ map (List.foldl f e) ∘ inits⁺
+  toList-scanl⁺ : toList ∘ scanl⁺ f e ≗ List.map (List.foldl f e) ∘ List.inits
+  ```
+
 * In `Data.List.Properties`:
   ```agda
   applyUpTo-∷ʳ          : applyUpTo f n ∷ʳ f n ≡ applyUpTo f (suc n)

src/Data/List/Base.agda

@@ -193,12 +193,18 @@ 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)
+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 []       = [] ∷ []
-tails (x ∷ xs) = (x ∷ xs) ∷ tails xs
+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
@@ -217,8 +223,11 @@ scanr f e (x ∷ xs) with scanr f e xs
 ... | 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
+scanl {A = A} {B = B} f 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
 
 -- Tabulation
 

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⁺ {A = A} xs = [] ∷ go xs
+  where
+  go : List A → List (List A)
+  go []       = []
+  go (x ∷ xs) = List.[ x ] ∷ List.map (x ∷_) (go xs)
+
+-- Scanl
+
+scanl⁺ : (A → B → A) → A → List B → List⁺ A
+scanl⁺ {A = A} {B = B} f 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
+
 -- Reverse
 
 reverse : List⁺ A → List⁺ A

src/Data/List/NonEmpty/Properties.agda

@@ -113,6 +113,39 @@ 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)
 
+toList-map : ∀ (f : A → B) xs → toList (map f xs) ≡ List.map f (toList xs)
+toList-map f (x ∷ xs) = refl
+
+------------------------------------------------------------------------
+-- inits
+
+toList-inits⁺ : (xs : List A) → toList (inits⁺ xs) ≡ List.inits xs
+toList-inits⁺ []       = refl
+toList-inits⁺ (x ∷ xs) = cong (([] ∷_) ∘ List.map (x ∷_)) (toList-inits⁺ xs)
+
+------------------------------------------------------------------------
+-- scanl
+
+module _ (f : A → B → A) where
+
+  private
+    h = List.foldl f
+
+  scanl⁺-defn : ∀ e → scanl⁺ f e ≗ 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 tail eq) (List.map-∘ _)
+
+  toList-scanl⁺ : ∀ e → toList ∘ scanl⁺ f e ≗ List.map (h e) ∘ List.inits
+  toList-scanl⁺ e xs = begin
+    toList (scanl⁺ f e xs)
+      ≡⟨ cong toList (scanl⁺-defn e xs) ⟩
+    toList (map (h e) (inits⁺ xs))
+      ≡⟨ toList-map (h e) (inits⁺ xs) ⟩
+    List.map (h e) (toList (inits⁺ xs))
+      ≡⟨ cong (List.map (h e)) (toList-inits⁺ xs) ⟩
+    List.map (h e) (List.inits xs) ∎
+
 ------------------------------------------------------------------------
 -- groupSeqs
 

src/Data/List/Properties.agda

@@ -628,23 +628,23 @@ 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
+  = cong₂ (λ z → f x z ∷_) (∷-injectiveˡ eq) 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-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