Library GraphTheory.mgraph

Require Import Morphisms RelationClasses.
Require CMorphisms CRelationClasses. From mathcomp Require Import all_ssreflect.
Require Import edone finite_quotient preliminaries bij equiv digraph setoid_bigop structures.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Set Bullet Behavior "Strict Subproofs".

Directed Labeled Multigraphs

Finite labeled directed multigraphs (not pointed, Definition 4.4)
We use a single endpoint function for "source" and "target" of edges. This frequently allows us to treat the cases for source and target as a single case in proofs. Further, this allows view ing multigraphs as undirected with b : bool being one end and ~~ b the other.

Set Primitive Projections.
Record graph (Lv Le : Type) : Type :=
Graph {
vertex:> finType;
edge: finType;
endpoint: bool edge vertex;
vlabel: vertex Lv;
elabel: edge Le }.
Unset Primitive Projections.
Notation source := (endpoint false).
Notation target := (endpoint true).

Section s1.
Variables (Lv Le : Type).
Local Notation graph := (graph Lv Le).
Local Notation Graph := (@Graph Lv Le).

Basic Operations

These operations require no structures on either label type
empty graph
Definition void_graph := Graph (fun _vfun) vfun vfun.

graph with a single vertex
Definition unit_graph a := Graph (fun _vfun) (fun _: unita) vfun.

adding an edge to a graph
Definition add_edge (G: graph) (x y: G) (u: Le): graph :=
@Graph (vertex G) (option_finType (edge G))
(fun b ematch e with Some eendpoint b e | Noneif b then y else x end)
(@vlabel _ _ G)
(fun ematch e with Some eelabel e | Noneu end).
Notation "G ∔ [ x , u , y ]" := (@add_edge G x y u) (at level 20, left associativity).

disjoint union (Definition 4.5)
We use an explicit sum_finType F G, because [finType of F + G] generates a significantly bigger term
Definition union (F G : graph) : graph :=
{| vertex := sum_finType F G;
edge := sum_finType (edge F) (edge G);
endpoint b := sumf (@endpoint _ _ F b) (@endpoint _ _ G b);
vlabel e := match e with inl evlabel e | inr evlabel e end;
elabel e := match e with inl eelabel e | inr eelabel e end;
|}.

Infix "⊎" := union (at level 50, left associativity).

Definition unl {G H: graph} (x: G): G H := inl x.
Definition unr {G H: graph} (x: H): G H := inr x.

derived operations (Definition 4.7)
Definition two_graph a b := unit_graph a unit_graph b.
Definition edge_graph a u b := two_graph a b [inl tt, u, inr tt].
Definition add_vertex G a := G unit_graph a.

Section Subgraphs.
Variables (G : graph) (V : {set G}) (E : {set edge G}).
Definition consistent := e b, e \in E endpoint b e \in V.
Hypothesis in_V : consistent.

Definition sub_vertex := sig_finType (fun xx \in V).
Definition sub_edge := sig_finType (fun ee \in E).

Definition subgraph_for :=
{| vertex := sub_vertex;
edge := sub_edge;
endpoint b e := Sub (endpoint b (val e)) (in_V b (valP e));
vlabel x := vlabel (val x);
elabel e := elabel (val e);
|}.

edge deletion is treated as a special case, because this avoids the change in the vertex type

Definition remove_edges :=
{| vertex := G;
edge := sig_finType (fun e: edge Ge \notin E);
endpoint b e := endpoint b (val e);
vlabel x := vlabel x;
elabel e := elabel (val e); |}.

End Subgraphs.

Lemma consistent_setD (G : graph) (V : {set G}) E E' :
consistent V E consistent V (E :\: E').
Proof. movecon_E e b /setDP [? _]. exact: con_E. Qed.

Frequently used consistent sets of vertices and edges

Lemma consistentT (G : graph) (E : {set edge G}) : consistent setT E.
Proof. by []. Qed.

Lemma consistentTT (G : graph) : consistent [set: G] [set: edge G].
Proof. done. Qed.

Section Edges.
Variables (G : graph).
Implicit Types (x y : G).

Definition edges x y :=
[set e | (source e == x) && (target e == y)].

Definition edge_set (S : {set G}) :=

[set e | (source e \in S) && (target e \in S)].

Lemma edge_set1 x : edge_set [set x] = edges x x.
Proof. apply/setPe. by rewrite !inE. Qed.

Lemma edge_in_set e (A : {set G}) x y :
x \in A y \in A e \in edges x y e \in edge_set A.
Proof. moveHx Hy. rewrite !inE ⇒ /andP[/eqP->/eqP->]. by rewrite Hx. Qed.

Definition incident x e := [ b, endpoint b e == x].
Definition edges_at x := [set e | incident x e].

Definition edges_in (V : {set G}) := (\bigcup_(x in V) edges_at x)%SET.

Lemma edges_in1 (x : G) : edges_in [set x] = edges_at x.
Proof. by rewrite /edges_in big_set1. Qed.

End Edges.

Definition induced_proof (G: graph) (S : {set G}) : consistent S (edge_set S).
Proof. movee b; rewrite inE=>/andP[? ?]; by case b. Qed.

Definition induced (G: graph) (S : {set G}) := subgraph_for (@induced_proof G S).

Lemma consistent_del1 (G : graph) (x : G) : consistent [set¬ x] (~: edges_at x).
Proof. movee b. rewrite !inE. apply: contraNneq ⇒ <-. by existsb b. Qed.

Definition remove_vertex (G : graph) (z : G) : graph :=
subgraph_for (@consistent_del1 G z).

End s1.

Arguments consistentT [Lv Le G] E.
Arguments consistentTT [Lv Le] G.

Arguments edges_at [Lv Le G] x, [Lv Le] G x.

Declare Scope graph_scope.
Bind Scope graph_scope with graph.
Delimit Scope graph_scope with G.

Arguments unit_graph {Lv} Le a, {Lv Le} a.
Arguments two_graph {Lv} Le a b, {Lv Le} a b.

Arguments union {Lv Le} F G.
Infix "⊎" := union (at level 50, left associativity) : graph_scope.
Arguments unl {Lv Le G H}.
Arguments unr {Lv Le G H}.

Arguments add_edge {Lv Le} G x y u.
Notation "G ∔ [ x , u , y ]" := (add_edge G x y u) (at level 20, left associativity).
Arguments add_vertex {Lv Le} G a.
Notation "G ∔ a" := (add_vertex G a) (at level 20, left associativity) : graph_scope.

Operations that require structures on labels

Section s2.
Variables (Lv: comMonoid) (Le : elabelType).
Local Notation graph := (graph Lv Le).
Local Notation Graph := (@Graph Lv Le).
Local Open Scope cm_scope.

adding a label to a vertex (cumulative w.r.t existing label)
Definition add_vlabel (G: graph) (x: G) (a: Lv): graph :=
@Graph (vertex G) (edge G)
(@endpoint _ _ G)
(fun vif v==x then a vlabel v else vlabel v)
(@elabel _ _ G).
Notation "G [tst x <- a ]" := (@add_vlabel G x a) (at level 20, left associativity).

quotient (Definition 4.6): merging vertices according to an equivalence relation
Definition merge (G: graph) (r : equiv_rel G) :=
{| vertex := quot r;
edge := edge G;
endpoint b e := \pi (endpoint b e);
vlabel c := \big[cm_op/1]_(w | \pi w == c) vlabel w;
elabel e := elabel e |}.
Arguments merge _ _: clear implicits.
Notation merge_seq G l := (merge G (eqv_clot l)).

Homomorphisms

Class is_hom (F G: graph) (hv: F G) (he: edge F edge G) (hd: edge F bool): Prop := Hom
{ endpoint_hom: e b, endpoint b (he e) = hv (endpoint (hd e (+) b) e);
vlabel_hom: v, vlabel v (\big[cm_op/1]_(u | hv u == v) vlabel u);
elabel_hom: e, elabel (he e) ≡[hd e] elabel e;
}.

Lemma hom_id G: @is_hom G G id id xpred0.
Proof. split ⇒ // v. by rewrite big_pred1_eq. Qed.

Lemma hom_comp F G H hv he hd kv ke kd :
@is_hom F G hv he hd @is_hom G H kv ke kd
is_hom (kv \o hv) (ke \o he) (fun ehd e (+) kd (he e)).
Proof.
intros E E'. split.
movee b=>/=; first by rewrite 2!endpoint_hom addbA.
- movex/=. rewrite vlabel_hom (eqv_bigr _ (fun u _vlabel_hom (is_hom := E) u)).
rewrite [X in _ X](partition_big _ (fun ukv u == x)); last by move=>?;apply.
apply: eqv_bigry /eqP <-. apply: eqv_big ⇒ // z.
case e: (_ == y) ⇒ //. by rewrite (eqP e) eqxx.
- movee/=.
generalize (@elabel_hom _ _ _ _ _ E e).
generalize (@elabel_hom _ _ _ _ _ E' (he e)).
case (hd e); case (kd (he e)); simpl.
+ apply eqv11.
+ apply eqv01.
+ apply eqv10.
+ apply transitivity.
Qed.

Isomorphisms

When the underlying functions are bijective, as is the case with isomorphisms, the definition of homomorphism simlifies to the follwing, which does not require a bigop for gathering vertex labels

Class is_ihom (F G: graph) (hv: F G) (he: edge F edge G) (hd: edge F bool): Prop := IHom
{ endpoint_ihom: e b, endpoint b (he e) = hv (endpoint (hd e (+) b) e);
vlabel_ihom: v, vlabel (hv v) vlabel v;
elabel_ihom: e, elabel (he e) ≡[hd e] elabel e }.

Lemma ihom_id G: @is_ihom G G id id xpred0.
Proof. by split. Qed.

Lemma ihom_sym (F G: graph) (hv: bij F G) (he: bij (edge F) (edge G)) hd:
is_ihom hv he hd
is_ihom hv^-1 he^-1 (hd \o he^-1).
Proof.
intro H. split.
- movee b=>/=. by rewrite -{3}(bijK' he e) endpoint_ihom bijK addbA addbb.
- movex/=. by rewrite -{2}(bijK' hv x) vlabel_ihom.
- movee/=. generalize (@elabel_ihom _ _ _ _ _ H (he^-1 e)).
rewrite -{3}(bijK' he e) bijK'. by symmetry.
Qed.

Lemma hom_ihom (F G: graph) (hv: F G) (he: (edge F) (edge G)) hd :
injective hv is_hom hv he hd is_ihom hv he hd.
Proof. moveinj_hv [? H ?]. split ⇒ // v. by rewrite H big_inj2_eq. Qed.

Lemma ihom_hom (F G: graph) (hv: bij F G) (he: (edge F) (edge G)) hd :
is_ihom hv he hd is_hom hv he hd.
Proof. move ⇒ [? H ?]. split ⇒ // v. by rewrite big_bij_eq -H bijK'. Qed.

Universe S.
Set Primitive Projections.
Record iso (F G: graph): Type@{S} :=
Iso { iso_v:> bij F G;
iso_e: bij (edge F) (edge G);
iso_d: edge F bool;
iso_ihom: is_ihom iso_v iso_e iso_d }.
Infix "≃" := iso (at level 79).
Notation "h '.e'" := (iso_e h) (at level 2, left associativity, format "h '.e'").
Notation "h '.d'" := (iso_d h) (at level 2, left associativity, format "h '.d'").
Global Existing Instance iso_ihom.
Global Instance iso_hom (F G : graph) (h : F G) : is_hom h h.e h.d.
Proof. exact: ihom_hom. Qed.

Lemma endpoint_iso F G (h: iso F G) b e: endpoint b (h.e e) = h (endpoint (h.d e (+) b) e).
Proof. exact: endpoint_ihom. Qed.

Lemma vlabel_iso F G (h: iso F G) v: vlabel (h v) vlabel v.
Proof. exact: vlabel_ihom. Qed.

Lemma elabel_iso F G (h: iso F G) e: elabel (h.e e) ≡[h.d e] elabel e.
Proof. exact: elabel_ihom. Qed.

Definition iso_id {G}: G G := @Iso _ _ bij_id bij_id _ (ihom_id G).
Hint Resolve iso_id : core.
Definition iso_sym F G: F G G F.
Proof.
movef.
eapply Iso with (bij_sym f) (bij_sym f.e) _ =>/=.
apply ihom_sym, f.
Defined.

Definition iso_comp F G H: F G G H F H.
Proof.
movef g.
eapply Iso with (bij_comp f g) (bij_comp f.e g.e) _ =>/=.
apply hom_ihom; first by apply: inj_comp.
apply hom_comp; apply iso_hom.
Defined.

Global Instance iso_Equivalence: CEquivalence iso.
Proof. constructor. exact @iso_id. exact @iso_sym. exact @iso_comp. Defined.

Lemma endpoint_iso' F G (h: iso F G) b e:
endpoint b (h.e^-1 e) = h^-1 (endpoint (h.d (h.e^-1 e) (+) b) e).
Proof. apply (endpoint_iso (iso_sym h)). Qed.

Lemma vlabel_iso' F G (h: iso F G) v: vlabel (h^-1 v) vlabel v.
Proof. apply (vlabel_iso (iso_sym h)). Qed.

Lemma elabel_iso' F G (h: iso F G) e: elabel (h.e^-1 e) ≡[h.d (h.e^-1 e)] elabel e.
Proof. apply (elabel_iso (iso_sym h)). Qed.

Definition Iso' (F G: graph)
(fv: F G) (fv': G F)
(fe: edge F edge G) (fe': edge G edge F) fd:
cancel fv fv' cancel fv' fv
cancel fe fe' cancel fe' fe
is_ihom fv fe fd F G.
Proof. movefv1 fv2 fe1 fe2 E. (Bij fv1 fv2) (Bij fe1 fe2) fd. apply E. Defined.

Tactic Notation "Iso" uconstr(f) uconstr(g) uconstr(h) :=
match goal with |- ?F ?Gapply (@Iso F G f g h) end.

isomorphisms about local and global operations

Global Instance unit_graph_iso: CProper (eqv ==> iso) (@unit_graph Lv Le).
Proof.
intros a b ab. Iso bij_id bij_id xpred0.
abstract by split=>//=;symmetry.
Defined.

Lemma add_edge_iso'' F G (h: F G) x x' (ex: h x = x') y y' (ey: h y = y') u v (e: u v):
F [x, u, y] G [x', v, y'].
Proof.
Iso (iso_v h) (option_bij (h.e)) (fun ematch e with Some eh.d e | Nonefalse end).
abstract by split; rewrite -?ex -?ey; repeat first [apply h|symmetry; apply e|case].
Defined.

Lemma add_edge_iso' F G (h: F G) x u v y (e: u v): F [x, u, y] G [h x, v, h y].

Lemma add_edge_iso F G (h: F G) x u y: F [x, u, y] G [h x, u, h y].

Lemma add_edge_C F x u y z v t: F [x, u, y] [z, v, t] F [z, v, t] [x, u, y].
Proof.
Iso bij_id option2_swap xpred0.
abstract by split; repeat case.
Defined.

Lemma add_edge_rev F x u v y (e: u ≡' v): F [x, u, y] F [y, v, x].
Proof.
Iso bij_id bij_id (fun xmatch x with Some _false | Nonetrue end).
abstract (split; (repeat case)=>//=; by apply Eqv'_sym).
Defined.

Lemma add_edge_vlabel F x a y u z: F [tst x <- a] [y, u, z] F [y, u, z] [tst x <- a].
Proof. reflexivity. Defined.

Lemma add_vlabel_iso'' F G (h: F G) x x' (ex: h x = x') a b (e: a b):
F [tst x <- a] G [tst x' <- b].
Proof.
Iso h h.e h.d.
split; try apply h.
movev/=. rewrite -ex inj_eq=>/=. 2: by apply bij_injective.
by case eq_op; rewrite ?e vlabel_iso.
Defined.

Lemma add_vlabel_iso' F G (h: F G) x a b (e: a b): F [tst x <- a] G [tst h x <- b].

Lemma add_vlabel_iso F G (h: F G) x a: F [tst x <- a] G [tst h x <- a].

Lemma add_vlabel_C F x a y b: F [tst x <- a] [tst y <- b] F [tst y <- b] [tst x <- a].
Proof.
Iso bij_id bij_id xpred0.
split=>//=. movev.
case eq_op; case eq_op=>//.
by rewrite 2!monA (monC a b).
Defined.

Lemma add_vlabel_unit a x b: unit_graph a [tst x <- b] unit_graph (ab).
Proof. apply (unit_graph_iso (monC b a)). Defined.

Lemma add_vlabel_mon0 G x: G [tst x <- 1] G.
Proof.
Iso bij_id bij_id xpred0.
split=>//=. movev.
case eq_op=>//. by rewrite monC monU.
Defined.

Global Instance union_iso: CProper (iso ==> iso ==> iso) union.
Proof.
intros F F' f G G' g.
(sum_bij f g) (sum_bij f.e g.e) (fun ematch e with inl ef.d e | inr eg.d e end).
abstract (split; [
move=>[e|e] b/=; by rewrite endpoint_iso |
casex/=; apply vlabel_iso |
casee/=; apply elabel_iso ]).
Defined.

Lemma union_C G H: G H H G.
Proof.
bij_sumC bij_sumC xpred0.
abstract by split; case.
Defined.

Lemma union_A F G H: F (G H) F G H.
Proof.
bij_sumA bij_sumA xpred0.
abstract by split; repeat case.
Defined.

Lemma union_add_edge_l F G x u y: F [x, u, y] G (F G) [unl x, u, unl y].
Proof.
Iso bij_id (@sum_option_l _ _) xpred0.
abstract by split; repeat case.
Defined.

Lemma union_add_edge_r F G x u y: F G [x, u, y] (F G) [unr x, u, unr y].
Proof.
etransitivity. apply union_C.
etransitivity. apply (add_edge_iso (union_C _ _)).
reflexivity.
Defined.

Lemma union_add_vlabel_l F G x a: F [tst x <- a] G (F G) [tst unl x <- a].
Proof.
Iso bij_id bij_id xpred0.
abstract by split; repeat case.
Defined.

Lemma union_add_vlabel_r F G x a: F G [tst x <- a] (F G) [tst unr x <- a].
Proof.
etransitivity. apply union_C.
etransitivity. apply (add_vlabel_iso (union_C _ _)).
reflexivity.
Defined.

Lemma add_vlabel_two a b (x: unit+unit) c:
two_graph a b [tst x <- c] two_graph (if x then ac else a) (if x then b else bc).
Proof.
case x; case=>/=.
Defined.

Lemma add_vlabel_edge a u b (x: unit+unit) c:
edge_graph a u b [tst x <- c] edge_graph (if x then ac else a) u (if x then b else bc).
Proof.
by case x; case.
Defined.

Section merge_surj.
Variable (G: graph) (r: equiv_rel G).
Variable (H: graph) (fv: G H) (fv': H G).
Variable (fe: bij (edge G) (edge H)) (fd : pred (edge G)).
Hypothesis Hr: x y, reflect (kernel fv x y) (r x y).
Hypothesis Hsurj: cancel fv' fv.
Hypothesis Hhom : is_hom fv fe fd.
Lemma merge_surj: merge G r H.
Proof.
Iso (quot_kernel Hr Hsurj) fe fd. split; intros=>/=.
- by rewrite (endpoint_hom (is_hom := Hhom)) quot_kernelE.
- rewrite vlabel_hom. apply: eqv_biglx. apply/eqP/eqPE.
× move:E=>/Hr/eqquotP E. rewrite E. apply reprK.
× by rewrite -E quot_kernelE.
- exact:(elabel_hom (is_hom := Hhom)).
Defined.
Lemma merge_surjE (x: G): merge_surj (\pi x) = fv x.
Proof. by rewrite quot_kernelE. Qed.
End merge_surj.
Global Opaque merge_surj.

Section h_merge_nothing'.
Variables (F: graph) (r: equiv_rel F).
Hypothesis H: x y: F, r x y x=y.
Lemma merge_nothing': merge F r F.
Proof.
apply merge_surj with id id bij_id xpred0 =>//.
- intros. apply Bool.iff_reflect.
split. intros →. by rewrite equiv_refl.
intro E. apply H. by rewrite E.
- exact: hom_id.
Defined.
Lemma merge_nothing'E x: merge_nothing' (\pi x) = x.
Proof. by rewrite /=merge_surjE. Qed.
End h_merge_nothing'.
Global Opaque merge_nothing'.

Section merge_merge.
Variables (F: graph) (e: equiv_rel F) (e': equiv_rel (merge F e)).
Lemma hom_merge_merge: is_ihom (quot_quot e': merge _ e' merge F _) bij_id xpred0.
Proof.
split; intros=>//=; first by rewrite -equiv_comp_pi.
rewrite [X in X _](partition_big (fun x\pi x) (fun w\pi w == v)).
- apply: eqv_bigrw pw. apply: eqv_bigx //.
case: (altP (\pi x =P w)) ⇒ // ?. subst w. by rewrite -(eqP pw) quot_quotE eqxx.
- movex. by rewrite -[v]reprK -[repr v]reprK quot_quotE !eqmodE.
Qed.
Lemma merge_merge: merge (merge F e) e' merge F (equiv_comp e').
Proof. eexists. eapply hom_merge_merge. Defined.
Lemma merge_mergeE x: merge_merge (\pi (\pi x)) = \pi x.
Proof. apply quot_quotE. Qed.
End merge_merge.
Global Opaque merge_merge.

Section merge.
Variables (F G: graph) (h: iso F G) (l: pairs F).
Definition h_merge: bij (merge_seq F l) (merge_seq G (map_pairs h l)).
eapply bij_comp. apply (quot_bij h). apply quot_same. apply eqv_clot_iso.
Defined.
Lemma h_mergeE (x: F): h_merge (\pi x) = \pi h x.
Proof. by rewrite /=quot_bijE quot_sameE. Qed.
Lemma merge_hom: is_ihom h_merge h.e h.d.
Proof.
split; intros=>/=.
- rewrite endpoint_iso. symmetry. apply h_mergeE.
- rewrite quot_sameE. symmetry.
apply: (eqv_big_bij (f := h)); first exact: bij_perm_enum.
+ movex. rewrite eqmodE eqv_clot_map; last exact: bij_injective.
apply/eqP/idP ⇒ [<-|/eqquotP ->]; by [exact: piK'|rewrite reprK].
+ movex _. by rewrite vlabel_iso.
- apply elabel_iso.
Qed.
Definition merge_iso: merge_seq F l merge_seq G (map_pairs h l) := Iso merge_hom.
Lemma merge_isoE (x: F): merge_iso (\pi x) = \pi h x.
Proof. apply h_mergeE. Qed.
End merge.
Global Opaque h_merge merge_iso.

Section merge_same'.
Variables (F: graph) (h k: equiv_rel F).
Hypothesis H: h =2 k.
Lemma merge_same'_hom: is_ihom (quot_same H: merge _ h merge _ k) bij_id xpred0.
Proof.
split; intros=>//; try (rewrite /=; apply/eqquotP; rewrite -H; apply: piK').
apply (eqv_big_bij (f := bij_id)) ⇒ //; first exact: bij_perm_enum.
movex. by rewrite -(reprK v) quot_sameE 2!eqmodE H.
Qed.
Definition merge_same': merge F h merge F k := Iso merge_same'_hom.
Lemma merge_same'E (x: F): merge_same' (\pi x) = \pi x.
Proof. apply quot_sameE. Qed.
End merge_same'.
Global Opaque merge_same'.

Section merge_same.
Variables (F: graph) (h k: pairs F).
Hypothesis H: eqv_clot h =2 eqv_clot k.
Definition merge_same: iso (merge_seq F h) (merge_seq F k) := merge_same' H.
Definition merge_sameE (x: F): merge_same (\pi x) = \pi x := merge_same'E H x.
End merge_same.
Global Opaque merge_same.

Section merge_nothing.
Variables (F: graph) (h: pairs F).
Hypothesis H: List.Forall (fun pp.1 = p.2) h.
Definition merge_nothing: merge_seq F h F.
Proof. apply merge_nothing', eqv_clot_nothing', H. Defined.
Lemma merge_nothingE (x: F): merge_nothing (\pi x) = x.
Proof. apply merge_nothing'E. Qed.
End merge_nothing.
Global Opaque merge_nothing.

Section merge_merge_seq.
Variables (F: graph) (h k: pairs F) (k': pairs (merge_seq F h)).
Hypothesis kk': k' = map_pairs (pi (eqv_clot h)) k.
Definition merge_merge_seq: merge_seq (merge_seq F h) k' merge_seq F (h++k).
eapply iso_comp. apply merge_merge. apply merge_same'.
abstract by rewrite kk'; apply eqv_clot_cat.
Defined.
Lemma merge_merge_seqE (x: F): merge_merge_seq (\pi (\pi x)) = \pi x.
Proof. by rewrite /=merge_mergeE merge_same'E. Qed.
End merge_merge_seq.
Global Opaque merge_merge_seq.

Lemma eqv_clot_map_lr (F G : finType) (l : pairs F) x y :
eqv_clot (map_pairs inl l) (@inl F G x) (@inr F G y) = false.
Proof. rewrite (@eqv_clot_mapF _) ?inr_codom_inl //. exact: inl_inj. Qed.

Lemma union_equiv_l_eqv_clot (A B: finType) (l: pairs A):
union_equiv_l B (eqv_clot l) =2 eqv_clot (map_pairs inl l).
Proof.
rewrite /union_equiv_l/=/union_equiv_l_rel. move ⇒ [x|x] [y|y].
+ rewrite (@eqv_clot_map _ _ _ _ _ (@inl A B)) //. exact: inl_inj.
+ by rewrite eqv_clot_map_lr.
+ by rewrite equiv_sym eqv_clot_map_lr.
+ by rewrite eqv_clot_map_eq ?sum_eqE // inr_codom_inl.
Qed.

Lemma merge_add_edge (G: graph) (r: equiv_rel G) x u y:
merge (G [x, u, y]) r merge G r [\pi x, u, \pi y].
Proof. Iso bij_id bij_id xpred0. split=>//. case=>//. by case. Defined.
Lemma merge_add_edgeE (G: graph) (r: equiv_rel G) x u y (z: G):
@merge_add_edge G r x u y (\pi z) = \pi z.
Proof. by []. Qed.

Lemma merge_add_vlabel (G: graph) (r: equiv_rel G) x a:
merge (G [tst x <- a]) r merge G r [tst \pi x <- a].
Proof.
Iso bij_id bij_id xpred0. split=>//= v. case: (altP (v =P \pi x)) ⇒ [-> {v}|D].
- rewrite (bigD1 x) // [in X in _ X](bigD1 x) // ?eqxx monA. apply: mon_eqv ⇒ //.
apply: eqv_bigry /andP [_ H]. by rewrite (negbTE H).
- apply: (eqv_big_bij (f := bij_id)) ⇒ //.
+ exact: bij_perm_enum.
+ move ⇒ /= y /eqP ?. case: (altP (y =P x)) ⇒ // ?; subst. by rewrite eqxx in D.
Defined.
Lemma merge_add_vlabelE (G: graph) (r: equiv_rel G) x a (z: G):
@merge_add_vlabel G r x a (\pi z) = \pi z.
Proof. by []. Qed.

isomorphisms about union and merge (Lemma 4.11)

Section union_merge_l.
Variables (F G: graph) (l: pairs F).
Definition h_union_merge_l: bij (merge_seq F l G)%G (merge_seq (F G) (map_pairs unl l)).
Proof. eapply bij_comp. apply union_quot_l. apply quot_same. apply union_equiv_l_eqv_clot. Defined.
Lemma hom_union_merge_l: is_ihom h_union_merge_l bij_id xpred0.
Proof.
split; try by case; intros=>//=; rewrite ?union_quot_lEl ?union_quot_lEr quot_sameE //.
movex. rewrite /=quot_sameE. case:x=>[x|x].
have x0 := repr x.
- pose f (z : F + G) := if z is inl z' then z' else x0.
etransitivity. apply: (reindex_onto (@inl _ _) f) ⇒ /=.
+ move ⇒ [i|i] //=.
by rewrite eq_sym eqmodE eqv_clot_map_lr.
+ rewrite [X in X _]big_mkcond [X in _ X]big_mkcond.
apply: eqv_bigrz _ ⇒ /=.
rewrite eqmodE eqv_clot_map. 2: apply inl_inj.
rewrite eqxx andbT -{2}(reprK x) eqmodE//.
- apply (big_pred1 (inr x))=>y.
rewrite eqmodE. case yz.
+ by rewrite eqv_clot_map_lr.
+ apply eqv_clot_map_eq. by rewrite inr_codom_inl.
Qed.
Definition union_merge_l: merge_seq F l G merge_seq (F G) (map_pairs unl l) :=
Iso hom_union_merge_l.
Lemma union_merge_lEl (x: F): union_merge_l (@unl _ _ (merge_seq F l) _ (\pi x)) = \pi unl x.
Proof. by rewrite /=union_quot_lEl quot_sameE. Qed.
Lemma union_merge_lEr (x: G): union_merge_l (unr x) = \pi unr x.
Proof. by rewrite /=union_quot_lEr quot_sameE. Qed.
Lemma union_merge_lE' (x: F+G):
union_merge_l^-1 (\pi x) =
match x with inl y ⇒ @unl _ _ (merge_seq F l) _ (\pi y) | inr yunr y end.
Proof. by rewrite /=quot_sameE' union_quot_lE'. Qed.
End union_merge_l.
Global Opaque union_merge_l.

Lemma map_map_pairs {A B C} (f: A B) (g: B C) l:
map_pairs g (map_pairs f l) = map_pairs (g \o f) l.
Proof. by rewrite /map_pairs -map_comp. Qed.

Lemma map_pairs_id {A} (l: pairs A): map_pairs id l = l.
Proof. elim l=>//=[[a a'] q]/=. congruence. Qed.

Section union_merge_r.

Variables (F G: graph) (l: pairs G).
Lemma union_merge_r: F merge_seq G l merge_seq (F G) (map_pairs unr l).
Proof.
eapply iso_comp. apply union_C.
eapply iso_comp. apply union_merge_l.
eapply iso_comp. apply (merge_iso (union_C _ _)).
apply merge_same. abstract by rewrite map_map_pairs.
Defined.
Lemma union_merge_rEr (x: G): union_merge_r (@unr _ _ _ (merge_seq G l) (\pi x)) = \pi (unr x).
Proof.
rewrite /=. rewrite (union_merge_lEl F _ x).
rewrite (merge_isoE (union_C G F) _ (unl x)).
by rewrite merge_sameE.
Qed.
Lemma union_merge_rEl (x: F): union_merge_r (unl x) = \pi (unl x).
Proof.
rewrite /=. rewrite (union_merge_lEr _ x) .
rewrite (merge_isoE (union_C G F) _ (unr x)).
by rewrite merge_sameE.
Qed.
End union_merge_r.
Global Opaque union_merge_r.

Section merge_union_K.
Variables (F K: graph) (h: pairs (F+K)) (k: K F).
Definition union_K_pairs := map_pairs (sum_left k) h.

Hypothesis kv: x: K, vlabel x = 1.
Hypothesis kh: x: K, unr x = unl (k x) %[mod (eqv_clot h)].

Lemma equiv_clot_Kl: union_K_equiv (eqv_clot h) =2 eqv_clot union_K_pairs.
Proof.
movex y. rewrite /union_K_equiv map_equivE.
rewrite !eqv_clotE. set e1 := rel_of_pairs _. set e2 := rel_of_pairs _.
apply/idP/idP.
- suff S u v : equiv_of e1 u v equiv_of e2 (sum_left k u) (sum_left k v) by apply: S.
apply: equiv_ofE ⇒ {u v} [[u|u] [u'|u']] /= H.
all: rewrite /e2 /sum_left; apply: sub_equiv_of; apply/mapP.
+ by (unl u,unl u').
+ by (unl u,unr u').
+ by (unr u,unl u').
+ by (unr u,unr u').
- apply: equiv_ofE ⇒ {x y} x x' xx'.
have kh' z : equiv_of e1 (unr z) (unl (k z)).
{ rewrite -eqv_clotE. apply/eqquotP. exact: kh. }
case/mapP : xx' ⇒ [[[u|u] [v|v]] H] /= [-> ->] {x x'}.
+ exact: sub_equiv_of.
+ etransitivity. 2: apply kh'. by apply sub_equiv_of.
+ etransitivity. symmetry; apply kh'. by apply sub_equiv_of.
+ etransitivity. 2: apply kh'. etransitivity. symmetry; apply kh'. by apply sub_equiv_of.
Qed.

Definition h_merge_union_K: bij (merge_seq (union F K) h) (merge_seq F union_K_pairs).
eapply bij_comp. apply quot_union_K with k. apply kh.
apply quot_same. apply equiv_clot_Kl.
Defined.

Hypothesis ke: edge K False.

Definition h_merge_union_Ke1 (e: edge (merge_seq (union F K) h))
: edge (merge_seq F union_K_pairs) :=
match e with inl ee | inr ematch ke e with end end.

Definition h_merge_union_Ke:
bij (edge (merge_seq (union F K) h)) (edge (merge_seq F union_K_pairs)).
h_merge_union_Ke1 inlx//. by case x.
Defined.

Lemma hom_merge_union_K: is_ihom h_merge_union_K h_merge_union_Ke xpred0.
Proof.
split; try (case; intros =>//=; by rewrite quot_union_KE quot_sameE).
movev/=.
rewrite quot_sameE/=.
have x0 : F. { case: (repr v). exact: id. exact k. }
etransitivity. apply: (reindex_onto (sum_left (fun _ : Kx0)) (@inl _ _)) ⇒ //.
rewrite /= [X in X _]big_mkcond [X in _ X]big_mkcond /=.
apply: eqv_bigr ⇒ [[x|x]] /= _.
- rewrite eqxx andbT eqmodE. rewrite -{2}(reprK v) eqmodE.
rewrite -equiv_clot_Kl. simpl. rewrite /map_equiv_rel/=.
set (r := repr _). case r=>//= w.
generalize (kh w). rewrite -eqmodE. move <-. by rewrite eqmodE.
- rewrite andbC kv -[X in X _]/1. by case: ifP.
Qed.

Definition merge_union_K: merge_seq (F K) h merge_seq F union_K_pairs :=
Iso hom_merge_union_K.
Lemma merge_union_KE (x: F+K): merge_union_K (\pi x) = \pi (sum_left k x).
Proof. by rewrite /=quot_union_KE quot_sameE. Qed.
End merge_union_K.
Global Opaque merge_union_K.

Lemma two_graph_swap a b: two_graph a b two_graph b a.
Proof. apply union_C. Defined.

Proof. moveF G h a b ab. apply (union_iso h (unit_graph_iso ab)). Defined.

Subgraphs and Induced Subgraphs

Definition subgraph (H G : graph) :=
hv he hd, @is_ihom H G hv he hd injective hv injective he.

Section Sub.
Variables (G : graph) (V : {set G}) (E : {set edge G}).
Hypothesis con : consistent V E.

Lemma subgraph_sub : subgraph (subgraph_for con) G.
Proof. val, val, xpred0. split ⇒ //=. split; exact: val_inj. Qed.

Lemma remove_edges_sub : subgraph (remove_edges E) G.
Proof. id, val, xpred0. split ⇒ //=. split. apply inj_id. apply val_inj. Qed.
End Sub.

Lemma induced_sub (G: graph) (S : {set G}) : subgraph (induced S) G.
Proof. exact: subgraph_sub. Qed.

Lemma incident_iso (F G : graph) (h : F G) (x : F) (e : edge F) :
incident x e = incident (h x) (h.e e).
Proof.
rewrite /incident. apply/existsP/existsP ⇒ [] [b] E; (h.d e (+) b).
- by rewrite endpoint_iso bij_eq in E.
Qed.

Lemma edges_at_iso (F G : graph) (h : F G) (x : F) :
edges_at (h x) = [set h.e e | e in edges_at x].
Proof.
apply/setPe. by rewrite -[e](bijK' h.e) bij_mem_imset !inE (incident_iso h).
Qed.

Lemma setT_bij_hom (G : graph) :
@is_ihom (subgraph_for (consistentTT G)) G setT_bij setT_bij xpred0.
Proof. by []. Qed.

Definition iso_subgraph_forT (G : graph) : subgraph_for (consistentTT G) G :=
Iso (setT_bij_hom G).

End s2.

Arguments add_vlabel {Lv Le} G x a.
Notation "G [tst x <- a ]" :=
(add_vlabel G x a) (at level 20, left associativity) : graph_scope.

Arguments merge {Lv Le} _ _.
Notation merge_seq G l := (merge G (eqv_clot l)).

Arguments iso {Lv Le}.
Arguments iso_id {_ _ _}.
Infix "≃" := iso (at level 79).
Notation "h '.e'" := (iso_e h) (at level 2, left associativity, format "h '.e'").
Notation "h '.d'" := (iso_d h) (at level 2, left associativity, format "h '.d'").

Tactic Notation "Iso" uconstr(f) uconstr(g) uconstr(h) :=
match goal with |- ?F ?Grefine (@Iso _ _ F G f g h _) end.

Global Hint Resolve iso_id : core.

Merging Subgraphs

This construction allows transforming a quotient on G[V1,E1] + G[V2,E2] into a quotient on G[V1 :|: V2, E1 :|: E2], provided the edge sets are disjoint and the quotient merges all duplicated verices (i.e., those occurring both in V1 and in V2. The underlying function on vertices from G[V1,E1] + G[V2,E2] to G[V1 :|: V2, E1 :|: E2] simply drops the inl/inr. For the converse direction, we inject into G[V1,E1] if possible and otherwise into G[V1,E2]. Note that this only yields a bijection after quotienting.

Section MergeSubgraph.
Variable (Le : elabelType).
Notation graph := (graph unit Le).
Variables (G : graph) (V1 V2 : {set G}) (E1 E2 : {set edge G})
(con1 : consistent V1 E1) (con2 : consistent V2 E2)
(h : pairs (subgraph_for con1 subgraph_for con2)%G).

Lemma consistentU : consistent (V1 :|: V2) (E1 :|: E2).
Proof using con1 con2.
movee b. case/setUPE.
- by rewrite !inE con1.
- by rewrite !inE con2.
Qed.

Hypothesis eqvI : x (inU : x \in V1) (inV : x \in V2),
inl (Sub x inU) = inr (Sub x inV) %[mod eqv_clot h].

Hypothesis disE : [disjoint E1 & E2].

Local Notation G1 := (subgraph_for con1).
Local Notation G2 := (subgraph_for con2).
Local Notation G12 := (subgraph_for consistentU).

Definition h' := map_pairs (@merge_union_fwd _ _ _) h.
Lemma eqv_clot_union_rel : merge_union_rel (eqv_clot h) =2 eqv_clot h'.
Proof.
movex y. rewrite /merge_union_rel /h' map_equivE. apply/idP/idP.
- have aux z : merge_union_fwd (merge_union_bwd z) = z %[mod eqv_clot (map_pairs (@merge_union_fwd _ _ _) h)].
{ apply/eqquotP. case: merge_union_bwdP ⇒ *; apply: eq_equiv; by apply: val_inj. }
moveH. apply/eqquotP. rewrite -[_ x]aux -[_ y]aux. apply/eqquotP.
move: H. apply: eqv_clot_map'.
- rewrite eqv_clotE. apply: equiv_ofE ⇒ /= {x y} x y.
rewrite /rel_of_pairs/=. case/mapP ⇒ /= [[u v]] in_h [-> ->].
apply/eqquotP. rewrite 2!(merge_union_can eqvI). apply/eqquotP.
exact: eqv_clot_pair.
Qed.

Definition merge_subgraph_v : bij (merge_seq (G1 G2) h) (merge_seq G12 h') :=
Eval hnf in (bij_comp (merge_union eqvI) (quot_same eqv_clot_union_rel)).

Definition merge_subgraph_e : bij (edge G1 + edge G2) (edge G12) :=
merge_disjoint_union disE.

Lemma merge_subgraph_hom : is_ihom merge_subgraph_v merge_subgraph_e xpred0.
Proof.
rewrite /merge_subgraph_e /merge_subgraph_v.
split=>//.
- casex b /=; rewrite merge_unionE quot_sameE; congr pi; exact: val_inj.
- casee //.
Qed.

Definition merge_subgraph_iso : merge_seq (G1 G2) h merge_seq G12 h' :=
Iso merge_subgraph_hom.

Lemma merge_subgraph_isoE x0 :
( x, merge_subgraph_iso (\pi (inl x)) = \pi (insubd x0 (val x))) ×
( y, merge_subgraph_iso (\pi (inr y)) = \pi (insubd x0 (val y))).
Proof.
split ⇒ [x|y].
all: rewrite /= !quot_sameE.
all: apply/eqquotP; rewrite -eqv_clot_union_rel; apply/eqquotP.
all: symmetry; rewrite -merge_union_can'; apply: merge_union_fwd_hom ⇒ //.
all: rewrite reprK /merge_union_bwd.
- case: setU_dec; rewrite val_insubd !inE !(valP x) //=. 2: by case.
movea. by rewrite valK'.
- case: setU_dec; rewrite !val_insubd !inE !(valP y) !orbT //=.
+ movea. by rewrite -{2}[y]valK' ?(valP y).
+ casea b /=. by rewrite valK'.
Qed.

End MergeSubgraph.

Walks

Definition mgraph_rel Lv Le (G : graph Lv Le) : rel G :=
fun x y[ e, (source e == x) && (target e == y)].

Definition digraph_of Lv Le (G : graph Lv Le) := DiGraph (@mgraph_rel Lv Le G).

Section Walk.
Variable (Lv Le : Type) (G : graph Lv Le).
Implicit Types (x y z : G) (e : edge G) (w : seq (edge G)).

Fixpoint walk x y w :=
if w is e :: w' then (source e == x) && walk (target e) y w' else x == y.

Definition eseparates x y (E : {set edge G}) :=
w, walk x y w exists2 e, e \in E & e \in w.

Definition line_graph := DiGraph [rel e1 e2 : edge G | target e1 == source e2].

Lemma walk_of_line e1 e2 (p : @Path line_graph e1 e2) :
walk (source e1) (target e2) (nodes p).
Proof.
case: pp pth_p. rewrite nodesE /= eqxx /=.
elim: p e1 pth_p ⇒ [e1 pth_p|e w IHw e1].
- by rewrite (pathp_nil pth_p) /= eqxx.
- by rewrite pathp_cons /edge_rel /= eq_sym ⇒ /andP [-> /IHw].
Qed.

Lemma line_of_walk x y w : walk x y w ~~ nilp w
e1 e2 (p : @Path line_graph e1 e2), [/\ source e1 = x, target e2 = y & nodes p = w].
Proof.
elim: w x ⇒ //= e [|e' w] IH x /andP[src_e walk_w] _.
- e. e. (@idp line_graph e).
rewrite nodesE /idp /= (eqP src_e). split ⇒ //. exact/eqP.
- case: (IH _ walk_w _) ⇒ // e1 [e2] [p] [P1 P2 P3].
have ee1 : @edge_rel line_graph e e1 by apply/eqP; rewrite P1.
e. e2. (pcat (edgep ee1) p). rewrite (eqP src_e) P2. split ⇒ //.
rewrite !nodesE /= in P3 ×. case: P3 ⇒ ? ?. by subst.
Qed.

End Walk.