proposition: Lemma cpmask_adj cp cm : config_prog cp -> proper_cpmask cp cm -> forall x, (x \in fband (cpmask (cpadj cm cp) cp)) = has (adj x) (cpmask cm cp).
proof: Proof. have cpW p: config_prog p -> nilp p || config_prog p by rewrite orbC => ->. rewrite /cpmask => /cpW; elim: cp cm => [|s cp IHcp] [mr mk] cp_ok /= m_ok u. rewrite cpring0 /adj orbit_id has_predU unfold_in !(eq_has (fconnect_id _)). by case: mr mk u m_ok => [|[] [|[] []]] // [] // []. rewrite orFb in cp_ok; case: s => // [n||] in u cp_ok m_ok *. - set cm := Cfmask _ mk; have [/eqP Emr _] := andP m_ok. have {}m_ok: proper_cpmask cp cm by rewrite /= size_rotr. move: (cpadj_proper m_ok) {IHcp}(IHcp cm (cpW cp cp_ok) m_ok). case: (cpadj cm cp) => mr' mk' /andP[/eqP Emr' _] IHm. rewrite -(size_rotr n) -size_ring_cpmap in Emr. rewrite cpring_ecpR fband_cat has_cat -(rotrK n mr). rewrite (eq_has_r (mem_mask_rot n Emr)) /= -has_cat -IHm fband_cat. congr (_ || _); apply: eq_has_r; apply: mem_mask_rot. by rewrite size_ring_cpmap. - have [cpQ cp'ok]: cubic_prog cp /\ nilp cp || config_prog cp. by case: (cp) cp_ok => // a cp1 cp1ok ; rewrite config_prog_cubic. have Ggt1 := cpmap_proper cpQ; set G := cpmap cp in Ggt1 u *. have{cpQ} plainGY := plain_ecpY G (cpmap_plain cpQ). have [[/eqP Emr _] nXFnG] := (andP m_ok, cface_node_ecpY G). have: 2 < size mr by rewrite Emr -size_ring_cpmap ltnS -size_proper_cpring. case: mr => [|b0 [|b1 [|b2 mr]]] // in m_ok Emr * => _. set cm := Cfmask _ mk; have{m_ok} cm_ok: proper_cpmask cp cm by []. have{IHcp cp'ok cp_ok} [] := (cpmap_simple cp_ok, IHcp cm cp'ok cm_ok). case: (cpadj _ _) (cpadj_proper cm_ok) => mr' mk' /andP[]. case: Emr mr' => <- [|a0 [|a2 mr']] // _ _; rewrite [cpker _]/= cpring_ecpY. rewrite -/G {cm_ok}/cm head_proper_cpring // /behead map_cons. have [[x uFx] _ /(_ x)IHx | XFu simpleGY _] := fband_icpY u; last first. rewrite -(eq_has (adjF XFu)) (eq_has (adj_ecpY Ggt1)) has_cat. rewrite !has_mask_cons !unfold_in -(eq_has (same_cface XFu)). rewrite !(eq_has (@cface_ecpY _ _)) has_cat !has_mask_cons mem_head !andbF. rewrite -!map_mask 2!has_map !has_pred0 /= connect0 nXFnG orbT !andbT. rewrite -!orbA -has_cat -map_cat orbF; congr [|| _, _ | _]; symmetry. have:= simpleGY; rewrite [cpker _]/= 2!cat_cons (simple_catCA [::_] [::_]). rewrite 2!simple_cons (closed_connect (fbandF _) nXFnG) => /andP[_]. rewrite -simple_cons -cat_cons -!map_cons -cat1s -cat_rcons -map_cat. rewrite -catA map_cat simple_cat andbA andbAC !has_map => /andP[_]. apply: contraNF => /hasP[v X'v XFv]; apply/hasP; exists v => {XFv}//. by move: X'v; rewrite !mem_cat => /orP[]/mem_mask->; rewrite ?orbT. rewrite (eq_has (adjF uFx)) unfold_in {u uFx}(eq_has (same_cface uFx)). rewrite !has_cat !has_mask_cons (same_connect_r cfaceC nXFnG) !cface_icpY. rewrite (adjFr nXFnG) !adj_icpY -(cfaceC (ecpY G)) cface_ecpY andbF orFb. rewrite (adjC plainGY) (adj_ecpY Ggt1) -!map_mask unfold_in !has_map. rewrite !(eq_has (cface_icpY G x)) !(eq_has (adj_icpY G x)) -!(orbC b1). have:= IHx; rewrite unfold_in !has_cat !has_mask_cons /= -(orbCA (b1 && _)). by case: b1 => //=; do 2!case: (cface x _) => //; rewrite !andbF. have [simpleGH [/eqP Emr Emk]] := (cpmap_simple cp_ok, andP m_ok). rewrite /= in cp_ok; have cpQ := config_prog_cubic cp_ok. have [Ggt1 Ggt2] := (cpmap_proper cpQ, cfmap_long cp_ok). set G := cpmap _ in Ggt1 Ggt2 u *; have nXFnG := cface_node_ecpH Ggt1. have{cpQ} plainGH := plain_ecpH G (cpmap_plain cpQ). have: 2 < size mr by rewrite Emr -size_ring_cpmap -size_long_cpring. case: mk Emk mr => // b1' mk _ [|b0 [|b1 [|b2 mr]]] // in m_ok Emr * => _. set cm := Cfmask _ mk; have{m_ok} cm_ok: proper_cpmask cp cm by []. have{IHcp cpW cp_ok simpleGH} [] := (simpleGH, IHcp _ (cpW _ cp_ok) cm_ok). rewrite [cpker _]/= cpring_ecpH // (head_long_cpring Ggt2) [drop 2 _]/=. case: (cpadj _ _) {cm_ok}(cpadj_proper cm_ok) => mr' mk' /andP[]. rewrite -{}Emr {}/cm; case: mr' => [|a0 [|a1 [|a2 mr']]] // _ _. have [[x uFx] _ /(_ x)IHx | XFu simpleG _] := fband_icpH u; last first. rewrite -(eq_has (adjF XFu)) (eq_has (adj_ecpH Ggt1)) has_cat map_cons. rewrite !has_mask_cons !unfold_in -(eq_has (same_cface XFu)). rewrite has_cat !has_mask_cons connect0 (same_connect_r cfaceC nXFnG). rewrite !(cface_ecpH Ggt1) !(eq_has (cface_ecpH Ggt1)) !andbF. rewrite -!map_mask 2!has_map !has_pred0 /= !connect0 nXFnG !orbT !andbT. rewrite -!orbA -!(orbCA b1') -has_cat orbF !orbA; congr (_ || _); symmetry. have:= simpleG; rewrite (simple_catCA _ [:: _]) catA map_cons !cat_cons. rewrite (simple_catCA [:: _; _] [:: _]) -!map_cat simple_cons => /andP[_]. rewrite (simple_catCA [:: _] [:: _]) -cat_rcons simple_cons. rewrite (closed_connect (fbandF _) nXFnG) -simple_cons -cat_cons. rewrite simple_cat !has_map andbA andbAC => /andP[_]. apply: contraNF => /hasP[v X'v XFv]; apply/hasP; exists v => {XFv}//. by move: X'v; rewrite !mem_cat => /orP[]/mem_mask->; rewrite ?orbT. rewrite (eq_has (adjF uFx)) unfold_in {u uFx}(eq_has (same_cface uFx)). rewrite !has_cat map_cons !has_mask_cons (same_connect_r cfaceC nXFnG). rewrite !cface_icpH (adjFr nXFnG) !adj_icpH -(cfaceC (ecpH G)) cface_ecpH //. rewrite andbF (adjC plainGH) (adj_ecpH Ggt1) unfold_in -!map_mask !has_map. rewrite !(eq_has (cface_icpH G x)) !(eq_has (adj_icpH G x)) {3}/has. move: IHx; rewrite unfold_in !has_cat !has_mask_cons -!orbA -!(orbC b1). rewrite -!(orbCA (b1' && _)) -2!(orbCA ((b1 || a1) && _)) -!(orbCA (b1 && _)). by case: b1 => //=; do 3?case: (cface x _) => //; rewrite !andbF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)