1.Consider the following definition :

Set Implicit Arguments.

(* potentialy infinite trees with internal nodes labeled with type A *)

CoInductive LTree (A : Set) : Set :=
LLeaf : LTree A
| LBin : A -> (LTree A) -> (LTree A) -> LTree A.

Define the following predicates and functions :

(is_LLeaf t) is a proposition meaning "t is a leaf".
(L_root t) returns the label of the root of t (if exists)
(L_left_son t) returns the left son of t (if exists)
(L_right_son t) returns the right son of t (if exists)
(L_subtree p t) returns the subtree of t at path p (if exists)
(LTree_label p t) returns the label at path p (if exists)


2. Define the function graft such that (graft t t') is the tree obtained by replacing all leaves of t by t'.

3. Prove unfold lemmas for grafting, i.e. the following theorems :

Lemma graft_unfold1 : forall (A:Set) (t': LTree A), graft LLeaf t' = t'.

Lemma graft_unfold2: forall (A:Set)(a:A) (t1 t2 t':LTree A), (graft (LBin a t1 t2) t')= (LBin a (graft t1 t') (graft t2 t')).

Lemma graft_unfold : forall (A:Set) (t t': LTree A),
graft t t' = match t with
| LLeaf => t'
| LBin n t1 t2 => LBin n (graft t1 t') (graft t2 t')
end.

4. Define four predicates on potentially infinite binary trees :

(a) Having some infinite branch
(b) Having only infinite branches
(c) Having some finite branch
(d) Having only finite branches (i.e. being finite)

For each of the preceding predicates, build an example tree, then prove that it satisfies this predicate. Prove the following theorems (for any tree t) :

(i) If every branch of t is finite, t has no infinite branch.
(ii) If t has some infinite branch, the not every branch of t is finite.
(iii) If t has some finite branch, then not every branch of t is infinite.
(iv) If t has no finite branch, then every branch of t is infinite.
(v) If t is finite, then (graft t (LLeaf A))=t.
(vi) (in classical logic :) if not every branch of t is finite, then t has some infinite branch.

5. Define (coinductively) the notion of bisimilarity on LTree A.

6. Prove that, if some tree t1 has only infinite branches, then t1 and (graft t1 t2) are bisimilar.