proposition: Lemma wagner_no_cross (G : sgraph) (x y : G) (s : seq G) : kplanar G -> ucycle (--) s -> x -- y -> x \notin s -> y \notin s -> let X := [seq z <- s | x -- z] in let Y := [seq z <- s | y -- z] in 2 <= #|X| -> 2 <= #|Y| -> exists2 z, z \in X & {subset Y <= rcons (arc s z (next X z)) (next X z) }.
proof: Proof. move => [K33_free K5_free] ucycle_s xy xNs yNs X Y Xgt1 Ygt1. have uniq_s := ucycle_uniq ucycle_s. pose XY := [set z in X | z \in Y]. have sub_s : {subset XY <= s}. { by move => z; rewrite !inE !mem_filter -!andbA=> /and3P [_ -> _]. } have [X_sub_s Y_sub_s] : {subset X <= s} /\ {subset Y <= s}. { by split => u; rewrite mem_filter => /andP [_ ->]. } have maxXY : #|XY| <= 2. { apply: contra_notT K5_free; rewrite leqNgt negbK => card_XY. have [p []]:= subseq_of_subset (uniq_s) sub_s card_XY. move: p => [//|u1 [//|u2 [//|u3 [|//]]]] => P1 _ P2. set u := _ :: _ in P1 P2. have: uniq u by apply: subseq_uniq P2 _. rewrite /= !inE negb_or andbT -andbA [u1 == u3]eq_sym => /and3P [U1 U3 U2]. have [N1 N2 N3] : [/\ next u u1 = u2, next u u2 = u3 & next u u3 = u1]. by rewrite /= !eqxx !ifN // eq_sym. pose phi (i : 'K_5) : {set G} := match i with | Ordinal 0 _ => [set x] | Ordinal 1 _ => [set y] | Ordinal 2 _ => [set z in arc s u1 u2] | Ordinal 3 _ => [set z in arc s u2 u3] | Ordinal 4 _ => [set z in arc s u3 u1] | _ => set0 end. apply: (@minor_of_rmap _ _ phi). have head_s := head_arc _ uniq_s. have [? ? ?] : [/\ u1 \in s, u2 \in s & u3 \in s]. { by split;apply: (mem_subseq P2); rewrite !inE eqxx. } apply: ordered_rmap; first apply: ord_inj; split. - case;case => [|[|[|[|[|//]]]]] /= _; try exact: set10. all: match goal with |- is_true ([set _ in arc _ ?u1 _] != set0) => by apply/set0Pn; exists u1; rewrite inE head_s end. - case;case => [|[|[|[|[|//]]]]] /= _; try exact: connected1. all: apply: connected_arc => //. all: by apply: (mem_subseq P2); rewrite !inE eqxx. - case;case => [|[|[|[|[|//]]]]] /= i; case;case => [|[|[|[|[|//]]]]] //= {i} _ _ _. 1-7: rewrite disjoints1 ?in_set1 ?sg_edgeNeq //. 1-3: by apply: contraNN xNs; rewrite inE; exact: mem_arc. 1-3: by apply: contraNN yNs; rewrite inE; exact: mem_arc. all: repeat under eq_disjoint => z do rewrite inE //. all: repeat under eq_disjoint_r => z do rewrite inE //. 1: rewrite -{1}N1 -{1}N2. 2: rewrite -{1}N1 -{3}N3. 3: rewrite -{1}N2 -{1}N3. all: by apply: (arc_next_disjoint uniq_s) => //; rewrite 1?eq_sym // !inE eqxx. - have E z : z \in u -> (x -- z)*(y -- z). { by move/P1;rewrite !inE !mem_filter => -/andP[/andP[? ?] /andP[? ?]]; split. } case;case => [|[|[|[|[|//]]]]] /= i; case;case => [|[|[|[|[|//]]]]] //= {i} _ _ _. 1-7: apply/neighbor1P. 8-10: apply/neighborP. + by exists y; rewrite ?inE. + exists u1. by rewrite E ?inE ?eqxx. by rewrite inE head_s. + exists u2. by rewrite E ?inE ?eqxx. by rewrite inE head_s. + exists u3. by rewrite E ?inE ?eqxx. by rewrite inE head_s. + exists u1. by rewrite E ?inE ?eqxx. by rewrite inE head_s. + exists u2. by rewrite E ?inE ?eqxx. by rewrite inE head_s. + exists u3. by rewrite E ?inE ?eqxx. by rewrite inE head_s. + exists (last u1 (arc s u1 u2)), u2. by rewrite !inE last_mem head_s // arc_edge. + exists u1,(last u3 (arc s u3 u1)). by rewrite !inE last_mem head_s // sgP arc_edge. + exists (last u2 (arc s u2 u3)), u3. by rewrite !inE last_mem head_s // arc_edge. } have no_cross : ~ exists x1 x2 y1 y2, [/\ x1 \in X, x2 \in X, y1 \in Y , y2 \in Y & subcycle [:: x1; y1; x2; y2] s]. { apply: contra_not K33_free => -[x1] [x2] [y1] [y2] [x1X x2X y1Y y2Y subs]. pose u := [:: x1; y1; x2; y2]. pose phi (i : 'K_3,3) : {set G} := match i with | inl (Ordinal 0 _) => [set x] | inr (Ordinal 0 _) => [set y] | inl (Ordinal 1 _) => [set z in arc s y1 x2] | inl (Ordinal 2 _) => [set z in arc s y2 x1] | inr (Ordinal 1 _) => [set z in arc s x1 y1] | inr (Ordinal 2 _) => [set z in arc s x2 y2] | _ => set0 end. suff: minor_rmap phi by apply minor_of_rmap. have head_s := head_arc _ uniq_s. have xz z : z \in X -> x -- z by rewrite !mem_filter => /andP[-> _]. have yz z : z \in Y -> y -- z by rewrite !mem_filter => /andP[-> _]. have : uniq u. apply: subcycle_uniq subs _. apply: ucycle_uniq ucycle_s. rewrite /u /= !inE !negb_or -!andbA andbT => /and5P[? ? ? ? /andP [? ?]]. have u_sub_s := mem_subcycle subs. apply: ordered_rmap; first exact: pickle_Knn_inj; split. - case; case; case => [|[|[|//]]] /= _; try exact: set10. all: match goal with |- is_true ([set _ in arc _ ?u1 _] != set0) => apply/set0Pn; exists u1; rewrite inE head_s // 1?eq_sym // end. all: by apply: u_sub_s; rewrite !inE eqxx. - case; case; case => [|[|[|//]]] /= _; try exact: connected1. all: apply: connected_arc; rewrite // 1?eq_sym //. all: by apply: u_sub_s; rewrite !inE eqxx. - case; case; case => [|[|[|//]]] /= i; case; case; case => [|[|[|//]]] //= {i} _ _ _. all: rewrite ?disjoints1 ?[[disjoint _ & [set _]]]disjoint_sym ?disjoints1 ?inE. 3: by rewrite sg_edgeNeq. all: try solve [apply: contraNN xNs; apply: mem_arc]. all: try solve [apply: contraNN yNs; apply: mem_arc]. all: apply: (arc_subcycle_disjoints uniq_s subs). all: by rewrite ?inE /= ?eqxx // ?ifN // 1?eq_sym. - case; case; case => [|[|[|//]]] /= i; case; case; case => [|[|[|//]]] //= {i} _ _ _. 4,7 : rewrite neighborC. 1-5 : apply/neighbor1P. 6-9: apply/neighborP. + by exists y; rewrite ?inE. + by exists x1; rewrite ?xz // inE head_s // 1?eq_sym // u_sub_s ?inE ?eqxx. + by exists x2; rewrite ?xz // inE head_s // 1?eq_sym // u_sub_s ?inE ?eqxx. + by exists y1; rewrite ?yz // inE head_s // 1?eq_sym // u_sub_s ?inE ?eqxx. + by exists y2; rewrite ?yz // inE head_s // 1?eq_sym // u_sub_s ?inE ?eqxx. + exists y1, (last x1 (arc s x1 y1)). by rewrite sgP !inE last_mem head_s ?arc_edge // u_sub_s ?inE ?eqxx. + exists (last y1 (arc s y1 x2)), x2. by rewrite !inE last_mem head_s ?arc_edge // u_sub_s ?inE ?eqxx. + exists (last y2 (arc s y2 x1)), x1. by rewrite !inE last_mem head_s ?arc_edge // 1?eq_sym // u_sub_s ?inE ?eqxx. + exists y2, (last x2 (arc s x2 y2)). by rewrite sgP !inE last_mem head_s ?arc_edge // 1?eq_sym // u_sub_s ?inE ?eqxx. } suff: ~ forall x, x \in X -> exists2 y, y \in Y & y \notin rcons (arc s x (next X x)) (next X x). { move => NC; apply/exists_inPP => [u|]; first exact/allP. apply: contra_notT NC => /exists_inPn H u u_X. have [v v_Y ?] := allPn (H _ u_X); by exists v. } apply: contra_not no_cross => not_contained. have [uniq_X uniq_Y] : uniq X /\ uniq Y by rewrite filter_uniq // filter_uniq. have subcycle_X : subcycle X s by rewrite subseq_subcyle // filter_subseq. have size_X : 2 <= size X by rewrite -(card_uniqP _). have [/allP Y_sub_X |/allPn [y1 y1_Y y1NX]] := (boolP (all (fun z => z \in X) Y)). - have [y1 [y2 [defY y1Dy2]]]: exists y1 y2, Y = [:: y1; y2] /\ y1 != y2. { suff: size Y == 2. by move: uniq_Y; destruct Y as [|y1 [|y2 [|]]]; rewrite //= inE andbT; exists y1,y2. rewrite eqn_leq -(card_uniqP _) // Ygt1 andbT. apply: leq_trans maxXY. apply: subset_leq_card. apply/subsetP => y1 inY. by rewrite inE Y_sub_X inY . } have {defY} eqY : Y =i [set y1;y2] by move=>?; rewrite defY !inE. have xDy xi yi : xi \notin Y -> yi \in Y -> xi == yi = false. by move=> xiNY; apply: contraTF => /eqP<-. gen have H,Py1 : y1 y2 eqY y1Dy2 / prev X y1 \notin Y. { have ? : y1 \in X by rewrite Y_sub_X // eqY !inE eqxx. apply/negP => py_Y. have E : prev X y1 = y2. by apply: contraTeq py_Y => C; rewrite eqY !inE negb_or C eq_sym prev_neq. move/Y_sub_X : (py_Y) => /not_contained [z z_Y]. rewrite mem_rcons inE E negb_or => /andP[zDny2]. move: z_Y; rewrite eqY => /set2P [z_y1|->]. - by subst z; rewrite -E next_prev ?eqxx in zDny2. - by rewrite head_arc // ?next_neq // ?X_sub_s // ?mem_next Y_sub_X // eqY !inE eqxx. } have := H y2 y1; rewrite setUC eq_sym => /(_ eqY y1Dy2) => {H} Py2. have [y1_X y1_Y y2_X y2_Y] : [/\ y1 \in X, y1 \in Y, y2 \in X & y2 \in Y]. by rewrite !Y_sub_X !eqY !inE !eqxx. pose x1 := prev X y1; pose x2 := prev X y2. rewrite -/x1 -/x2 in Py1 Py2. exists x1, x2, y1, y2; rewrite !path.mem_prev; split => //. apply: subcycle_trans subcycle_X. have x1Dx2 : x1 != x2. { apply:contra_neq y1Dy2 => eq_x. by rewrite -[y1](next_prev uniq_X) -/x1 eq_x next_prev. } have [x1_X x2_X] : x1 \in X /\ x2 \in X by rewrite !path.mem_prev !Y_sub_X. have [i X1 X2 arc1 arc2 rot_i] := rot_to_arc uniq_X x1_X x2_X x1Dx2. rewrite -(subcycle_rot_r i) rot_i; apply: subseq_subcyle. rewrite /= eqxx -cat1s; apply: cat_subseq; rewrite /= ?eqxx sub1seq. + have := next_mem_arc uniq_X x1_X x2_X x1Dx2. by rewrite next_prev // mem_rcons -arc1 !inE ![y1 == _]eq_sym !xDy. + rewrite eq_sym in x1Dx2; have := next_mem_arc uniq_X x2_X x1_X x1Dx2. by rewrite next_prev // mem_rcons -arc2 !inE ![y2 == _]eq_sym !xDy. - have y1_s : y1 \in s by move: y1_Y; rewrite mem_filter => /andP[_ ->]. have [x1 x1_X x1_y1] := subcycle_get_arc y1_s uniq_s subcycle_X size_X. have [y2 y2_Y foo] := not_contained _ x1_X. set x2 := next X x1 in x1_y1 foo. exists x1,x2,y1,y2. rewrite !mem_next; split => //. have [x1_s x2_s] : x1 \in s /\ x2 \in s by rewrite !X_sub_s // mem_next. have x1Dx2 : x1 != x2 by exact: next_neq. have [i s1 s2 def_s1 def_s2 rot_s] := rot_to_arc uniq_s x1_s x2_s x1Dx2. rewrite -(subcycle_rot_r i) rot_s subseq_subcyle //= eqxx -cat1s. apply: cat_subseq; rewrite /= ?eqxx sub1seq. + move: x1_y1. rewrite -def_s1 inE [_ == _](_ : _ = false) //. by apply: contraNF y1NX => /eqP ->. + have:= Y_sub_s _ y2_Y; rewrite -(mem_rot i) rot_s -cat_cons -[x2 :: _]cat1s. by rewrite catA cats1 def_s1 mem_cat (negbTE foo). 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)