(* Time-stamp: "modifie le  4 Jul 2009 a 07:25 par Pierre Lescanne sur boucherotte" *)
(* ~/Documents/COQ/GAMES/EXTENSIVE/bintree.v *)
(********************************************************************************)
(*                             bintree.v                                        *)
(*                                                                          	*)
(**                       © Pierre Lescanne                   	                *)
(*                                                                          	*)
(*		       LIP (ENS-Lyon, CNRS, INRIA) 				*)
(*                                                                          	*)
(*                                                                          	*)
(** Developed in V8.1                                                June 2009   *)
(********************************************************************************)

Inductive Bintree : Set :=
| btNil: Bintree 
| btNode: Bintree -> Bintree -> Bintree.

Definition LeftBin (b:Bintree): Bintree :=
match b with
| btNil => btNil
| btNode bl _ => bl
end.

Definition RightBin (b:Bintree): Bintree :=
match b with
| btNil => btNil
| btNode _ br => br
end.

Lemma NodeLeftRight: forall b, btNil = b \/ btNode (LeftBin b) (RightBin b) = b.
Proof.
induction b; [left | right]; simpl; trivial.
Qed.

CoInductive LBintree : Set :=
| LbtNil: LBintree 
| LbtNode: LBintree -> LBintree -> LBintree.

CoInductive InfiniteLBT: LBintree -> Prop := 
| IBTLeft : forall bl br, InfiniteLBT bl -> InfiniteLBT (LbtNode bl br)
| IBTRight : forall bl br, InfiniteLBT br -> InfiniteLBT (LbtNode bl br).

CoFixpoint LBackbone: LBintree := LbtNode LBackbone LbtNil.

CoFixpoint Zig: LBintree := LbtNode Zag LbtNil
with Zag: LBintree := LbtNode LbtNil Zig.

Definition LBintree_id (b:LBintree): LBintree :=
match b with 
| LbtNil => LbtNil
| LbtNode b1 b2 => LbtNode b1  b2
end.

Lemma LBintree_id_lemma: forall b, LBintree_id b = b.
Proof.
intro b.
case b.
simpl; trivial.
intros. 
simpl; trivial.
Qed.

Lemma  InfiniteBackbone: InfiniteLBT LBackbone.
Proof.
cofix H.
replace LBackbone with (LbtNode LBackbone LbtNil).
apply IBTLeft.
apply H.
pattern LBackbone at 2.
replace LBackbone with (LBintree_id LBackbone).
trivial.
apply LBintree_id_lemma.
Qed.

Lemma Zag_decomp:  (LbtNode LbtNil Zig) = Zag.
Proof.
replace Zag with (LBintree_id Zag).
trivial.
apply LBintree_id_lemma.
Qed.

Lemma Zig_decomp:  (LbtNode Zag LbtNil) = Zig.
Proof.
replace Zig with (LBintree_id Zig).
trivial.
apply LBintree_id_lemma.
Qed.

Lemma InfiniteZig:  InfiniteLBT Zig.
Proof.
cofix H.
replace Zig with (LbtNode Zag LbtNil).
apply IBTLeft.
replace Zag with (LbtNode LbtNil Zig).
apply IBTRight.
apply H.
apply Zag_decomp.
apply Zig_decomp.
Qed.

Lemma InfiniteZag:  InfiniteLBT Zag.
Proof.
replace Zag with (LbtNode LbtNil Zig).
apply IBTRight.
apply InfiniteZig.
apply Zag_decomp.
Qed.