[ refactor ] Stream's iterate

CHANGELOG.md

@@ -134,6 +134,7 @@ Other minor additions
 * Added new proof to `Codata.Stream.Properties`:
   ```agda
   splitAt-map : splitAt n (map f xs) ≡ map (map f) (map f) (splitAt n xs)
+  lookup-iterate-identity : lookup n (iterate f a) ≡ fold a f n
   ```
 
 * Added new function to `Data.Fin.Base`:

src/Codata/Stream.agda

@@ -93,12 +93,10 @@ module _ {ℓ ℓ₁ ℓ₂} {A : Set ℓ} {B : Set ℓ₁} {C : Set ℓ₂} whe
  zipWith : ∀ {i} → (A → B → C) → Stream A i → Stream B i → Stream C i
  zipWith f (a ∷ as) (b ∷ bs) = f a b ∷ λ where .force → zipWith f (as .force) (bs .force)
 
-module _ {ℓ} {A : Set ℓ} where
-
- iterate : ∀ {i} → (A → A) → A → Stream A i
- iterate f a = a ∷ λ where .force → map f (iterate f a)
-
+module _ {a} {A : Set a} where
 
+  iterate : (A → A) → A → Stream A ∞
+  iterate f = unfold < f , id >
 
 ------------------------------------------------------------------------
 -- Legacy

src/Codata/Stream/Properties.agda

@@ -12,13 +12,18 @@ open import Codata.Stream
 open import Codata.Stream.Bisimilarity
 
 open import Data.Nat.Base
+open import Data.Nat.GeneralisedArithmetic using (fold; fold-pull)
+
 import Data.Vec as Vec
 import Data.Product as Prod
 
 open import Function
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
 
-module _ {a b} {A : Set a} {B : Set b} where
+------------------------------------------------------------------------
+-- repeat
+
+module _ {a} {A : Set a} where
 
  lookup-repeat-identity : (n : ℕ) (a : A) → lookup n (repeat a) ≡ a
  lookup-repeat-identity zero    a = Eq.refl
@@ -67,3 +72,17 @@ module _ {a b} {A : Set a} {B : Set b} where
   splitAt-map zero    f xs       = Eq.refl
   splitAt-map (suc n) f (x ∷ xs) =
     Eq.cong (Prod.map₁ (f x Vec.∷_)) (splitAt-map n f (xs .force))
+
+------------------------------------------------------------------------
+-- iterate
+
+module _ {a} {A : Set a} where
+
+  lookup-iterate-identity : ∀ n f (a : A) → lookup n (iterate f a) ≡ fold a f n
+  lookup-iterate-identity zero     f a = Eq.refl
+  lookup-iterate-identity (suc n)  f a = begin
+    lookup (suc n) (iterate f a) ≡⟨⟩
+    lookup n (iterate f (f a))   ≡⟨ lookup-iterate-identity n f (f a) ⟩
+    fold (f a) f n               ≡⟨ fold-pull (const ∘′ f) (f a) Eq.refl (λ _ → Eq.refl) n ⟩
+    f (fold a f n)               ≡⟨⟩
+    fold a f (suc n)             ∎ where open Eq.≡-Reasoning