------------------------------------------------------------------------
-- 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)
-- Weak head normal forms.
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) ∎