------------------------------------------------------------------------ -- Nested applications of the defined function can be handled ------------------------------------------------------------------------ module Nested where open import Coinduction open import Data.Stream open import Function ------------------------------------------------------------------------ -- 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 (x ∷ xs≈ys) = x ∷ ♯ 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) = x ∷ ♯ 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 ♯′_ = ♯_ φ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) ∎