Sync iterate and replicate for List and Vec

CHANGELOG.md

@@ -1032,27 +1032,37 @@ 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)
     lookupWith : ∀[ P ⇒ Q ⇒ R ] → All P xs → (i : Any Q xs) → R (Any.lookup i)
     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
 ------------------
 
@@ -2415,7 +2425,7 @@ Additions to existing modules
   gcd-zero  : Zero 1ℤ gcd
   ```
 
-* Added new functions in `Data.List.Base`:
+* Added new functions and definitions to `Data.List.Base`:
   ```agda
   takeWhileᵇ   : (A → Bool) → List A → List A
   dropWhileᵇ   : (A → Bool) → List A → List A
@@ -2440,6 +2450,7 @@ Additions to existing modules
   ++-rawMagma     : Set a → RawMagma a _
   ++-[]-rawMonoid : Set a → RawMonoid a _
 
+  iterate : (A → A) → A → ℕ → List A
   insertAt : (xs : List A) → Fin (suc (length xs)) → A → List A
   updateAt : (xs : List A) → Fin (length xs) → (A → A) → List A
   ```
@@ -2501,14 +2512,21 @@ Additions to existing modules
   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 ≡ []
 
   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
 
+  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
+  iterate-id     : iterate id x n ≡ replicate n x
+  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)
   length-removeAt′  : length xs ≡ suc (length (removeAt xs k))
   removeAt-insertAt : removeAt (insertAt xs i v) ((cast (sym (length-insertAt xs i v)) i)) ≡ xs
@@ -2936,6 +2954,12 @@ Additions to existing modules
   lookup-cast₂  : lookup xs (Fin.cast eq i) ≡ lookup (cast (sym eq) xs) i
   cast-reverse  : cast eq ∘ reverse ≗ reverse ∘ cast eq
 
+  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'
 
   ++-assoc     : cast eq ((xs ++ ys) ++ zs) ≡ xs ++ (ys ++ zs)

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))
 

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 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)

src/Data/List/Properties.agda

@@ -43,6 +43,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
@@ -118,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
 
@@ -621,13 +618,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)
-
 ------------------------------------------------------------------------
 -- scanr
 
@@ -858,6 +848,48 @@ 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)
+
+------------------------------------------------------------------------
+-- 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) n (x : A) →
+                 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)
+
+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 : ∀ 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 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)
+lookup-iterate f x (suc n) zero    = refl
+lookup-iterate f x (suc n) (suc i) = lookup-iterate f (f x) n i
+
 ------------------------------------------------------------------------
 -- splitAt
 

src/Data/Vec/Base.agda

@@ -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
 
 insertAt : Vec A n → Fin (suc n) → A → Vec A (suc n)
 insertAt xs       zero     v = v ∷ xs

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.Core using (Dec; does; yes; no; _×-dec_; map′)
 open import Relation.Nullary.Negation.Core using (contradiction)
+import Data.Nat.GeneralisedArithmetic as ℕ
 
 open ≡-Reasoning
 
@@ -1098,6 +1099,29 @@ toList-replicate : ∀ (n : ℕ) (x : A) →
 toList-replicate zero    x = refl
 toList-replicate (suc n) x = cong (_ List.∷_) (toList-replicate n x)
 
+------------------------------------------------------------------------
+-- iterate
+
+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
+take-iterate (suc n) f x = cong (_ ∷_) (take-iterate n f (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 (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 : ∀ 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