proposition: Lemma cfctr_correct mr mc cp (G := cpmap cp) (r := cpring G) : size mr = cprsize cp -> size mc = ctrmsize cp -> let cc := mask mr r ++ mask mc (ctrenum cp) in forall k : G -> color, cc_coloring cc k -> if cfctr mr mc cp is Some cpc then let r' := cpring (cpmap cpc) in exists2 k', coloring k' & map k' r' = map k (mask (map negb mr) r) else True.
proof: Proof. have has_mask2_F T (a : pred T) p1 p2 m1 m2 : ~~ has a (p1 ++ p2) -> has a (mask m1 p1 ++ mask m2 p2) = false. - by apply: contraNF; rewrite !has_cat => /orP[]/has_mask->; rewrite ?orbT. rewrite {}/r {}/G; elim: cp => // s cp IHcp in mr mc *. case Dcpc: (cfctr mr mc _) (cfctr_config_prog mr mc (s :: cp)) => // [cpc]. case: s => // [n||] in Dcpc *; rewrite implyTb => cp_ok Emr Emc; have cpQ := config_prog_cubic cp_ok; rewrite /= in cpQ Dcpc Emr Emc; move: IHcp (cpmap_plain cpQ) (cpmap_proper cpQ); rewrite [cpmap (_ :: _)]/=; set G := cpmap cp => IHcp plainG ntG. - rewrite cpring_ecpR; rewrite -(size_rotr n) in Emr. move=> k [kE kF]; have{IHcp} := IHcp _ _ Emr Emc k. case: (cfctr _ mc cp) cpc Dcpc => // [cpc] _ [<-]. rewrite [cpmap (_ :: _)]/=; set Gc := cpmap cpc. case=> [|k' k'col Ek']; first split=> // x. rewrite kE !(mem_insertE plainG); apply: {x}eq_has_r => x. rewrite !mem_cat; congr (_ || _); rewrite -{1}(rotrK n mr). by apply: mem_mask_rot; rewrite Emr -size_ring_cpmap. exists k'; rewrite // cpring_ecpR -{3}(rotrK n mr) 2!map_rot {}Ek' mask_rot. by rewrite map_rot -map_take count_map. by rewrite size_map size_ring_cpmap. - rewrite /G. case Dcp: cp mc mr Emc Emr Dcpc => [|s cp'] [|b3 mc] [|b1 [|b2 mr]] //. case: mr {cp Dcp G cp_ok cpQ IHcp plainG ntG} => [|b3 [|b4 mr]] // _ _. set G := cpmap [::]; case: ifP => // b123 [<-] {cpc}; rewrite cpring_ecpY. case: b1 b2 b3 b123 => [] [] // [] // _; rewrite cpring0 -/G => k [kE kF]. - exists (k \o icpY G). by split=> y; [case: y (kE (icpY G y)) | case: y; apply/eqP]. congr (_ :: _); have:= kE (node (ecpY G)). by rewrite !inE /= -(eqcP (kF _)) => /eqP->; rewrite -(eqcP (kF _)). - exists (k \o icpY G). by split=> y; [case: y (kE (icpY G y)) | case: y; apply/eqP]. by congr (_ :: _); rewrite /= -(eqcP (kF _)). - exists (fun y => k (if y then ecpY G : ecpY G else node (ecpY G))) => //. split=> y /=; last by case: y; apply/eqP. have:= kE (node (ecpY G)); rewrite inE -(eqcP (kF _)) nodeK. by case: y => //; rewrite eq_sym. by rewrite cpring_ecpY cpring0; exists k. rewrite -Dcp cpring_ecpY ![size _ = _]/= -/G => [] [Emc] [Emr]. have Ecp: ctrenum (CpY :: cp) = map (icpY G) (node G :: ctrenum cp). by rewrite /= /G Dcp. case: ifP => // b123; have plainGX: plain (ecpY G) := plain_ecpY G plainG. case: (cfctr _ mc cp) {IHcp Emr}(IHcp (b3 :: mr) mc Emr Emc) => //. move: cpc => _ cpc IHcp [<-] k [kE kF]; pose h := k \o icpY G. have hF: invariant face h =1 G. move=> x; apply/eqP; apply: (fconnect_invariant kF). by rewrite cface_icpY cfaceC fconnect1. have hE: invariant edge h =i insertE (mask (b3 :: mr) (cpring G) ++ mask mc (ctrenum cp)). - move=> x; rewrite inE /h /= icpY_edge; apply: (etrans (kE _)). rewrite !mem_insertE // {2}head_cpring Ecp. rewrite (eq_has (plain_orbit plainG x)) (eq_has (plain_orbit plainGX _)). rewrite !has_cat -icpY_edge map_cons !has_mask_cons !andbF !orFb. by rewrite orbCA -!orbA; congr (_ || _); rewrite -!map_mask !has_map. case: {IHcp}(IHcp h) {Emc}; first by split. set Gc := cpmap cpc => h' h'col Eh. have{h'col} [[h'E h'F] ntGc] := (h'col, coloring_proper_cpring Gc h'col). case: ifP => b12; rewrite -/Gc. exists h' => //; rewrite {h' hE h'E h'F}Eh /behead head_cpring /h. rewrite !map_mask map_comp !map_cons -/G. rewrite -(fconnect_invariant kF (cface_node_ecpY G)). case: b1 b2 b3 b12 b123 kE => [] [] [] // _ _ kE; congr (_ :: _). have:= etrans (kE _) (mem_head _ _). by rewrite inE -(eqcP (kF _)) nodeK => /eqP. have hEr: all (invariant edge h) (mask (b3 :: mr) (cpring G)). apply/allP=> x rGx; rewrite [invariant _ _ _]hE mem_insertE //. by apply/hasP; exists x; rewrite ?connect0 // mem_cat rGx. have nGN'r: fpath (finv node) (node G) (behead (cpring G)). move: (cycle_rev_cpring G); rewrite head_cpring lastI rev_rcons -lastI. by rewrite (cycle_path (G : G)) /= -(fpath_finv nodeI); case/andP. have h'nGc: h' (node Gc) = h (node G). move: hEr Eh {hE kE}; rewrite head_cpring (head_cpring Gc). elim: {mr}(b3 :: mr) (node G) (behead _) nGN'r => // [b mr IHcp]. case: b => [x [|y p] | x p _ _ [Dx]] //=; first by case mr. case/andP=> /eqP Dy yN'p /andP[/eqcP <-]. by rewrite -(eqcP (hF _)) -(f_finv nodeI x) nodeK Dy; apply: IHcp. case: b1 b2 b3 b12 {b123} => [] [] [] // _ in Eh kE hE hEr *. pose k' u := oapp h' (k (ecpY G)) [pick x | cface u (icpU Gc x)]. have k'F: invariant face k' =1 ecpU Gc. by move=> u; apply/eqP; congr oapp; apply: eq_pick => x; rewrite -cface1. have Ek' x: k' (icpU Gc x) = h' x. rewrite /k'; case: pickP => [y | /(_ x)/idP[]//]. by rewrite cface_icpU cfaceC => /(fconnect_invariant h'F). have k'X: k' (ecpU Gc) = k (ecpY G). by rewrite /k'; case: pickP => // y; rewrite cface_ecpU. have k'nX: k' (node (ecpU Gc)) = k (node (ecpY G)). rewrite (fconnect_invariant kF (cface_node_ecpY _)). by rewrite -(eqcP (k'F _)) /= Ek' h'nGc. exists k'; last first. rewrite [cpmap _]/= -/Gc cpring_ecpU 4!map_cons {1 2}/negb k'nX. rewrite !mask_cons !map_cat !map_nseq k'X; congr [::_, _ & _]. by rewrite -map_mask -!map_comp -/h (eq_map Ek') Eh head_cpring. suffices k'EX: invariant edge k' (ecpU Gc) = false. split=> // -[||x] //; first by rewrite inE eq_sym. rewrite -/cpmap -/Gc in x *; rewrite -/(icpU Gc x) inE -(icpU_edge Gc). by rewrite !Ek'; apply: h'E. apply/eqP => k'eX; have/esym/eqP/idPn[] := kE (node (ecpY G)). rewrite inE -k'nX -(eqcP (kF _)) nodeK -k'X -k'eX eqxx eqb_id. rewrite mem_insertE // mask_cons has_mask2_F // -mem_insertE //. have:= uniq_ctrenum cp_ok; rewrite [cpmap _]/= -/G cpring_ecpY. by rewrite -cat1s -catA insertE_cat cons_uniq inE => /andP[/norP[]]. pose k' u := oapp h' (k (ecpY G)) [pick x | cface u (icpY Gc x)]. have k'F: invariant face k' =1 ecpY Gc. by move=> u; apply/eqP; congr oapp; apply: eq_pick => x; rewrite -cface1. have Ek' x: k' (icpY Gc x) = h' x. rewrite /k' -/Gc; case: pickP => [y | /(_ x)/idP[]//]. by rewrite cface_icpY cfaceC => /(fconnect_invariant h'F). have k'X: k' (ecpY Gc) = k (ecpY G). by rewrite /k' -/Gc; case: pickP => // y; rewrite cface_ecpY. have k'nX: k' (node (ecpY Gc)) = k (node (ecpY G)). rewrite (fconnect_invariant k'F (cface_node_ecpY _)) Ek' h'nGc. by rewrite (fconnect_invariant kF (cface_node_ecpY _)). have h'Gc: h' Gc = h G. rewrite head_proper_cpring // in Eh. move: nGN'r Eh hEr {hE kE}; rewrite head_proper_cpring //=. case/andP=> [_ GN'r] [_ Eh]; move: GN'r Eh. elim: mr (G : G) (drop 2 _) => // [b mr IHmr]. case: b => [x [|y p] | x p _ [Dx]] //=; first by case mr. case/andP=> /eqP Dy yN'r Eh /andP[/eqcP <-]; move: Eh. by rewrite -(eqcP (hF _)) -(f_finv nodeI x) nodeK Dy; apply: IHmr. exists k'; last first. rewrite [cpmap _]/= -/Gc !cpring_ecpY 4!map_cons {1 2}/negb. rewrite k'nX !mask_cons !map_cat !map_nseq k'X; congr [:: _, _ & _]. rewrite -map_mask -!map_comp -/h (eq_map Ek'). by move: Eh; rewrite head_cpring (head_cpring G); case. suffices k'EX u: cface u (ecpY Gc) -> invariant edge k' u = false. split; rewrite // [cpmap _]/= -/Gc => u. have [[x uFx] | XFu] := fband_icpY u; last first. by apply: k'EX; rewrite cfaceC. have [[y euFy] | XFeu] := fband_icpY (edge u); last first. have eeu: edge (edge u) = u. by move: XFeu {uFx}; rewrite cface_ecpY; case: u => [||[||z]]. by rewrite inE eq_sym -{1}eeu [_ == _]k'EX // cfaceC. rewrite inE (fconnect_invariant k'F uFx) (fconnect_invariant k'F euFy). have: adj x y by rewrite -(adj_icpY Gc) -(adjF uFx) -(adjFr euFy) adjE. case/adjP=> z xFz zRy; rewrite !Ek' (fconnect_invariant h'F xFz). by rewrite -(fconnect_invariant h'F zRy); apply: h'E. move=> uFX; rewrite inE (fconnect_invariant k'F uFX) k'X. have{uFX}: adj (ecpY Gc) (edge u) by rewrite -(adjF uFX) adjE. rewrite (adj_ecpY ntGc) unfold_in => /hasP[_ /mapP[y GcNy ->] euFy]. rewrite {u euFy}(fconnect_invariant k'F euFy) Ek'. move: (uniq_ctrenum cp_ok) kE GcNy; rewrite [cpmap _]/= -/G cpring_ecpY. move Dx: (ecpY G : ecpY G) {mc hE}(_ :: mc) (ctrenum _) => x mc p. move Dnx: (node x) => nx /= /and4P[nxE'p _ xE'p _]; move: nxE'p xE'p. rewrite !inE !negb_or !andbA => /andP[_]. rewrite !(mem_insertE plainGX) => nxE'p /andP[_ xE'p] kE /pred2P[]->{y}. rewrite -[x]nodeK Dnx h'nGc /h eq_sym. rewrite (eqcP (kF _)) /= -(fconnect_invariant kF (cface_node_ecpY _)). by rewrite Dx Dnx [_ == _](kE nx) (mem_insertE plainGX) has_mask2_F. have <-: k (edge x) = h' Gc. by rewrite -(eqcP (kF _)) h'Gc -Dx /= nodeK (negPf ntG). by rewrite [_ == _](kE x) (mem_insertE plainGX) has_mask2_F. case: mr mc Emc Emr Dcpc => [|b1 [|b2 mr]] // [|b3 [|b4 [|b5 mc]]] //. case: ifP => // b314_325; case: ifP => // b12mr [Emc] Emr. rewrite /= in Emc Emr. have{IHcp}:= IHcp [:: b4, b5 & mr] mc Emr Emc. case: (cfctr _ mc cp) cpc => // [cpc] _ IHcp [<-] k [kE kF]. pose h := k \o icpH G. have hF: invariant face h =1 G. by move=> x; apply/eqP/(fconnect_invariant kF); rewrite cface_icpH -cface1. have plainGX : plain (ecpH G) := plain_ecpH G plainG. have hE: invariant edge h =i insertE (mask [:: b4, b5 & mr] (cpring G) ++ mask mc (ctrenum cp)). - move=> x; rewrite inE /h /comp icpH_edge [_ == _]kE !mem_insertE //. rewrite cpring_ecpH // {2}head_proper_cpring //. rewrite (eq_has (plain_orbit plainG x)) (eq_has (plain_orbit plainGX _)). rewrite !has_cat -icpH_edge [ctrenum _]/= !has_mask_cons. rewrite !andbF !orFb orbCA -!orbA; congr 1 (_ || _). rewrite [node _]/= /long_cpring [~~ _]/= nodeK (negPf ntG) andbF orFb orbCA. by congr [|| _, _ | _]; rewrite -map_mask has_map. have{IHcp} [//|h' h'col Eh'] := IHcp h; set Gc := cpmap cpc in h' h'col Eh' *. have{h'col} [[h'E h'F] ntGc] := (h'col, coloring_proper_cpring Gc h'col). have kefX: k (edge (face (ecpH G))) = h G. apply: (fconnect_invariant kF); apply connect1; apply/eqP. by rewrite /= nodeK (negPf ntG). have hEr: all (invariant edge h) (mask [:: b4, b5 & mr] (cpring G)). apply/allP=> x rGx; rewrite [invariant _ _ _]hE mem_insertE //. by apply/hasP; exists x; rewrite ?connect0 // mem_cat rGx. have nGN'r: fpath (finv node) (node G) (rcons (behead (cpring G)) (node G)). rewrite (fpath_finv nodeI) last_rcons belast_rcons -head_cpring. have:= cycle_rev_cpring G. by rewrite head_cpring (cycle_path (G : G)) rev_cons last_rcons. case: b3 b314_325 hE hEr kE Eh'. case: b1 b2 b4 b5 {b12mr} => [] // [] // [] [] // _ _ _ kE Eh'. exists h'; rewrite // -/Gc Eh' head_proper_cpring // cpring_ecpH //. rewrite !map_mask !map_cons -map_comp. rewrite (fconnect_invariant kF (cface_node_ecpH ntG)) -/(h (node G)). congr [:: _, _ & _]; apply: eqP; rewrite -(eqcP (kF _)) -kefX [_ == _]kE. by rewrite insertE_cat mem_cat mem_head orbT. case b12: (b1 && b2). case: b1 b2 b12 b12mr b4 b5 => [] [] // _ b_mr [] // [] // _ hE hEr kE Eh'. have longGc: long_cpring Gc. rewrite size_long_cpring -(size_map h') Eh'; move/eqP: Emr b_mr. rewrite -size_ring_cpmap; case: (cpring G) => [|x0 [|x1 p]] //= {x0 x1}. rewrite !eqSS => /eqP eq_sz; rewrite !(size_mask, size_map) //. by rewrite !ltnS count_map -has_count has_predC => ->. rewrite (head_proper_cpring ntG) head_proper_cpring //= in Eh'. have{Eh'} [h'nGc h'Gc Eh'] := Eh'. have h'feGc: h' (face (edge Gc)) = h (face (edge G)). rewrite head_long_cpring //= in Eh'; move: nGN'r Eh' hEr. rewrite head_proper_cpring //= drop0 => /andP[_]. elim: (mr) {-2}(G : G) (drop 2 _) => [|b m IHm] // x [|y p] //=. case/andP=> /eqP Dy yN'p; rewrite -(finv_eq_can nodeK x) Dy. case: b => [/= Eh' | []//] /andP[/eqcP <-] hEp. by rewrite -(eqcP (hF _)) (IHm _ _ yN'p). have Eh'A: h' (node Gc) = h' (face (edge Gc)). rewrite h'nGc h'feGc (eqcP (hF (edge G))). rewrite /h /= -(fconnect_invariant kF (cface_node_ecpH ntG)). transitivity (k (face (edge (node (ecpH G))))); apply: eqP. by rewrite eq_sym (eqcP (kF _)) [_ == _]kE head_cpring mem_head. rewrite nodeK eq_sym -(eqcP (kF _)) /= nodeK (negPf ntG) eqxx. by rewrite [_ == _](kE (ecpH G)) cpring_ecpH // 2?mem_behead ?mem_head. have h'FA: invariant (@face (ecpA Gc)) h' =1 Gc. rewrite /invariant /= /ecpA_face => x; rewrite inE. case: ifP => _; first exact: h'F; case: (x =P _) => [Dx|_]. by rewrite -(eqcP (h'F x)) Dx -Eh'A eqxx. case: (face x =P _) => [Dfx | _]; last exact: h'F. by rewrite -(eqcP (h'F x)) Dfx -Eh'A eqxx. exists h'; last first. rewrite [cpmap _]/= -/Gc cpring_ecpA longGc cpring_ecpH //=. by rewrite -map_mask -map_comp; rewrite drop_behead in Eh'. split; rewrite //= /ecpA_edge /= -/Gc => x /=. case: ifP => _; first exact: h'E. case: (x =P _) => [Dx | _]. by rewrite -(eqcP (h'F _)) nodeK Eh'A (eqcP (h'F _)) Dx; apply: h'E. case: (x =P _) => [Dx | _]; last exact: h'E. by rewrite -(eqcP (h'F _)) -Eh'A -(canLR nodeK Dx) (eqcP (h'F _)); apply: h'E. case: b1 b2 {b12mr}b12 b4 b5 => [] [] // _ [] [] // _; rewrite [cpmap _]/= -/Gc => hE hEr kE Eh'. - exists h'; rewrite // Eh' (head_proper_cpring ntG) cpring_ecpH //. rewrite !map_mask !map_cons -map_comp; congr (_ :: _). apply/esym/eqP; rewrite /h /= -(fconnect_invariant kF (cface_node_ecpH ntG)). rewrite -[y in k y](nodeK (ecpH G)) (eqcP (kF _)) [_ == _]kE. by rewrite head_cpring mem_head. - pose k' u := oapp h' Color0 [pick x | cface u (icpK Gc x)]. have k'F: invariant face k' =1 ecpK Gc. by move=> u; apply/eqP; congr oapp; apply: eq_pick => x; rewrite -cface1. have Ek' x: k' (icpK _ x) = h' x. rewrite /k' -/Gc; case: pickP => [y | /(_ x)/idP[]//]. by rewrite cface_icpK cfaceC => /(fconnect_invariant h'F). rewrite (head_proper_cpring ntG) (head_proper_cpring ntGc) /= in Eh'. have{Eh'} [hnGc hGc Eh'] := Eh'. have kX: k (ecpH G) = h' (node Gc). apply: eqP; rewrite hnGc -(nodeK (ecpH G)) (eqcP (kF _)). rewrite /h /= -(fconnect_invariant kF (cface_node_ecpH ntG)) [_ == _]kE. by rewrite head_cpring mem_head. exists k'; last first. rewrite cpring_ecpK cpring_ecpH // map_mask !map_cons -!map_comp. rewrite (eq_map Ek') Eh' map_mask kX; congr (_ :: _). by rewrite (fconnect_invariant k'F (cface_node_ecpK _)) Ek'. set x0 : ecpK Gc := ecpN (ecpR' Gc). suffices k'EX: invariant edge k' x0 = false. split=> // [] [||x] //; first by rewrite inE eq_sym. by rewrite -[Icp x]/(icpK Gc x) inE -icpK_edge !Ek'; apply: h'E. rewrite inE; have <-: h' (face (edge Gc)) = k' (edge x0). rewrite (eqcP (h'F _)) -Ek'; apply/(fconnect_invariant k'F)/connect1/eqP. by rewrite /ecpK /x0 ecpR'_eq /= nodeK eqxx. have <-: k (ecpH G) = k' x0. rewrite kX -Ek'; apply/esym/(fconnect_invariant k'F)/connect1/eqP. by rewrite /ecpK /x0 ecpR'_eq. have <-: (h (face (edge G)) = h' (face (edge Gc))). move/eqP: Emr; move: nGN'r hEr; rewrite -size_ring_cpmap -/G. rewrite (head_proper_cpring ntG) /= !eqSS => /andP[_]. move: (mr) {-2}(G : G) (drop 2 (cpring G)) Eh'. elim=> [|b m IHm] x [|y p] //= Eh' /andP[/eqP/(canRL (f_finv nodeI))->]. suffices /eqP->: long_cpring Gc = false by rewrite nodeK. by rewrite size_long_cpring -(size_map h') head_proper_cpring //= Eh'. case: b Eh' => /= Eh' yN'Hp. by rewrite nodeK => /andP[/eqP<-]; rewrite -(eqcP (hF _)); apply: IHm. have longGc: long_cpring Gc. by rewrite size_long_cpring -(size_map h') head_proper_cpring //= Eh'. by rewrite head_long_cpring // in Eh'; rewrite nodeK; case: Eh'. have <-: k (edge (ecpH G)) = h (face (edge G)). rewrite (eqcP (hF _)); apply/esym/(fconnect_invariant kF)/connect1/eqP. by rewrite /= nodeK (negPf ntG) eqxx. have:= uniq_ctrenum cp_ok; rewrite [_ == _]kE [cpmap _]/= -/G cpring_ecpH //. rewrite 2!cat_cons (insertE_cat [:: _; _]) (insertE_cat [:: _]) -catA. rewrite uniq_catCA -insertE_cat catA cat1s cons_uniq inE orFb !mem_insertE //. by rewrite 2!mask_cons cat0s -mask_cons => /andP[/has_mask2_F->]. - exists h'; rewrite // Eh' (head_proper_cpring ntG) cpring_ecpH //. rewrite !map_mask !map_cons -map_comp; congr (_ :: _). apply/eqP; rewrite (fconnect_invariant kF (cface_node_ecpH ntG)). by rewrite -{1}(nodeK G) (eqcP (hF _)) [_ == _]hE head_cpring mem_head. - pose k' u := oapp h' Color0 [pick x | cface u (icpK Gc x)]. have k'F: invariant face k' =1 ecpK Gc. by move=> u; apply/eqP; congr oapp; apply/eq_pick=> x; rewrite -cface1. have Ek' x: k' (icpK _ x) = h' x. rewrite /k' -/Gc; case: pickP => [y | /(_ x)/idP[]//]. by rewrite cface_icpK cfaceC => /(fconnect_invariant h'F). rewrite (head_proper_cpring ntG) (head_proper_cpring ntGc) /= in Eh'. have{Eh'} [h'nGc h'Gc Eh'] := Eh'. exists k'; last first. rewrite cpring_ecpK cpring_ecpH // map_mask !map_cons -!map_comp. rewrite (eq_map Ek') Eh' map_mask; congr (_ :: _). rewrite (fconnect_invariant k'F (cface_node_ecpK _)) Ek'. by rewrite (fconnect_invariant kF (cface_node_ecpH ntG)). set x0 : ecpK Gc := ecpN (ecpR' Gc). suffices k'EX: invariant edge k' x0 = false. split=> // -[||x] //; first by rewrite inE eq_sym. by rewrite -[Icp x]/(icpK Gc x) inE -icpK_edge !Ek' [_ == _]h'E. rewrite inE; have <-: h' (face (edge Gc)) = k' (edge x0). rewrite (eqcP (h'F _)) -Ek'; apply/(fconnect_invariant k'F)/connect1/eqP. by rewrite /ecpK /x0 ecpR'_eq /= nodeK eqxx. have <-: h (face (edge G)) = h' (face (edge Gc)). move/eqP: Emr; move: nGN'r hEr; rewrite -size_ring_cpmap -/G. rewrite (head_proper_cpring ntG) /= !eqSS => /andP[_]. move: (mr) {-2}(G : G) (drop 2 (cpring G)) Eh'. elim=> [|b m IHm] x [|y p] //= Eh' /andP[/eqP/(canRL (f_finv nodeI))->]. suffices /eqP->: long_cpring Gc = false by rewrite nodeK. by rewrite size_long_cpring -(size_map h') head_proper_cpring //= Eh'. case: b Eh' => /= Eh' yN'p. by rewrite nodeK -(eqcP (hF _)) => /andP[/eqP<-]; apply: IHm. have longGc: (long_cpring Gc). by rewrite size_long_cpring -(size_map h') head_proper_cpring //= Eh'. by rewrite nodeK head_long_cpring // in Eh' *; case: Eh'. have <-: k (edge (ecpH G)) = h (face (edge G)). rewrite (eqcP (hF _)); apply/esym/(fconnect_invariant kF)/connect1/eqP. by rewrite /= nodeK (negPf ntG) eqxx. have <-: k (node (ecpH G)) = k' x0. rewrite (fconnect_invariant kF (cface_node_ecpH ntG)) -[k _]/(h (node G)). rewrite -h'nGc -Ek'; apply/esym/(fconnect_invariant k'F)/connect1/eqP. by rewrite /ecpK /x0 ecpR'_eq. have <-: k (edge (node (ecpH G))) = k (edge (ecpH G)). rewrite -(eqcP (kF _)) nodeK; apply/esym/eqP. by rewrite [_ == _]kE cpring_ecpH ?mem_head. have:= uniq_ctrenum cp_ok; rewrite [_ == _]kE [cpmap _]/= -/G cpring_ecpH //. rewrite mask_cons cat0s cat_cons (insertE_cat [:: _]) cons_uniq inE andbC. rewrite !mem_insertE // => /andP[_] /norP[_]; apply: contraNF. case/hasP=> [z p_z nXEz]; apply/hasP; exists z => {nXEz}//. by move: p_z; rewrite !mem_cat => /orP[]/mem_mask->; rewrite ?orbT. - pose k' u := oapp h' (k (ecpH G)) [pick x | cface u (icpU Gc x)]. have k'F: invariant face k' =1 ecpU Gc. by move=> u; apply/eqP; congr oapp; apply/eq_pick=> x; rewrite -cface1. have Ek' x: k' (icpU Gc x) = h' x. rewrite /k' -/Gc; case: pickP => [y | /(_ x)/idP[]//]. by rewrite cface_icpU cfaceC => /(fconnect_invariant h'F). have k'X: k' (ecpU Gc) = k (ecpH G). by rewrite /k'; case: pickP => // y; rewrite cface_ecpU. rewrite (head_proper_cpring ntG) head_cpring /= in Eh'. have k'eX: h (face (edge G)) = k' (edge (ecpU Gc)). have <-: h' (node Gc) = k' (edge (ecpU Gc)) by rewrite -(eqcP (k'F _)) -Ek'. move: nGN'r hEr; rewrite (head_proper_cpring ntG) /= => /andP[_ GN'r]. case/and3P=> _ _; move: (mr) {-2}(G : G) (drop 2 (cpring G)) Eh' GN'r. elim=> [|b m IHm] x [|y p] //= Eh' /andP[/eqP/(canRL (f_finv nodeI))->]. rewrite nodeK; case: b Eh' => [|] /= Eh' yN'p; last by case: Eh'. by case/andP=> /eqcP<-; rewrite -(eqcP (hF _)); apply: IHm. exists k'; last first. rewrite cpring_ecpU cpring_ecpH // map_mask !map_cons -!map_comp -/cpmap. rewrite (eq_map Ek') head_cpring map_cons Eh' k'X map_mask; congr (_ :: _). rewrite (fconnect_invariant kF (cface_node_ecpH ntG)) -[k _]/(h (node G)). apply: (etrans (esym k'eX)); transitivity (h G); apply: eqP. by rewrite (eqcP (hF _)) [_ == _]hE head_proper_cpring // !inE eqxx !orbT. by rewrite -{1}(nodeK G) (eqcP (hF _)) [_ == _]hE head_cpring mem_head. suffices k'EX: invariant edge k' (ecpU Gc) = false. split=> // [] [||x] //; first by rewrite inE eq_sym. by rewrite -[Icp x]/(icpU Gc x) inE -icpU_edge !Ek' [_ == _]h'E. rewrite inE k'X -k'eX. have <-: k (edge (ecpH G)) = h (face (edge G)). rewrite (eqcP (hF _)); apply/esym/(fconnect_invariant kF)/connect1/eqP. by rewrite /= nodeK (negPf ntG) eqxx. have:= uniq_ctrenum cp_ok; rewrite [_ == _]kE [cpmap _]/= -/G cpring_ecpH //. rewrite 2!mask_cons !cat0s 2!cat_cons (insertE_cat [:: _; _]) 3!cons_uniq. by case/and4P=> _ _; rewrite inE !mem_insertE // => /has_mask2_F->. - pose k' u := oapp h' (k (ecpH G)) [pick x | cface u (icpY Gc x)]. have k'F: invariant face k' =1 ecpY Gc. by move=> u; apply/eqP; congr oapp; apply/eq_pick=> x; rewrite -cface1. have Ek' x: k' (icpY Gc x) = h' x. rewrite /k' -/Gc; case: pickP => [y | /(_ x)/idP[]//]. by rewrite cface_icpY cfaceC => /(fconnect_invariant h'F). have k'X: k' (ecpY Gc) = k (ecpH G). by rewrite /k'; case: pickP => // y; rewrite cface_ecpY. rewrite (head_proper_cpring ntG) head_cpring /= in Eh'. have{Eh'} [h'nGc Eh'] := Eh'. have hnG: h (node G) = h G. rewrite -{2}(nodeK G) (eqcP (hF _)); apply/esym/eqP. by rewrite [_ == _]hE head_cpring mem_head. have k'nX: k' (node (ecpY Gc)) = k (node (ecpH G)). rewrite (fconnect_invariant k'F (cface_node_ecpY _)) Ek' h'nGc -hnG. by rewrite (fconnect_invariant kF (cface_node_ecpH ntG)). have h'Gc: h' Gc = h (face (edge G)). rewrite head_proper_cpring //= in Eh'; move: nGN'r hEr {hE kE}. rewrite head_proper_cpring //= => /andP[_ GN'r] /andP[_]; move: Eh' GN'r. elim: (mr) {-2}(G : G) (drop 2 (cpring G)) => [|b m IHm] x [|y p] //= Eh'. case/andP=> /eqP/(canRL (f_finv nodeI))-> yN'p; rewrite nodeK. case: b => /= [|[]//] in Eh' * => /andP[/eqP <- /(IHm y)-> //]. exact/eqP/hF. exists k'; last first. rewrite [cpmap _]/= cpring_ecpY cpring_ecpH // !map_mask !map_cons. by rewrite k'nX k'X -!map_comp (eq_map Ek') Eh' map_mask. suffices k'EX u: cface u (ecpY Gc) -> invariant edge k' u = false. rewrite [cpmap _]/= -/Gc; split=> // u. have [[x uFx] | XFu] := fband_icpY u; last by rewrite k'EX // cfaceC. have [[y euFy] | XFeu] := fband_icpY (edge u); last first. have eeu: edge (edge u) = u. by move: XFeu {uFx}; rewrite cface_ecpY; case: u => [||[||z]]. by rewrite inE eq_sym -{1}eeu [_ == _]k'EX // cfaceC. rewrite inE (fconnect_invariant k'F uFx) (fconnect_invariant k'F euFy) !Ek'. have: adj x y by rewrite -(adj_icpY Gc) -(adjF uFx) -(adjFr euFy) adjE. case/adjP=> z xFz zRy; rewrite (fconnect_invariant h'F xFz). by rewrite -(fconnect_invariant h'F zRy) [_ == _]h'E. move=> uFX; rewrite inE (fconnect_invariant k'F uFX) k'X. have{uFX}: adj (ecpY Gc) (edge u) by rewrite -(adjF uFX) adjE. rewrite (adj_ecpY ntGc) unfold_in => /hasP[_ /mapP[y GcNy ->] euFX]. rewrite {u euFX}(fconnect_invariant k'F euFX) Ek'. move: kE (uniq_ctrenum cp_ok); rewrite [cpmap _]/= -/G cpring_ecpH // => kE. rewrite 2!cat_cons (insertE_cat [:: _; _]) cat_uniq has_sym andbCA andbC. rewrite -all_predC => /andP[_ /and4P[]]; rewrite 9?(mem_insertE, inE) //. move=> rE'nX _ rE'X _; move: GcNy; rewrite !inE => /pred2P[]->. rewrite h'nGc -hnG -[h _](fconnect_invariant kF (cface_node_ecpH ntG)). rewrite eq_sym -[z in k z]nodeK (eqcP (kF _)) [_ == _]kE 2!mask_cons !cat0s. by rewrite mem_insertE // has_mask2_F. rewrite h'Gc; have <-: k (edge (ecpH G)) = h (face (edge G)). rewrite (eqcP (hF _)); apply/esym/(fconnect_invariant kF)/connect1/eqP. by rewrite /= nodeK (negPf ntG) /= eqxx. by rewrite [_ == _]kE 2!mask_cons !cat0s mem_insertE // has_mask2_F. - pose k' u := oapp h' (k (ecpH G)) [pick x | cface u (icpY Gc x)]. have k'F: invariant face k' =1 ecpY Gc. by move=> u; apply/eqP; congr oapp; apply/eq_pick=> x; rewrite -cface1. have Ek' x: k' (icpY Gc x) = h' x. rewrite /k' -/Gc; case: pickP => [y | /(_ x)/idP[]//]. by rewrite cface_icpY cfaceC => /(fconnect_invariant h'F). have k'X: k' (ecpY Gc) = k (ecpH G). by rewrite /k'; case: pickP => // y; rewrite cface_ecpY. rewrite (head_proper_cpring ntG) head_cpring /= in Eh'. have{Eh'} [h'nGc Eh'] := Eh'. have hfeG: h (face (edge G)) = h G. by apply/eqP; rewrite (eqcP (hF _)) [_ == _]hE head_proper_cpring ?mem_head. have k'nX: k' (node (ecpY Gc)) = k (node (ecpH G)). rewrite (fconnect_invariant k'F (cface_node_ecpY _)) Ek' h'nGc. by rewrite (fconnect_invariant kF (cface_node_ecpH ntG)). have h'Gc: h' Gc = h (face (edge G)). rewrite head_proper_cpring //= in Eh'; move: nGN'r hEr {hE kE}. rewrite head_proper_cpring //= => /andP[_ GN'r] /andP[_]; move: GN'r Eh'. elim: (mr) {-2}(G : G) (drop 2 (cpring G)) => [|b m IHm] x [|y p] //=. case/andP=> /eqP/(canRL (f_finv nodeI))-> yN'p; rewrite nodeK. by case: b => [? /andP[/eqcP<-]|[]//]; rewrite -(eqcP (hF _)); apply: IHm. exists k'; last first. rewrite /cpmap -/cpmap cpring_ecpY cpring_ecpH // !map_mask !map_cons k'nX. by rewrite k'X -!map_comp (eq_map Ek') Eh' map_mask. suffices k'EX u: cface u (ecpY Gc) -> invariant edge k' u = false. rewrite [cpmap _]/= -/Gc; split=> // u. have [[x uFx] | XFu] := fband_icpY u; last by apply: k'EX; rewrite cfaceC. have [[y euFy] | XFeu] := fband_icpY (edge u); last first. have eeu: edge (edge u) = u. by move: XFeu {uFx}; rewrite cface_ecpY; case: u => [||[||z]]. by rewrite inE eq_sym -{1}eeu; apply: k'EX; rewrite cfaceC. rewrite inE (fconnect_invariant k'F uFx) (fconnect_invariant k'F euFy) !Ek'. have: adj x y by rewrite -(adj_icpY Gc) -(adjF uFx) -(adjFr euFy) adjE. case/adjP=> z xFz zRy; rewrite (fconnect_invariant h'F xFz). by rewrite -(fconnect_invariant h'F zRy) [_ == _]h'E. move=> uFX; rewrite inE (fconnect_invariant k'F uFX) k'X. have{uFX}: adj (ecpY Gc) (edge u) by rewrite -(adjF uFX) adjE. rewrite (adj_ecpY ntGc) unfold_in => /hasP[ _ /mapP[y GcNy ->] euFX]. rewrite {u euFX}(fconnect_invariant k'F euFX) Ek'. move: kE (uniq_ctrenum cp_ok); rewrite [cpmap _]/= -/G cpring_ecpH //. rewrite 2!mask_cons !cat0s 2!cat_cons (insertE_cat [:: _; _]) cat_uniq => kE. rewrite has_sym -all_predC andbA andbAC => /andP[_ /and4P[]]. rewrite 9?(mem_insertE, inE) // => rE'nX _ rE'X _. move: GcNy; rewrite !inE => /pred2P[]->. rewrite h'nGc -[h _](fconnect_invariant kF (cface_node_ecpH ntG)) eq_sym. rewrite -{1}(nodeK (ecpH G)) (eqcP (kF _)) [_ == _]kE mem_insertE //. exact: has_mask2_F. rewrite h'Gc; have <-: k (edge (ecpH G)) = h (face (edge G)). rewrite (eqcP (hF _)); apply/esym/(fconnect_invariant kF)/connect1/eqP. by rewrite /= nodeK (negPf ntG) /= eqxx. by rewrite [_ == _]kE mem_insertE // has_mask2_F. pose k' u := oapp h' (k (ecpH G)) [pick x | cface u (icpH Gc x)]. have k'F: invariant face k' =1 ecpH Gc. by move=> u; apply/eqP; congr oapp; apply/eq_pick=> x; rewrite -cface1. have Ek' x: k' (icpH Gc x) = h' x. rewrite /k' -/Gc; case: pickP => [y | /(_ x)/idP[]//]. by rewrite cface_icpH cfaceC => /(fconnect_invariant h'F). have k'X: k' (ecpH Gc) = k (ecpH G). by rewrite /k'; case: pickP => // y; rewrite cface_ecpH. rewrite (head_proper_cpring ntG) head_proper_cpring //= in Eh'. have{Eh'} [h'nGc h'Gc Eh'] := Eh'. have k'nX: k' (node (ecpH Gc)) = k (node (ecpH G)). rewrite (fconnect_invariant k'F (cface_node_ecpH ntGc)) Ek' h'nGc. by rewrite (fconnect_invariant kF (cface_node_ecpH ntG)). have h'feGc: h' (face (edge Gc)) = h (face (edge G)). move/eqP: Emr; move: nGN'r hEr {hE kE}; rewrite -size_ring_cpmap -/G. rewrite head_proper_cpring //= !eqSS => /andP[_]. elim: (mr) {-2}(G : G) (drop 2 (cpring G)) Eh' => [|b m IHm] x [|y p] //= Eh'; case/andP=> /eqP/(canRL (f_finv nodeI))-> yN'p; rewrite nodeK. - suffices /eqP->: long_cpring Gc = false by rewrite -h'nGc. by rewrite size_long_cpring -(size_map h') head_proper_cpring //= Eh'. case: b Eh' => /= Eh'. by case/andP=> /eqcP=> <-; rewrite -(eqcP (hF _)); apply: IHm. have longGc: long_cpring Gc. by rewrite size_long_cpring -(size_map h') head_proper_cpring //= Eh'. by rewrite (head_long_cpring longGc) in Eh'; case: Eh'. exists k'; last first. rewrite [cpmap _]/= !cpring_ecpH // !map_mask !map_cons. by rewrite k'nX k'X -!map_comp (eq_map Ek') Eh' map_mask. suffices k'EX u: cface u (ecpH Gc) -> invariant edge k' u = false . split=> //; rewrite [cpmap _]/= -/Gc => u. have [[x uFx] | XFu] := fband_icpH u; last first. by apply: k'EX; rewrite cfaceC. have [[y euFy] | XFeu] := fband_icpH (edge u); last first. have eeu: edge (edge u) = u. by move: XFeu {uFx}; rewrite cface_ecpH; case: u => [||[||[||z]]]. by rewrite inE eq_sym -{1}eeu; apply: k'EX; rewrite cfaceC. rewrite inE (fconnect_invariant k'F uFx) (fconnect_invariant k'F euFy) !Ek'. have: adj x y by rewrite -(adj_icpH Gc) -(adjF uFx) -(adjFr euFy) adjE. case/adjP=> z xFz zRy; rewrite (fconnect_invariant h'F xFz). by rewrite -(fconnect_invariant h'F zRy) [_ == _]h'E. move=> uFX; rewrite inE (fconnect_invariant k'F uFX) k'X. have{uFX}: adj (ecpH Gc) (edge u) by rewrite -(adjF uFX) adjE. rewrite (adj_ecpH ntGc) unfold_in => /hasP[ _ /mapP[y GcNy ->] euFy]. rewrite {u euFy}(fconnect_invariant k'F euFy) Ek'. move: kE (uniq_ctrenum cp_ok); rewrite [cpmap _]/= -/G cpring_ecpH //. rewrite /ctrenum -/ctrenum -/G 3!mask_cons !cat0s => kE. rewrite -[p in _ ++ p]cat1s 2!insertE_cat uniq_catCA -!insertE_cat. rewrite 3!cat_cons -2!cat_rcons -cat_cons insertE_cat cat_uniq has_sym andbCA. rewrite /rcons {2}/insertE -all_predC /all 15?(mem_insertE, inE) //. case/andP=> /and3P[rE'fX _] /and3P[rE'nX _] /andP[rE'X _] _. move: GcNy; rewrite !inE => /predU1P[|/pred2P[]] ->{y}. - rewrite h'nGc -[h _](fconnect_invariant kF (cface_node_ecpH ntG)). rewrite eq_sym -{1}(nodeK (ecpH G)) (eqcP (kF _)) [_ == _]kE. by rewrite mem_insertE // has_mask2_F. - rewrite h'Gc -(eqcP (kF _)); have <-: k (edge (face (ecpH G))) = h G. by apply/(fconnect_invariant kF)/connect1/eqP; rewrite /= nodeK (negPf ntG). by rewrite [_ == _]kE mem_insertE // has_mask2_F. rewrite h'feGc; have <-: k (edge (ecpH G)) = h (face (edge G)). rewrite (eqcP (hF _)); apply/esym/(fconnect_invariant kF)/connect1/eqP. by rewrite /= nodeK (negPf ntG) /= eqxx. by rewrite [_ == _]kE mem_insertE // has_mask2_F. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree) fourcolor(cfcolor)