proposition: Lemma ostep_of' (F G : graph2) : step F G -> inhabited (Σ F' G', (open F ⩭2 F') * ostep F' G' * (G' ⩭2 open G)).
proof: Proof. Proof with eauto with typeclass_instances vset. case => {F G}. - move => G a. constructor. have ? : fresh (vset (open G)) \notin pIO (open G ∔ [fresh (vset (open G)), a]). { rewrite pIO_add. apply: pIO_fresh. exact: freshP. } e2split. + apply: open_add_vertex. + apply: (ostep_v0 (z := fresh (vset (open G)))) => //. * by rewrite /= !inE eqxx. * by rewrite edges_at_added_vertex // freshP. + apply eqvG_iso2R... by rewrite add_vertexK // freshP. - move => G x u a. constructor. e2split. + apply: oiso2_trans. apply: open_add_edge. apply: oiso2_add_edge. apply open_add_vertex. 2: instantiate (1 := fresh (eset (open G))). 5: instantiate (1 := u). all: idtac... + rewrite !open_add_vertexE. set z := fresh _. set e := fresh _. apply: (@ostep_v1 _ _ (inj_v x) z e u). * rewrite edges_at_add_edge edges_at_added_vertex ?fsetU0 //. exact: freshP. * rewrite !pIO_add. apply: pIO_fresh. exact: freshP. * exact: oarc_added_edge. * exact: inj_vNfresh. + set z := fresh _. set e := fresh _. rewrite /= updateE. etransitivity. 2: symmetry. 2: apply: open_add_test. eapply eqvG_iso2... * apply remove_vertex_graph => //=. -- apply add_test_graph. by apply: add_edge_graph'; rewrite !inE ?eqxx ?inj_v_open. -- rewrite !pIO_add. constructor. apply: pIO_fresh. exact: freshP. * rewrite -remove_vertex_add_test add_edgeKr ?add_vertexK ?freshP //. - move => G x y u a v. constructor. pose (z := fresh (vset (open G))). pose (e1 := fresh (eset (open G))). pose (e2 := fresh (e1 |` eset (open G))). have ? : e1 != e2. { apply: contraTneq (@freshP (e1 |` eset (open G))). rewrite -/e2 => <-. by rewrite !inE eqxx. } exists (open G ∔ [z,a] ∔ [e1, inj_v x, u, z] ∔ [e2,z,v,inj_v y])%O. eexists; split; first split. + apply: oiso2_trans. apply: open_add_edge. unshelve apply: oiso2_add_edge'. apply: oiso2_trans. apply: open_add_edge. unshelve apply: oiso2_add_edge'. apply: oiso2_trans. apply: open_add_vertex. exact: oiso2_id. all: try abstract by rewrite ?freshP ?inE ?inj_v_open. 1: abstract (by rewrite /= !inE eqxx). 3: abstract (by rewrite /= !inE eqxx). 1-2: abstract by rewrite !oiso2E // ?inE ?inj_v_open ?eqxx. all: by rewrite !oiso2E // ?inE ?inj_v_open ?eqxx. + apply (@ostep_v2 _ _ (inj_v x) (inj_v y) z e1 e2 u v). all: rewrite ?pIO_add ?pIO_fresh ?inj_v_fresh ?freshP //. * by rewrite edges_at_add_edgeL edges_at_add_edge edges_at_added_vertex ?freshP ?fsetU0 1?fsetUC. * apply: oarc_add_edge => //. exact: oarc_added_edge. * exact: oarc_added_edge. + rewrite /= updateE. have E : open G ∔ [z, a] ∔ [e1, inj_v x, u, z] ∔ [e2, z, v, inj_v y] \ z ≡G open G. { by rewrite add_edgeKl ?add_edgeKr ?add_vertexK ?freshP. } apply: oiso2_trans _ (oiso2_sym _). 2: apply: open_add_edge. unshelve apply: oiso2_add_edge'. apply: eqvG_iso2R E. 1: { rewrite (sameE E). case: (leqP e1 e2) => _; rewrite ?freshP //. apply: freshP'. apply: fsubsetUr. } all: rewrite ?eqvG_iso2E ?freshP //=. all: by rewrite ?inE ?inj_v_open ?inj_vNfresh. - move => G x u. pose (e := fresh (eset (open G))). constructor. e2split. + apply: open_add_edge. + apply: (@ostep_e0 _ _ (inj_v x) e u). exact: oarc_added_edge. + rewrite /= update_eq. apply: oiso2_trans _ (oiso2_sym _). 2:apply: open_add_test. eapply eqvG_iso2R... rewrite add_edge_remove_edgesK ?inE //. by rewrite remove_edgesD // fdisjointX1 freshP. - move => G x y u v. constructor. pose (e1 := fresh (eset (open G))). pose (e2 := fresh (e1 |` eset (open G))). have ? : e1 != e2. { apply: contraTneq (@freshP (e1 |` eset (open G))). rewrite -/e2 => <-. by rewrite !inE eqxx. } exists (open G ∔ [e1, inj_v x, u, inj_v y] ∔ [e2, inj_v x, v, inj_v y])%O. eexists; split; first split. + apply: oiso2_trans. apply: open_add_edge. unshelve apply: oiso2_add_edge'. apply: open_add_edge. all: by rewrite ?freshP ?inj_v_open ?open_add_edgeE. + apply: (@ostep_e2 _ _ (inj_v x) (inj_v y) e1 e2 u v) => //. * apply: oarc_add_edge => //. exact: oarc_added_edge. * exact: oarc_added_edge. + apply: oiso2_trans _ (oiso2_sym _). 2: apply: open_add_edge. unshelve apply: oiso2_add_edge'. { apply eqvG_iso2R... rewrite !add_edge_remove_edgesK ?inE ?eqxx //. rewrite remove_edgesD // fdisjointXU !fdisjointX1 freshP freshP' //. apply: fsubsetUr. } 1: by rewrite maxn_fsetD. all: by rewrite ?eqvG_iso2E ?freshP //= ?inj_v_open. 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)