proposition: Theorem contract_coloring (r cc : seq G) : valid_contract r cc -> cc_colorable cc.
proof: Proof. case=> _ cc_sparse cc_1to4 cc_triad. have{r cc_sparse cc_triad}: forall p, ~ contract_ring cc p. case/or4P: cc_1to4 => /eqP Ecc; try by apply: contract3_valid; rewrite ?Ecc. by have /exists_inP[x0 _]:= cc_triad Ecc; apply: triad_valid. have{cc_1to4}: #|G| < (0 < size cc) + #|G| by case: (size cc) cc_1to4. move: {2}(size cc) (leqnn (size cc)) => n. move: {-2}#|G| minG (cexG : planar_bridgeless_plain_precubic G) => nG min_nG. elim: n G cc => [|n IHn] G0 [|x cc] geoG0 //=. - by move=> _ /min_nG[] // k; exists k. - exact: (IHn G0 [::]). rewrite /= add1n !ltnS => le_cc_n G0_lenG ring'cc. have plainG0: plain G0 := geoG0; have ee0 := plain_eq geoG0. have bridge'G0 := bridgeless_cface geoG0. have D_E0 (y : G0): cedge x y = (y == x) || (y == edge x). by rewrite (plain_orbit geoG0) !inE. pose G1 := WalkupF x; pose h1 (u : G1) : G0 := val u. have Ih1: injective h1 by apply: val_inj. have x'ex: edge x != x by rewrite (plain_neq geoG0). pose uex : G1 := sub (edge x) x'ex. pose G2 := WalkupF uex; pose h2 (w : G2) : G1 := val w. have Ih2: injective h2 by apply: val_inj. pose h w := h1 (h2 w); have Ih: injective h := inj_comp Ih1 Ih2. have Eh: codom h =i predC (cedge x). move=> y; rewrite inE D_E0; apply/imageP/norP => [[w _ ->] | [x'y ex'y]]. by rewrite (valP w) (valP (val w)). by exists ((sub (sub y x'y : G1) : _ -> G2) ex'y). have xE'h w: cedge x (h w) = false. by apply: negPf; rewrite -[~~ _]Eh codom_f. have hN w w': cnode w w' = cnode (h w) (h w') by rewrite !fconnect_skip. have hE w w': cedge w w' = cedge (h w) (h w') by rewrite !fconnect_skip. have h_e w: h (edge w) = edge (h w). have ewP: edge (h w) \in codom h by rewrite Eh inE -cedge1r -[~~ _]Eh codom_f. rewrite -(f_iinv ewP); congr h; symmetry. by do 2 apply: (valE_skip nodeI); apply: (f_iinv ewP). pose xR y := has (cface y) [:: x; edge x]. have hF w w': cface w w' = (if xR (h w) then xR (h w') else cface (h w) (h w')). transitivity (cface (h2 w) (h2 w')). rewrite [cface _ _](eq_fconnect (glink_fp_skip_edge _)) ?fconnect_skip //. by rewrite /glink /= orbCA -val_eqE /= ee0 !eqxx. case: ifP => xRw; last exact: (same_cskip_edge (negbT _)). by apply: cskip_edge_merge; first rewrite /cross_edge /= bridge'G0. have ee2 w: edge (edge w) = w :> G2 by apply: Ih; rewrite !h_e ee0. have plainG2: plain G2. by apply/plainP => w _; split; rewrite // -(inj_eq Ih) h_e plain_neq. have geoG2: planar_bridgeless_plain_precubic G2. repeat split; auto; first exact (planar_WalkupF _ (planar_WalkupF _ geoG0)). apply/existsP=> [] [w wFew]. have [y xEy cycRwy]: exists2 y, cedge x y & cycle rlink [:: h w; y]. move: wFew; rewrite hF h_e /= bridge'G0. case: ifP => //; rewrite /xR /= !orbF => /orP[wFx | wFex]. rewrite cfaceC -(same_cface wFx) bridge'G0 /= => ewFex. by exists (edge x); rewrite ?fconnect1 /rlink //= ewFex ee0 cfaceC wFx. rewrite orbC cfaceC -(same_cface wFex) bridge'G0 /= => ewFx. by exists x; rewrite /rlink //= ewFx cfaceC wFex. case: (ring'cc [:: h w; y]); split => [||z]. - rewrite /scycle cycRwy simple_recI /=; have [ewRy _] := andP cycRwy. by rewrite unfold_in /= cfaceC -(same_cface ewRy) cfaceC bridge'G0. - by apply: contraTneq (codom_f h w) => Dy; rewrite Eh inE cedge1r Dy xEy. by rewrite !inE orbA => /eqP ->; rewrite -D_E0 xEy. apply/subsetP=> w _; apply: leq_trans (precubic_leq geoG0 (h w)). rewrite /order -(card_image Ih); apply/subset_leq_card/subsetP=> y. by case/imageP=> w1 wNw1 ->; rewrite inE -hN. pose cc1 := filter (predC (cedge x)) cc; pose cc2 := preim_seq h cc1. have Excc y: (y \in insertE (x :: cc)) = cedge x y || (y \in insertE cc1). rewrite /= !inE orbA -D_E0 !mem_insertE //; apply: orb_id2l=> xN'y. rewrite !(eq_has (plain_orbit geoG0 y)) !(has_sym [:: y; _]) /=. by rewrite !mem_filter !inE -cedge1r xN'y. have hcc2: map h cc2 = cc1. by apply: map_preim => y; rewrite Eh mem_filter => /andP[]. have hEcc1 w1: (h w1 \in insertE cc1) = (w1 \in insertE cc2). by rewrite !mem_insertE // -hcc2 has_map; apply: eq_has => w; rewrite /= hE. have le_cc2_cc: size cc2 <= size cc. by rewrite -(size_map h) hcc2 size_filter count_size. have{IHn} [] := IHn G2 cc2 geoG2 (leq_trans le_cc2_cc le_cc_n). - rewrite -card_S_Walkup card_Walkup (leq_trans (leq_pred _)) //. by rewrite (leq_trans G0_lenG) // leq_addl. - move=> p [URp nt_p cc_p] //. have [cycRp UpF] := andP URp; have Up := simple_uniq UpF. have UhpF: simple (map h p). rewrite /simple -map_comp map_inj_in_uniq // => w1 w2 pw1 pw2. move/(rootP cfaceC)=> w1Fw2; apply: (simple_cface UpF) pw1 pw2 _. by rewrite hF /xR (eq_has (same_cface w1Fw2)); case: (has _ _). have cc_hp: {subset map h (behead p) <= insertE cc}. move=> _ /mapP[w1 pw1 ->]. by have:= Excc (h w1); rewrite /= !inE orbA -D_E0 xE'h hEcc1 cc_p. suffices cycRhp: scycle rlink (map h p). have [] := ring'cc (map h p); split=> //. by case: (p) nt_p => [|w0 [|w1 [|w2 p2]]]; rewrite /= -?h_e. by rewrite behead_map => y /cc_hp cc_y; rewrite 2?mem_behead. apply: wlog_neg; rewrite UhpF andbT => cyc'Rhp. pose prevRh := [pred w | rlink (h (prev p w)) (h w)]. have{cyc'Rhp} /hasP[w1 pw1 /= prevRh'w1]: has (predC prevRh) p. rewrite has_predC; apply: contra cyc'Rhp => /allP cycRhp. rewrite cycle_from_prev ?map_inj_uniq // => _ /mapP[w1 pw1 ->]. by rewrite prev_map //; apply: cycRhp. have [i1 p1 Dp1] := rot_to pw1; pose w0 := last w1 p1. have p1'w1: w1 \notin p1 by move: Up; rewrite -(rot_uniq i1) Dp1 => /andP[]. have /andP[w0Rw1 w1Rp1]: rlink w0 w1 && path rlink w1 p1. by have:= cycRp; rewrite -(rot_cycle i1) Dp1 (cycle_path w1). have{prevRh'w1} hw0R'w1: ~~ rlink (h w0) (h w1). move: prevRh'w1; rewrite -(prev_rot i1) // prev_nth Dp1 mem_head. by rewrite -{2}[p1]cats0 index_cat (negPf p1'w1) addn0 nth_last. have /andP[xRew0 xRw1]: xR (edge (h w0)) && xR (h w1). by move: w0Rw1; rewrite /rlink hF h_e [cface _ _](negPf hw0R'w1). have /hasP[x1 xEx1 w1Fx1] := xRw1 : has _ [:: x; _]. have /hasP[x0 xEx0 ew0Fx0] := xRew0 : has _ [:: x; _]. have ex0_x1: edge x0 = x1. have: cedge x0 x1. by rewrite -!plain_orbit // in xEx0 xEx1; rewrite -(same_cedge xEx0). rewrite plain_orbit // !inE => /pred2P[] // x01. by rewrite /rlink (same_cface ew0Fx0) -x01 cfaceC w1Fx1 in hw0R'w1. pose q1 := x0 :: (map h (w1 :: p1)). have p1R'x: ~~ has (preim h xR) p1. apply: contra p1'w1 => /hasP[w2 p1w2 /= xRw2]. have w1Fw2: cface w1 w2 by rewrite hF xRw1. by rewrite (scycle_cface URp _ _ w1Fw2) // -(mem_rot i1) Dp1 mem_behead. have cycRq1: cycle rlink q1. rewrite (cycle_path x0) /= {1 2}/rlink last_map ew0Fx0 ex0_x1 cfaceC w1Fx1. elim: (p1) (w1) p1R'x w1Rp1 => //= w3 p2 IHp w2 /norP[xR'w3 xR'p2] /andP[]. by rewrite {1 3}/rlink cfaceC hF (negPf xR'w3) cfaceC h_e => -> /IHp->. case Dp: p => // [w p0] in nt_p. have /rot_to[i2 q2 Dq2]: h w \in q1. by rewrite /q1 -Dp1 inE mem_map // mem_rot Dp mem_head orbT. have URq2: scycle rlink (h w :: q2). rewrite -Dq2 /scycle rot_cycle cycRq1 /= simple_rot /q1 simple_cons. apply/andP; split; last by rewrite -Dp1 /= map_rot simple_rot. rewrite unfold_in; apply: contra p1R'x => /hasP[x3]. rewrite /= inE -has_map => /predU1P[-> /idPn[] | p1x3 x0Fx3]. by rewrite cfaceC (same_cface w1Fx1) -ex0_x1 cfaceC bridge'G0. by apply/hasP; exists x3 => //=; apply/hasP; exists x0; rewrite // cfaceC. case: (ring'cc (h w :: q2)); split=> //. move: nt_p; rewrite -Dp -Dq2 proper_ring_rot // -(proper_ring_rot i1) //. by rewrite Dp1 /q1 /=; case: (p1). move=> y q2y; rewrite /= !inE orbA -mem_seq2. move: (mem_behead q2y); rewrite -Dq2 mem_rot /q1 -Dp1 /= inE map_rot mem_rot. move/predU1P=> [->|]; first by rewrite xEx0. rewrite Dp /= inE (negPf (memPn _ y q2y)) => [/mapP[u p0u ->]|]. by rewrite orbC cc_hp // map_f // Dp. by case/andP: URq2 => _ /simple_uniq/andP[]. move=> k [kE /fconnect_invariant kF]. pose a y := [pred w | cface y (h w)]. have nt_ah w: ~ a (h w) =1 pred0 by move/(_ w); rewrite /= connect0. have ae0 y: a y =1 pred0 -> a (edge y) =1 pred0. move=> ay0 w; have [hy | h'y] := boolP (y \in codom h). by case/idP: (ay0 (iinv hy)); rewrite /= f_iinv connect0. have [hfy | h'fy] := boolP (face y \in codom h). by case/idP: (ay0 (iinv hfy)); rewrite /= f_iinv fconnect1. move: h'y h'fy; rewrite !Eh !negbK => /same_cedge xEy. rewrite xEy plain_orbit // mem_seq2 orbC => /pred2P[fy_ey | fy_y]. by have:= bridge'G0 y; rewrite -fy_ey fconnect1. move: (precubic_leq geoG0 y) (f_finv nodeI y); rewrite /finv. rewrite -[_ <= 3](mem_iota 0 4) !inE -{1}orderSpred /=. case/or3P=> /eqP-> /= => [ny_y | nny_y | n3y_y]; last 1 first. - have:= bridge'G0 (face (edge y)); rewrite -{2}(canRL nodeK n3y_y). by rewrite 2!cface1r nodeK -{2}fy_y -{2}[y]ee0 edgeK connect0. - by have:= bridge'G0 y; rewrite -{1}[y]nodeK ny_y -cface1 connect0. have cycFy1: fcycle face [:: edge y]. by rewrite /= -(canRL nodeK nny_y) (canF_eq nodeK) ee0 fy_y eqxx. rewrite (fconnect_cycle cycFy1) ?inE ?eqxx //. by move: (xE'h w); rewrite xEy plain_orbit // mem_seq2 => /norP[_ /negPf]. pose k0 y := oapp k Color0 (pick (a y)). have k0h w: k0 (h w) = k w. rewrite /k0; case: pickP => [w1 /= wFw1 | /nt_ah//]; apply: kF. by rewrite hF cfaceC wFw1 /xR (eq_has (same_cface wFw1)); case: (has _ _). have k0ex: k0 x = k0 (edge x). rewrite /k0; case: pickP => [w /= wFx | /ae0 aex0]; last first. by case: pickP => // w1; rewrite aex0. case: pickP => /= [w1 w1Fex | /ae0/(_ w)]; last by rewrite ee0 /= wFx. by apply: kF; rewrite hF /xR /= cfaceC wFx /= orbCA cfaceC w1Fex. exists k0; split=> y; last first. by apply/eqP; rewrite /k0 -(@eq_pick _ (a y)) // => w /=; rewrite cface1. rewrite Excc !inE /invariant in kE *. have [] := boolP (cedge x y). by rewrite plain_orbit // mem_seq2 => /pred2P[]->; rewrite ?ee0 -k0ex eqxx. by rewrite -[~~ _]Eh => hy; rewrite -(f_iinv hy) -h_e !k0h [_ == _]kE hEcc1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap walkup geometry color coloring patch) fourcolor(snip revsnip birkhoff)