proposition: Proposition wagner3 (G : sgraph) : 3.-connected G -> kplanar G -> inhabited (plane_embedding G).
proof: Proof. elim/card_ind : G => G IH conn_G kplanar_G. have [le_5_G|le_G_4] := (ltnP 4 #|G|); last first. { suff i : diso 'K_4 G. by exists; apply: diso_plane_embedding i; apply: K4_plane_emb. have/eqP -> : 4 == #|G| by rewrite eqn_leq le_G_4 (proj1 conn_G). by apply/diso_sym/diso_Kn; apply: kconnected_complete le_G_4. } have [x [y [xy conn_G1]]] := contract_three_connected le_5_G conn_G. set G1 := smerge2 G x y in conn_G1. have kplanar_G1 := kplanar_minor (smerge2_minor xy) kplanar_G. have [|g1] := IH G1 _ conn_G1 kplanar_G1. by rewrite card_sig [X in _ < X](@cardD1x _ _ y). wlog simple_g1 : g1 / simple_hmap (emb_map g1). { move => W; have [g1'] := simple_embedding g1; exact: W. } have xDy : x != y by rewrite (sg_edgeNeq xy). pose v_xy : G1 := Sub x xDy. pose G2 := induced [set~ v_xy]. have conn_G2 : 2.-connected G2 by apply/konnected_del1. have G2Dx (u : G2) : val2 u != x. { by apply: contraTneq (valP u); rewrite !inE negbK -val_eqE -/(val2 _) => ->. } have conn2_G1 : 2.-connected G1 by apply: (@kconnectedW 1); rewrite addn1. pose g2 := @del_vertex_plane_embedding _ g1 v_xy conn2_G1 simple_g1. have := @del_vertex_neighbor_face G1 g1 v_xy conn2_G1 simple_g1. rewrite -/G2 -/g2; case => [s2 face_s2 neighb_s2]. pose X : seq G2 := [seq z <- s2 | x -- val2 z]. pose Y : seq G2 := [seq z <- s2 | y -- val2 z]. have uniq_s2 : uniq s2 by apply:face_uniq face_s2. have uniq_X : uniq X by apply: filter_uniq. have uniq_Y : uniq Y by apply: filter_uniq. have degG (z : G) : 3 <= #|N(z)| by apply: kconnected_degree. have inG2P u (uDx : u != x) (uDy : u != y) : Sub u uDy \in [set~ v_xy]. by rewrite !inE -val_eqE. have eq_X : val2 @: X =i N(x) :\ y. { move=> z; rewrite !inE. apply/imsetP/andP => [[z0 z0X -> {z}]|[zDy xz]]. move: z0X; rewrite mem_filter => /andP[-> _]; by rewrite (valP (val z0)). have zDx : z != x by apply: contraTneq xz => ->; rewrite sgP. exists (Sub (Sub z zDy) (inG2P _ zDx zDy)) => //. rewrite /X mem_filter /= xz /= -(@mem_map G2 G1 val) //=. by apply: neighb_s2; rewrite /= inE /edge_rel/= eqxx zDx sg_sym xz. } have sizeX : 1 < size X. { rewrite -(card_uniqP _) // -!(card_imset _ val_inj) -imset_comp. rewrite (eq_card eq_X). apply: leq_trans (leq_cardsD1 _ _). rewrite -ltnS; apply: leq_trans (degG x) _. exact: leqSpred. } have eq_Y : val2 @: Y =i N(y) :\ x. { move=> z; rewrite !inE. apply/imsetP/andP => [[z0 z0X -> {z}]|[zDx yz]]. by move: z0X; rewrite mem_filter => /andP[-> _]. have zDy : z != y by apply: contraTneq yz => ->; rewrite sgP. exists (Sub (Sub z zDy) (inG2P _ zDx zDy)) => //. rewrite /Y mem_filter /= yz -(@mem_map G2 G1 val) //. by apply: neighb_s2; rewrite /= inE /edge_rel/= eqxx zDx [z -- y]sgP yz orbT. } have sizeY : 1 < size Y. { rewrite -(card_uniqP _) //; rewrite -!(card_imset _ val_inj) -imset_comp. rewrite (eq_card eq_Y). apply: leq_trans (leq_cardsD1 _ _). rewrite -ltnS; apply: leq_trans (degG y) _. exact: leqSpred. } have v2 : G2 by move: sizeX; destruct X. pose inG2 (u : G) : G2 := insubd v2 (insubd v_xy u). have inG2E u (uDx : u != x) (uDy : u != y) : inG2 u = Sub (Sub u uDy) (inG2P _ uDx uDy) :> G2. { rewrite /inG2 !insubdT ?inG2P // => p. exact: val_inj. } have inG2K (u : G2) : inG2 (val (val u)) = u. { rewrite inG2E ?(valP (val u)) // ?G2Dx // => p q. by do 2 apply: val_inj. } have [x1 x1_X Y_segment] : exists2 x1, x1 \in X & {subset Y <= rcons (arc s2 x1 (next X x1)) (next X x1) }. { pose s := [seq val x | x <- [seq val x | x <- s2]]. have uniq_s : uniq s by rewrite !map_inj_uniq //; exact: val_inj. have xNs : x \notin s. by apply/negP => /mapP [? /mapP [x0] _ ->] /eqP; apply/negP; rewrite eq_sym G2Dx. have yNs : y \notin s. { apply/negP => /mapP [? /mapP [y0 _ ->]] /eqP. by apply/negP; rewrite eq_sym (valP (val y0)). } have ucycle_s : ucycle (--) s. { apply: smerge2_ucycle xNs. rewrite -ucycle_induced /ucycle uniq_s2 andbT. exact: sface_cyle face_s2. } pose X' := [seq z <- s | x -- z]. pose Y' := [seq z <- s | y -- z]. have size_X' : 2 <= #|X'|. { suff -> : X' = map val (map val X). by rewrite (card_uniqP _) ?map_inj_uniq // !size_map. by rewrite /X'/s/X !filter_map. } have size_y' : 2 <= #|Y'|. { suff -> : Y' = map val (map val Y). by rewrite (card_uniqP _) ?map_inj_uniq // !size_map. by rewrite /Y'/s/Y !filter_map. } have [z Z1 Z2] := wagner_no_cross kplanar_G ucycle_s xy xNs yNs size_X' size_y'. rewrite -/X' -/Y' in Z2. move: Z1; rewrite mem_filter => /andP [xz z_s]. have zDy : z != y by apply: contraTneq z_s => ->. have zDv : (Sub z zDy : G1) \in [set~ v_xy] by rewrite !inE -val_eqE /= eq_sym sg_edgeNeq. pose x1 := Sub (Sub z zDy) zDv : G2. exists x1. - rewrite mem_filter /= xz //=. by move: z_s; rewrite -[z]/(val (val x1)) !mem_map. - move => u u_Y. rewrite -(@mem_map _ _ val2); last exact: val2_inj. rewrite map_rcons map_arc 1?map_comp -/s -!/(val2 _); last exact: val2_inj. rewrite -next_map; last exact: val2_inj. have -> : map val2 X = X' by rewrite /X' /s !filter_map /= -map_comp. apply: Z2. move: u_Y. rewrite !mem_filter => /andP[->] /=. by rewrite /s /val2 !mem_map. } set x2 := next X x1 in Y_segment. have x2_X : x2 \in X by rewrite mem_next. have x1Dx2 : x1 != x2 by apply next_neq. have [x1_s1 x2_s2] : x1 \in s2 /\ x2 \in s2. split; [exact: sub_filter x1_X|exact: sub_filter x2_X]. have [] := @plane_add_node' _ g2 x2 x1 s2 [set z in X] => //. - by rewrite eq_sym. - by move=> z; rewrite inE; apply: arc_remainder => //; exact: filter_subseq. - by rewrite inE. - by rewrite inE. - move => g' face_g'. set G' := add_node G2 _ in g' face_g'. set s2' := (Some _ :: _ : seq G') in face_g'. pose Y' : {set G'} := None |: Some @: [set z in Y]. have [||g''] := @plane_add_node_simple G' g' _ Y' None _ face_g'. + by rewrite in_setU1 eqxx. + move=>z; rewrite !inE => /predU1P [->|/imsetP [z0]]; first by rewrite eqxx. rewrite !inE => /Y_segment. rewrite mem_rcons inE => /predU1P [-> -> //|z_arc ->]; first by rewrite eqxx. rewrite mem_map ?z_arc //; exact: Some_inj. + suff i: diso (add_node G' Y') G by exists; apply: diso_plane_embedding g'' i. set G'' := add_node _ _. pose fwd (x0 : G'') : G := if x0 isn't Some z0 then y else if z0 isn't Some z then x else val2 z. pose bwd (x0 : G) : G'' := if x0 == y then None else if x0 == x then Some None else Some (Some (inG2 x0)). have can_fwd : cancel fwd bwd. { move => [[x0|]|]; rewrite /bwd ?eqxx ?(negPf xDy) //. by rewrite (negbTE (valP (val x0))) (negbTE (G2Dx x0)) inG2K. } have can_bwd : cancel bwd fwd. { move=> u. rewrite /fwd/bwd. have [-> //|yDu] := eqVneq u y; have [-> //|xDu] := eqVneq u x. by rewrite inG2E. } have dhom_fwd : is_dhom fwd. { move => [[u|]|] [[v|]|] //=. - move => uv. by rewrite (@smerge2_val_edge _ x y) ?induced_edge //; exact: G2Dx. - by rewrite {1}/edge_rel/={1}/edge_rel/= inE mem_filter sgP => /andP[-> _]. - by rewrite {1}/edge_rel/= !(inE, mem_imset) // orFb mem_filter sgP => /andP[-> _]. - by rewrite {1}/edge_rel/={1}/edge_rel/= inE mem_filter => /andP[-> _]. - by rewrite {1}/edge_rel/= !(inE, mem_imset) // orFb mem_filter => /andP[-> _]. - by rewrite [y -- x]sgP. } have inG2Y u : u != x -> u != y -> u -- y -> inG2 u \in Y. { move=> uDx uDy uy. rewrite inG2E -!(@mem_imset _ _ val) // -imset_comp eq_Y /=. by rewrite !inE uDx sgP. } have inG2X u : u != x -> u != y -> u -- x -> inG2 u \in X. { move=> uDx uDy uy. rewrite inG2E -!(@mem_imset _ _ val) // -imset_comp eq_X /=. by rewrite !inE uDy sgP. } have dhom_bwd : is_dhom bwd. { move => u v uv; rewrite /bwd. have [?|uDy] := eqVneq u y; first subst u. have [E|vDy] := eqVneq v y; first by rewrite E sgP in uv. have [?|vDx] := eqVneq v x; first by rewrite /edge_rel/= !inE eqxx. by rewrite /edge_rel/= inE mem_imset // !inE inG2Y 1?sgP. have [?|uDx] := eqVneq u x;first subst u. have [E|vDx] := eqVneq v x; first by rewrite E sgP in uv. have [?|vDy] := eqVneq v y; first by rewrite /edge_rel/= !inE eqxx. by rewrite /edge_rel/= /edge_rel/= inE inG2X 1?sgP. have [?|vDy] := eqVneq v y; first subst v. by rewrite /edge_rel/= inE mem_imset // !inE inG2Y. have [?|vDx] := eqVneq v x; first subst v. by rewrite /edge_rel/= /edge_rel/= inE inG2X. rewrite /edge_rel /= /edge_rel/= /edge_rel/=. rewrite -induced_edge /edge_rel/= !inG2E /=. by rewrite -(@smerge2_val_edge _ x y). } exact: (@Diso _ _ (Bij can_fwd can_bwd) dhom_fwd dhom_bwd). Qed.
imports: HB(structures) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(sgraph connectivity minor excluded) fourcolor(hypermap geometry walkup color coloring combinatorial4ct) GraphTheory(set_tac) GraphTheory(hmap_ops smerge embedding arc K4plane)