Sync iterate and replicate for List and Vec (#2051)

CHANGELOG.md

@@ -1058,27 +1058,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
 ------------------
 
@@ -2441,7 +2451,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
@@ -2466,6 +2476,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
  ```
@@ -2527,14 +2538,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
@@ -2964,6 +2982,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