proposition: Lemma smerge2_glue2 (G H : sgraph) (x1 y1 : G) (x2 y2 : H) (p1 : inl y1 != inr x2) (p2 : inr y2 != inr x2) : x1 != y1 -> x1 -- y1 -> diso (smerge2 (smerge2 (G ∔ H)%sg (inl x1) (inr x2)) (Sub (inl y1) p1) (Sub (inr y2) p2)) (glue2 G x1 y1 H x2 y2).
proof: Proof. move=> x1Dy1 x1y1. set U' := smerge2 (G ∔ H)%sg (inl x1) (inr x2). set U := smerge2 _ _ _. have x1Nx2 : ~~ inl x1 -- inr x2 :> (G ∔ H)%sg by []. have y1Ny2 p q : ~~ (Sub (inl y1) p) -- (Sub (inr y2) q) :> U'. { by rewrite /edge_rel/= eq_sym (inj_eq inl_inj) (negbTE x1Dy1). } set V := glue2 _ _ _ _ _ _. pose f (u : U) : V := match val (val u) with | inl z => inl z | inr z => glue2_r z end. pose y1' : U := (Sub (Sub (inl y1) isT) isT). pose x1' : U' := (Sub (inl x1) isT). pose g (v : V) : U := match v with | inl z => Sub (Sub (inl z) isT) isT | inr z => insubd y1' (insubd x1' (inr (val z))) end. have gP1 z : z \notin [set x2; y2] -> val (insubd x1' (inr z)) = inr z. { move=> ?; rewrite insubdK // -topredE/= (inj_eq inr_inj); set_tac. } have gP2 z : z \notin [set x2; y2] -> val (val (insubd y1' (insubd x1' (inr z)))) = inr z. { move=> ?. rewrite val_insubd -val_eqE gP1 //= ifT ?gP1 // (inj_eq inr_inj). by set_tac. } have can_f : cancel f g. { rewrite /f/g. move => [[[u|u] U2] U1] => /=; do 2 apply: val_inj => //=. rewrite /glue2_r altF altF. rewrite !insubdK //=. rewrite -val_eqE /= in U1. by rewrite -topredE/= -val_eqE insubdK. } have can_g : cancel g f. { rewrite /f/g. move => [v|[v Hv]] //=. move : {-}(Hv); rewrite !(inE,negb_or) => /andP[vDx2 vDy2]. rewrite insubdK; last by rewrite -topredE/= -val_eqE /= val_insubd vDx2. rewrite insubdK // /glue2_r !altF; congr (inr _). exact: val_inj. } have hom_g : is_dhom g. { move => [u|[u Hu]] [v|[v Hv]]; rewrite /g/=. - move => ?. by do 2 apply: smerge2_edge. - rewrite {1}/edge_rel/=. case/orP => -/andP[/eqP-> ev]. + apply: smerge2_edge. apply: smerge2edgeL => //; by rewrite gP2 // sgP. + apply: smerge2edgeL => //; first by rewrite -val_eqE. by apply: smerge2_edge; rewrite gP2 //= sgP. - rewrite {1}/edge_rel/=. case/orP => -/andP[/eqP-> ev]. + rewrite sgP. apply: smerge2_edge. apply: smerge2edgeL => //. by rewrite gP2 // sgP. + rewrite sgP. apply: smerge2edgeL => //; first by rewrite -val_eqE. by apply: smerge2_edge; rewrite gP2 //= sgP. - rewrite {1}/edge_rel/= => uv. do 2 apply: smerge2_edge. by rewrite !gP2. } have hom_f : is_dhom f. { rewrite /is_dhom. apply: smerge2Ecase => //; first by move=> ? ?; rewrite sgP. - move => [u Hu] [v Hv] /= uv. move: Hu Hv. pattern u,v. apply: smerge2Ecase => //= {u v uv}. + move=> u v; split => A Hu Hv; rewrite sgP; apply: A. + move => [[u|u] Hu] [[v|v] Hv] //; rewrite /f/=. rewrite -?val_eqE /= !(inj_eq inr_inj) => uv uDy2 vDy2. by rewrite /glue2_r !altF /edge_rel/=. + move => [[u|u] Hu] // [[v|v] Hv] //=; first by rewrite andbF. case/andP=> [eq_u vx2]; rewrite /f/= -val_eqE /= (inj_eq inr_inj) => _ vDy2. rewrite /glue2_r 2!altF /edge_rel/=; apply/orP;left; apply/andP; split => //. by rewrite sgP. - move => [u Hu] [v Hv] /= => /andP[/eqP ?]; subst u; rewrite /f/=. rewrite smerge2edgeD // => /or3P []. + case: v Hv => -[v|v] Hv' Hv //= vy2. rewrite -val_eqE /= in Hv. rewrite /glue2_r 2!altF. rewrite /edge_rel/= eqxx [y2 -- _]sgP. by apply/orP; right. + case/andP => [def_v E]. rewrite (eqP def_v). by rewrite /edge_rel/= sgP. + done. } exact: Diso'' can_f can_g hom_f hom_g. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity minor treewidth arc set_tac)