```------------------------------------------------------------------------
-- An ad-hoc but straightforward solution to the problem of showing
-- that elegant definitions of the Hamming numbers (see EWD 792) and
-- the Fibonacci sequence are productive
------------------------------------------------------------------------

module StreamProg where

open import Coinduction
import Stream as S
open S using (Stream; _≺_; _≈_; Ord; lt; eq; gt)
open import Data.Nat
open import Relation.Binary
private
module SS {A} = Setoid (S.setoid A)
import IO

------------------------------------------------------------------------
-- Stream programs

infixr 5 _≺_

data Prog (A : Set) : Set1 where
_≺_     : (x : A) (xs : ∞₁ (Prog A)) → Prog A
zipWith : ∀ {B C} (f : B → C → A)
(xs : Prog B) (ys : Prog C) → Prog A
map     : ∀ {B} (f : B → A) (xs : Prog B) → Prog A
merge   : (cmp : A → A → Ord)
(xs : Prog A) (ys : Prog A) → Prog A

data WHNF A : Set1 where
_≺_ : (x : A) (xs : Prog A) → WHNF A

whnf : ∀ {A} → Prog A → WHNF A
whnf (x ≺ xs)          = x ≺ ♭₁ xs
whnf (zipWith f xs ys) with whnf xs | whnf ys
whnf (zipWith f xs ys) | x ≺ xs′ | y ≺ ys′ = f x y ≺ zipWith f xs′ ys′
whnf (map f xs)        with whnf xs
whnf (map f xs)        | x ≺ xs′ = f x ≺ map f xs′
whnf (merge cmp xs ys) with whnf xs | whnf ys
whnf (merge cmp xs ys) | x ≺ xs′ | y ≺ ys′ with cmp x y
whnf (merge cmp xs ys) | x ≺ xs′ | y ≺ ys′ | lt = x ≺ merge cmp xs′ (y ≺ ♯₁ ys′)
whnf (merge cmp xs ys) | x ≺ xs′ | y ≺ ys′ | eq = x ≺ merge cmp xs′ ys′
whnf (merge cmp xs ys) | x ≺ xs′ | y ≺ ys′ | gt = y ≺ merge cmp (x ≺ ♯₁ xs′) ys′

mutual

value : ∀ {A} → WHNF A → Stream A
value (x ≺ xs) = x ≺ ♯ ⟦ xs ⟧

⟦_⟧ : ∀ {A} → Prog A → Stream A
⟦ xs ⟧ = value (whnf xs)

------------------------------------------------------------------------
-- Examples

fib : Prog ℕ
fib = 0 ≺ ♯₁ zipWith _+_ fib (1 ≺ ♯₁ fib)

cmp : ℕ → ℕ → Ord
cmp m n = toOrd (compare m n)
where
toOrd : ∀ {m n} → Ordering m n → Ord
toOrd (less _ _)    = lt
toOrd (equal _)     = eq
toOrd (greater _ _) = gt

hamming : Prog ℕ
hamming = 1 ≺ ♯₁ merge cmp (map (_*_ 2) hamming) (map (_*_ 3) hamming)

main = IO.run (S.putStream (S._⋎_ ⟦ fib ⟧ ⟦ hamming ⟧))

------------------------------------------------------------------------
-- The definition of fib is correct

-- ⟦_⟧ is homomorphic with respect to zipWith/S.zipWith.

zipWith-hom : ∀ {A B C} (_∙_ : A → B → C) xs ys →
⟦ zipWith _∙_ xs ys ⟧ ≈ S.zipWith _∙_ ⟦ xs ⟧ ⟦ ys ⟧
zipWith-hom _∙_ xs ys with whnf xs | whnf ys
zipWith-hom _∙_ xs ys | x ≺ xs′ | y ≺ ys′ =
(x ∙ y) ≺ ♯ zipWith-hom _∙_ xs′ ys′

-- S.zipWith is a congruence.

zipWith-cong : ∀ {A B C} (_∙_ : A → B → C) {xs xs′ ys ys′} →
xs ≈ xs′ → ys ≈ ys′ →
S.zipWith _∙_ xs ys ≈ S.zipWith _∙_ xs′ ys′
zipWith-cong _∙_ (x ≺ xs≈) (y ≺ ys≈) =
(x ∙ y) ≺ ♯ zipWith-cong _∙_ (♭ xs≈) (♭ ys≈)

-- Unfortunately Agda's definitional equality for coinductive
-- constructors is currently a little strange, so the result type
-- cannot be written out completely here:

fib-correct′ :
⟦ fib ⟧ ≈ 0 ≺ ♯ S.zipWith _+_ ⟦ fib ⟧ (1 ≺ _ {- ♯ ⟦ fib ⟧ -})
fib-correct′ = 0 ≺ ♯ zipWith-hom _+_ fib (1 ≺ ♯₁ fib)

-- Fortunately there is a workaround.

fib-correct : ⟦ fib ⟧ ≈ 0 ≺ ♯ S.zipWith _+_ ⟦ fib ⟧ (1 ≺ ♯ ⟦ fib ⟧)
fib-correct =
0 ≺ ♯ SS.trans (zipWith-hom  _+_ fib     (1 ≺ ♯₁ fib))
(zipWith-cong _+_ SS.refl (1 ≺ ♯ SS.refl))

------------------------------------------------------------------------
-- The definition of hamming is correct

-- ⟦_⟧ is homomorphic with respect to map/S.map.

map-hom : ∀ {A B} (f : A → B) xs →
⟦ map f xs ⟧ ≈ S.map f ⟦ xs ⟧
map-hom f xs with whnf xs
... | x ≺ xs′ = f x ≺ ♯ map-hom f xs′

-- ⟦_⟧ is homomorphic with respect to merge/S.merge.

merge-hom : ∀ {A} (cmp : A → A → Ord) xs ys →
⟦ merge cmp xs ys ⟧ ≈ S.merge cmp ⟦ xs ⟧ ⟦ ys ⟧
merge-hom cmp xs ys with whnf xs | whnf ys
... | x ≺ xs′ | y ≺ ys′ with cmp x y
...   | lt = x ≺ ♯ merge-hom cmp xs′ _
...   | eq = x ≺ ♯ merge-hom cmp xs′ ys′
...   | gt = y ≺ ♯ merge-hom cmp _ ys′

-- S.merge is a congruence.

merge-cong : ∀ {A} (cmp : A → A → Ord) {xs xs′ ys ys′} →
xs ≈ xs′ → ys ≈ ys′ →
S.merge cmp xs ys ≈ S.merge cmp xs′ ys′
merge-cong cmp (x ≺ xs≈) (y ≺ ys≈) with cmp x y
... | lt = x ≺ ♯ merge-cong cmp (♭ xs≈) (y ≺ ys≈)
... | eq = x ≺ ♯ merge-cong cmp (♭ xs≈) (♭ ys≈)
... | gt = y ≺ ♯ merge-cong cmp (x ≺ xs≈) (♭ ys≈)

-- hamming is correct.

hamming-correct : ⟦ hamming ⟧ ≈
1 ≺ ♯ S.merge cmp (S.map (_*_ 2) ⟦ hamming ⟧)
(S.map (_*_ 3) ⟦ hamming ⟧)
hamming-correct =
1 ≺ ♯ SS.trans (merge-hom cmp (map (_*_ 2) hamming)
(map (_*_ 3) hamming))
(merge-cong cmp (map-hom (_*_ 2) hamming)
(map-hom (_*_ 3) hamming))
```