proposition: Lemma plane_add_edge (G : sgraph) (g : plane_embedding G) (x y : G) (s1 s2 : seq G) : let s := x :: s1 ++ y :: s2 in x != y -> sface g s -> exists2 g' : plane_embedding (add_edge x y), sface g' [:: y, x & s1] & sface g' [:: x,y & s2].
proof: Proof. move=> s xDy sface_xy. case: sface_xy => dx E. set o := orbit face dx in E. pose dy := nth dx o (size s1).+1. have lt_size_o : (size s1).+1 < size o. { by rewrite -[size o](size_map g) -E /s -cat_cons size_cat /= addnS addSn !ltnS leq_addr. } have g_y : g dy = y. { rewrite /dy -(nth_map _ x) -?E //. by rewrite /s -cat_cons nth_cat ltnn subnn. } have g_x : g dx = x. { by move: E; rewrite /o/orbit/s -orderSpred/=; case => -> _. } have dxDdy : dx != dy. { by apply: contra_neq xDy => dxy; rewrite -g_x dxy g_y. } have dx_dy : cface dx dy by rewrite fconnect_orbit mem_nth //. set D := emb_map g in dx o E dy g_x lt_size_o g_y dxDdy dx_dy . pose D' := h_add_edge dxDdy. pose g' (d : D') : add_edge x y := match d with IcpX => x | IcpXe => y | Icp z => g z end. have [plain_D surj_g vertex_g edge_g] := emb_embedding g. have plain_D' : plain D' by apply: add_edge_plain. have embedding_g' : embedding g'. { split => //. - move=> z. have [dz ->] := codomP (surj_g z). by apply/codomP; exists (Icp dz). - have ? := @nodeI D'. have cnode_Icp := add_edge_cnodeE dxDdy. have fD' : add_edge_node dx dy = @node D' by []. move => [||d1] [||d2]; rewrite /= ?connect0 ?eqxx //= ?fD'. 1,3: by rewrite ?[cnode _ (IcpX : D')]cnodeC add_edge_cnodeXXe vertex_g g_x g_y ?[y == x]eq_sym. all: rewrite -?g_x -?g_y. 1-2: rewrite ?[_ _ IcpX](@cnodeC D') //. 1-2: rewrite (@cnode1 D'). 3-4: rewrite (@cnode1r D'). 1-5: by rewrite cnode_Icp -?cnode1 -?cnode1r. - have adjn_Icp := @add_edge_adjn D _ _ dxDdy. pose m (d : D') := match d with IcpX => 1 | IcpXe => 2 | _ => 0 end. move => d1 d2; wlog: d1 d2 / m d1 <= m d2 => [W|]. { have [|/ltnW] := leqP (m d1) (m d2); first exact: W. rewrite sg_sym adjnC //. exact: W. } have dxdyF : cnode dx dy = false by rewrite vertex_g g_x g_y (negbTE xDy). move: d1 d2 => [||d1] [||d2] // _ ; rewrite /= ?sg_irrefl. + by rewrite adjn_node1 adjn_node1r /= adjn_Icp edge_g sg_irrefl -!cnode1 dxdyF. + by rewrite /edge_rel/= (negbTE xDy) !eq_refl orbT adjn_edge. + rewrite adjn_node1 adjn_node1r /= adjn_Icp edge_g sg_irrefl. by rewrite -!cnode1 cnodeC dxdyF. + rewrite adjn_node1r /= adjn_Icp -!cnode1 -adjn_node1r. rewrite dxdyF connect0 andbF andbT /=. rewrite edge_g [RHS]/edge_rel/= g_x (negbTE xDy) !andbF eqxx /=. by apply:orb_id2l => _; rewrite vertex_g g_y andb_idl // => /eqP->. + rewrite adjn_node1r /= adjn_Icp -!cnode1 -adjn_node1r [cnode dy dx]cnodeC. rewrite dxdyF connect0 andbF andbT /= edge_g [RHS]/edge_rel/=. rewrite [y == x]eq_sym eqxx (negbTE xDy) !andbF !orbF !andbT g_y. by apply:orb_id2l => _; rewrite vertex_g g_x andb_idl // => /eqP->. + rewrite adjn_Icp [RHS]/edge_rel/= edge_g !vertex_g g_x g_y. apply: orb_id2l => _; rewrite ?[x == _]eq_sym ?[y == _]eq_sym. rewrite ![(_ != _) && _]andb_idl ?[(g d2 == x) && _]andbC //. all: by move=> /andP[/eqP-> /eqP->]. } have planar_D := emb_planar g. have planar_D' : planar D' by apply: add_edge_planar. have [o' def_o] := orbit_case face dx; rewrite -/o in def_o. have dy_o' : dy \in o'. { by have := mem_nth dx lt_size_o; rewrite -/dy def_o inE eq_sym (negbTE dxDdy). } pose o1 := take (index dy o') o'; pose o2 := drop (index dy o').+1 o'. have size1 : size s1 = size o1. { rewrite /o1 size_take index_mem dy_o' /dy def_o /= index_uniq //. - by rewrite -ltnS -[(size o').+1]/(size (dx::o')) -def_o. - apply: subseq_uniq (orbit_uniq face dx). rewrite -/o def_o. exact: subseq_cons. } have [def_s1 def_s2 def_o'] : [/\ s1 = [seq g d | d <- o1], s2 = [seq g d | d <- o2] & o' = o1 ++ dy :: o2]. { move: size1 E. rewrite def_o /o1 /o2 /s. case/splitP : _ _ _ / dy_o' => [p1 p2 _] size1 /=. move/eqP; rewrite g_x eqseq_cons eqxx -cats1 -catA /= map_cat /=. by rewrite eqseq_cat ?size_map // eqseq_cons g_y eqxx /= => /andP[/eqP-> /eqP->]. } rewrite def_o' in def_o; exists (Build_plane_embedding embedding_g' planar_D'). - exists (IcpXe) => /=. rewrite add_edge_orbitXe //= -/o. rewrite def_o left_arc -?def_o ?orbit_uniq //= -map_comp g_x /=. by rewrite (@eq_map _ _ _ g) // def_s1. - exists (IcpX) => /=. rewrite add_edge_orbitX //= -/o. rewrite def_o right_arc -?def_o ?orbit_uniq //= -map_comp g_y /=. by rewrite (@eq_map _ _ _ g) // def_s2. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry color coloring walkup combinatorial4ct cfmap) GraphTheory(edone preliminaries bij digraph sgraph) GraphTheory(connectivity minor hmap_ops smerge hcycle arc)