proposition: Lemma ctree_restrict_correct h t r : ctree_proper h.+1 t -> let pt := ctree_restrict h t r in [/\ forall b, ctree_proper h.+1 (ctree_pair_sub pt b), ctree_partition t pt & forall et, ctree_sub (ctree_pair_sub pt false) et = ctree_sub t et - ctr_sub r et].
proof: Proof. elim: h => [|h' IHh] in t r *. move Dpt: (ctree_restrict 0 t r) => pt t_ok. case Dt: t t_ok Dpt => [lf1 lf2 lf3|lf|] lf_ok //. case Dr: r => [/= | bs gt r']; last rewrite /ctree_restrict -{bs gt r'}Dr. by move <-; split=> [[] | et | et] //; [case: ifP | rewrite subn0]. rewrite ctr_decr_eq ctree_leaf_pair_spec. have Dlf := ctree_proper_leaf_of_val (ctree_proper_sel _ lf_ok). have [[-> _ _ _] id_t] := (lf_ok, ctree_cons_spec lf1 lf2 lf3 : _ = _). rewrite -id_t in lf_ok; rewrite !(cdecr_leaf _ r lf_ok) !ctree_sub_cons /=. move: {Dlf}(Dlf Color1) (Dlf Color2) (Dlf Color3) => /=. move: (ctree_sub lf1 _) (ctree_sub lf2 _) (ctree_sub lf3 _) => n1 n2 n3. move=> Dlf1 Dlf2 Dlf3 <- {pt}; split=> [|et|et]. - case=> /=; last by apply: ctree_cons_proper; apply: ctree_leaf_of_proper. rewrite Dlf1 Dlf2 Dlf3; apply: ctree_cons_proper; by case: ifP => // _; apply: ctree_leaf_of_proper. - rewrite !ctree_mem_cons /= /ctree_mem; case: et => [|[] et] //=. + rewrite {}Dlf1; case: n1 => [|n1] //; move: (_ - _) => m1. by rewrite 2!ctree_sub_leaf_of; case: et; case: m1. + rewrite {}Dlf2; case: n2 => [|n2] //; move: (_ - _) => m2. by rewrite 2!ctree_sub_leaf_of; case: et; case: m2. rewrite {}Dlf3; case: n3 => [|n3] //; move: (_ - _) => m3. by rewrite 2!ctree_sub_leaf_of; case: et; case: m3. rewrite /= ctree_sub_cons /=; case: et => [|[] et] //=; by rewrite ?Dlf1 ?Dlf2 ?Dlf3 !ctree_sub_leaf_of; case: et. move=> Dpt; have{Dpt} -> /=: pt = ctree_empty_pair by case: r Dpt. by split; case. case: t => // [t1 t2 t3|] t_ok; last first. have <-: ctree_empty_pair = ctree_restrict h'.+1 CtreeEmpty r by case: r. by split; case. move Dpt: (ctree_restrict _ _ r) => /= pt. case Dr: r Dpt => [/= | bs gt r']; last rewrite -{bs gt r'}Dr. by move=> <-{pt}; split=> [[] //|et|et]; [case: ifP | rewrite subn0]. rewrite ctr_split_eq. have{IHh} IHe e := IHh _ (csplit r e) (ctree_proper_sel e t_ok). move: {IHe}(IHe Color1) (IHe Color2) (IHe Color3) => /=. case: (ctree_restrict _ t1 _) => [t1' t1'']. case: (ctree_restrict _ t2 _) => [t2' t2'']. case: (ctree_restrict _ t3 _) => [t3' t3'']. move=> [t1ok ppt1 Dt1'] [t2ok ppt2 Dt2'] [t3ok ppt3 Dt3'] <- {pt}; split=> [b0||et]; first 2 [exact: ctree_cons_pairs_partition]. rewrite ctree_cons_pairs_spec. by case: b0 (t1ok b0) (t2ok b0) (t3ok b0) (ctree_cons_proper) => /=; auto. rewrite ctree_sub0_cons_pairs {t1ok ppt1 t2ok ppt2 t3ok ppt3}. case: et => [|e et] //=; move: {Dt1' Dt2' Dt3'}(Dt1' et) (Dt2' et) (Dt3' et). rewrite !ctr_sub_csplit /=; case: et => [|e' et'] /= Et1' Et2' Et3'; case: e {t_ok}(ctree_proper_sel e t_ok) => //=. - by rewrite {}Et1'; case: t1. - by rewrite {}Et2'; case: t2. by rewrite {}Et3'; case: t3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color chromogram gtree ctree)