From HB Require Import structures.
From mathcomp Require Import all_boot.
Require Import tools combclass bintree.

Set Implicit Arguments.

Inductive ordtree : Set := OrdNode : seq ordtree -> ordtree.
Notation forest := (seq ordtree).

Lemma OrdNode_inj : injective OrdNode.

Section Recursion.

Variables (P : ordtree -> Type) (PF : seq ordtree -> Type).
Hypothesis HPnil : PF [::].
Hypothesis IHforest : forall tr f, P tr -> PF f -> PF (tr :: f).
Hypothesis IHtree : forall f, PF f -> P (OrdNode f).

Fixpoint recforest rt f : PF f :=
  if f is tr :: tlf then IHforest (rt tr) (recforest rt tlf)
  else HPnil.
Fixpoint rectree t : P t :=
  let: OrdNode f := t in IHtree (recforest rectree f).

End Recursion.
Definition indtreeforest
  (P : ordtree -> Prop) (PF : forest -> Prop) := @rectree P PF.

Fixpoint eq_forest (eqtr : ordtree -> ordtree -> bool) (f1 f2 : seq ordtree) :=
  match f1, f2 with
  | [::], [::] => true
  | tr1 :: tl1, tr2 :: tl2 => eqtr tr1 tr2 && eq_forest eqtr tl1 tl2
  | _, _ => false
  end.
Fixpoint eq_ordtree tr1 tr2 :=
  match tr1, tr2 with
    OrdNode f1, OrdNode f2 => eq_forest eq_ordtree f1 f2
  end.
Fact eq_ordtreeP : Equality.axiom eq_ordtree.

Section SimpleRecursion.

Variables (P : ordtree -> Type).
Hypothesis IHtree :
  forall f : forest, (forall t : ordtree, t \in f -> P t) -> P (OrdNode f).
Lemma rec_tree t : P t.

End SimpleRecursion.
Definition indtree (P : ordtree -> Prop) := @rec_tree P.

Fixpoint ord_to_bintree (t : ordtree) : bintree :=
  let fix f_to_bin t_to_bin (f : forest) : bintree :=
    match f with
    | [::] => BinLeaf
    | t :: ftl => BinNode (t_to_bin t) (f_to_bin t_to_bin ftl)
    end
  in let: OrdNode f := t in f_to_bin ord_to_bintree f.
Definition forest_to_bintree f := ord_to_bintree (OrdNode f).

Fixpoint bin_to_forest (t : bintree) : forest :=
  if t is BinNode l r then OrdNode (bin_to_forest l) :: bin_to_forest r
  else [::].
Definition bin_to_ordtree t := OrdNode (bin_to_forest t).

Lemma bin_to_forestK : cancel bin_to_forest forest_to_bintree.
Lemma bin_to_ordtreeK : cancel bin_to_ordtree ord_to_bintree.

Lemma ord_to_bintreeK : cancel ord_to_bintree bin_to_ordtree.
Lemma forest_to_bintreeK : cancel forest_to_bintree bin_to_forest.


Fixpoint size_ordtree t :=
  let: OrdNode f := t in (sumn [seq size_ordtree t | t <- f]).+1.
Lemma size_ordtreeE f :
  size_ordtree (OrdNode f) = (sumn [seq size_ordtree t | t <- f]).+1.
Lemma size_ordtree_pos t : size_ordtree t > 0.
Lemma size_tree_eq1 t : (size_ordtree t == 1) = (t == OrdNode [::]).
Lemma size_bin_to_ordtree bt :
  size_ordtree (bin_to_ordtree bt) = (size_tree bt).+1.
Lemma size_ord_to_bintree t :
  size_ordtree t = (size_tree (ord_to_bintree t)).+1.

Section OfSize.

Variable (n : nat).

Structure ordtreesz : predArgType :=
  OrdTreeSZ {trval :> ordtree; _ : size_ordtree trval == n}.

Lemma ordtreeszP (t : ordtreesz) : size_ordtree t = n.

End OfSize.

Section FinType.

Implicit Type (t : ordtree).

Definition enum_ordtreesz n :=
  if n is n'.+1 then [seq bin_to_ordtree b | b <- enum_bintreesz n']
  else [::].

Lemma size_mem_enum_ordtreeszP n t :
  t \in enum_ordtreesz n -> size_ordtree t = n.

Lemma enum_ordtreeszP n :
  all (fun t => size_ordtree t == n) (enum_ordtreesz n).

Lemma enum_ordtreesz_uniq n : uniq (enum_ordtreesz n).

Lemma mem_enum_ordtreesz n t :
  size_ordtree t == n -> t \in enum_ordtreesz n.

Lemma enum_ordtreesz_countE n t :
  size_ordtree t == n -> count_mem t (enum_ordtreesz n) = 1.

Theorem card_ordtreesz n : #|ordtreesz n.+1| = Catalan_bin n.

End FinType.

Fixpoint depth_ordtree t :=
  let: OrdNode f := t in (foldr maxn 0 [seq depth_ordtree t | t <- f]).+1.
Lemma depth_ordtreeE f :
  depth_ordtree (OrdNode f) = (foldr maxn 0 [seq depth_ordtree t | t <- f]).+1.
Lemma depth_ordtree_pos t : depth_ordtree t > 0.
Lemma depth_tree_eq1 t : (depth_ordtree t == 1) = (t == OrdNode [::]).
Lemma depth_tree_eq2P t :
  reflect (exists n, t = OrdNode (nseq n.+1 (OrdNode [::])))
    (depth_ordtree t == 2).