proposition: Lemma ostep_iso (F G H : pre_graph) : ostep F G -> F ⩭2 H -> Σ U, ostep H U * (G ⩭2 U).
proof: Proof. Proof with eauto with vset. case => {G}. - move => z Vz Iz zIO i. exists (H \ i z)%O. split. + apply ostep_v0. * exact: oiso2_vset. * by rewrite oiso2_edges_at // Iz imfset0. * by rewrite -oiso2_pIO. + exact: oiso2_remove_vertex. - move => x z e u Iz IOz arc_e xDz i. have [isF isH] : is_graph F /\ is_graph H by eauto with typeclass_instances. have Vz : z \in vset F by apply: oarc_vsetR arc_e. exists (H[adt i x <- [dom (u·elem_of (lv H (i z)))]] \ i z)%O. split. + apply: (ostep_v1 (e := efun_of i e)). * by rewrite oiso2_edges_at // Iz imfset1. * by rewrite -oiso2_pIO. * exact: oiso2_oarc arc_e. * apply: contra_neq xDz. apply: vfun_of_inj... + unshelve apply: oiso2_remove_vertex_. apply: oiso2_add_test... * by rewrite eqv_testE (rwT (oiso2_lv i Vz)). * done. * done. * by rewrite oiso2_add_testE. - move => x y z e1 e2 u v Iz e1De2 IOz xDz yDz arc_e1 arc_e2 i. have [isF isH] : is_graph F /\ is_graph H by eauto with typeclass_instances. have Vz : z \in vset F... set e : ET := maxn (efun_of i e1) (efun_of i e2). exists ((H \ i z) ∔ [e, i x, u·elem_of (lv H (i z))·v,i y])%O. split. + apply: (ostep_v2). * by rewrite oiso2_edges_at // Iz imfset1U imfset1. * apply: contra_neq e1De2. apply: efun_of_inj... by case: arc_e1. by case: arc_e2. * by rewrite -oiso2_pIO. * apply: contra_neq xDz. apply: vfun_of_inj... * apply: contra_neq yDz. apply: vfun_of_inj... * exact: oiso2_oarc arc_e1. * exact: oiso2_oarc arc_e2. + have @j : (F \ z) ⩭2 (H \ i z). exact: oiso2_remove_vertex. have jE : {in vset (F \ z), j =1 i}. exact: oiso2_remove_vertexE. rewrite -![i x]jE -?[i y]jE //=. apply (oiso2_add_edge j). * by rewrite /= Iz maxn_fsetD. * rewrite in_fsetD negb_and negbK oiso2_edges_at //. by rewrite Iz imfset1U imfset1 maxn_fset2. * rewrite in_fsetD1 xDz /=... * rewrite in_fsetD1 yDz /=... * move: (oiso2_lv i Vz) => X. Fail rewrite -X. apply: dot_eqv => //. apply dot_eqv => //. symmetry in X. etransitivity. exact X. done. * rewrite in_fsetD1 yDz /=... * rewrite in_fsetD1 xDz /=... - move => x e u arc_e i. have [isF isH] : is_graph F /\ is_graph H by eauto with typeclass_instances. exists ((H - [fset efun_of i e])[adt i x <- [1 ∥ le H (efun_of i e)]])%O. split. + apply: (ostep_e0 (e := efun_of i e)). exact: oiso2_oarc arc_e. + have @j : (F - [fset e]) ⩭2 (H - [fset efun_of i e]). { apply: (oiso2_remove_edges (i := i)). + abstract (rewrite fsub1set; by case: arc_e). + abstract (by rewrite imfset1). } have jE z (Vz : z \in vset F) : j z = i z. { exact: oiso2_remove_edgesE. } rewrite -!jE. apply: oiso2_add_test. * rewrite /=. exact: oarc_vsetL arc_e. * case: arc_e {j jE} => E _. move:(oiso2_le i E). move: (efun_of i e) => e'. move: (edir_of i e) => b X. symmetry. exact: eqvb_par1 X. * rewrite /=. exact: oarc_vsetL arc_e. - move => x y e1 e2 u v e1De2 arc_e1 arc_e2 i. have [isF isH] : is_graph F /\ is_graph H by eauto with typeclass_instances. set e : ET := maxn (efun_of i e1) (efun_of i e2). exists ((H - [fset efun_of i e1; efun_of i e2]) ∔ [e,i x, u∥v,i y])%O. split. + apply: (ostep_e2). * apply: contra_neq e1De2. apply: efun_of_inj... by case: arc_e1. by case: arc_e2. * exact: oiso2_oarc arc_e1. * exact: oiso2_oarc arc_e2. + have @j : (F - [fset e1; e2]) ⩭2 (H - [fset efun_of i e1; efun_of i e2]). { apply: (oiso2_remove_edges (i := i)). abstract (rewrite fsubUset !fsub1set; case: arc_e1 => -> _; by case: arc_e2). abstract (by rewrite imfset1U imfset1). } have jE z (Vz : z \in vset F) : j z = i z. { exact: oiso2_remove_edgesE. } rewrite -!jE. apply: oiso2_add_edge. * by rewrite maxn_fsetD. * by rewrite in_fsetD negb_and negbK maxn_fset2. * rewrite /=... * rewrite /=... * done. * apply: oarc_vsetR arc_e1. * apply: oarc_vsetL arc_e1. 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)