# [Agda] Working with coinductive trees?

Nils Anders Danielsson nad at chalmers.se
Sat Feb 25 13:39:42 CET 2012

```On 2012-02-24 16:11, Brandon Moore wrote:
> There's a bit of difficulty in Coq as unfolding terms has to
> be done by applying an equality, but it's mostly straightforward.

The lemma clo in your development relies on a feature of Coq which
breaks subject reduction.

> This seems to be rooted in generativity - it takes a bit of trouble
> with a with-clause to match on a delayed subterm, and even after doing
> so the results can't be recorded in the context by refining the
> subtree to look like (# pat).

Generativity is indeed annoying. You could try to avoid mentioning ♯_
unless absolutely possible. The attached development uses conditional
coinduction to accomplish this.

--

-------------- next part --------------
module SK where

open import Coinduction
open import Data.Bool

mutual

infixl 9 _\$_

data CL : Set where
S K : CL
_\$_ : ∀ {lc rc} (l : ∞⟨ lc ⟩CL) (r : ∞⟨ rc ⟩CL) → CL

∞⟨_⟩CL : Bool → Set
∞⟨ true  ⟩CL = ∞ CL
∞⟨ false ⟩CL =   CL

♭? : ∀ {b} → ∞⟨ b ⟩CL → CL
♭? {b = true}  x = ♭ x
♭? {b = false} x =   x

infixl 9 _\$⟶_
infix  4 _⟶_
infixr 2 _⟶⟨_⟩_
infix  2 _∎

data _⟶_ : CL → CL → Set where
K⟶     : ∀ {xc yc} {x : ∞⟨ xc ⟩CL} {y : ∞⟨ yc ⟩CL} → K \$ x \$ y ⟶ ♭? x
S⟶     : ∀ {xc yc zc} {x : ∞⟨ xc ⟩CL} {y : ∞⟨ yc ⟩CL} {z : ∞⟨ zc ⟩CL} →
S \$ x \$ y \$ z ⟶ (x \$ z) \$ (y \$ z)
_⟶⟨_⟩_ : ∀ x {y z : CL} (x⟶y : x ⟶ y) (y⟶z : y ⟶ z) → x ⟶ z
_∎     : ∀ x → x ⟶ x
_\$⟶_   : ∀ {xc x′c yc y′c}
{x : ∞⟨ xc ⟩CL} {x′ : ∞⟨ x′c ⟩CL}
{y : ∞⟨ yc ⟩CL} {y′ : ∞⟨ y′c ⟩CL}
(x⟶x′ : ♭? x ⟶ ♭? x′) (y⟶y′ : ♭? y ⟶ ♭? y′) → x \$ y ⟶ x′ \$ y′

I : CL
I = (S \$ K) \$ K

I-id : ∀ {xc} {x : ∞⟨ xc ⟩CL} → I \$ x ⟶ ♭? x
I-id {x = x} =
I \$ x              ⟶⟨ S⟶ ⟩
(K \$ x) \$ (K \$ x)  ⟶⟨ K⟶ ⟩
♭? x               ∎

SIω : CL
SIω = S \$ I \$ ♯ SIω

SIω-unroll : SIω ⟶ S \$ I \$ SIω
SIω-unroll =
SIω          ⟶⟨ (_ ∎) \$⟶ (_ ∎) ⟩
S \$ I \$ SIω  ∎

SIω-fix : ∀ {xc} (x : ∞⟨ xc ⟩CL) → SIω \$ x ⟶ x \$ (SIω \$ x)
SIω-fix x =
SIω \$ x              ⟶⟨ SIω-unroll \$⟶ (_ ∎) ⟩
(S \$ I \$ SIω) \$ x    ⟶⟨ S⟶ ⟩
(I \$ x) \$ (SIω \$ x)  ⟶⟨ I-id \$⟶ (_ ∎) ⟩
x \$ (SIω \$ x)        ∎
```