[Agda] Building Coinductive Trees

[Brandon Moore]

A much improved version of coinductive tree construction.
Adreas' suggestion to consider paths into values worked
quite well.


The forward conversion to a coinductive tree is now
pretty compact, and easy to adapt to changes in the
shape of the tree. (There are two minor questions about
things which are not successfully inferred).


I have trouble with the soundness proof (at the end). I think I've
matched on enough values that "split" should have reduced,
but is does not.


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

The tree type.

\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)
  Con3 : {n : ℕ} → P n → P n → P n → P (suc n)
\end{code}

The goal is to turn a function that produces
a tree of any given size into an infinite tree.

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

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

Of course, the output for different sizes should agree.
This is formalized by defining a prefix relation on
trees, and requiring that each tree produced by
a well formed builder be a prefix of any larger tree
it returns.

\begin{code}
data SubTree : ∀{n m} → P n → P m → Set where
  SubTrunc : ∀{n} (v : P n) → SubTree Truncated v
  SubCon1 : ∀{n m} {x : P n} {y : P m} → SubTree x y → SubTree (Con1 x) (Con1 y) 
  SubCon2 : ∀{n m} {xl xr : P n} {yl yr : P m} →
    SubTree xl yl → SubTree xr yr → SubTree (Con2 xl xr) (Con2 yl yr)
  SubCon3 : ∀{n m} {x1 x2 x3 : P n} {y1 y2 y3 : P m} →
    SubTree x1 y1 → SubTree x2 y2 → SubTree x3 y3 → SubTree (Con3 x1 x2 x3) (Con3 y1 y2 y3)

wf : builder → Set
wf b = (n m : ℕ) → n ≤ m → SubTree (b n) (b m)
\end{code}

To define the infinite tree corecursively, a well-formed builder
will have to be turned into some constructors, and well-formed
builders for the subtrees.

These builders will be defined by calling the original builder
at a larger size, and navigating to extract a subtree.
So, define (finite) paths.

\begin{code}
data Path : ℕ → Set where
  End : Path 0
  Con1 : ∀{n} → Path n → Path (suc n)
  Con2Left : ∀{n} → Path n → Path (suc n)
  Con2Right : ∀{n} → Path n → Path (suc n)
  Con3First : ∀{n} → Path n → Path (suc n)
  Con3Second : ∀{n} → Path n → Path (suc n)
  Con3Third : ∀{n} → Path n → Path (suc n)
\end{code}

To follow a path into a tree, that path must actually
correspond to nodes in the tree. Given the
predicate that checks this is the case, it's easy
to extract a subtree.

\begin{code}
data PathInTree : ∀{n m} → Path n → P m → Set where
  PathEnd : ∀{m} {t : P m} → PathInTree End t
  PathCon1 : ∀{n m} {p : Path n} {t : P m}
    → PathInTree p t → PathInTree (Con1 p) (Con1 t)
  PathCon2Left : ∀{n m} {p : Path n} {tl tr : P m}
    → PathInTree p tl → PathInTree (Con2Left p) (Con2 tl tr)
  PathCon2Right : ∀{n m} {p : Path n} {tl tr : P m}
    → PathInTree p tr → PathInTree (Con2Right p) (Con2 tl tr)
  PathCon3First : ∀{n m} {p : Path n} {t1 t2 t3 : P m}
    → PathInTree p t1 → PathInTree (Con3First p) (Con3 t1 t2 t3)
  PathCon3Second : ∀{n m} {p : Path n} {t1 t2 t3 : P m}
    → PathInTree p t2 → PathInTree (Con3Second p) (Con3 t1 t2 t3)
  PathCon3Third : ∀{n m} {p : Path n} {t1 t2 t3 : P m}
    → PathInTree p t3 → PathInTree (Con3Third p) (Con3 t1 t2 t3)

pathGet : ∀{n m} {p : Path n} {t : P (n + m)} → PathInTree p t → P m
pathGet {t = t} PathEnd = t
pathGet (PathCon1 p) = pathGet p
pathGet (PathCon2Left p) = pathGet p
pathGet (PathCon2Right p) = pathGet p
pathGet (PathCon3First p) = pathGet p
pathGet (PathCon3Second p) = pathGet p
pathGet (PathCon3Third p) = pathGet p
\end{code}

Two more lemmas on paths are necessary. One says that if a path exists
in a tree, it also exists in any extension of the tree.

\begin{code}
pathLem : ∀ {k n m} {p : Path k} {bn : P n} {bm : P m}
  → SubTree bn bm → PathInTree p bn → PathInTree p bm
pathLem snm PathEnd = PathEnd
pathLem (SubCon1 s) (PathCon1 p) = PathCon1 (pathLem s p)
pathLem (SubCon2 sl sr) (PathCon2Left p) = PathCon2Left (pathLem sl p)
pathLem (SubCon2 sl sr) (PathCon2Right p) = PathCon2Right (pathLem sr p)
pathLem (SubCon3 s1 s2 s3) (PathCon3First p) = PathCon3First (pathLem s1 p)
pathLem (SubCon3 s1 s2 s3) (PathCon3Second p) = PathCon3Second (pathLem s2 p)
pathLem (SubCon3 s1 s2 s3) (PathCon3Third p) = PathCon3Third (pathLem s3 p)
\end{code}

The other says that if one tree is a prefix of another, and the same path
exists in both trees, then extracting the corresponding subtree in each
tree also produces trees in the subtree relation.

Why is it necessary to pattern match on the first hidden integer?
I think the later pattern matches should make it obvious the path length
k is positive in each case.

\begin{code}
pathSquare : ∀ {k n m} {p : Path k} {bn : P (k + n)} {bm : P (k + m)}
  → (snm : SubTree bn bm) → (pn : PathInTree p bn) → (pm : PathInTree p bm) → SubTree (pathGet pn) (pathGet pm)
pathSquare snm PathEnd PathEnd = snm
pathSquare {suc _} (SubCon1 s) (PathCon1 x) (PathCon1 y) = pathSquare s x y
pathSquare {suc _} (SubCon2 sl sr) (PathCon2Left x) (PathCon2Left y) = pathSquare sl x y
pathSquare {suc _} (SubCon2 sl sr) (PathCon2Right x) (PathCon2Right y) = pathSquare sr x y
pathSquare {suc _} (SubCon3 s1 s2 s3) (PathCon3First x) (PathCon3First y) = pathSquare s1 x y
pathSquare {suc _} (SubCon3 s1 s2 s3) (PathCon3Second x) (PathCon3Second y) = pathSquare s2 x y
pathSquare {suc _} (SubCon3 s1 s2 s3) (PathCon3Third x) (PathCon3Third y) = pathSquare s3 x y
\end{code}

Given a well-formed builder and a path into its output of size k, a new builder can be defined
which calls the new builder at size k+n, uses the subtree proof from well-formedness to
show the path exists in this output as well, and extracts the corresponding subtree to
produces the result of requested size n.

\begin{code}
k≤k+n : (k n : ℕ) → k ≤ k + n
k≤k+n zero n = z≤n
k≤k+n (suc n) n' = s≤s (k≤k+n n n')

builderTail : (b : builder) (w : wf b) → ∀ {k} {pth : Path k} → PathInTree pth (b k) → builder
builderTail b w p n = pathGet (pathLem (w _ _ (k≤k+n _ n)) p)
\end{code}

To show this builder is well-formed, use the commutative square lemma.

Why can't inference supply the pathLem subterms?

\begin{code}
k+n≤k+m : (k : ℕ) {n m : ℕ} → n ≤ m → k + n ≤ k + m
k+n≤k+m zero n≤m = n≤m
k+n≤k+m (suc n) n≤m = s≤s (k+n≤k+m n n≤m)

builderTailWf : (b : builder) (w : wf b) {k : ℕ} {pth : Path k} (p : PathInTree pth (b k)) →
  wf (builderTail b w p)
builderTailWf b w {k} p n m n≤m = pathSquare (w _ _ (k+n≤k+m k n≤m))
  (pathLem (w _ _ (k≤k+n k n)) p)
  (pathLem (w _ _ (k≤k+n k m)) p)
\end{code}

Now the infinite tree can be formed. It seems to be
necessary to define a separate function that defines
the new builders, so a partially applied version can
appear in the with-clause, to be refined by matching
on (b 1). The intermediate type B is seems to make it
possible to get a bit closer to a proof of soundness.

\begin{code}
builderTail∃ : (b : builder) (w : wf b) → ∀ k (p : Path k) → PathInTree p (b k) → ∃ wf
builderTail∃ b w k p pit = builderTail b w pit , builderTailWf b w pit

data B : Set where
  Con1 : ∃ wf → B
  Con2 : ∃ wf → ∃ wf → B
  Con3 : ∃ wf → ∃ wf → ∃ wf → B

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

unroll : ∃ wf → C
unroll x with split x
unroll x | Con1 y = Con1 (♯ (unroll y))
unroll x | Con2 l r = Con2 (♯ (unroll l)) (♯ (unroll r))
unroll x | Con3 x1 x2 x3 = Con3 (♯ (unroll x1)) (♯ (unroll x2)) (♯ (unroll x3))
\end{code}

Finally, soundness should be shown.
To express soundness, define truncate from infinite
to finite trees.

\begin{code}
truncate : (n : ℕ) → C → P n
truncate zero _ = Truncated
truncate (suc n) (Con1 x) = Con1 (truncate n (♭ x))
truncate (suc n) (Con2 l r) = Con2 (truncate n (♭ l)) (truncate n (♭ r))
truncate (suc n) (Con3 x1 x2 x3) = Con3 (truncate n (♭ x1)) (truncate n (♭ x2)) (truncate n (♭ x3))
\end{code}

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}