proposition: Theorem Kempe_tree_closure_correct d ctu ctr gtu : let ktr0 Q := Q ctu ctr GtreeEmpty gtu in let ktrp := ktr_prop (Kempe_tree_closure d ctu ctr gtu) in ktr0 Kempe_valid -> [/\ ktrp Kempe_valid & forall sz, ktr0 (Kempe_complete (3 ^ d + sz)) -> ktrp (Kempe_complete sz.+1)].
proof: Proof. elim: d => [|d IHd] /= in ctu ctr gtu *. move Dctrr: (GtrCons _ ctr _) => ctrr [[ctu_ok Dctu] Dctr Dgtr Dgtu closedP]. move: (gtree_restrict_partition gtu ctrr) (gtree_mem0_restrict gtu ctrr). case: (gtree_restrict gtu ctrr) => gtr gtu' /= Pgt Pgtr. split=> [|sz [ctu_lt_sz ctr_closed]]. split=> // [|w gt_w | w gt_w | w gt'w Dw]; first split=> // et. - by rewrite Dctu gtree_sub_empty -(match_count_partition Pgt). - move: gt_w (Pgtr w) (Pgt w) => -> /esym/andP[gt_w _] /idP. by rewrite gt_w; split=> //; apply: Dgtu. - by apply: Dgtu; apply: contraFT (Pgt w) => /negPf->; rewrite gt_w orbT. case: (@idP (gtree_mem gtu w)) (Pgt w) => [_ | ? _]; last exact: closedP. rewrite Pgtr andbC; case gt_w: (gtr_mem _ w) => [] => [_ | /negbFE//]. by move: gt_w; rewrite -Dctrr /= orbF => /has_matchP[et /Dctr[]]; exists et. split=> [|et /= Pet]. case: ctu_lt_sz => [|[{}Dctr _]]; [by left | right; split=> // w]. by rewrite Pgtr -Dctrr Dctr /= andbC; case: has_matchP => // [] []. right; apply/eqP/match_countP=> [[w gt_w wMet]]; case/negP: (Pgt w). rewrite gt_w; case gtu_w: (gtree_mem gtu w); last by rewrite orbT. case/ctr_closed: Pet => [ct_et | /eqP/match_countP[]]; last by exists w. rewrite /eqb addbT negbK Pgtr gtu_w -Dctrr /= orbF. by apply/has_matchP; exists (etrace et); rewrite ?matchpg_etrace. move: (Kempe_tree_closure d) IHd ctu ctr gtu => ktc' IHktc'. suffices IHstep ktr: let ktrp := ktr_prop ktr in let ktrp' := ktr_prop (ktc_step ktc' ktr) in ktrp Kempe_valid -> [/\ ktrp' Kempe_valid & forall sz, ktrp (Kempe_complete (3 ^ d + sz.+1)) -> ktrp' (Kempe_complete sz.+1)]. - move=> ctu ctr gtu /IHktc'[/IHstep[/IHstep[valid full3] full2] full1]. split=> // sz; rewrite expnS -!addnA => /full1. by rewrite -addnS => /full2; rewrite -addnS => /full3. move Dktr': (ktc_step _ ktr) => ktr'; case: ktr => ctu [gtr gtu] /= in Dktr' *. case=> [[ctu_ok Dctu] _ Dgtr Dgtu closedP]. case: ifP Dktr' => [/ctree_empty_eq ctu0 <- //= | _]. by split=> // sz [_ ctr_closed]; split=> //; left; rewrite ctu0. case: gtree_emptyP => [gtr0 <- //= | _]. split=> // sz [_ ctr_closed]; split=> //; right; split=> // w. by rewrite gtr0 gtree_mem_empty. case gtree_emptyP => [gtu0 | _] <- {ktr'}/=. split; last by split; [left | right; rewrite gtree_sub_empty]. split=> //; do [by case | by rewrite -gtu0 | split=> // et]. by rewrite gtree_sub_empty if_same. have{ctu_ok}:= ctree_restrict_correct (CtrCons Bstack0 gtr CtrNil) ctu_ok. case: (ctree_restrict _ _ _) => ctu' ctr /= [ct_ok Pctu Dctu']. have{ct_ok} [/= ctr_ok ctu'_ok] := (ct_ok true, ct_ok false). suffices{IHktc'} [gt_valid gt_full]: [/\ Kempe_valid ctu' (ctree_rotlr ctr) GtreeEmpty gtu & forall sz, Kempe_complete sz.+1 ctu CtreeEmpty gtr gtu -> Kempe_complete sz ctu' (ctree_rotlr ctr) GtreeEmpty gtu]. - by case/IHktc': gt_valid; split=> // sz; rewrite addnS => /gt_full; move: sz. have {}Dctu': ctree_sub ctu' =1 even_fun et (sub_gt gtu et). by move=> et; rewrite Dctu' Dctu addn0; case: ifP; rewrite ?addKn. split=> [|sz [ctu_lt_sz ctr_closed]]. split=> // [|et0 ct_et0 | [] //]. by split=> // et; rewrite gtree_sub_empty Dctu'. have{ct_et0} [g ct_et]: exists g, ctree_mem ctr (permt g et0). move: ct_et0; rewrite (ctree_mem_rotlr _ ctr_ok). by case/orP; [exists Eperm312 | exists Eperm231]. set et := permt g et0 in ct_et. have{ct_et}[gtr_et gtu'et]: sub_gt gtr et != 0 /\ sub_gt gtu et == 0. case: ifP (Pctu et); rewrite ct_et ?orbT // -eqE eqb_id /ctree_mem. by rewrite Dctu Dctu' addnC; case: ifP => //; case: (sub_gt gtu et). have{gtr_et} sz_et: size et == h.+1. by case/match_countP: gtr_et => w /Dgtr[_ /andP[sz_w _]] /matchpg_size <-. split=> [P1 closedP1 P1et0|]; last by rewrite -(eqP sz_et) size_map. have{P1et0}-/closedP1[_ [w etMw wP1]]: P1 (ctrace et). by rewrite ctrace_permt; case/closedP1: P1et0. have w_bal: gram_balanced 0 false w. by have [_] := matchg_balanced etMw; rewrite sumt_ctrace. have Dw := matchg_cgram etMw; move: (take _ _) => w1 in Dw. have{etMw} etMw1: matchpg Bstack0 et w1 by rewrite -matchg_pg -Dw. have [gt_w1||et1 closedPet1 et1Mw1] := closedP w1. - by case/match_countP: gtu'et; exists w1. - by rewrite /init_gtree_spec (matchpg_size etMw1) sz_et -Dw. by apply: closedPet1 => //; apply: wP1; rewrite Dw matchg_pg -?Dw. split=> [|et /=]. have{ctu_lt_sz} [| [_ gtr0]] := ctu_lt_sz. rewrite (ctree_size_partition Pctu) addnC -ltn_subRL. case ctr0: (ctree_size ctr) => [|m]; last first. by move/leq_trans->; [left | rewrite subSS leq_subr]. by right; split=> [|[]] //; rewrite (ctree_size_proper ctr_ok ctr0). right; split => [|[]] //; rewrite (_ : ctr = CtreeEmpty) //. apply/(ctree_size_proper ctr_ok)/(@addnI (ctree_size ctu')). rewrite -(ctree_size_partition Pctu). rewrite (@ctree_size_partition ctu ctu' CtreeEmpty) // => et. case: ifP (Pctu et) => [|_ /norP[/negPf->] //]. rewrite /ctree_mem Dctu Dctu'; case: ifP => // _. by rewrite /gtree_sub match_count_0 => [-> // | w]; apply/negP. case=> [Pet | [e]]; first by case: (ctr_closed et) => //; [left | right]. set et1 := permt _ _ => /negP ctu'et1. case ctu'et: (ctree_mem ctu' (etrace et)); last first. right; apply: contraFeq ctu'et => /match_countP[w gt_w etMw]. rewrite /ctree_mem Dctu' even_etrace; apply/match_countP. by exists w; rewrite ?matchpg_etrace. case ctu_et1: (ctree_mem ctu et1); last first. by case: (ctr_closed et) => //; right=> //; exists e; rewrite ctu_et1. left; case: ifP (Pctu (etrace et)); rewrite ctu'et // /eqb /= => _ ctr_et. have:= Pctu et1; rewrite ctu_et1 (negPf ctu'et1) => /negbFE. rewrite (ctree_mem_rotlr _ ctr_ok) /= /et1 /edge_rot. by case: (e) ctr_et; by [rewrite permt_id => -> | move=> _ ->; rewrite ?orbT]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color chromogram coloring cfmap) fourcolor(cfcolor dyck ctree initctree gtree initgtree) fourcolor(gtreerestrict ctreerestrict)