[Agda] Building Coinductive Trees

[Brandon Moore]

I am trying to write some code to construct a coinductive tree, given

a function that returns a finite tree of any given size. I hope
someone can suggest a cleaner approach. This code I have seems
like it could be completed, but it's already quite messy, to only handle
one single constructor.


Literate agda:

\begin{code}
module CTest where
open import Data.Nat
open import Coinduction
open import Relation.Binary.PropositionalEquality
open import Data.Product
\end{code}

The inductive tree is indexed by size, and has interesting 1 and 2 argument
constructors, and a leaf to mark truncation. The coinductive tree just
has the two interesting constructors.

\begin{code}
data P : ℕ → Set where
  Truncated : P 0
  Con1 : (n : ℕ) → P n → P (suc n)
  Con2 : (n : ℕ) → P n → P n → P (suc n)

data C : Set where
  Con1 : ∞ C → C
  Con2 : ∞ C → ∞ C → C
\end{code}

A tree builder is just a function that returns a tree of any given size.

\begin{code}
builder = (n : ℕ) → P n
\end{code}

To ensure the limit is well defined, the tree produced at a given size
should be a prefix of the tree produced for all larger sizes.
Maybe this condition should be integrated directly into the definition
of a tree builder?

\begin{code}
truncate : (n m : ℕ) → n ≤ m → P m → P n
truncate .0 m z≤n p = Truncated
truncate .(suc m) .(suc n) (s≤s {m} {n} m≤n) (Con1 .n p)
  = Con1 m (truncate m n m≤n p)
truncate .(suc m) .(suc n) (s≤s {m} {n} m≤n) (Con2 .n p p')
  = Con2 m (truncate m n m≤n p) (truncate m n m≤n p')

wf_builder : builder → Set
wf_builder b = (n m : ℕ) (l : n ≤ m) → truncate n m l (b m) ≡ b n
\end{code}

To actually construct the infinite tree, I want to look at the
constructor a well-formed builder produces at size 1, define
new builders for all the recursive positions which invoke the original
builder at size suc n and return the resulting subtree, and prove
that the new builder is well-formed.

Proving all those lemmas is the problem.

Given the lemmas, I can unroll a builder one step
into the following representation.

\begin{code}
data B : Set where
  Con1 : ∃ wf_builder → B
  Con2 : ∃ wf_builder → ∃ wf_builder → B

check : (b : builder) → wf_builder b → B
check b wf = {!!}
\end{code}

and given that, unroll a builder all the way to an infinite tree.

\begin{code}
builderToC : ∃ wf_builder → C
builderToC (b , wf) with check b wf
builderToC (b , wf) | Con1 y = Con1 (♯ builderToC y)
builderToC (b , wf) | Con2 y y' = Con2 (♯ builderToC y) (♯ builderToC y')
\end{code}

The problem is in the lemmas. I'll just show the case for Con1.

First, an inversion lemma saying that if a truncated tree is headed
by a given constructor, then the original tree was headed by the
same constructor

\begin{code}
truncateInv1 : (n : ℕ) (p : P (suc n)) (m : ℕ) (m≤n : m ≤ n)
  → ∃ (λ x → truncate (suc m) (suc n) (s≤s m≤n) p ≡ Con1 m x)
  → ∃ λ x' → p ≡ Con1 n x'
truncateInv1 n (Con1 .n y) m m≤n (x , eq) = y , refl
truncateInv1 n (Con2 .n y y') m m≤n (x , ())
\end{code}

Next, use this to show that if a well-formed builder produces a
tree headed by the given constructor at head zero, then it does
so at all sizes.

\begin{code}
buildCon1 : (b : builder) → wf_builder b → b 1 ≡ Con1 0 Truncated
  → ∀ n → ∃ λ x → b (suc n) ≡ Con1 n x
buildCon1 b wf eq n = truncateInv1 n (b (suc n)) zero z≤n (Truncated ,
  trans (wf 1 (suc n) (s≤s z≤n)) eq)
\end{code}

These two lemmas would be required for each constructor

Now, make a new builder which calls the old builder at the next largest
size and returns the child of Con1, by extracting the witness from the
existential returned by the last lemma.

\begin{code}
buildCon1Child : (b : builder) → wf_builder b → b 1 ≡ Con1 0 Truncated
  → builder
buildCon1Child b wf eq n with b (suc n) | wf 1 (suc n) (s≤s z≤n)
buildCon1Child b wf eq .n | Con1 n y | _ = y
buildCon1Child b wf eq .n | Con2 n y y' | eq2 with trans eq2 eq ; ... | ()
\end{code}

One of these would be required for each recursive argument of each constructor.

That's bad enough, but what's even worse is proving that the resulting builders
are well-formed. Here's a single case.

\begin{code}
buildCon1ChildWf : (b : builder) (wf : wf_builder b) (eq : b 1 ≡ Con1 0 Truncated)
  → wf_builder (buildCon1Child b wf eq)
buildCon1ChildWf b wf eq n m n≤m with
   b (suc m) | wf 1 (suc m) (s≤s z≤n)
 | b (suc n) | wf 1 (suc n) (s≤s z≤n)
 | wf (suc n) (suc m) (s≤s n≤m)
buildCon1ChildWf b wf eq n m n≤m | bm | wfm | Con2 .n y y' | wfn | eqnm
  with trans wfn eq ; ... | ()
buildCon1ChildWf b wf eq n m n≤m
  | Con2 .m y y' | wfm | Con1 .n y0 | wfn | ()
buildCon1ChildWf b wf eq n m n≤m
  | Con1 .m y | wfm | Con1 .n y' | wfn | eqnm with truncate n m n≤m y
buildCon1ChildWf b wf eq n m n≤m
  | Con1 .m y | wfm | Con1 .n y' | wfn | refl | .y' = refl
\end{code}

Given that, it's possible to start filling in "check" from above

\begin{code}
check' : (b : builder) → wf_builder b → B
check' b wf with inspect (b 1)
check' b wf | Con1 .0 Truncated with-≡ eq
  = Con1 ((buildCon1Child b wf eq) , buildCon1ChildWf b wf eq)
check' b wf | Con2 .0 y y' with-≡ eq = {!!}
\end{code}