```------------------------------------------------------------------------
-- 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
open import Data.Nat
open import Data.Stream as S using (Stream; _∷_; _≈_)
open import Relation.Binary
import Relation.Binary.PropositionalEquality as P

private
module SS {A : Set} = Setoid (S.setoid A)

------------------------------------------------------------------------
-- Merging of streams

data Ord : Set where
lt : Ord
eq : Ord
gt : Ord

merge : {A : Set} → (A → A → Ord) → Stream A → Stream A → Stream A
merge cmp (x ∷ xs) (y ∷ ys) with cmp x y
... | lt = x ∷ ♯ merge cmp (♭ xs)   (y ∷ ys)
... | eq = x ∷ ♯ merge cmp (♭ xs)   (♭ ys)
... | gt = y ∷ ♯ merge cmp (x ∷ xs) (♭ ys)

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

infixr 5 _∷_

data StreamP (A : Set) : Set1 where
_∷_     : (x : A) (xs : ∞ (StreamP A)) → StreamP A
zipWith : ∀ {B C} (f : B → C → A)
(xs : StreamP B) (ys : StreamP C) → StreamP A
map     : ∀ {B} (f : B → A) (xs : StreamP B) → StreamP A
mergeP  : (cmp : A → A → Ord)
(xs : StreamP A) (ys : StreamP A) → StreamP A

data StreamW A : Set1 where
_∷_ : (x : A) (xs : StreamP A) → StreamW A

zipWithW : {A B C : Set} →
(A → B → C) → StreamW A → StreamW B → StreamW C
zipWithW f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWith f xs ys

mapW : {A B : Set} → (A → B) → StreamW A → StreamW B
mapW f (x ∷ xs) = f x ∷ map f xs

mergeW : {A : Set} →
(A → A → Ord) → StreamW A → StreamW A → StreamW A
mergeW cmp (x ∷ xs) (y ∷ ys) with cmp x y
... | lt = x ∷ mergeP cmp xs (y ∷ ♯ ys)
... | eq = x ∷ mergeP cmp xs ys
... | gt = y ∷ mergeP cmp (x ∷ ♯ xs) ys

whnf : ∀ {A} → StreamP A → StreamW A
whnf (x ∷ xs)           = x ∷ ♭ xs
whnf (zipWith f xs ys)  = zipWithW f (whnf xs) (whnf ys)
whnf (map f xs)         = mapW f (whnf xs)
whnf (mergeP cmp xs ys) = mergeW cmp (whnf xs) (whnf ys)

mutual

⟦_⟧W : ∀ {A} → StreamW A → Stream A
⟦ x ∷ xs ⟧W = x ∷ ♯ ⟦ xs ⟧P

⟦_⟧P : ∀ {A} → StreamP A → Stream A
⟦ xs ⟧P = ⟦ whnf xs ⟧W

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

fib : StreamP ℕ
fib = 0 ∷ ♯ zipWith _+_ fib (1 ∷ ♯ fib)

-- Alternative definition showing that definitions do not need to

fib′ : StreamP ℕ
fib′ = zipWith _+_ (0 ∷ ♯ fib′) (0 ∷ ♯ (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 : StreamP ℕ
hamming = 1 ∷ ♯ mergeP cmp (map (_*_ 2) hamming) (map (_*_ 3) hamming)

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

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

zipWith-hom : ∀ {A B C} (_∙_ : A → B → C) xs ys →
⟦ zipWith _∙_ xs ys ⟧P ≈ S.zipWith _∙_ ⟦ xs ⟧P ⟦ ys ⟧P
zipWith-hom _∙_ xs ys with whnf xs | whnf ys
zipWith-hom _∙_ xs ys | x ∷ xs′ | y ∷ ys′ =
P.refl ∷ ♯ zipWith-hom _∙_ 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 ⟧P ≈ 0 ∷ ♯ S.zipWith _+_ ⟦ fib ⟧P (1 ∷ _ {- ♯ ⟦ fib ⟧P -})
fib-correct′ = P.refl ∷ ♯ zipWith-hom _+_ fib (1 ∷ ♯ fib)

-- Fortunately there is a workaround.

fib-correct : ⟦ fib ⟧P ≈ 0 ∷ ♯ S.zipWith _+_ ⟦ fib ⟧P (1 ∷ ♯ ⟦ fib ⟧P)
fib-correct =
P.refl ∷ ♯ SS.trans (zipWith-hom _+_ fib (1 ∷ ♯ fib))
(S.zipWith-cong _+_ (SS.refl {x = 0 ∷ _})
(P.refl ∷ ♯ SS.refl))

-- For a proof showing that the given equation for fib has a unique
-- solution, see MapIterate.

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

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

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

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

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

-- merge is a congruence.

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

-- hamming is correct.

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