proposition: Lemma connector_cat (P A B : {set G}) n (p q : 'I_n -> pathS G) : #|P| = n -> separator A B P -> connector A P p -> connector P B q -> exists (r : 'I_n -> pathS G), connector A B r.
proof: Proof. move => card_P. subst n. move => sep_P con_p con_q. have mtch i : { j | fst (q j) = lst (p i) }. { pose x := lst (p i). have Hx : x \in codom (@fst G \o q). { apply: (inj_card_onto_pred (P := mem P)). - exact: fst_inj con_q. - move => j. exact: connector_fst con_q _. - by rewrite card_ord. - exact: connector_lst con_p _. } exists (iinv Hx). rewrite -[fst _]/((@fst G \o q) (iinv Hx)). by rewrite f_iinv. } have mtch_inj : injective (fun i => sval (mtch i)). { move => i i' E. move: (svalP (mtch i')). rewrite -E (svalP (mtch i)). exact : (lst_inj con_p). } pose pq i := pcatS (p i) (q (sval (mtch i))). have pqE i : exists j x y z (pi : Path x y) (qi : Path y z), [/\ p i = PathS pi, j = sval (mtch i), q j = PathS qi & pq i = PathS (pcat pi qi) ]. { pose j := sval (mtch i). have jP := svalP (mtch i) : fst (q j) = lst (p i). exists j. exists (fst (p i)). exists (lst (p i)). exists (lst (q j)). exists (tagged (p i)). exists (castL jP (tagged (q j))). split => //. - by rewrite {1}[p i]pathS_eta. - rewrite {1}[q j]pathS_eta. move: (jP). rewrite -jP => jP'. by rewrite (eq_irrelevance jP' erefl). - rewrite /pq -/j. rewrite -pcatSE -pathS_eta. move: (jP). rewrite -jP => jP'. by rewrite (eq_irrelevance jP' erefl) /= -pathS_eta. } have sepP i j x : x \in p i -> x \in q j -> x \in P. { exact: connector_sep sep_P con_p con_q. } exists pq. split. - move => i. move: (pqE i) => [j] [x] [y] [z] [pi] [qj] [Ep Ej Eq ->] /=. apply: irred_catI => [u u_p u_q||]. + have uP : u \in P. apply: (sepP i j u); rewrite ?Ep ?Eq //. move: (conn_end con_p i) => /setP/(_ u). rewrite Ep !inE /= u_p uP /=. by move/esym/eqP. + move: (conn_irred con_p i). by rewrite Ep. + move: (conn_irred con_q j). by rewrite Eq. - move => i. move: (pqE i) => [j] [x] [y] [z] [pi] [qj] [Ep Ej Eq ->] /=. apply/setP => u. rewrite !inE /=. apply/andP/eqP => [[/orP[u_pi|u_qj] uA]|->]. + move/(_ i u): (connector_left con_p). rewrite Ep /= u_pi uA. by apply. + suff ? : u = y. { subst. suff: lst (p i) = fst (p i) by rewrite Ep. apply: (lst_idp con_p _). by rewrite !Ep. } have Iq : irred qj. move: (conn_irred con_q j). by rewrite Eq. case/(isplitP Iq) def_q : _ / u_qj => [q1 q2 _ _ I]. have zB : z \in B. { move: (connector_lst con_q j). by rewrite Eq. } case: (sep_P _ _ q2) => // s sP in_q2. have ? : s = y. { by rewrite [s](connector_left con_q (i := j)) // Eq // def_q mem_pcat in_q2. } subst s. by rewrite [y]I // inE. + by rewrite inE /fst/= [x](_ : _ = fst (p i)) ?(connector_fst con_p) // Ep. - move => i. move: (pqE i) => [j] [x] [y] [z] [pi] [qj] [Ep Ej Eq ->] /=. apply/setP => u. rewrite !inE /=. apply/andP/eqP => [[/orP[u_pi|u_qj] uB]|->]. + have uz : u = y. { have Ip : irred pi. move: (conn_irred con_p i). by rewrite Ep. case/(isplitP Ip) def_p : _ / u_pi => [p1 p2 _ _ I]. have xA : x \in A. { move: (connector_fst con_p i). by rewrite Ep. } case: (sep_P _ _ p1) => // s sP in_p1. have ? : s = y. { by rewrite [s](connector_right con_p (i := i)) // Ep // def_p mem_pcat in_p1. } subst s. by rewrite [y]I // inE. } subst u. suff: fst (q j) = lst (q j). by rewrite Eq. apply: (fst_idp con_q _). by rewrite Eq. + move/(_ j u): (connector_right con_q). rewrite Eq /= u_qj uB. by apply. + by rewrite inE /lst/= [z](_ : _ = lst (q j)) ?(connector_lst con_q) // Eq. - move => i j iDj. move: (pqE i) => [i2] [x] [y] [z] [pi] [qi2] [Ep Ei Eq ->] /=. move: (pqE j) => [j2] [x'] [y'] [z'] [pj] [qj2] [Ep' Ej Eq' ->] /=. apply/eqP. apply: wlog_neg. case/set0Pn => u. rewrite !inE => /andP[]. case/orP => Hi; case/orP => Hj; case: notF. + move/setP/(_ u): (conn_disjoint con_p iDj). by rewrite Ep Ep' !inE Hi Hj. + have uP : u \in P. { apply: (@connector_sep P A B _ p q i j2 u) => //; by rewrite ?Ep ?Eq'. } have [? ?] : y' = u /\ y = u. { split. - by rewrite {1}[u](connector_left con_q (i := j2)) ?Eq'. - by rewrite {1}[u](connector_right con_p (i := i)) ?Ep. } subst y' y. apply: contraNT iDj => _. apply/eqP. apply: mtch_inj. rewrite -Ei -Ej. apply: (connector_eq con_q (x := u)); by rewrite ?Eq ?Eq' inE. + have uP : u \in P. { apply: (@connector_sep P A B _ p q j i2 u) => // ; by rewrite ?Ep' ?Eq. } have [? ?] : y' = u /\ y = u. { split. - by rewrite {1}[u](connector_right con_p (i := j)) ?Ep'. - by rewrite {1}[u](connector_left con_q (i := i2)) ?Eq. } subst y' y. apply: contraNT iDj => _. apply/eqP. apply: mtch_inj. rewrite -Ei -Ej. apply: (connector_eq con_q (x := u)); by rewrite ?Eq ?Eq' inE. + apply: contraNT iDj => _. apply/eqP. apply: mtch_inj. rewrite -Ei -Ej. apply: contraTeq isT => iDj. move/setP/(_ u): (conn_disjoint con_q iDj). by rewrite Eq Eq' !inE Hi Hj. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)