------------------------------------------------------------------------
-- Nested applications of the defined function can be handled
------------------------------------------------------------------------

module Nested where

open import Coinduction
open import Data.Stream
open import Function
import Relation.Binary.PropositionalEquality as P

------------------------------------------------------------------------
-- A definition of φ (x ∷ xs) = x ∷ φ (φ xs)

module φ where

infixr 5 _∷_

data StreamP (A : Set) : Set where
_∷_ : (x : A) (xs :  (StreamP A))  StreamP A
φP  : (xs : StreamP A)  StreamP A

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

φW  : {A : Set}  StreamW A  StreamW A
φW (x  xs) = x  φP (φP xs)

whnf : {A : Set}  StreamP A  StreamW A
whnf (x  xs)   = x   xs
whnf (φP xs)    = φW (whnf xs)

mutual

⟦_⟧W : {A : Set}  StreamW A  Stream A
x  xs ⟧W = x    xs ⟧P

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

⌈_⌉ : {A : Set}  Stream A  StreamP A
x  xs  = x     xs

φ : {A : Set}  Stream A  Stream A
φ xs =  φP  xs  ⟧P

open φ using (⟦_⟧P; ⟦_⟧W; φP; φW; φ; _∷_; ⌈_⌉)

------------------------------------------------------------------------
-- An equality proof language

module Equality where

φ-rhs : {A : Set}  (Stream A  Stream A)  Stream A  Stream A
φ-rhs φ (x  xs) = x   φ (φ ( xs))

SatisfiesEquation : {A : Set}  (Stream A  Stream A)  Set
SatisfiesEquation φ =  xs  φ xs  φ-rhs φ xs

infixr 5 _∷_
infix  4 _≈P_ _≈W_
infix  3 _∎
infixr 2 _≈⟨_⟩_

data _≈P_ {A : Set} : Stream A  Stream A  Set where
_∷_     :  (x : A) {xs ys}
(xs≈ys :  ( xs ≈P  ys))  x  xs ≈P x  ys
_≈⟨_⟩_  :  (xs : Stream A) {ys zs}
(xs≈ys : xs ≈P ys) (ys≈zs : ys ≈P zs)  xs ≈P zs
_∎      : (xs : Stream A)  xs ≈P xs
sym     :  {xs ys} (xs≈ys : xs ≈P ys)  ys ≈P xs
φP-cong : (xs ys : φ.StreamP A) (xs≈ys :  xs ⟧P ≈P  ys ⟧P)
φP xs ⟧P ≈P  φP ys ⟧P
lemma   : (φ₁ φ₂ : Stream A  Stream A)
(s₁ : SatisfiesEquation φ₁) (s₂ : SatisfiesEquation φ₂)
{xs ys} (xs≈ys : xs ≈P ys)  φ-rhs φ₁ xs ≈P φ-rhs φ₂ ys

-- Completeness.

completeP : {A : Set} {xs ys : Stream A}  xs  ys  xs ≈P ys
completeP (P.refl  xs≈ys) = _   completeP ( xs≈ys)

data _≈W_ {A : Set} : Stream A  Stream A  Set where
_∷_ :  x {xs ys} (xs≈ys :  xs ≈P  ys)  x  xs ≈W x  ys

transW : {A : Set} {xs ys zs : Stream A}
xs ≈W ys  ys ≈W zs  xs ≈W zs
transW (x  xs≈ys) (.x  ys≈zs) = x  (_ ≈⟨ xs≈ys  ys≈zs)

reflW : {A : Set} (xs : Stream A)  xs ≈W xs
reflW (x  xs) = x  ( xs )

symW : {A : Set} {xs ys : Stream A}  xs ≈W ys  ys ≈W xs
symW (x  xs≈ys) = x  sym xs≈ys

φW-cong : {A : Set} (xs ys : φ.StreamW A)
xs ⟧W ≈W  ys ⟧W   φW xs ⟧W ≈W  φW ys ⟧W
φW-cong (.x  xs) (.x  ys) (x  xs≈ys) =
x  φP-cong (φP xs) (φP ys) (φP-cong xs ys xs≈ys)

lemmaW : {A : Set} (φ₁ φ₂ : Stream A  Stream A)
(s₁ : SatisfiesEquation φ₁) (s₂ : SatisfiesEquation φ₂)
{xs ys}  xs ≈W ys  φ-rhs φ₁ xs ≈W φ-rhs φ₂ ys
lemmaW φ₁ φ₂ s₁ s₂ {.x  xs} {.x  ys} (x  xs≈ys) = x  (
φ₁ (φ₁ ( xs))        ≈⟨ completeP \$ s₁ (φ₁ ( xs))
φ-rhs φ₁ (φ₁ ( xs))  ≈⟨ lemma φ₁ φ₂ s₁ s₂ (
φ₁ ( xs)                ≈⟨ completeP \$ s₁ ( xs)
φ-rhs φ₁ ( xs)          ≈⟨ lemma φ₁ φ₂ s₁ s₂ xs≈ys
φ-rhs φ₂ ( ys)          ≈⟨ sym \$ completeP \$ s₂ ( ys)
φ₂ ( ys)                )
φ-rhs φ₂ (φ₂ ( ys))  ≈⟨ sym \$ completeP \$ s₂ (φ₂ ( ys))
φ₂ (φ₂ ( ys))        )

whnf : {A : Set} {xs ys : Stream A}  xs ≈P ys  xs ≈W ys
whnf (x  xs≈ys)               = x   xs≈ys
whnf (xs ≈⟨ xs≈ys  ys≈zs)     = transW (whnf xs≈ys) (whnf ys≈zs)
whnf (xs )                    = reflW xs
whnf (sym xs≈ys)               = symW (whnf xs≈ys)
whnf (lemma φ₁ φ₂ s₁ s₂ xs≈ys) = lemmaW φ₁ φ₂ s₁ s₂ (whnf xs≈ys)
whnf (φP-cong xs ys xs≈ys)     =
φW-cong (φ.whnf xs) (φ.whnf ys) (whnf xs≈ys)

-- Soundness.

mutual

soundW : {A : Set} {xs ys : Stream A}  xs ≈W ys  xs  ys
soundW (x  xs≈ys) = P.refl   soundP xs≈ys

soundP : {A : Set} {xs ys : Stream A}  xs ≈P ys  xs  ys
soundP xs≈ys = soundW (whnf xs≈ys)

open Equality
using (_≈P_; _∷_; _≈⟨_⟩_; _∎; sym; φP-cong; φ-rhs; SatisfiesEquation)

------------------------------------------------------------------------
-- Correctness

module Correctness where

-- Uniqueness of solutions for φ's defining equation.

φ-unique : {A : Set} (φ₁ φ₂ : Stream A  Stream A)
SatisfiesEquation φ₁  SatisfiesEquation φ₂
xs  φ₁ xs ≈P φ₂ xs
φ-unique φ₁ φ₂ hyp₁ hyp₂ xs =
φ₁ xs        ≈⟨ Equality.completeP (hyp₁ xs)
φ-rhs φ₁ xs  ≈⟨ Equality.lemma φ₁ φ₂ hyp₁ hyp₂ (xs )
φ-rhs φ₂ xs  ≈⟨ sym (Equality.completeP (hyp₂ xs))
φ₂ xs

-- The remainder of this module establishes the existence of a
-- solution.

⟦⌈_⌉⟧P : {A : Set} (xs : Stream A)    xs  ⟧P ≈P xs
⟦⌈ x  xs ⌉⟧P = x   ⟦⌈  xs ⌉⟧P

φ-cong : {A : Set} (xs ys : Stream A)  xs ≈P ys  φ xs ≈P φ ys
φ-cong xs ys xs≈ys =
φ xs            ≈⟨ φ xs
φP  xs  ⟧P  ≈⟨ φP-cong  xs   ys  lemma
φP  ys  ⟧P  ≈⟨ φ ys
φ ys
where
lemma =
xs  ⟧P  ≈⟨ ⟦⌈ xs ⌉⟧P
xs           ≈⟨ xs≈ys
ys           ≈⟨ sym ⟦⌈ ys ⌉⟧P
ys  ⟧P

-- ♯′ provides a workaround for Agda's strange definitional
-- equality.

infix 10 ♯′_

♯′_ : {A : Set}  A   A
♯′ x =  x

φW-hom : {A : Set} (xs : φ.StreamW A)
φW xs ⟧W ≈P head  xs ⟧W  ♯′ φ (φ (tail  xs ⟧W))
φW-hom (x  xs) = x   (
φP (φP xs) ⟧P                  ≈⟨ φP-cong (φP xs) (φP   xs ⟧P ) \$
φP-cong xs (  xs ⟧P )
(sym ⟦⌈  xs ⟧P ⌉⟧P)
φP (φP   xs ⟧P ) ⟧P         ≈⟨ φP-cong (φP   xs ⟧P )
φP   xs ⟧P  ⟧P
(sym ⟦⌈  φP   xs ⟧P  ⟧P ⌉⟧P)
φP   φP   xs ⟧P  ⟧P  ⟧P  )

φ-hom : {A : Set} (xs : φ.StreamP A)
φP xs ⟧P ≈P head  xs ⟧P  ♯′ φ (φ (tail  xs ⟧P))
φ-hom xs = φW-hom (φ.whnf xs)

φ-correct : {A : Set} (xs : Stream A)
φ xs ≈P φ-rhs φ xs
φ-correct (x  xs) =
φ (x  xs)                  ≈⟨ φ (x  xs)
φP  x  xs  ⟧P          ≈⟨ φ-hom  x  xs
x  ♯′ φ (φ    xs  ⟧P)  ≈⟨ x   φ-cong (φ    xs  ⟧P) (φ ( xs))
(φ-cong (   xs  ⟧P) ( xs) ⟦⌈  xs ⌉⟧P)
φ-rhs φ (x  xs)