proposition: Lemma ctree_init_tree_proper h : ctree_proper h (ctree_init_tree h).
proof: Proof. case Dh: h => [|h'] //=; rewrite /ctree_init_tree. move Dltab: (ctree_leaf_table _) => ltab /=; move Dtab: (iter _ _ ltab) => tab. have{Dtab ltab Dltab} [Dsz sub_ok]: h' + size tab = h.+1 /\ forall i b0, i < size tab -> ctree_proper h' (ctree_table_sub tab i b0). - have:= leqnSn h'; rewrite -{tab}Dtab -Dh. elim: (h') => [_ | n IHn /leqW ltnh]. rewrite /= -{ltab}Dltab -Dh ctree_leaf_table_size; split=> // i b0 leih. rewrite ctree_leaf_table_sub //; case: ifP => // _. exact: ctree_leaf_of_proper. move Dctp': (ctree_proper n.+1) => ctp' /=. case: (iter n _ ltab) {IHn}(IHn ltnh) => [|pt0 tab] [Dn tab_ok]. by rewrite -Dn /= addn0 ltnn in ltnh. rewrite /= addSnnS size_pairmap /=; split=> {Dn}// i b0 ltitab. move/tab_ok: (ltnW ltitab); move/(tab_ok i.+1): (ltitab) => {tab_ok}. rewrite /ctree_table_sub (nth_pairmap ctz) {ltitab}//=. case: (nth _ _ i) => t0 t1; case: {i tab}(nth _ _ i) => t2 t3. do 2![move=> t_ok; move: {t_ok}(t_ok false) (t_ok true) => /= ? ?]. by case: b0; rewrite /= -Dctp'; apply ctree_cons_proper. have{h Dh} Dsz: size tab = 2 by apply: (@addnI h'); rewrite Dsz Dh addn2. case: tab Dsz => [|[t0 t1] [|[t2 t3] tab']] //= _ in sub_ok *. have ok1 := sub_ok 1 _ isT. move: {sub_ok ok1}(sub_ok 0 true isT) (ok1 false) (ok1 true). rewrite /ctree_table_sub {t0 tab'}/= => t1ok t2ok t3ok. apply ctree_cons_proper; [ move: t1 t1ok {t2 t2ok t3 t3ok} | move: {t1 t1ok} t2 t2ok {t3 t3ok} | move: {t1 t1ok t2 t2ok} t3 t3ok ]; elim: h' => [|h IHh] [t1 t2 t3|lf|] //= [_ t1ok t2ok t3ok]; by apply ctree_cons_proper => //; apply: IHh. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color ctree dyck)