proposition: Lemma diso_separation1 (G : sgraph) (V1 V2 : {set G}) (x : G) (xV1 : x \in V1) (xV2 : x \in V2) : separation V1 V2 -> V1 :&: V2 = [set x] -> let G' := (induced V1 ∔ induced V2)%sg in diso (smerge2 G' (inl (Sub x xV1)) (inr (Sub x xV2))) G.
proof: Proof. move=> sepV capV G'. have sepV' u v : u \in V1 -> v \in V2 -> u != x -> v != x -> u -- v = false. { move=> uV1 vV2 uDx vDx. apply: sepV.2. - apply: contraNN uDx => uV2. by rewrite -in_set1 -capV !inE uV1. - apply: contraNN vDx => vV1. by rewrite -in_set1 -capV !inE vV2. } set x1 : G' := inl (Sub x xV1); set x2 : G' := inr (Sub x xV2). set H := smerge2 _ _ _. have h_dec (u : G) : ({ uV1 : u \in V1 | inl (Sub u uV1) != x2 }) + ({ uV2 : u \in V2 | inr (Sub u uV2) != x2 }). { case: {-}_ /(boolP (u \in V1)) => [p|uNV1]; first by left; exists p. have uV2 : u \in V2 by apply: sep_inR sepV _. right; exists uV2; rewrite (inj_eq inr_inj) -val_eqE /=. by rewrite -in_set1 -capV inE negb_and uNV1. } pose h (u : G) : H := match h_dec u with inl (exist uV1 uDx2) => Sub (inl (Sub u uV1)) uDx2 | inr (exist uV2 uDx2) => Sub (inr (Sub u uV2)) uDx2 end. pose g (x : H) : G := match val x with inl z => val z | inr z => val z end. have can_g : cancel g h. { move => [[u uDx2|u uDx2]]; rewrite /g/h/=; apply: val_inj => /=. - case: (h_dec _) => -[uV uDx2']; first by rewrite valK'. case: notF ; rewrite (inj_eq inr_inj) -val_eqE /= in uDx2'. by rewrite -in_set1 -capV inE (valP u) uV in uDx2'. - case: (h_dec _) => -[uV uDx2']; last by rewrite /= valK'. case: notF ; rewrite (inj_eq inr_inj) -val_eqE /= in uDx2. by rewrite -in_set1 -capV inE (valP u) uV in uDx2. } have can_h : cancel h g. { by move => u; rewrite /h/g; case: (h_dec u) => -[uV uDx2]. } have hom_g : is_dhom g. { move => u v. rewrite {1}/edge_rel/= /g. rewrite -[sval u]/(val u) -[sval v]/(val v). case: (eqVneq (val u) x1) => [->|_]; case: (eqVneq (val v) x1) => [->|_] /=. - by rewrite sgP. - by case: (sval v) => -[z Hz] /=; rewrite {1 2}/edge_rel/= ?orbF 1?sg_sym. - by case: (sval u) => -[z Hz]; rewrite {1 2}/edge_rel/= ?orbF. - by case: (sval u) => -[z Hz]; case: (sval v) => -[z' Hz']. } have hom_h : is_dhom h. { move => u v uv; rewrite /h. case: (h_dec u) => -[uV uDx2]; case: (h_dec v) => -[vV vDx2] => //. - by apply: smerge2_edge. - rewrite /edge_rel/= !(inj_eq inl_inj) -!val_eqE /=. rewrite (inj_eq inr_inj) -val_eqE /= in vDx2. case: (eqVneq u x) => [?|vDx] /=; first by subst u; rewrite sgP. by rewrite sepV' in uv. - have uDx : u != x by rewrite (inj_eq inr_inj) -val_eqE /= in uDx2. rewrite /edge_rel/= !(inj_eq inl_inj) -!val_eqE /=. case: (eqVneq v x) => [?|vDx] /=; first by subst v. by rewrite sgP sepV' in uv. } exact: Diso'' can_g can_h _ _. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity minor treewidth arc set_tac)