[Agda] Working with coinductive trees?

[Nils Anders Danielsson]

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.

-- 
/NAD

-------------- 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)        ∎