[Agda] Building Coinductive Trees

[Andreas Abel]

Hi Brandon,

just on a general note, you are implementing the semantics of 
coinductive data as limit of inductive data for the special case of some 
trees.

In terms of vectors and streams, if you have a sequence

   v : (n : Nat) -> Vec A n

of vectors that are subvectors of each other, then it is in bijection 
with a stream

   s : Stream A

conceived as the limit of the vector sequence.

I do not think there is some method much easier than what you are doing. 
  The only thing you could maybe change is to define your subtree 
predicate, wf_builder, inductively.  In terms of vectors,

   data SubVector (A : Set)(m : Nat) :
     forall {n} -> Vec A n -> Vec A (n + m) -> Set
   where
     subNil  : forall (v : Vec A m) -> SubVector A nil v
     subCons : forall {n}(a : A)(w : Vec A n)(v : Vec A (n + m)) ->
       SubVector A w v -> SubVector A (a :: w) (a :: v)

I am attaching a partial development, maybe it provides some inspiration 
for you.  Unfortunately, I have to return to my tax declaration now.

--Andreas

On 17.05.11 5:39 PM, Brandon Moore wrote:
> 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}
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
-------------- next part --------------
module BrandonMoore where

open import Level
open import Coinduction
open import Data.Nat
open import Data.Vec
open import Data.Stream renaming (head to headS; tail to tailS)
open import Relation.Binary.PropositionalEquality

-- * Trivial properties of vector equality

vec0IsNil : {A : Set} (v : Vec A 0) -> v ≡ []
vec0IsNil [] = refl 

vecSIsCons : {A : Set}{n : ℕ} (v : Vec A (suc n)) -> v ≡ head v ∷ tail v
vecSIsCons (a ∷ as) = refl

-- ∷-cong : {A : Set}{n : ℕ}{v w : Vec A n}(a : A) -> v ≡ w -> a ∷ v ≡ a ∷ w
∷-cong : {A : Set}{n : ℕ}{v w : Vec A n}{a b : A} -> 
  a ≡ b -> v ≡ w -> _≡_ {A = Vec A (suc n)} (a ∷ v) (a ∷ w)
∷-cong refl refl = refl

-- * Streams as a sequence of vectors of increasing length

VecStr : Set -> Set
VecStr A = (n : ℕ) -> Vec A n

headVS : {A : Set} -> VecStr A -> A
headVS s = Data.Vec.head (s 1)

tailVS : {A : Set} -> VecStr A -> VecStr A
tailVS s n = Data.Vec.tail (s (suc n))

-- * Converting to proper streams and back

build : {A : Set} -> VecStr A -> Stream A
build s = Stream._∷_ (headVS s) (♯ (build (tailVS s))) 

unroll : {A : Set} -> Stream A -> VecStr A
unroll s 0 = []
unroll s (suc n) = Vec._∷_ (headS s) (unroll (tailS s) n)

-- * Subvector, inductively

data SubVec {A : Set}{m : ℕ} : 
    forall {n} -> Vec A n -> Vec A (n + m) -> Set
  where 
    subNil  : forall (v : Vec A m) -> SubVec [] v
    subCons : forall {n}(a : A){w : Vec A n}{v : Vec A (n + m)} ->
      SubVec w v -> SubVec (a ∷ w) (a ∷ v)

subVecTail : forall {A m n}{w : Vec A (suc n)} {v : Vec A (suc (n + m))} -> 
  SubVec w v -> SubVec (tail w) (tail v)
subVecTail (subCons a p) = p

-- * Well-formed sequences of vectors

WF : {A : Set} -> VecStr A -> Set
WF {A = A} s = forall n m -> SubVec (s n) (s (n + m))

tailWF : {A : Set}(s : VecStr A) -> WF s -> WF (tailVS s)
tailWF s p n m = subVecTail (p (suc n) m)

unrollWF : {A : Set}(s : Stream A) -> WF (unroll s)
unrollWF s zero m = subNil (unroll s m)
unrollWF s (suc n) m = subCons (headS s) (unrollWF (tailS s) n m)

-- * The difficult theorem:
--
--   Starting at a well-formed vector sequence s,
--   if we build a proper stream from it and unroll it again,
--   we get the same sequence.

sound : {A : Set}(s : VecStr A)(p : WF s)(n : ℕ) -> unroll (build s) n ≡ s n
sound s p zero = sym (vec0IsNil (s 0))
sound s p (suc n) with inspect (s (suc n)) 
sound s p (suc n) | (a ∷ as) with-≡ eq = {!eq -- ∷-cong ? ?!}
-- sound s p (suc n) rewrite vecSIsCons (s (suc n)) = {!∷-cong ? ?!}