[Agda] Building Coinductive Trees

[Nils Anders Danielsson]

On 2011-05-22 00:40, Brandon Moore wrote:

> split : ∃ wf → B
> split (b , w) with b 1 | builderTail∃ b w 1
> split (b , w) | Con1 Truncated | bt
>    = Con1 (bt _ (PathCon1 PathEnd))
> split (b , w) | Con2 Truncated Truncated | bt
>    = Con2 (bt _ (PathCon2Left PathEnd))
>           (bt _ (PathCon2Right PathEnd))
> split (b , w) | Con3 Truncated Truncated Truncated | bt
>    = Con3 (bt _ (PathCon3First PathEnd))
>           (bt _ (PathCon3Second PathEnd))
>           (bt _ (PathCon3Third PathEnd))

> Why isn't pattern matching on (b 1) enough to make split reduce?
> The remaining goals are:
>
> ?0 : b (suc n) ≡ truncate (suc n)
>    (unroll (b , w) | (split (b , w) | Con1 y | bt))
> ?1 : b (suc n) ≡ truncate (suc n)
>    (unroll (b , w) | (split (b , w) | Con2 y y' | bt))
> ?2 : b (suc n) ≡ truncate (suc n)
>    (unroll (b , w) | (split (b , w) | Con3 y y' y0 | bt))
>
> split' doesn't seem to require pattern matching on anything else.
> Why hasn't this already reduced?
>
> \begin{code}
> sound : (root : ∃ wf) → (n : ℕ) → proj₁ root n ≡ truncate n (unroll root)
> sound (b , w) zero with b 0; ... | Truncated = refl
> sound (b , w) (suc n) with b 1 | builderTail∃ b w 1
> sound (b , w) (suc n) | Con1 y | bt = {!!}
> sound (b , w) (suc n) | Con2 y y' | bt = {!!}
> sound (b , w) (suc n) | Con3 y y' y0 | bt = {!!}
> \end{code}

In split the pattern is not "Con1 y" but "Con1 Truncated".

-- 
/NAD