Sync iterate and replicate for List and Vec

CHANGELOG.md

@@ -910,27 +910,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
 ------------------
 
@@ -2183,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
@@ -2202,14 +2212,13 @@ 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
- catMaybes : List (Maybe A) → List A
- ap : List (A → B) → List A → List B
- ++-rawMagma : Set a → RawMagma 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`:
@@ -2269,13 +2278,22 @@ 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
+ 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)
  ```
 
 * Added new patterns and definitions to `Data.Nat.Base`:
@@ -2696,7 +2714,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
- 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'
 

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
 
@@ -834,6 +824,60 @@ 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 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]
+
+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
 
 insert : Vec A n → Fin (suc n) → A → Vec A (suc n)
 insert xs zero v = v ∷ xs
@@ -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)

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)
@@ -31,6 +30,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
 
@@ -1068,6 +1068,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