proposition: Lemma steps_of_ostep (G H : pre_graph) (isG : is_graph G) (isH : is_graph H) : ostep G H -> steps (pack G) (pack H).
proof: Proof. Proof with eauto with typeclass_instances. move => S. case: S isG isH => {H}. - move => z Vz Iz IOz isG isH. have h : pack G ≃2 pack (G \ z) ∔ lv G z by exact: expand_isolated. apply: cons_step h _ (steps_refl _). by constructor. - move => x z e u He Hz arc_e xDz isG isH. wlog edge_e : G He Hz {arc_e} isG isH / is_edge G e x u z. { move => W. case: (oarc_cases arc_e) => {arc_e} edge_e; first exact: W. etransitivity. apply: iso_step. apply: (flip_edge_iso e). etransitivity. apply: W => //. - by rewrite ?edges_at_flip_edge. - exact: flipped_edge. - apply: iso_step. apply: eqvG_pack. rewrite flip_edge_add_test flip_edgeK //=. by rewrite edges_at_test He !inE. } set a := lv G z in isH *. have xV : x \in vset G by eauto with vset. have x_remove_z : x \in vset (G \ z) by eauto with vset. have z_remove_z : z \notin vset (G \ z) by rewrite !inE eqxx. have h : pack G ≃2 pack (G \ z) ∔ a ∔ [inl (pack_v x), u, inr tt]. { exact: expand_pendant He edge_e _. } apply: cons_step h _ _. constructor. apply iso_step. apply: iso2_comp. apply: pack_add_test => //. apply: eqvG_pack. by rewrite remove_vertex_add_test. - move => x y z e1 e2 u v Iz e1De2 Hz xDz yDz arc_e1 arc_e2 isG isH. wlog edge_e1 : G Iz Hz {arc_e1} arc_e2 isG isH / is_edge G e1 x u z. { move => W. case: (oarc_cases arc_e1) => {arc_e1} edge_e1; first exact: W. etransitivity. apply: iso_step. apply: (flip_edge_iso e1). etransitivity. unshelve eapply (W (flip_edge G e1)) => //. - abstract by apply: add_edge_graph'; rewrite !inE ?xDz ?yDz ; [apply: (is_edge_vsetR edge_e1)|apply: oarc_vsetR arc_e2]. - by rewrite ?edges_at_flip_edge. - exact: oarc_flip_edge. - exact: flipped_edge. - apply: iso_step. apply: eqvG_pack. rewrite flip_edgeK //=. by rewrite Iz !inE eqxx. } wlog edge_e2 : G Iz Hz {arc_e2} edge_e1 isG isH / is_edge G e2 z v y. { move => W. case: (oarc_cases arc_e2) => {arc_e2} edge_e2; first exact: W. etransitivity. apply: iso_step. apply: (flip_edge_iso e2). etransitivity. unshelve eapply (W (flip_edge G e2)) => //. - abstract by apply: add_edge_graph'; rewrite !inE ?xDz ?yDz; [apply: (is_edge_vsetL edge_e1)|apply: is_edge_vsetL edge_e2]. - by rewrite ?edges_at_flip_edge. - exact: is_edge_flip_edge. - exact: flipped_edge. - apply: iso_step. apply: eqvG_pack. rewrite flip_edgeK //=. by rewrite Iz !inE eqxx. } set a := lv G z in isH *. have xV : x \in vset G by eauto with vset. have yV : y \in vset G by eauto with vset. have x_remove_z : x \in vset (G \ z) by eauto with vset. have y_remove_z : y \in vset (G \ z) by eauto with vset. have z_remove_z : z \notin vset (G \ z) by rewrite !inE eqxx. have [h] : pack G ≃2p pack (G \ z) ∔ a ∔ [inl (pack_v x),u,inr tt] ∔ [inr tt,v,inl (pack_v y)]. { apply: expand_chain. exact: Iz. all: try done. } apply: cons_step h _ _. constructor. apply: iso_step. apply: iso2_comp (iso2_sym _) _. apply: (@pack_add_edge' (G \ z)). by rewrite /= Iz maxn_fsetD. reflexivity. - move => x e u arc_e isG isH. wlog edge_e : G u {arc_e} isG isH / is_edge G e x u x. { move => W. case: (oarc_cases arc_e) => {arc_e} edge_e; first apply: W edge_e. etransitivity. apply: iso_step. apply: (flip_edge_iso e). etransitivity. apply: (W _ u). - exact: flipped_edge. - apply: iso_step. apply: eqvG_pack. rewrite flip_edgeK' ?inE ?eqxx //= updateE. rewrite (_ : [1∥(le G e)°] ≡ [1∥(le G e)]) //. exact: par_tst_cnv. } have h : pack G ≃2 pack (G - [fset e]) ∔ [pack_v x,le G e,pack_v x]. { exact: expand_loop edge_e. } apply: cons_step h _ _. constructor. apply: iso_step. apply: iso2_comp. apply: pack_add_test. + by eauto with vset. + exact: pack_irrelevance. - move => x y e1 e2 u v e1De2 arc_e1 arc_e2 isF isH. wlog edge_e1 : G {arc_e1} arc_e2 isF isH / is_edge G e1 x u y. { move => W. case: (oarc_cases arc_e1) => {arc_e1} edge_e1; first exact: W. etransitivity. apply: iso_step. apply: (flip_edge_iso e1). etransitivity. unshelve eapply (W (flip_edge G e1)) => //. - abstract by apply: add_edge_graph' => /=; eauto with vset. - exact: oarc_flip_edge. - exact: flipped_edge. - apply: iso_step. apply: eqvG_pack. rewrite flip_edgeK' //=. by rewrite !inE eqxx. } wlog edge_e2 : G {arc_e2} edge_e1 isF isH / is_edge G e2 x v y. { move => W. case: (oarc_cases arc_e2) => {arc_e2} edge_e2; first exact: W. etransitivity. apply: iso_step. apply: (flip_edge_iso e2). etransitivity. unshelve eapply (W (flip_edge G e2)) => //. - abstract by apply: add_edge_graph' => /=; eauto with vset. - exact: is_edge_flip_edge. - exact: flipped_edge. - apply: iso_step. apply: eqvG_pack. rewrite flip_edgeK' //=. by rewrite !inE eqxx. } have h : pack G ≃2 pack (G - [fset e1; e2]) ∔ [pack_v x,u,pack_v y] ∔ [pack_v x,v,pack_v y]. { exact: expand_parallel. } apply: cons_step h _ _. constructor. apply: iso_step. apply: iso2_comp (iso2_sym _) _. apply: (@pack_add_edge' (G - [fset e1;e2])). + by rewrite maxn_fsetD. + reflexivity. Qed.
imports: Coq(Relation_Definitions Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph mgraph2) GraphTheory(rewriting open_confluence finmap_plus)