proposition: Lemma cpcolor0_correct cp : @cp_extcol cp [::] (fun _ => cpcolor0 cp) (ccons true).
proof: Proof. set cp2 := [::]; set G := cpmap cp2; set k : G -> color := ccons true. have dG: cpmap [::] = G :> hypermap by []. have tr_k: trace (map k (cpring G)) = [:: Color1; Color1] by rewrite cpring0. have col_k: coloring k by split; case. elim: cp => [|s cp1 IHcp] in (cp2) G (k) col_k tr_k dG *. by case: (cpcolor1_correct [::] col_k); rewrite tr_k. case: (cpcolor1_correct (s :: cp1) col_k); rewrite tr_k. have ringG: cpring G = [:: node G; G : G]. by case: _ / dG (G : G) => b; apply: cpring0. have k_nG: k (node G) = Color1 +c (k G). by move: tr_k; rewrite ringG => [] [<-]; rewrite addcK. have GF'nG: cface (node G) G = false. by case: _ / dG (G : G); case; rewrite fconnect_id. have G'nG: (node G == G :> G) = false by case: _ / dG (G : G); case. have GnG x: x = G :> G \/ x = node G. by apply/pred2P; case: _ / dG (G : G) x; do 2!case. case: s => // [n||]. - have [] // := IHcp (CpR n :: cp2) k. by rewrite cpring_ecpR map_rot trace_rot tr_k; case: n => [|[|[]]]. - pose k' u := if cface u (ecpY G) then Color2 else if cface u (icpY G G) then Color0 else Color3. have dF (u v : ecpY G): cface u v = (v \in [:: u; face u]). apply: fconnect_cycle (mem_head u _) v. by case: _ / dG (G : G) u; do 4?case. have /= <-: trace (map k' (cpring (ecpY G))) = [:: Color1; Color2; Color3]. by rewrite cpring_ecpY ringG /= /k' !dF; case: _ / dG (G : G); do 3?case. have k'F: invariant face k' =1 ecpY G. by move=> u; apply/eqP; rewrite /k' -!cface1. have k'col: coloring k'. by split=> // u; rewrite /= /k' !dF; case: _ / dG (G : G) u; do 6?case. have [et et_ok etP] := @cpcolor1_correct cp1 (CpY :: cp2) _ k'col. rewrite [cpmap _ ]/= -/G in et et_ok etP; split=> {et_ok}//. apply: {etP}(iffP etP) => [] [k0 k0ccol /(_ _)/=Dk0]. pose h0 := locked Eperm231. exists (fun x => k G +c h0 (k0 x)) => [|x]; first exact: gcol_perm. rewrite /= Dk0 /k' cfaceC dF cface_icpY /= addcC; unlock h0. by have [-> | ->] := GnG x; [rewrite connect0 add0c | rewrite GF'nG]. pose e0 := k G +c k0 (@injcp cp1 (CpY :: cp2) (ecpY G)). pose h0 := if e0 == Color2 then Eperm321 else Eperm312. exists (fun x => h0 (k G) +c h0 (k0 x)) => [|u]; first exact: gcol_perm. have [/= k0col _] := k0ccol; rewrite -permc_addc /k'. have [[x uFx] | XFu] := @fband_icpY G G u. rewrite !(same_cface uFx) cfaceC dF (gcol_cface k0col uFx) Dk0 cface_icpY. have [-> | ->] := GnG x; first by rewrite addcc permc0 connect0. by rewrite GF'nG k_nG addcC addcK /h0; case: ifP. rewrite cfaceC XFu -(gcol_cface k0col XFu) -/e0 {}/h0. have /(gcol_adj k0col)/and3P[]:= adj_ecpY (coloring_proper_cpring G col_k). by rewrite !Dk0 -!(addc_eq0 (k _)) k_nG -addcA -/e0; case: e0. pose k' e u := if u == ecpU G :> ecpU G then Color1 else if u == icpU G G then e else Color0. have k'F e: invariant face (k' e) =1 ecpU G. by rewrite /k'; case: _ / dG e (G : G); do 4?case. have k'col e: e != Color0 -> coloring (k' e). by case: e; split=> //; rewrite /k'; case: _ / dG (G : G); do 3?case. have Ek' e: trace (map (k' e) (cpring (ecpU G))) = [:: Color1; Color1; e; e]. by rewrite cpring_ecpU ringG /= /k'; case: _ / dG e (G : G); do 3?case. have [] := @cpcolor1_correct cp1 (CpU :: cp2) _ (k'col Color2 isT). have{k'col} [] := @cpcolor1_correct cp1 (CpU :: cp2) _ (k'col Color1 isT). rewrite [cpmap _]/= -/G /cpcolor0 !{}Ek' => t1ok t1P t2ok t2P. split; first exact: ctree_union_proper. rewrite {t1ok t2ok}(ctree_mem_union (ttail et0) t2ok t1ok); apply: (iffP orP). case=> [/t2P | /t1P] [k0 k0ccol /(_ _)/=Dk0]. exists (fun x => k (node G) +c Eperm213 (k0 x)); first exact: gcol_perm. move=> x; rewrite /= Dk0 /k' /= (inj_eq (@ecp_inj _)) addcC. by have [-> | ->] := GnG x; [rewrite eqxx k_nG addKc | rewrite G'nG add0c]. exists (fun x => k (node G) +c Eperm123 (k0 x)); first exact: gcol_perm. move=> x; rewrite /= Dk0 /k' /= (inj_eq (@ecp_inj _)) addcC. by have [-> | ->] := GnG x; [rewrite eqxx k_nG addKc | rewrite G'nG add0c]. case=> k0 k0ccol /(_ _)/=Dk0; rewrite -/G in k0 k0ccol Dk0. have [/=k0col _] := k0ccol. pose e0 := k (node G) +c k0 (@injcp cp1 (CpU :: cp2) (ecpU G)). have nz_e0: e0 != Color0. by rewrite addc_eq0 -Dk0; case/andP: (gcol_adj k0col (@adj_ecpU _ _)). have [e01 | n1_e0] := eqVneq e0 Color1. right; apply/t1P; exists (fun w => k (node G) +c Eperm123 (k0 w)) => [|u]. exact: gcol_perm. have [[x uFx] | XFu] := fband_icpU u. rewrite (fconnect_invariant (k'F _) uFx) /= (gcol_cface k0col uFx) Dk0. rewrite /k' (inj_eq (@ecp_inj _)) /=. by have [-> | ->] := GnG x; [rewrite eqxx k_nG addcK | rewrite G'nG addcc]. rewrite -(fconnect_invariant (k'F _) XFu) /= -(gcol_cface k0col XFu) /k'. by rewrite eqxx. left; apply/t2P; pose h0 := if e0 == Color2 then Eperm213 else Eperm231. exists (fun w => h0 (k (node G)) +c h0 (k0 w)); first exact: gcol_perm. move=> u; rewrite /= -permc_addc; have [[x uFx] | XFu] := fband_icpU u. rewrite (fconnect_invariant (k'F _) uFx) /= (gcol_cface k0col uFx) Dk0. rewrite /k' (inj_eq (@ecp_inj _)) /=. have [-> | ->] := GnG x; last by rewrite G'nG addcc permc0. by rewrite eqxx k_nG addcK /h0; case: ifP. rewrite -(fconnect_invariant (k'F _) XFu) /= -(gcol_cface k0col XFu) /k' -/e0. by rewrite {}/h0; case: e0 nz_e0 n1_e0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree)