From 6cdafa9db254ae1070c54c9608cbeca8a2f1b017 Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Wed, 9 Aug 2023 17:29:38 -0400
Subject: [PATCH 01/20] Add `iterate` for List

---
 CHANGELOG.md            | 17 ++++++++++++++---
 src/Data/List/Base.agda |  4 ++++
 2 files changed, 18 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 420d85fddc..3dd013a261 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2206,10 +2206,21 @@ Additions to existing modules
 
 * Added new functions and definitions to `Data.List.Base`:
   ```agda
-  catMaybes : List (Maybe A) → List A
-  ap : List (A → B) → List A → List B
-  ++-rawMagma : Set a → RawMagma a _
+  takeWhileᵇ      : (A → Bool) → List A → List A
+  dropWhileᵇ      : (A → Bool) → List A → List A
+  filterᵇ         : (A → Bool) → List A → List A
+  partitionᵇ      : (A → Bool) → List A → List A × List A
+  spanᵇ           : (A → Bool) → List A → List A × List A
+  breakᵇ          : (A → Bool) → List A → List A × List A
+  linesByᵇ        : (A → Bool) → List A → List (List A)
+  wordsByᵇ        : (A → Bool) → List A → List (List A)
+  derunᵇ          : (A → A → Bool) → List A → List A
+  deduplicateᵇ    : (A → A → Bool) → List A → List A
+  catMaybes       : List (Maybe A) → List A
+  ap              : List (A → B) → List A → List B
+  ++-rawMagma     : Set a → RawMagma a _
   ++-[]-rawMonoid : Set a → RawMonoid a _
+  iterate         : (A → A) → A → ℕ → List A
   ```
 
 * Added new proofs in `Data.List.Relation.Binary.Lex.Strict`:
diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index 9817cf8648..aa65abe5f6 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -188,6 +188,10 @@ replicate : ℕ → A → List A
 replicate zero    x = []
 replicate (suc n) x = x ∷ replicate n x
 
+iterate : (A → A) → A → ℕ → List A
+iterate f k zero    = []
+iterate f k (suc n) = k ∷ iterate f (f k) n
+
 inits : List A → List (List A)
 inits []       = [] ∷ []
 inits (x ∷ xs) = [] ∷ map (x ∷_) (inits xs)

From ce41ac988719303b1fa4db2584d656bd7a46e4b1 Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Thu, 10 Aug 2023 10:27:17 -0400
Subject: [PATCH 02/20] Update argument names

---
 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 aa65abe5f6..a59638636b 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -189,8 +189,8 @@ replicate zero    x = []
 replicate (suc n) x = x ∷ replicate n x
 
 iterate : (A → A) → A → ℕ → List A
-iterate f k zero    = []
-iterate f k (suc n) = k ∷ iterate f (f k) n
+iterate s z zero    = []
+iterate s z (suc n) = z ∷ iterate s (s z) n
 
 inits : List A → List (List A)
 inits []       = [] ∷ []

From 4a1b45fbeb6ff575e10c0b5a0e52755b0654c8b2 Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Sat, 12 Aug 2023 14:06:38 -0400
Subject: [PATCH 03/20] Properties for `List.iterate`, `List.replicate`,
 `Vec.iterate`

---
 src/Data/List/Base.agda       |  4 ++--
 src/Data/List/Properties.agda | 38 +++++++++++++++++++++++++++++++++++
 src/Data/Vec/Properties.agda  | 11 ++++++++++
 3 files changed, 51 insertions(+), 2 deletions(-)

diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index a59638636b..24bb3535a1 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -189,8 +189,8 @@ replicate zero    x = []
 replicate (suc n) x = x ∷ replicate n x
 
 iterate : (A → A) → A → ℕ → List A
-iterate s z zero    = []
-iterate s z (suc n) = z ∷ iterate s (s z) n
+iterate f e zero    = []
+iterate f e (suc n) = e ∷ iterate f (f e) n
 
 inits : List A → List (List A)
 inits []       = [] ∷ []
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index eb403f8b91..4a061bb28e 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -30,6 +30,7 @@ open import Data.Product.Base as Prod
 import Data.Product.Relation.Unary.All as Prod using (All)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Data.These.Base as These using (These; this; that; these)
+open import Data.Vec.Base as Vec using (toList)
 open import Data.Fin.Properties using (toℕ-cast)
 open import Function.Base using (id; _∘_; _∘′_; _∋_; _-⟨_∣; ∣_⟩-_; _$_; const; flip)
 open import Function.Definitions using (Injective)
@@ -628,6 +629,43 @@ length-replicate : ∀ n {x : A} → length (replicate n x) ≡ n
 length-replicate zero    = refl
 length-replicate (suc n) = cong suc (length-replicate n)
 
+lookup-replicate : ∀ n (x : A) (i : Fin (length (replicate n x))) → lookup (replicate n x) i ≡ x
+lookup-replicate (suc n) x zero    = refl
+lookup-replicate (suc n) x (suc i) = lookup-replicate n x i
+
+map-replicate :  ∀ (f : A → B) (x : A) n →
+                 map f (replicate n x) ≡ replicate n (f x)
+map-replicate f x zero    = refl
+map-replicate f x (suc n) = cong (_ ∷_) (map-replicate f x n)
+
+zipWith-replicate : ∀ n (_⊕_ : A → B → C) (x : A) (y : B) →
+                    zipWith _⊕_ (replicate n x) (replicate n y) ≡ replicate n (x ⊕ y)
+zipWith-replicate zero    _⊕_ x y = refl
+zipWith-replicate (suc n) _⊕_ x y = cong (x ⊕ y ∷_) (zipWith-replicate n _⊕_ x y)
+
+------------------------------------------------------------------------
+-- iterate
+
+length-iterate : ∀ n {f} {x : A} → length (iterate f x n) ≡ n
+length-iterate zero    = refl
+length-iterate (suc n) = cong suc (length-iterate n)
+
+toList-iterate : ∀ n {f} {x : A} → toList (Vec.iterate f x {n = n}) ≡ iterate f x n
+toList-iterate zero    = refl
+toList-iterate (suc n) = cong (_ ∷_) (toList-iterate n)
+
+iterate-id : ∀ n {x : A} → iterate id x n ≡ replicate n x
+iterate-id zero    = refl
+iterate-id (suc n) = cong (_ ∷_) (iterate-id n)
+
+take-iterate : ∀ n {f} {x : A} → take n (iterate f x n) ≡ iterate f x n
+take-iterate zero    = refl
+take-iterate (suc n) = cong (_ ∷_) (take-iterate n)
+
+drop-iterate : ∀ n {f} {x : A} → drop n (iterate f x n) ≡ []
+drop-iterate zero    = refl
+drop-iterate (suc n) = drop-iterate n
+
 ------------------------------------------------------------------------
 -- scanr
 
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 8113d0a932..52b9053b17 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -1068,6 +1068,17 @@ toList-replicate : ∀ (n : ℕ) (x : A) →
 toList-replicate zero    x = refl
 toList-replicate (suc n) x = cong (_ List.∷_) (toList-replicate n x)
 
+------------------------------------------------------------------------
+-- iterate
+
+length-iterate : ∀ n f (x : A) → length (iterate f x {n}) ≡ n
+length-iterate zero    f x = refl
+length-iterate (suc n) f x = cong suc refl
+
+iterate-id : ∀ (x : A) n → iterate id x {n} ≡ replicate x
+iterate-id x zero    = refl
+iterate-id x (suc n) = cong (_ ∷_) (iterate-id (id x) n)
+
 ------------------------------------------------------------------------
 -- tabulate
 

From b9e5c28cb5b08cc26b75e06b2fa981142c2d245e Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Sat, 12 Aug 2023 14:30:42 -0400
Subject: [PATCH 04/20] Update CHANGELOG

---
 CHANGELOG.md | 45 ++++++++++++++++++++++++++++++++++-----------
 1 file changed, 34 insertions(+), 11 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3dd013a261..860482838e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2206,21 +2206,23 @@ Additions to existing modules
 
 * Added new functions and definitions to `Data.List.Base`:
   ```agda
-  takeWhileᵇ      : (A → Bool) → List A → List A
-  dropWhileᵇ      : (A → Bool) → List A → List A
-  filterᵇ         : (A → Bool) → List A → List A
-  partitionᵇ      : (A → Bool) → List A → List A × List A
-  spanᵇ           : (A → Bool) → List A → List A × List A
-  breakᵇ          : (A → Bool) → List A → List A × List A
-  linesByᵇ        : (A → Bool) → List A → List (List A)
-  wordsByᵇ        : (A → Bool) → List A → List (List A)
-  derunᵇ          : (A → A → Bool) → List A → List A
-  deduplicateᵇ    : (A → A → Bool) → List A → List A
+  takeWhileᵇ   : (A → Bool) → List A → List A
+  dropWhileᵇ   : (A → Bool) → List A → List A
+  filterᵇ      : (A → Bool) → List A → List A
+  partitionᵇ   : (A → Bool) → List A → List A × List A
+  spanᵇ        : (A → Bool) → List A → List A × List A
+  breakᵇ       : (A → Bool) → List A → List A × List A
+  linesByᵇ     : (A → Bool) → List A → List (List A)
+  wordsByᵇ     : (A → Bool) → List A → List (List A)
+  derunᵇ       : (A → A → Bool) → List A → List A
+  deduplicateᵇ : (A → A → Bool) → List A → List A
+
   catMaybes       : List (Maybe A) → List A
   ap              : List (A → B) → List A → List B
   ++-rawMagma     : Set a → RawMagma a _
   ++-[]-rawMonoid : Set a → RawMonoid a _
-  iterate         : (A → A) → A → ℕ → List A
+
+  iterate : (A → A) → A → ℕ → List A
   ```
 
 * Added new proofs in `Data.List.Relation.Binary.Lex.Strict`:
@@ -2281,12 +2283,27 @@ Additions to existing modules
 
   take-all : n ≥ length xs → take n xs ≡ xs
 
+<<<<<<< HEAD
   take-[] : take m [] ≡ []
   drop-[] : drop m [] ≡ []
 
   map-replicate : map f (replicate n x) ≡ replicate n (f x)
 
   drop-drop : drop n (drop m xs) ≡ drop (m + n) xs
+=======
+  take-[] : ∀ m → take  m [] ≡ []
+  drop-[] : ∀ m → drop  m [] ≡ []
+
+  lookup-replicate  : lookup (replicate n x) i ≡ x
+  map-replicate     : map f (replicate n x) ≡ replicate n (f x)
+  zipWith-replicate : zipWith _⊕_ (replicate n x) (replicate n y) ≡ replicate n (x ⊕ y)
+
+  length-iterate : length (iterate f x n) ≡ n
+  toList-iterate : toList (Vec.iterate f x {n = n}) ≡ iterate f x n
+  iterate-id     : iterate id x n ≡ replicate n x
+  take-iterate   : take n (iterate f x n) ≡ iterate f x n
+  drop-iterate   : drop n (iterate f x n) ≡ []
+>>>>>>> dd0d05e65 (Update CHANGELOG)
   ```
 
 * Added new patterns and definitions to `Data.Nat.Base`:
@@ -2707,6 +2724,7 @@ Additions to existing modules
   lookup-cast   : lookup (cast eq xs) (Fin.cast eq i) ≡ lookup xs i
   lookup-cast₁  : lookup (cast eq xs) i ≡ lookup xs (Fin.cast (sym eq) i)
   lookup-cast₂  : lookup xs (Fin.cast eq i) ≡ lookup (cast (sym eq) xs) i
+<<<<<<< HEAD
   cast-reverse : cast eq ∘ reverse ≗ reverse ∘ cast eq
 
   zipwith-++ : zipWith f (xs ++ ys) (xs' ++ ys') ≡ zipWith f xs xs' ++ zipWith f ys ys'
@@ -2726,6 +2744,11 @@ Additions to existing modules
 * Added new proofs in `Data.Vec.Membership.Propositional.Properties`:
   ```agda
   index-∈-fromList⁺ : Any.index (∈-fromList⁺ v∈xs) ≡ indexₗ v∈xs
+=======
+
+  length-iterate : length (iterate f x {n}) ≡ n
+  iterate-id     : iterate id x {n} ≡ replicate x
+>>>>>>> dd0d05e65 (Update CHANGELOG)
   ```
 
 * Added new proofs in `Data.Vec.Functional.Properties`:

From 35c1420a48299e6675f8ad0242a5b54130889f03 Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Sun, 13 Aug 2023 21:18:26 -0400
Subject: [PATCH 05/20] Add `lookup-iterate` and update CHANGELOG

---
 CHANGELOG.md                  | 20 ++++++++++++++++----
 src/Data/List/Properties.agda |  5 +++++
 src/Data/Vec/Properties.agda  | 19 ++++++++++++++++---
 3 files changed, 37 insertions(+), 7 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 860482838e..f7074d422b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2276,6 +2276,7 @@ Additions to existing modules
   drop-map : drop n (map f xs) ≡ map f (drop n xs)
   head-map : head (map f xs) ≡ Maybe.map f (head xs)
 
+<<<<<<< HEAD
   take-suc               : take (suc m) xs ≡ take m xs ∷ʳ lookup xs i
   take-suc-tabulate      : take (suc m) (tabulate f) ≡ take m (tabulate f) ∷ʳ f i
   drop-take-suc          : drop m (take (suc m) xs) ≡ [ lookup xs i ]
@@ -2290,10 +2291,20 @@ Additions to existing modules
   map-replicate : map f (replicate n x) ≡ replicate n (f x)
 
   drop-drop : drop n (drop m xs) ≡ drop (m + n) xs
-=======
+
   take-[] : ∀ m → take  m [] ≡ []
   drop-[] : ∀ m → drop  m [] ≡ []
 
+  take-suc               : let m = toℕ i in take (suc m) xs ≡ take m xs ∷ʳ lookup xs i
+  take-suc-tabulate      : let m = toℕ i in take (suc m) (tabulate f) ≡ take m (tabulate f) ∷ʳ f i
+  drop-take-suc          : let m = toℕ i in drop m (take (suc m) xs) ≡ [ lookup xs i ]
+  drop-take-suc-tabulate : let m = toℕ i in drop m (take (suc m) (tabulate f)) ≡ [ f i ]
+
+  take-all : n ≥ length xs → take n xs ≡ xs
+
+  take-[] : take m [] ≡ []
+  drop-[] : drop m [] ≡ []
+
   lookup-replicate  : lookup (replicate n x) i ≡ x
   map-replicate     : map f (replicate n x) ≡ replicate n (f x)
   zipWith-replicate : zipWith _⊕_ (replicate n x) (replicate n y) ≡ replicate n (x ⊕ y)
@@ -2303,7 +2314,7 @@ Additions to existing modules
   iterate-id     : iterate id x n ≡ replicate n x
   take-iterate   : take n (iterate f x n) ≡ iterate f x n
   drop-iterate   : drop n (iterate f x n) ≡ []
->>>>>>> dd0d05e65 (Update CHANGELOG)
+  lookup-iterate : lookup (iterate f x n) i ≡ ℕ.iterate f x (toℕ i)
   ```
 
 * Added new patterns and definitions to `Data.Nat.Base`:
@@ -2744,11 +2755,12 @@ Additions to existing modules
 * Added new proofs in `Data.Vec.Membership.Propositional.Properties`:
   ```agda
   index-∈-fromList⁺ : Any.index (∈-fromList⁺ v∈xs) ≡ indexₗ v∈xs
-=======
 
   length-iterate : length (iterate f x {n}) ≡ n
   iterate-id     : iterate id x {n} ≡ replicate x
->>>>>>> dd0d05e65 (Update CHANGELOG)
+  take-iterate   : take n (iterate f x {n + m}) ≡ iterate f x
+  drop-iterate   : drop n (iterate f x) ≡ []
+  lookup-iterate : lookup (iterate f x) i ≡ ℕ.iterate f x (toℕ i)
   ```
 
 * Added new proofs in `Data.Vec.Functional.Properties`:
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 4a061bb28e..13e4fee1dd 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -44,6 +44,7 @@ open import Relation.Nullary using (¬_; Dec; does; _because_; yes; no; contradi
 open import Relation.Nullary.Decidable as Decidable using (isYes; map′; ⌊_⌋; ¬?; _×-dec_)
 open import Relation.Unary using (Pred; Decidable; ∁)
 open import Relation.Unary.Properties using (∁?)
+import Data.Nat.GeneralisedArithmetic as ℕ
 
 
 open ≡-Reasoning
@@ -666,6 +667,10 @@ drop-iterate : ∀ n {f} {x : A} → drop n (iterate f x n) ≡ []
 drop-iterate zero    = refl
 drop-iterate (suc n) = drop-iterate n
 
+lookup-iterate : ∀ f n (x : A) (i : Fin (length (iterate f x n))) → lookup (iterate f x n) i ≡ ℕ.iterate f x (toℕ i)
+lookup-iterate f (suc n) x zero    = refl
+lookup-iterate f (suc n) x (suc i) = lookup-iterate f n (f x) i
+
 ------------------------------------------------------------------------
 -- scanr
 
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 52b9053b17..4755ead808 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -31,6 +31,7 @@ open import Relation.Binary.PropositionalEquality
 open import Relation.Unary using (Pred; Decidable)
 open import Relation.Nullary.Decidable using (Dec; does; yes; no; _×-dec_; map′)
 open import Relation.Nullary.Negation using (contradiction)
+import Data.Nat.GeneralisedArithmetic as ℕ
 
 open ≡-Reasoning
 
@@ -1075,9 +1076,21 @@ length-iterate : ∀ n f (x : A) → length (iterate f x {n}) ≡ n
 length-iterate zero    f x = refl
 length-iterate (suc n) f x = cong suc refl
 
-iterate-id : ∀ (x : A) n → iterate id x {n} ≡ replicate x
-iterate-id x zero    = refl
-iterate-id x (suc n) = cong (_ ∷_) (iterate-id (id x) n)
+iterate-id : ∀ n (x : A) → iterate id x {n} ≡ replicate x
+iterate-id zero x    = refl
+iterate-id (suc n) x = cong (_ ∷_) (iterate-id n (id x))
+
+take-iterate : ∀ n f (x : A) → take n (iterate f x {n + m}) ≡ iterate f x
+take-iterate zero    f x = refl
+take-iterate (suc n) f x = cong (_ ∷_) (take-iterate n f (f x))
+
+drop-iterate : ∀ n f (x : A) → drop n (iterate f x) ≡ []
+drop-iterate zero    f x = refl
+drop-iterate (suc n) f x = drop-iterate n f (f x)
+
+lookup-iterate :  ∀ f (i : Fin n) (x : A) → lookup (iterate f x) i ≡ ℕ.iterate f x (toℕ i)
+lookup-iterate f zero    x = refl
+lookup-iterate f (suc i) x = lookup-iterate f i (f x)
 
 ------------------------------------------------------------------------
 -- tabulate

From 77ccad3ed2e773a76f1958d0b286455561f0a51c Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Fri, 18 Aug 2023 00:08:57 -0400
Subject: [PATCH 06/20] Add drop-all + review comments

---
 CHANGELOG.md                  |  3 ++-
 src/Data/List/Properties.agda | 24 ++++++++++++++----------
 src/Data/Vec/Properties.agda  |  6 +-----
 3 files changed, 17 insertions(+), 16 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index f7074d422b..5e7aea2fb7 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2301,6 +2301,7 @@ Additions to existing modules
   drop-take-suc-tabulate : let m = toℕ i in drop m (take (suc m) (tabulate f)) ≡ [ f i ]
 
   take-all : n ≥ length xs → take n xs ≡ xs
+  drop-all : n ≥ length xs → drop n xs ≡ []
 
   take-[] : take m [] ≡ []
   drop-[] : drop m [] ≡ []
@@ -2758,7 +2759,7 @@ Additions to existing modules
 
   length-iterate : length (iterate f x {n}) ≡ n
   iterate-id     : iterate id x {n} ≡ replicate x
-  take-iterate   : take n (iterate f x {n + m}) ≡ iterate f x
+  take-iterate   : take n (iterate f x {n + m}) ≡ iterate f x {n}
   drop-iterate   : drop n (iterate f x) ≡ []
   lookup-iterate : lookup (iterate f x) i ≡ ℕ.iterate f x (toℕ i)
   ```
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 13e4fee1dd..143c5090ea 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -626,11 +626,11 @@ sum-++ (x ∷ xs) ys = begin
 ------------------------------------------------------------------------
 -- replicate
 
-length-replicate : ∀ n {x : A} → length (replicate n x) ≡ n
-length-replicate zero    = refl
-length-replicate (suc n) = cong suc (length-replicate n)
+length-replicate : ∀ n (x : A) → length (replicate n x) ≡ n
+length-replicate zero    x = refl
+length-replicate (suc n) x = cong suc (length-replicate n x)
 
-lookup-replicate : ∀ n (x : A) (i : Fin (length (replicate n x))) → lookup (replicate n x) i ≡ x
+lookup-replicate : ∀ n (x : A) (i : Fin n) → lookup (replicate n x) (cast (sym (length-replicate n x)) i) ≡ x
 lookup-replicate (suc n) x zero    = refl
 lookup-replicate (suc n) x (suc i) = lookup-replicate n x i
 
@@ -647,9 +647,9 @@ zipWith-replicate (suc n) _⊕_ x y = cong (x ⊕ y ∷_) (zipWith-replicate n _
 ------------------------------------------------------------------------
 -- iterate
 
-length-iterate : ∀ n {f} {x : A} → length (iterate f x n) ≡ n
-length-iterate zero    = refl
-length-iterate (suc n) = cong suc (length-iterate n)
+length-iterate : ∀ n f (x : A) → length (iterate f x n) ≡ n
+length-iterate zero    f x = refl
+length-iterate (suc n) f x = cong suc (length-iterate n f (f x))
 
 toList-iterate : ∀ n {f} {x : A} → toList (Vec.iterate f x {n = n}) ≡ iterate f x n
 toList-iterate zero    = refl
@@ -667,9 +667,9 @@ drop-iterate : ∀ n {f} {x : A} → drop n (iterate f x n) ≡ []
 drop-iterate zero    = refl
 drop-iterate (suc n) = drop-iterate n
 
-lookup-iterate : ∀ f n (x : A) (i : Fin (length (iterate f x n))) → lookup (iterate f x n) i ≡ ℕ.iterate f x (toℕ i)
-lookup-iterate f (suc n) x zero    = refl
-lookup-iterate f (suc n) x (suc i) = lookup-iterate f n (f x) i
+lookup-iterate : ∀ n f (x : A) (i : Fin n) → lookup (iterate f x n) (cast (sym (length-iterate n f x)) i) ≡ ℕ.iterate f x (toℕ i)
+lookup-iterate (suc n) f x zero    = refl
+lookup-iterate (suc n) f x (suc i) = lookup-iterate n f (f x) i
 
 ------------------------------------------------------------------------
 -- scanr
@@ -877,6 +877,10 @@ drop-drop zero n xs = refl
 drop-drop (suc m) n [] = drop-[] n
 drop-drop (suc m) n (x ∷ xs) = drop-drop m n xs
 
+drop-all : (n : ℕ) (xs : List A) → n ≥ length xs → drop n xs ≡ []
+drop-all n       []       _ = drop-[] n
+drop-all (suc n) (x ∷ xs) p = drop-all n xs (≤-pred p)
+
 ------------------------------------------------------------------------
 -- splitAt
 
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 4755ead808..10c613a359 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -1072,15 +1072,11 @@ toList-replicate (suc n) x = cong (_ List.∷_) (toList-replicate n x)
 ------------------------------------------------------------------------
 -- iterate
 
-length-iterate : ∀ n f (x : A) → length (iterate f x {n}) ≡ n
-length-iterate zero    f x = refl
-length-iterate (suc n) f x = cong suc refl
-
 iterate-id : ∀ n (x : A) → iterate id x {n} ≡ replicate x
 iterate-id zero x    = refl
 iterate-id (suc n) x = cong (_ ∷_) (iterate-id n (id x))
 
-take-iterate : ∀ n f (x : A) → take n (iterate f x {n + m}) ≡ iterate f x
+take-iterate : ∀ n f (x : A) → take n (iterate f x {n + m}) ≡ iterate f x {n}
 take-iterate zero    f x = refl
 take-iterate (suc n) f x = cong (_ ∷_) (take-iterate n f (f x))
 

From a1650184e8df2b1c04cad58571f8fea9477f448d Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Fri, 18 Aug 2023 00:30:39 -0400
Subject: [PATCH 07/20] Fix tests

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

diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 143c5090ea..5b639743ad 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -626,11 +626,11 @@ sum-++ (x ∷ xs) ys = begin
 ------------------------------------------------------------------------
 -- replicate
 
-length-replicate : ∀ n (x : A) → length (replicate n x) ≡ n
-length-replicate zero    x = refl
-length-replicate (suc n) x = cong suc (length-replicate n x)
+length-replicate : ∀ n {x : A} → length (replicate n x) ≡ n
+length-replicate zero    = refl
+length-replicate (suc n) = cong suc (length-replicate n)
 
-lookup-replicate : ∀ n (x : A) (i : Fin n) → lookup (replicate n x) (cast (sym (length-replicate n x)) i) ≡ x
+lookup-replicate : ∀ n (x : A) (i : Fin n) → lookup (replicate n x) (cast (sym (length-replicate n)) i) ≡ x
 lookup-replicate (suc n) x zero    = refl
 lookup-replicate (suc n) x (suc i) = lookup-replicate n x i
 
@@ -647,11 +647,11 @@ zipWith-replicate (suc n) _⊕_ x y = cong (x ⊕ y ∷_) (zipWith-replicate n _
 ------------------------------------------------------------------------
 -- iterate
 
-length-iterate : ∀ n f (x : A) → length (iterate f x n) ≡ n
-length-iterate zero    f x = refl
-length-iterate (suc n) f x = cong suc (length-iterate n f (f x))
+length-iterate : ∀ n {f} {x : A} → length (iterate f x n) ≡ n
+length-iterate zero    = refl
+length-iterate (suc n) = cong suc (length-iterate n)
 
-toList-iterate : ∀ n {f} {x : A} → toList (Vec.iterate f x {n = n}) ≡ iterate f x n
+toList-iterate : ∀ n {f} {x : A} → toList (Vec.iterate f x {n}) ≡ iterate f x n
 toList-iterate zero    = refl
 toList-iterate (suc n) = cong (_ ∷_) (toList-iterate n)
 
@@ -667,7 +667,7 @@ drop-iterate : ∀ n {f} {x : A} → drop n (iterate f x n) ≡ []
 drop-iterate zero    = refl
 drop-iterate (suc n) = drop-iterate n
 
-lookup-iterate : ∀ n f (x : A) (i : Fin n) → lookup (iterate f x n) (cast (sym (length-iterate n f x)) i) ≡ ℕ.iterate f x (toℕ i)
+lookup-iterate : ∀ n f (x : A) (i : Fin n) → lookup (iterate f x n) (cast (sym (length-iterate n)) i) ≡ ℕ.iterate f x (toℕ i)
 lookup-iterate (suc n) f x zero    = refl
 lookup-iterate (suc n) f x (suc i) = lookup-iterate n f (f x) i
 

From 0d939436bd2c523c1fc0f87f2cb0edc1ad114b1b Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Fri, 18 Aug 2023 17:32:57 -0400
Subject: [PATCH 08/20] Move `toList-iterate` to `Vec.Properties`

---
 CHANGELOG.md                  | 15 ++++++---------
 src/Data/List/Properties.agda |  5 -----
 src/Data/Vec/Properties.agda  |  5 ++++-
 3 files changed, 10 insertions(+), 15 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 5e7aea2fb7..aa0e442cbc 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2311,7 +2311,6 @@ Additions to existing modules
   zipWith-replicate : zipWith _⊕_ (replicate n x) (replicate n y) ≡ replicate n (x ⊕ y)
 
   length-iterate : length (iterate f x n) ≡ n
-  toList-iterate : toList (Vec.iterate f x {n = n}) ≡ iterate f x n
   iterate-id     : iterate id x n ≡ replicate n x
   take-iterate   : take n (iterate f x n) ≡ iterate f x n
   drop-iterate   : drop n (iterate f x n) ≡ []
@@ -2736,8 +2735,12 @@ Additions to existing modules
   lookup-cast   : lookup (cast eq xs) (Fin.cast eq i) ≡ lookup xs i
   lookup-cast₁  : lookup (cast eq xs) i ≡ lookup xs (Fin.cast (sym eq) i)
   lookup-cast₂  : lookup xs (Fin.cast eq i) ≡ lookup (cast (sym eq) xs) i
-<<<<<<< HEAD
-  cast-reverse : cast eq ∘ reverse ≗ reverse ∘ cast eq
+
+  length-iterate : length (iterate f x {n}) ≡ n
+  iterate-id     : iterate id x {n} ≡ replicate x
+  take-iterate   : take n (iterate f x {n + m}) ≡ iterate f x {n}
+  drop-iterate   : drop n (iterate f x) ≡ []
+  lookup-iterate : lookup (iterate f x) i ≡ ℕ.iterate f x (toℕ i)
 
   zipwith-++ : zipWith f (xs ++ ys) (xs' ++ ys') ≡ zipWith f xs xs' ++ zipWith f ys ys'
 
@@ -2756,12 +2759,6 @@ Additions to existing modules
 * Added new proofs in `Data.Vec.Membership.Propositional.Properties`:
   ```agda
   index-∈-fromList⁺ : Any.index (∈-fromList⁺ v∈xs) ≡ indexₗ v∈xs
-
-  length-iterate : length (iterate f x {n}) ≡ n
-  iterate-id     : iterate id x {n} ≡ replicate x
-  take-iterate   : take n (iterate f x {n + m}) ≡ iterate f x {n}
-  drop-iterate   : drop n (iterate f x) ≡ []
-  lookup-iterate : lookup (iterate f x) i ≡ ℕ.iterate f x (toℕ i)
   ```
 
 * Added new proofs in `Data.Vec.Functional.Properties`:
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 5b639743ad..3b264cfdec 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -30,7 +30,6 @@ open import Data.Product.Base as Prod
 import Data.Product.Relation.Unary.All as Prod using (All)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Data.These.Base as These using (These; this; that; these)
-open import Data.Vec.Base as Vec using (toList)
 open import Data.Fin.Properties using (toℕ-cast)
 open import Function.Base using (id; _∘_; _∘′_; _∋_; _-⟨_∣; ∣_⟩-_; _$_; const; flip)
 open import Function.Definitions using (Injective)
@@ -651,10 +650,6 @@ length-iterate : ∀ n {f} {x : A} → length (iterate f x n) ≡ n
 length-iterate zero    = refl
 length-iterate (suc n) = cong suc (length-iterate n)
 
-toList-iterate : ∀ n {f} {x : A} → toList (Vec.iterate f x {n}) ≡ iterate f x n
-toList-iterate zero    = refl
-toList-iterate (suc n) = cong (_ ∷_) (toList-iterate n)
-
 iterate-id : ∀ n {x : A} → iterate id x n ≡ replicate n x
 iterate-id zero    = refl
 iterate-id (suc n) = cong (_ ∷_) (iterate-id n)
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 10c613a359..6736a34193 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -22,7 +22,6 @@ open import Data.Sum.Base using ([_,_]′)
 open import Data.Sum.Properties using ([,]-map)
 open import Data.Vec.Base
 open import Function.Base
--- open import Function.Inverse using (_↔_; inverse)
 open import Function.Bundles using (_↔_; mk↔′)
 open import Level using (Level)
 open import Relation.Binary.Definitions using (DecidableEquality)
@@ -1088,6 +1087,10 @@ lookup-iterate :  ∀ f (i : Fin n) (x : A) → lookup (iterate f x) i ≡ ℕ.i
 lookup-iterate f zero    x = refl
 lookup-iterate f (suc i) x = lookup-iterate f i (f x)
 
+toList-iterate : ∀ n f (x : A) → toList (iterate f x {n}) ≡ List.iterate f x n
+toList-iterate zero    f x = refl
+toList-iterate (suc n) f x = cong (_ List.∷_) (toList-iterate n f (f x))
+
 ------------------------------------------------------------------------
 -- tabulate
 

From cf26ba5c88bcb1274a0ed86266de9b47347d9d73 Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Sun, 20 Aug 2023 20:21:58 -0400
Subject: [PATCH 09/20] `iterate` now takes `n` as an explicit arg

---
 CHANGELOG.md                              | 10 ++++++++++
 src/Codata/Guarded/Stream/Properties.agda |  2 +-
 src/Data/Vec/Base.agda                    |  8 ++++----
 src/Data/Vec/Properties.agda              | 10 +++++-----
 4 files changed, 20 insertions(+), 10 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index aa0e442cbc..ddeea9337c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -910,17 +910,20 @@ Non-backwards compatible changes
     Tactic.RingSolver
     Tactic.RingSolver.Core.NatSet
     ```
+
   * Moved & renamed from `Data.Vec.Relation.Unary.All`
     to `Data.Vec.Relation.Unary.All.Properties`:
     ```
     lookup ↦ lookup⁺
     tabulate ↦ lookup⁻
     ```
+
   * Renamed in `Data.Vec.Relation.Unary.Linked.Properties`
     and `Codata.Guarded.Stream.Relation.Binary.Pointwise`:
     ```
     lookup ↦ lookup⁺
     ```
+
   * Added the following new definitions to `Data.Vec.Relation.Unary.All`:
     ```
     lookupAny : All P xs → (i : Any Q xs) → (P ∩ Q) (Any.lookup i)
@@ -928,9 +931,16 @@ Non-backwards compatible changes
     lookup : All P xs → (∀ {x} → x ∈ₚ xs → P x)
     lookupₛ : P Respects _≈_ → All P xs → (∀ {x} → x ∈ xs → P x)
     ```
+
   * `excluded-middle` in `Relation.Nullary.Decidable.Core` has been renamed to
     `¬¬-excluded-middle`.
 
+  * `iterate` in `Data.Vec.Base` now takes `n` (the length of `Vec`) as an
+    explicit argument.
+    ```agda
+    iterate : (A → A) → A → ∀ n → Vec A n
+    ```
+
 Major improvements
 ------------------
 
diff --git a/src/Codata/Guarded/Stream/Properties.agda b/src/Codata/Guarded/Stream/Properties.agda
index a07a614b59..41b19ec947 100644
--- a/src/Codata/Guarded/Stream/Properties.agda
+++ b/src/Codata/Guarded/Stream/Properties.agda
@@ -255,7 +255,7 @@ lookup-interleave-odd (suc n) as bs = lookup-interleave-odd n (as .tail) (bs .ta
 ------------------------------------------------------------------------
 -- Properties of take
 
-take-iterate : ∀ n f (x : A) → take n (iterate f x) ≡ Vec.iterate f x
+take-iterate : ∀ n f (x : A) → take n (iterate f x) ≡ Vec.iterate f x n
 take-iterate zero    f x = P.refl
 take-iterate (suc n) f x = cong (x ∷_) (take-iterate n f (f x))
 
diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda
index 6752ec1b06..8bc983684f 100644
--- a/src/Data/Vec/Base.agda
+++ b/src/Data/Vec/Base.agda
@@ -9,7 +9,7 @@
 module Data.Vec.Base where
 
 open import Data.Bool.Base using (Bool; true; false; if_then_else_)
-open import Data.Nat.Base
+open import Data.Nat.Base as N
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.List.Base as List using (List)
 open import Data.Product.Base as Prod using (∃; ∃₂; _×_; _,_; proj₁; proj₂)
@@ -60,9 +60,9 @@ lookup : Vec A n → Fin n → A
 lookup (x ∷ xs) zero    = x
 lookup (x ∷ xs) (suc i) = lookup xs i
 
-iterate : (A → A) → A → ∀ {n} → Vec A n
-iterate s z {zero}  = []
-iterate s z {suc n} = z ∷ iterate s (s z)
+iterate : (A → A) → A → ∀ n → Vec A n
+iterate s z zero    = []
+iterate s z (suc n) = z ∷ iterate s (s z) n
 
 insert : Vec A n → Fin (suc n) → A → Vec A (suc n)
 insert xs       zero     v = v ∷ xs
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 6736a34193..c9b555f62b 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -1071,23 +1071,23 @@ toList-replicate (suc n) x = cong (_ List.∷_) (toList-replicate n x)
 ------------------------------------------------------------------------
 -- iterate
 
-iterate-id : ∀ n (x : A) → iterate id x {n} ≡ replicate x
+iterate-id : ∀ n (x : A) → iterate id x n ≡ replicate x
 iterate-id zero x    = refl
 iterate-id (suc n) x = cong (_ ∷_) (iterate-id n (id x))
 
-take-iterate : ∀ n f (x : A) → take n (iterate f x {n + m}) ≡ iterate f x {n}
+take-iterate : ∀ n f (x : A) → take n (iterate f x (n + m)) ≡ iterate f x n
 take-iterate zero    f x = refl
 take-iterate (suc n) f x = cong (_ ∷_) (take-iterate n f (f x))
 
-drop-iterate : ∀ n f (x : A) → drop n (iterate f x) ≡ []
+drop-iterate : ∀ n f (x : A) → drop n (iterate f x (n + zero)) ≡ []
 drop-iterate zero    f x = refl
 drop-iterate (suc n) f x = drop-iterate n f (f x)
 
-lookup-iterate :  ∀ f (i : Fin n) (x : A) → lookup (iterate f x) i ≡ ℕ.iterate f x (toℕ i)
+lookup-iterate :  ∀ f (i : Fin n) (x : A) → lookup (iterate f x n) i ≡ ℕ.iterate f x (toℕ i)
 lookup-iterate f zero    x = refl
 lookup-iterate f (suc i) x = lookup-iterate f i (f x)
 
-toList-iterate : ∀ n f (x : A) → toList (iterate f x {n}) ≡ List.iterate f x n
+toList-iterate : ∀ n f (x : A) → toList (iterate f x n) ≡ List.iterate f x n
 toList-iterate zero    f x = refl
 toList-iterate (suc n) f x = cong (_ List.∷_) (toList-iterate n f (f x))
 

From c6ab59359bd3a6ac247e1fbf1b4d0bb4bb3ea2fa Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Thu, 14 Sep 2023 17:48:39 +0530
Subject: [PATCH 10/20] Rewrite take-iterate and drop-iterate

---
 src/Data/List/Properties.agda | 93 ++++++++++++++++++-----------------
 1 file changed, 49 insertions(+), 44 deletions(-)

diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 3b264cfdec..cba2cc31a9 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -622,50 +622,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)
 
-------------------------------------------------------------------------
--- replicate
-
-length-replicate : ∀ n {x : A} → length (replicate n x) ≡ n
-length-replicate zero    = refl
-length-replicate (suc n) = cong suc (length-replicate n)
-
-lookup-replicate : ∀ n (x : A) (i : Fin n) → lookup (replicate n x) (cast (sym (length-replicate n)) i) ≡ x
-lookup-replicate (suc n) x zero    = refl
-lookup-replicate (suc n) x (suc i) = lookup-replicate n x i
-
-map-replicate :  ∀ (f : A → B) (x : A) n →
-                 map f (replicate n x) ≡ replicate n (f x)
-map-replicate f x zero    = refl
-map-replicate f x (suc n) = cong (_ ∷_) (map-replicate f x n)
-
-zipWith-replicate : ∀ n (_⊕_ : A → B → C) (x : A) (y : B) →
-                    zipWith _⊕_ (replicate n x) (replicate n y) ≡ replicate n (x ⊕ y)
-zipWith-replicate zero    _⊕_ x y = refl
-zipWith-replicate (suc n) _⊕_ x y = cong (x ⊕ y ∷_) (zipWith-replicate n _⊕_ x y)
-
-------------------------------------------------------------------------
--- iterate
-
-length-iterate : ∀ n {f} {x : A} → length (iterate f x n) ≡ n
-length-iterate zero    = refl
-length-iterate (suc n) = cong suc (length-iterate n)
-
-iterate-id : ∀ n {x : A} → iterate id x n ≡ replicate n x
-iterate-id zero    = refl
-iterate-id (suc n) = cong (_ ∷_) (iterate-id n)
-
-take-iterate : ∀ n {f} {x : A} → take n (iterate f x n) ≡ iterate f x n
-take-iterate zero    = refl
-take-iterate (suc n) = cong (_ ∷_) (take-iterate n)
-
-drop-iterate : ∀ n {f} {x : A} → drop n (iterate f x n) ≡ []
-drop-iterate zero    = refl
-drop-iterate (suc n) = drop-iterate n
-
-lookup-iterate : ∀ n f (x : A) (i : Fin n) → lookup (iterate f x n) (cast (sym (length-iterate n)) i) ≡ ℕ.iterate f x (toℕ i)
-lookup-iterate (suc n) f x zero    = refl
-lookup-iterate (suc n) f x (suc i) = lookup-iterate n f (f x) i
-
 ------------------------------------------------------------------------
 -- scanr
 
@@ -876,6 +832,55 @@ drop-all : (n : ℕ) (xs : List A) → n ≥ length xs → drop n xs ≡ []
 drop-all n       []       _ = drop-[] n
 drop-all (suc n) (x ∷ xs) p = drop-all n xs (≤-pred p)
 
+------------------------------------------------------------------------
+-- replicate
+
+length-replicate : ∀ n {x : A} → length (replicate n x) ≡ n
+length-replicate zero    = refl
+length-replicate (suc n) = cong suc (length-replicate n)
+
+lookup-replicate : ∀ n (x : A) (i : Fin n) → lookup (replicate n x) (cast (sym (length-replicate n)) i) ≡ x
+lookup-replicate (suc n) x zero    = refl
+lookup-replicate (suc n) x (suc i) = lookup-replicate n x i
+
+map-replicate :  ∀ (f : A → B) (x : A) n →
+                 map f (replicate n x) ≡ replicate n (f x)
+map-replicate f x zero    = refl
+map-replicate f x (suc n) = cong (_ ∷_) (map-replicate f x n)
+
+zipWith-replicate : ∀ n (_⊕_ : A → B → C) (x : A) (y : B) →
+                    zipWith _⊕_ (replicate n x) (replicate n y) ≡ replicate n (x ⊕ y)
+zipWith-replicate zero    _⊕_ x y = refl
+zipWith-replicate (suc n) _⊕_ x y = cong (x ⊕ y ∷_) (zipWith-replicate n _⊕_ x y)
+
+------------------------------------------------------------------------
+-- iterate
+
+length-iterate : ∀ n {f} {x : A} → length (iterate f x n) ≡ n
+length-iterate zero    = refl
+length-iterate (suc n) = cong suc (length-iterate n)
+
+iterate-id : ∀ n {x : A} → iterate id x n ≡ replicate n x
+iterate-id zero    = refl
+iterate-id (suc n) = cong (_ ∷_) (iterate-id n)
+
+module _ n f x where
+  open import Data.List.Base
+  private
+    xs = iterate f x n
+    n≥length[xs] : n ≥ length xs
+    n≥length[xs] rewrite length-iterate n {f} {x} = ≤-refl
+    
+  take-iterate : take n xs ≡ xs
+  take-iterate = take-all n xs n≥length[xs]
+
+  drop-iterate : drop n xs ≡ []
+  drop-iterate = drop-all n xs n≥length[xs]
+
+lookup-iterate : ∀ n f (x : A) (i : Fin n) → lookup (iterate f x n) (cast (sym (length-iterate n)) i) ≡ ℕ.iterate f x (toℕ i)
+lookup-iterate (suc n) f x zero    = refl
+lookup-iterate (suc n) f x (suc i) = lookup-iterate n f (f x) i
+
 ------------------------------------------------------------------------
 -- splitAt
 

From 5dab7747dd306a3b1a21b3d905cb1da2eecc6ad9 Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Thu, 14 Sep 2023 10:59:23 +0530
Subject: [PATCH 11/20] Update CHANGELOG.md

Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
---
 CHANGELOG.md | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index ddeea9337c..31a55fa19c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2746,11 +2746,12 @@ Additions to existing modules
   lookup-cast₁  : lookup (cast eq xs) i ≡ lookup xs (Fin.cast (sym eq) i)
   lookup-cast₂  : lookup xs (Fin.cast eq i) ≡ lookup (cast (sym eq) xs) i
 
-  length-iterate : length (iterate f x {n}) ≡ n
-  iterate-id     : iterate id x {n} ≡ replicate x
-  take-iterate   : take n (iterate f x {n + m}) ≡ iterate f x {n}
-  drop-iterate   : drop n (iterate f x) ≡ []
-  lookup-iterate : lookup (iterate f x) i ≡ ℕ.iterate f x (toℕ i)
+  length-iterate : length (iterate f x n) ≡ n
+  iterate-id     : iterate id x n ≡ replicate x
+  take-iterate   : take n (iterate f x (n + m)) ≡ iterate f x n
+  drop-iterate   : drop n (iterate f x n) ≡ []
+  lookup-iterate : lookup (iterate f x n) i ≡ ℕ.iterate f x (toℕ i)
+  toList-iterate : toList (iterate f x n) ≡ List.iterate f x n
 
   zipwith-++ : zipWith f (xs ++ ys) (xs' ++ ys') ≡ zipWith f xs xs' ++ zipWith f ys ys'
 

From b7cecfdd88c36061c5da14a8de9fed1331a63b0d Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Thu, 14 Sep 2023 18:25:12 +0530
Subject: [PATCH 12/20] Fix tests

---
 src/Data/List/Properties.agda | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index cba2cc31a9..a89663f726 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -864,13 +864,12 @@ iterate-id : ∀ n {x : A} → iterate id x n ≡ replicate n x
 iterate-id zero    = refl
 iterate-id (suc n) = cong (_ ∷_) (iterate-id n)
 
-module _ n f x where
-  open import Data.List.Base
+module _ n f {x : A} where
   private
     xs = iterate f x n
     n≥length[xs] : n ≥ length xs
     n≥length[xs] rewrite length-iterate n {f} {x} = ≤-refl
-    
+
   take-iterate : take n xs ≡ xs
   take-iterate = take-all n xs n≥length[xs]
 

From fee563fbc5b7fd360baa91ffa84eb59c1c6f9c6b Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Thu, 14 Sep 2023 20:45:01 +0530
Subject: [PATCH 13/20] Order of args

---
 src/Data/List/Properties.agda |  5 +++--
 src/Data/Vec/Base.agda        |  2 +-
 src/Data/Vec/Properties.agda  | 18 +++++++++---------
 3 files changed, 13 insertions(+), 12 deletions(-)

diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index a89663f726..412f6f8dcb 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -839,7 +839,8 @@ length-replicate : ∀ n {x : A} → length (replicate n x) ≡ n
 length-replicate zero    = refl
 length-replicate (suc n) = cong suc (length-replicate n)
 
-lookup-replicate : ∀ n (x : A) (i : Fin n) → lookup (replicate n x) (cast (sym (length-replicate n)) i) ≡ x
+lookup-replicate : ∀ n (x : A) (i : Fin n) →
+                   lookup (replicate n x) (cast (sym (length-replicate n)) i) ≡ x
 lookup-replicate (suc n) x zero    = refl
 lookup-replicate (suc n) x (suc i) = lookup-replicate n x i
 
@@ -864,7 +865,7 @@ iterate-id : ∀ n {x : A} → iterate id x n ≡ replicate n x
 iterate-id zero    = refl
 iterate-id (suc n) = cong (_ ∷_) (iterate-id n)
 
-module _ n f {x : A} where
+module _ f {x : A} n where
   private
     xs = iterate f x n
     n≥length[xs] : n ≥ length xs
diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda
index 8bc983684f..bca49fb138 100644
--- a/src/Data/Vec/Base.agda
+++ b/src/Data/Vec/Base.agda
@@ -9,7 +9,7 @@
 module Data.Vec.Base where
 
 open import Data.Bool.Base using (Bool; true; false; if_then_else_)
-open import Data.Nat.Base as N
+open import Data.Nat.Base
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.List.Base as List using (List)
 open import Data.Product.Base as Prod using (∃; ∃₂; _×_; _,_; proj₁; proj₂)
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index c9b555f62b..bc97ceb2ad 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -1071,9 +1071,9 @@ toList-replicate (suc n) x = cong (_ List.∷_) (toList-replicate n x)
 ------------------------------------------------------------------------
 -- iterate
 
-iterate-id : ∀ n (x : A) → iterate id x n ≡ replicate x
-iterate-id zero x    = refl
-iterate-id (suc n) x = cong (_ ∷_) (iterate-id n (id x))
+iterate-id : ∀ (x : A) n → iterate id x n ≡ replicate x
+iterate-id x zero    = refl
+iterate-id x (suc n) = cong (_ ∷_) (iterate-id (id x) n)
 
 take-iterate : ∀ n f (x : A) → take n (iterate f x (n + m)) ≡ iterate f x n
 take-iterate zero    f x = refl
@@ -1083,13 +1083,13 @@ drop-iterate : ∀ n f (x : A) → drop n (iterate f x (n + zero)) ≡ []
 drop-iterate zero    f x = refl
 drop-iterate (suc n) f x = drop-iterate n f (f x)
 
-lookup-iterate :  ∀ f (i : Fin n) (x : A) → lookup (iterate f x n) i ≡ ℕ.iterate f x (toℕ i)
-lookup-iterate f zero    x = refl
-lookup-iterate f (suc i) x = lookup-iterate f i (f x)
+lookup-iterate :  ∀ f (x : A) (i : Fin n) → lookup (iterate f x n) i ≡ ℕ.iterate f x (toℕ i)
+lookup-iterate f x zero    = refl
+lookup-iterate f x (suc i) = lookup-iterate f (f x) i
 
-toList-iterate : ∀ n f (x : A) → toList (iterate f x n) ≡ List.iterate f x n
-toList-iterate zero    f x = refl
-toList-iterate (suc n) f x = cong (_ List.∷_) (toList-iterate n f (f x))
+toList-iterate : ∀ f (x : A) n → toList (iterate f x n) ≡ List.iterate f x n
+toList-iterate f x zero    = refl
+toList-iterate f x (suc n) = cong (_ List.∷_) (toList-iterate f (f x) n)
 
 ------------------------------------------------------------------------
 -- tabulate

From 78971ac0ac993ab6785028540e6b74b2893df403 Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Thu, 14 Sep 2023 22:01:01 +0530
Subject: [PATCH 14/20] More reordering

---
 src/Data/List/Properties.agda | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 412f6f8dcb..bdfcae178f 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -844,10 +844,10 @@ lookup-replicate : ∀ n (x : A) (i : Fin n) →
 lookup-replicate (suc n) x zero    = refl
 lookup-replicate (suc n) x (suc i) = lookup-replicate n x i
 
-map-replicate :  ∀ (f : A → B) (x : A) n →
+map-replicate :  ∀ (f : A → B) n (x : A) →
                  map f (replicate n x) ≡ replicate n (f x)
-map-replicate f x zero    = refl
-map-replicate f x (suc n) = cong (_ ∷_) (map-replicate f x n)
+map-replicate f zero    x = refl
+map-replicate f (suc n) x = cong (_ ∷_) (map-replicate f n x)
 
 zipWith-replicate : ∀ n (_⊕_ : A → B → C) (x : A) (y : B) →
                     zipWith _⊕_ (replicate n x) (replicate n y) ≡ replicate n (x ⊕ y)
@@ -861,7 +861,7 @@ length-iterate : ∀ n {f} {x : A} → length (iterate f x n) ≡ n
 length-iterate zero    = refl
 length-iterate (suc n) = cong suc (length-iterate n)
 
-iterate-id : ∀ n {x : A} → iterate id x n ≡ replicate n x
+iterate-id : ∀ {x : A} n → iterate id x n ≡ replicate n x
 iterate-id zero    = refl
 iterate-id (suc n) = cong (_ ∷_) (iterate-id n)
 
@@ -877,9 +877,9 @@ module _ f {x : A} n where
   drop-iterate : drop n xs ≡ []
   drop-iterate = drop-all n xs n≥length[xs]
 
-lookup-iterate : ∀ n f (x : A) (i : Fin n) → lookup (iterate f x n) (cast (sym (length-iterate n)) i) ≡ ℕ.iterate f x (toℕ i)
-lookup-iterate (suc n) f x zero    = refl
-lookup-iterate (suc n) f x (suc i) = lookup-iterate n f (f x) i
+lookup-iterate : ∀ f (x : A) n (i : Fin n) → lookup (iterate f x n) (cast (sym (length-iterate n)) i) ≡ ℕ.iterate f x (toℕ i)
+lookup-iterate f x (suc n) zero    = refl
+lookup-iterate f x (suc n) (suc i) = lookup-iterate f (f x) n i
 
 ------------------------------------------------------------------------
 -- splitAt

From a9f4f57a176d252d896048ca547b8f4e08ebcbcf Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Sun, 17 Sep 2023 12:21:59 +0530
Subject: [PATCH 15/20] Fix CHANGELOG

---
 CHANGELOG.md | 19 +------------------
 1 file changed, 1 insertion(+), 18 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 31a55fa19c..e2fb081be4 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2286,36 +2286,19 @@ Additions to existing modules
   drop-map : drop n (map f xs) ≡ map f (drop n xs)
   head-map : head (map f xs) ≡ Maybe.map f (head xs)
 
-<<<<<<< HEAD
   take-suc               : take (suc m) xs ≡ take m xs ∷ʳ lookup xs i
   take-suc-tabulate      : take (suc m) (tabulate f) ≡ take m (tabulate f) ∷ʳ f i
   drop-take-suc          : drop m (take (suc m) xs) ≡ [ lookup xs i ]
   drop-take-suc-tabulate : drop m (take (suc m) (tabulate f)) ≡ [ f i ]
 
   take-all : n ≥ length xs → take n xs ≡ xs
+  drop-all : n ≥ length xs → drop n xs ≡ []
 
-<<<<<<< HEAD
   take-[] : take m [] ≡ []
   drop-[] : drop m [] ≡ []
 
-  map-replicate : map f (replicate n x) ≡ replicate n (f x)
-
   drop-drop : drop n (drop m xs) ≡ drop (m + n) xs
 
-  take-[] : ∀ m → take  m [] ≡ []
-  drop-[] : ∀ m → drop  m [] ≡ []
-
-  take-suc               : let m = toℕ i in take (suc m) xs ≡ take m xs ∷ʳ lookup xs i
-  take-suc-tabulate      : let m = toℕ i in take (suc m) (tabulate f) ≡ take m (tabulate f) ∷ʳ f i
-  drop-take-suc          : let m = toℕ i in drop m (take (suc m) xs) ≡ [ lookup xs i ]
-  drop-take-suc-tabulate : let m = toℕ i in drop m (take (suc m) (tabulate f)) ≡ [ f i ]
-
-  take-all : n ≥ length xs → take n xs ≡ xs
-  drop-all : n ≥ length xs → drop n xs ≡ []
-
-  take-[] : take m [] ≡ []
-  drop-[] : drop m [] ≡ []
-
   lookup-replicate  : lookup (replicate n x) i ≡ x
   map-replicate     : map f (replicate n x) ≡ replicate n (f x)
   zipWith-replicate : zipWith _⊕_ (replicate n x) (replicate n y) ≡ replicate n (x ⊕ y)

From eb60eb10fcab3e3f5943e176a4a7fbcf697ece67 Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Sun, 17 Sep 2023 12:26:38 +0530
Subject: [PATCH 16/20] No length-iterate for Vec

---
 CHANGELOG.md | 1 -
 1 file changed, 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index e2fb081be4..560eac2906 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2729,7 +2729,6 @@ Additions to existing modules
   lookup-cast₁  : lookup (cast eq xs) i ≡ lookup xs (Fin.cast (sym eq) i)
   lookup-cast₂  : lookup xs (Fin.cast eq i) ≡ lookup (cast (sym eq) xs) i
 
-  length-iterate : length (iterate f x n) ≡ n
   iterate-id     : iterate id x n ≡ replicate x
   take-iterate   : take n (iterate f x (n + m)) ≡ iterate f x n
   drop-iterate   : drop n (iterate f x n) ≡ []

From 59061517eeaf690b7de0a873d19891d4b022c37d Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Sun, 17 Sep 2023 12:48:30 +0530
Subject: [PATCH 17/20] Cleanup

---
 CHANGELOG.md                  |  2 +-
 src/Data/List/Properties.agda | 15 ++++++---------
 src/Data/Vec/Base.agda        |  2 +-
 3 files changed, 8 insertions(+), 11 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 560eac2906..e1a5cefa74 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2307,7 +2307,7 @@ Additions to existing modules
   iterate-id     : iterate id x n ≡ replicate n x
   take-iterate   : take n (iterate f x n) ≡ iterate f x n
   drop-iterate   : drop n (iterate f x n) ≡ []
-  lookup-iterate : lookup (iterate f x n) i ≡ ℕ.iterate f x (toℕ i)
+  lookup-iterate : lookup (iterate f x n) (cast (sym (length-iterate f x n)) i) ≡ ℕ.iterate f x (toℕ i)
   ```
 
 * Added new patterns and definitions to `Data.Nat.Base`:
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index bdfcae178f..138fbc652a 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -119,10 +119,6 @@ map-injective finj {x ∷ xs} {y ∷ ys} eq =
   let fx≡fy , fxs≡fys = ∷-injective eq in
   cong₂ _∷_ (finj fx≡fy) (map-injective finj fxs≡fys)
 
-map-replicate : ∀ (f : A → B) n x → map f (replicate n x) ≡ replicate n (f x)
-map-replicate f zero    x = refl
-map-replicate f (suc n) x = cong (_ ∷_) (map-replicate f n x)
-
 ------------------------------------------------------------------------
 -- mapMaybe
 
@@ -857,9 +853,9 @@ zipWith-replicate (suc n) _⊕_ x y = cong (x ⊕ y ∷_) (zipWith-replicate n _
 ------------------------------------------------------------------------
 -- iterate
 
-length-iterate : ∀ n {f} {x : A} → length (iterate f x n) ≡ n
-length-iterate zero    = refl
-length-iterate (suc n) = cong suc (length-iterate n)
+length-iterate : ∀ f (x : A) n → length (iterate f x n) ≡ n
+length-iterate f x zero    = refl
+length-iterate f x (suc n) = cong suc (length-iterate f (f x) n)
 
 iterate-id : ∀ {x : A} n → iterate id x n ≡ replicate n x
 iterate-id zero    = refl
@@ -869,7 +865,7 @@ module _ f {x : A} n where
   private
     xs = iterate f x n
     n≥length[xs] : n ≥ length xs
-    n≥length[xs] rewrite length-iterate n {f} {x} = ≤-refl
+    n≥length[xs] rewrite length-iterate f x n = ≤-refl
 
   take-iterate : take n xs ≡ xs
   take-iterate = take-all n xs n≥length[xs]
@@ -877,7 +873,8 @@ module _ f {x : A} n where
   drop-iterate : drop n xs ≡ []
   drop-iterate = drop-all n xs n≥length[xs]
 
-lookup-iterate : ∀ f (x : A) n (i : Fin n) → lookup (iterate f x n) (cast (sym (length-iterate n)) i) ≡ ℕ.iterate f x (toℕ i)
+lookup-iterate : ∀ f (x : A) n (i : Fin n) →
+  lookup (iterate f x n) (cast (sym (length-iterate f x n)) i) ≡ ℕ.iterate f x (toℕ i)
 lookup-iterate f x (suc n) zero    = refl
 lookup-iterate f x (suc n) (suc i) = lookup-iterate f (f x) n i
 
diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda
index bca49fb138..e1bbddc919 100644
--- a/src/Data/Vec/Base.agda
+++ b/src/Data/Vec/Base.agda
@@ -272,7 +272,7 @@ drop m xs = proj₁ (proj₂ (splitAt m xs))
 group : ∀ n k (xs : Vec A (n * k)) →
         ∃ λ (xss : Vec (Vec A k) n) → xs ≡ concat xss
 group zero    k []                  = ([] , refl)
-group (suc n) k xs  = 
+group (suc n) k xs  =
   let ys , zs , eq-split = splitAt k xs in
   let zss , eq-group     = group n k zs in
    (ys ∷ zss) , trans eq-split (cong (ys ++_) eq-group)

From 4bea1410d7bf9d041c8c8d2a9810094975c04240 Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Sun, 17 Sep 2023 12:50:55 +0530
Subject: [PATCH 18/20] Clean CHANGELOG

---
 CHANGELOG.md | 16 +---------------
 1 file changed, 1 insertion(+), 15 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index e1a5cefa74..bb8d04a185 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2193,7 +2193,7 @@ Additions to existing modules
   gcd-zero  : Zero 1ℤ gcd
   ```
 
-* Added new functions in `Data.List`:
+* Added new functions and definitions to `Data.List.Base`:
   ```agda
   takeWhileᵇ   : (A → Bool) → List A → List A
   dropWhileᵇ   : (A → Bool) → List A → List A
@@ -2212,20 +2212,6 @@ Additions to existing modules
   find         : Decidable P → List A → Maybe A
   findIndex    : Decidable P → (xs : List A) → Maybe $ Fin (length xs)
   findIndices  : Decidable P → (xs : List A) → List $ Fin (length xs)
-  ```
-
-* Added new functions and definitions to `Data.List.Base`:
-  ```agda
-  takeWhileᵇ   : (A → Bool) → List A → List A
-  dropWhileᵇ   : (A → Bool) → List A → List A
-  filterᵇ      : (A → Bool) → List A → List A
-  partitionᵇ   : (A → Bool) → List A → List A × List A
-  spanᵇ        : (A → Bool) → List A → List A × List A
-  breakᵇ       : (A → Bool) → List A → List A × List A
-  linesByᵇ     : (A → Bool) → List A → List (List A)
-  wordsByᵇ     : (A → Bool) → List A → List (List A)
-  derunᵇ       : (A → A → Bool) → List A → List A
-  deduplicateᵇ : (A → A → Bool) → List A → List A
 
   catMaybes       : List (Maybe A) → List A
   ap              : List (A → B) → List A → List B

From c8301f25f2a2cc8eaa1ca134039a4870864e4246 Mon Sep 17 00:00:00 2001
From: MatthewDaggitt <matthewdaggitt@gmail.com>
Date: Wed, 4 Oct 2023 17:43:16 +0900
Subject: [PATCH 19/20] Remove derivative take-iterate and drop-iterate

---
 src/Data/List/Properties.agda | 18 +++---------------
 1 file changed, 3 insertions(+), 15 deletions(-)

diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 84766d7f42..5afce0cd54 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -881,21 +881,9 @@ length-iterate : ∀ f (x : A) n → length (iterate f x n) ≡ n
 length-iterate f x zero    = refl
 length-iterate f x (suc n) = cong suc (length-iterate f (f x) n)
 
-iterate-id : ∀ {x : A} n → iterate id x n ≡ replicate n x
-iterate-id zero    = refl
-iterate-id (suc n) = cong (_ ∷_) (iterate-id n)
-
-module _ f {x : A} n where
-  private
-    xs = iterate f x n
-    n≥length[xs] : n ≥ length xs
-    n≥length[xs] rewrite length-iterate f x n = ≤-refl
-
-  take-iterate : take n xs ≡ xs
-  take-iterate = take-all n xs n≥length[xs]
-
-  drop-iterate : drop n xs ≡ []
-  drop-iterate = drop-all n xs n≥length[xs]
+iterate-id : ∀ (x : A) n → iterate id x n ≡ replicate n x
+iterate-id x zero    = refl
+iterate-id x (suc n) = cong (_ ∷_) (iterate-id x n)
 
 lookup-iterate : ∀ f (x : A) n (i : Fin n) →
   lookup (iterate f x n) (cast (sym (length-iterate f x n)) i) ≡ ℕ.iterate f x (toℕ i)

From b490a5dfd39ab1faceca0074c9fcb7efe80b194d Mon Sep 17 00:00:00 2001
From: MatthewDaggitt <matthewdaggitt@gmail.com>
Date: Wed, 4 Oct 2023 17:44:10 +0900
Subject: [PATCH 20/20] Updated CHANGELOG

---
 CHANGELOG.md | 2 --
 1 file changed, 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 0c93ad315a..c9118a5b4d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2525,8 +2525,6 @@ Additions to existing modules
 
   length-iterate : length (iterate f x n) ≡ n
   iterate-id     : iterate id x n ≡ replicate n x
-  take-iterate   : take n (iterate f x n) ≡ iterate f x n
-  drop-iterate   : drop n (iterate f x n) ≡ []
   lookup-iterate : lookup (iterate f x n) (cast (sym (length-iterate f x n)) i) ≡ ℕ.iterate f x (toℕ i)
 
   length-insertAt   : length (insertAt xs i v) ≡ suc (length xs)