proposition: Theorem Wagner (G : sgraph) : no_isolated G -> ~ minor G 'K_3,3 /\ ~ minor G 'K_5 -> inhabited (plane_embedding G).
proof: Proof. elim/card_ind : G => G IH no_iso. have [largeG|smallG _] := ltnP 4 #|G|; last first. exact: small_planar smallG no_iso. have [|[S lt3S sepS]] := @connectedVseparator G 3 (ltnW largeG). exact: wagner3. wlog ssepS : S lt3S {sepS} / smallest vseparator S. { move=> W; have [B smallB] := ex_smallest (@vseparatorP G) sepS. apply: (W B) => //. apply: leq_trans lt3S. exact: smallB.2. } have [V1 [V2 [psepV defS]]] := vseparator_separation ssepS.1. have [|no_is1 no_iso2] := separation_no_isolated psepV _ no_iso. by rewrite -defS. move=> kplG. have [/cards2P[x[y [xDy Sxy]]]|SN2] := boolP (#|S| == 2). { pose G1 := @induced (add_edge G x y) V1; pose G2 := @induced (add_edge G x y) V2. have [ltG1 ltG2] : #|G1| < #|G| /\ #|G2| < #|G|. by rewrite !card_sig !(proper_separation_card psepV). have psepV' : @proper_separation (add_edge G x y) V1 V2. by apply: add_edge_proper_separation psepV; rewrite -defS Sxy !inE eqxx. have [no_iso1' no_iso2'] : no_isolated G1 /\ no_isolated G2. { apply: separation_no_isolated => //; last exact: add_edge_no_isolated. by rewrite -defS; apply: add_edge_smallest_vseparator; rewrite // Sxy !inE eqxx. } have [kplanar1 kplanar2] : kplanar G1 /\ kplanar G2. by apply: kplanar_add_edge; rewrite // -?defS. case: (IH G1) => // g1; case (IH G2) => // g2. have sepV : @separation (add_edge G x y) V1 V2. by apply: add_edge_separation psepV.1; rewrite -defS Sxy !inE eqxx. have [] : inhabited (plane_embedding (add_edge G x y)). { apply: (@edge_plane_embedding (add_edge G x y) _ _ x y) sepV g1 g2. by rewrite /edge_rel/= !eqxx xDy. by rewrite -defS. } exact: subgraph_plane_embedding (add_edge_subgraph _ _) no_iso. } pose G1 := induced V1; pose G2 := induced V2. have [ltG1 ltG2] : #|G1| < #|G| /\ #|G2| < #|G|. by rewrite !card_sig !(proper_separation_card psepV). have [[g1] [g2]] : inhabited (plane_embedding G1) /\ inhabited (plane_embedding G2). split; apply: IH => //; apply: kplanar_minor kplG; exact: induced_minor. have [/cards1P[x Sx]|SN1] := boolP (#|S| == 1). { apply: vertex_plane_embedding (psepV.1) g1 g2; rewrite -defS; exact: Sx. } have {lt3S SN1 SN2} S0 : S = set0. { apply/cards0_eq/eqP; move: lt3S. by rewrite 4!(ltnS,leq_eqVlt) (negPf SN1) (negPf SN2) ltnS leqn0. } constructor; apply: diso_plane_embedding (@diso_separation _ V1 V2 _ _). - exact: union_plane_embedding. - exact: psepV.1. - by rewrite -setI_eq0 -defS S0. 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)