proposition: Lemma ctree_sub_init_tree h (et : colseq) : let et_ok := [&& size et == h, Color0 \notin ctrace et & even_trace et] in ctree_sub (ctree_init_tree h) et = (if et_ok then dyck (count_cbit1 (ctrace et)) else 0).
proof: Proof. case Dh: h => [|h']; [by case: et | rewrite /ctree_init_tree [_.-1]/= -Dh]. move Dltab: (ctree_leaf_table h) => ltab; move Dtab: (iter _ _ ltab) => tab. have{ltab Dtab Dltab} [Dsz Dsub]: h' + size tab = h.+1 /\ forall i, i < size tab -> forall b0 et, let cet := rcons et (ccons (odd i) b0 +c sumt et) in let et_ok := (size et == h') && (Color0 \notin cet) in ctree_sub (ctree_table_sub tab i b0) et = (if et_ok then dyck (i + count_cbit1 cet) else 0). - have:= leqnSn h'; rewrite -{et tab}Dtab -Dh. elim: (h') => [_ | n IHn /leqW ltnh] /=. rewrite -{ltab}Dltab ctree_leaf_table_size add0n; split=> //= i ileh b0. rewrite ctree_leaf_table_sub //; move: (ccons _ _) => c. by case=> *; rewrite ?addc0; case: ifP => // _; apply: ctree_sub_leaf_of. case: (iter n _ _) {IHn}(IHn ltnh) => [|pt tab] [Dn tab_ok]. by rewrite -Dn /= addn0 ltnn in ltnh. rewrite /= size_pairmap addSnnS {}Dn; split=> // i ltitab b0. move: {tab_ok}(tab_ok i (ltnW ltitab)) (tab_ok i.+1 ltitab). rewrite /ctree_table_sub (nth_pairmap ctz) {ltitab}//=. case: {pt}(nth _ _ i) => t0 t1; case: {tab}(nth _ _ i) => t2 t3. do 2![move=> Dsub; move: {Dsub}(Dsub false) (Dsub true) => /= ? ?]. case=> [|e et]; first by case: b0; rewrite ctree_sub_cons. rewrite /= addcA eqSS -[_ +c e]ccons_cbits inE. rewrite cbit0_addc cbit0_ccons cbit1_addc cbit1_ccons. case: e; rewrite /= ?addbT ?addbF -1?addSnnS; by case: b0; rewrite /= ctree_sub_cons /= ?andbF ?add0n. have {}Dsz: size tab = 2 by apply: (@addnI h'); rewrite Dsz Dh addnC. case: tab Dsz => [|[t0 t1] [|[t2 t3] tab']] //= _ in Dsub *. move Dtec: {-}(even_trace et) => tec; rewrite /= ctree_sub_cons {h}Dh. case: et => [|e et] //= in Dtec *; rewrite eqSS. move: {Dsub}(Dsub 0 isT true et) (Dsub 1 isT false et) (Dsub 1 isT true et). rewrite /ctree_table_sub {t0 tab'}/= => Dt1 Dt2 Dt3. case: e Dtec; [by rewrite andbF | move: t1 Dt1 | move: t2 Dt2 | move: t3 Dt3]; by clear=> t Dt Dtec; transitivity (if tec then ctree_sub t et else 0); [ rewrite -{h' tec Dt}Dtec; elim: et t => [|e et IHet] [t1 t2 t3|lf|]; rewrite /= ?if_same // ctree_sub_cons //; case: e; rewrite /= ?if_same | by rewrite Dtec andbA andbC; case tec]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color ctree dyck)