(* (c) P. Casteran *) Set Implicit Arguments. Require Export List. (* potentialy infinite trees with internal nodes labeled with type A *) CoInductive LTree (A:Type) : Type := LLeaf : LTree A | LBin : A -> LTree A -> LTree A -> LTree A. Implicit Arguments LLeaf [A]. Definition is_LLeaf (A:Type) (t:LTree A) : Prop := match t with | LLeaf => True | _ => False end. Definition L_root (A:Type) (t:LTree A) : option A := match t with | LLeaf => None | LBin r _ _ => Some r end. Definition L_left_son (A:Type) (t:LTree A) : option (LTree A) := match t with | LLeaf => None | LBin _ t1 _ => Some t1 end. Definition L_right_son (A:Type) (t:LTree A) : option (LTree A) := match t with | LLeaf => None | LBin _ _ t2 => Some t2 end. Inductive direction : Type := | d0 : direction (* left *) | d1 : direction (* right *). Definition path := list direction. (* The subtree at path p *) Fixpoint L_subtree (A:Type) (p:path) (t:LTree A) {struct p} : option (LTree A) := match p with | nil => Some t | d0 :: p' => match t with | LLeaf => None | LBin a t1 t2 => L_subtree p' t1 end | d1 :: p' => match t with | LLeaf => None | LBin a t1 t2 => L_subtree p' t2 end end. Inductive label (A:Type) : Type := | node_label : A -> label A | leaf_label : label A. (* the label at path p *) Definition LTree_label (A:Type) (t:LTree A) (p:path) : option (label A) := match L_subtree p t with | None => None | Some t' => match t' with | LLeaf => Some (leaf_label A) | LBin x _ _ => Some (node_label x) end end. Lemma LTree_label_rw_leaf : forall (A:Type) (d:direction) (p:path), LTree_label (LLeaf (A:=A)) (d :: p) = None. Proof. unfold LTree_label in |- *; intros A d p; case d; simpl in |- *; auto. Qed. Lemma LTree_label_rw_root_bin : forall (A:Type) (a:A) (t1 t2:LTree A), LTree_label (LBin a t1 t2) nil = Some (node_label a). Proof. unfold LTree_label in |- *; simpl in |- *; auto. Qed. Lemma LTree_label_rw_root_leaf : forall A:Type, LTree_label (LLeaf (A:=A)) nil = Some (leaf_label A). Proof. unfold LTree_label in |- *; simpl in |- *; auto. Qed. Lemma LTree_label_rw0 : forall (A:Type) (a:A) (t1 t2:LTree A) (p:path), LTree_label (LBin a t1 t2) (d0 :: p) = LTree_label t1 p. Proof. unfold LTree_label in |- *; simpl in |- *; auto. Qed. Lemma LTree_label_rw1 : forall (A:Type) (a:A) (t1 t2:LTree A) (p:path), LTree_label (LBin a t1 t2) (d1 :: p) = LTree_label t2 p. Proof. unfold LTree_label in |- *; simpl in |- *; auto. Qed. (* Decomposition lemma for LTree *) Definition LTree_decomp (A:Type) (t: LTree A) : LTree A := match t with LLeaf => LLeaf | LBin a t1 t2 => (LBin a t1 t2) end. Lemma LTree_decompose : forall (A : Type) (t: LTree A), t = LTree_decomp t. Proof. destruct t; trivial. Qed. Ltac LTree_unfold term := apply trans_equal with (1 := LTree_decompose term).