(* Basic facts of Graph Theory
* Made in 2018 by Daniel Severin
* Runs on Coq 8.6 and requires MathComp 1.6.1 and sgraph.v *)
From mathcomp Require Import all_ssreflect.
Require Import sgraph.
Set Implicit Arguments.
Unset Strict Implicit.
(**********************************************************************************)
Section Preliminaries1.
Variable T : finType.
Variables u v : T.
Variables A B : {set T}.
Lemma sum_disjoint_union : forall f : T -> nat, A :&: B = ∅ ->
Σ(i in T | i ∈ (A :|: B)) f i = Σ(i in T | i ∈ A) f i + Σ(i in T | i ∈ B) f i.
Proof.
move=> f /eqP disjAB.
rewrite setI_eq0 in disjAB.
have H1 : forall i : T, i ∈ (A :|: B) = (i ∈ [predU A & B]).
move=> i ; by rewrite in_setU.
have H2 : Σ(i in T | i ∈ (A :|: B)) f i = Σ(i in T | i ∈ [predU A & B]) f i.
apply: eq_bigl => i ; by rewrite H1.
rewrite H2.
exact: bigU.
Qed.
Lemma sum_empty : forall f : T -> nat, Σ(i in T | i ∈ ∅) f i = 0.
Proof.
move=> f.
rewrite (eq_bigl (fun i => false)).
by rewrite big_pred0_eq.
move=> i ; by rewrite in_set0 andbF.
Qed.
Lemma sum_singleton : forall f : T -> nat, Σ(i in T | i ∈ ❴u❵) f i = f u.
Proof.
move=> f.
rewrite (eq_bigl (fun i => i == u)) ; last first.
move=> i.
by rewrite in_set1.
rewrite -big_filter.
have H1: \sum_(i <- (cons u nil)) f i = f u by rewrite big_cons big_nil.
rewrite -H1.
apply congr_big => [ | // | //].
by rewrite filter_index_enum enum1.
Qed.
Lemma set_minus_union : B ⊆ A -> A = (A :\: B) :|: B.
Proof.
move=> BinA.
apply/eqP.
rewrite eqEsubset.
apply/andP ; split.
(* first case: x ∈ A implies x ∈ (A - B cup B) *)
apply/subsetP => x xinA.
by rewrite in_setU in_setD orb_andl xinA orNb andTb orTb.
(* second case: x ∈ (A - B cup B) -> x ∈ A *)
apply/subsetP => x.
rewrite in_setU in_setD orb_andl orNb andTb => /orP.
elim=> //.
by apply (subsetP BinA).
Qed.
Lemma set_minus_disjoint : (A :\: B) :&: B = ∅.
Proof. by rewrite setIDAC -setIDA setDv setI0. Qed.
Lemma set_pair_disjoint : (u <> v) -> ❴u❵ :&: ❴v❵ = ∅.
Proof.
move=> uneqv.
apply/setP => x.
apply/setIP.
rewrite in_set0 !in_set1.
elim=> xisu.
move/eqP: xisu -> => /eqP uisv.
contradiction.
Qed.
Lemma subset_inter : B ⊆ A -> B = A :&: B.
Proof.
move=> BinA.
apply/eqP.
rewrite eqEsubset.
apply/andP ; split.
apply/subsetP => x xinB ; by rewrite in_setI xinB ((subsetP BinA) x xinB).
apply/subsetP => x ; by rewrite in_setI => /andP [_ xinB].
Qed.
Lemma pair_absorb : ❴u; u❵ = ❴u❵.
Proof. apply/setP => x ; by rewrite in_set1 in_set2 orbb. Qed.
Lemma pair_commute : ❴u; v❵ = ❴v; u❵.
Proof. apply/setP => x ; by rewrite !in_set2 orbC. Qed.
End Preliminaries1.
(**********************************************************************************)
Section Preliminaries2.
Variable T : finType.
Lemma set_minus_union1 : forall (u : T) (A : {set T}), u ∈ A -> A = (A :\: ❴u❵) :|: ❴u❵.
Proof.
move=> u A uinA.
apply: set_minus_union.
apply/subsetP => i.
rewrite in_set1 => ieqx.
by move/eqP: ieqx ->.
Qed.
Lemma set21_subset : forall (u v : T) (A : {set T}), ❴u; v❵ ⊆ A -> u ∈ A.
Proof. move=> u v A uvsubA ; apply: (subsetP uvsubA u) ; exact: set21. Qed.
Lemma set22_subset : forall (u v : T) (A : {set T}), ❴u; v❵ ⊆ A -> v ∈ A.
Proof. move=> u v A ; rewrite pair_commute ; exact: set21_subset. Qed.
Lemma doubleton_eq_left : forall u v w : T, ❴u; v❵ = ❴u; w❵ <-> v = w.
Proof.
move=> u v w.
rewrite /iff ; split ; last by move->.
(* we prove the hard case: {u, v} = {u, w} -> v = w *)
move=> uvisuw.
apply/eqP.
move: (set22 u v) => H1.
rewrite uvisuw in_set2 in H1.
case/orP: H1 => [visu | // ].
rewrite -!(eqP visu) pair_absorb in uvisuw.
move: (set22 v w) => H2.
by rewrite eq_sym -in_set1 uvisuw.
Qed.
Lemma doubleton_eq_right : forall u v w : T, ❴u; w❵ = ❴v; w❵ <-> u = v.
Proof.
move=> u v w.
rewrite (pair_commute u w) (pair_commute v w).
exact: doubleton_eq_left.
Qed.
Lemma doubleton_eq_iff : forall u v w x: T, ❴u; v❵ = ❴w; x❵ <->
((u = w /\ v = x) \/ (u = x /\ v = w)).
Proof.
move=> u v w x.
rewrite /iff ; split ; last first.
(* first case : <- *)
case => [ [uisw visx] | [uisx visw] ].
by rewrite uisw visx.
by rewrite uisx visw pair_commute.
(* second case : -> *)
move=> uviswx.
move: (set21 u v) => uinwx.
rewrite uviswx in_set2 in uinwx.
case/orP: uinwx => [/eqP uisw|/eqP uisx].
left ; split => //.
move: (doubleton_eq_left w v x) => [dbl_eq_left _].
apply: dbl_eq_left.
by rewrite -[in X in X = _] uisw.
right ; split => //.
move: (doubleton_eq_right v w x) => [dbl_eq_right _].
apply: dbl_eq_right.
rewrite -[in X in X = _] uisx -uviswx.
exact: pair_commute.
Qed.
Lemma pair_neq_card2 : forall u v : T, (u <> v) <-> #|❴u; v❵| = 2.
Proof.
move=> u v.
rewrite /iff ; split.
(* first case: -> *)
move=> uneqv.
rewrite cardsU !cards1.
by rewrite (set_pair_disjoint uneqv) cards0.
(* second case: <- *)
move=> eis2 ueqv.
by rewrite ueqv (pair_absorb v) cards1 in eis2.
Qed.
Lemma pair_card2_exists : forall S : {set T}, #|S| = 2 -> exists u v : T, u <> v /\ S = ❴u; v❵.
Proof.
move=> S Sis2.
(* we first extract an element u *)
have: exists u : T, u ∈ S by apply/set0Pn ; rewrite -card_gt0 Sis2 ltn0Sn.
move=> [u uine].
exists u.
have Sminusuis1: #|S :\: ❴u❵| == 1.
rewrite (cardsD1 u S) uine in Sis2.
by rewrite -(eqn_add2l 1) Sis2.
(* then, an element v *)
have: exists v : T, v ∈ (S :\: ❴u❵).
by apply/set0Pn ; rewrite -card_gt0 (eqP Sminusuis1) ltn0Sn.
move=> [v vinSminusu].
exists v.
rewrite in_setD1 in vinSminusu.
move: vinSminusu => /andP [-/eqP vnequ vinS].
split ; [ exact: not_eq_sym vnequ | ].
apply/eqP.
rewrite eq_sym eqEcard.
apply/andP ; split.
apply/subsetP => x xinuv.
rewrite in_set2 in xinuv.
case/orP: xinuv => [xisu|xisv].
by move/eqP: xisu ->.
by move/eqP: xisv ->.
rewrite pair_commute.
move: vnequ.
rewrite (pair_neq_card2 v u) => vucard2.
by rewrite vucard2 Sis2 /=.
Qed.
End Preliminaries2.
(**********************************************************************************)
Variable T : finType.
Variables u v : T.
Variables A B : {set T}.
Lemma sum_disjoint_union : forall f : T -> nat, A :&: B = ∅ ->
Σ(i in T | i ∈ (A :|: B)) f i = Σ(i in T | i ∈ A) f i + Σ(i in T | i ∈ B) f i.
Proof.
move=> f /eqP disjAB.
rewrite setI_eq0 in disjAB.
have H1 : forall i : T, i ∈ (A :|: B) = (i ∈ [predU A & B]).
move=> i ; by rewrite in_setU.
have H2 : Σ(i in T | i ∈ (A :|: B)) f i = Σ(i in T | i ∈ [predU A & B]) f i.
apply: eq_bigl => i ; by rewrite H1.
rewrite H2.
exact: bigU.
Qed.
Lemma sum_empty : forall f : T -> nat, Σ(i in T | i ∈ ∅) f i = 0.
Proof.
move=> f.
rewrite (eq_bigl (fun i => false)).
by rewrite big_pred0_eq.
move=> i ; by rewrite in_set0 andbF.
Qed.
Lemma sum_singleton : forall f : T -> nat, Σ(i in T | i ∈ ❴u❵) f i = f u.
Proof.
move=> f.
rewrite (eq_bigl (fun i => i == u)) ; last first.
move=> i.
by rewrite in_set1.
rewrite -big_filter.
have H1: \sum_(i <- (cons u nil)) f i = f u by rewrite big_cons big_nil.
rewrite -H1.
apply congr_big => [ | // | //].
by rewrite filter_index_enum enum1.
Qed.
Lemma set_minus_union : B ⊆ A -> A = (A :\: B) :|: B.
Proof.
move=> BinA.
apply/eqP.
rewrite eqEsubset.
apply/andP ; split.
(* first case: x ∈ A implies x ∈ (A - B cup B) *)
apply/subsetP => x xinA.
by rewrite in_setU in_setD orb_andl xinA orNb andTb orTb.
(* second case: x ∈ (A - B cup B) -> x ∈ A *)
apply/subsetP => x.
rewrite in_setU in_setD orb_andl orNb andTb => /orP.
elim=> //.
by apply (subsetP BinA).
Qed.
Lemma set_minus_disjoint : (A :\: B) :&: B = ∅.
Proof. by rewrite setIDAC -setIDA setDv setI0. Qed.
Lemma set_pair_disjoint : (u <> v) -> ❴u❵ :&: ❴v❵ = ∅.
Proof.
move=> uneqv.
apply/setP => x.
apply/setIP.
rewrite in_set0 !in_set1.
elim=> xisu.
move/eqP: xisu -> => /eqP uisv.
contradiction.
Qed.
Lemma subset_inter : B ⊆ A -> B = A :&: B.
Proof.
move=> BinA.
apply/eqP.
rewrite eqEsubset.
apply/andP ; split.
apply/subsetP => x xinB ; by rewrite in_setI xinB ((subsetP BinA) x xinB).
apply/subsetP => x ; by rewrite in_setI => /andP [_ xinB].
Qed.
Lemma pair_absorb : ❴u; u❵ = ❴u❵.
Proof. apply/setP => x ; by rewrite in_set1 in_set2 orbb. Qed.
Lemma pair_commute : ❴u; v❵ = ❴v; u❵.
Proof. apply/setP => x ; by rewrite !in_set2 orbC. Qed.
End Preliminaries1.
(**********************************************************************************)
Section Preliminaries2.
Variable T : finType.
Lemma set_minus_union1 : forall (u : T) (A : {set T}), u ∈ A -> A = (A :\: ❴u❵) :|: ❴u❵.
Proof.
move=> u A uinA.
apply: set_minus_union.
apply/subsetP => i.
rewrite in_set1 => ieqx.
by move/eqP: ieqx ->.
Qed.
Lemma set21_subset : forall (u v : T) (A : {set T}), ❴u; v❵ ⊆ A -> u ∈ A.
Proof. move=> u v A uvsubA ; apply: (subsetP uvsubA u) ; exact: set21. Qed.
Lemma set22_subset : forall (u v : T) (A : {set T}), ❴u; v❵ ⊆ A -> v ∈ A.
Proof. move=> u v A ; rewrite pair_commute ; exact: set21_subset. Qed.
Lemma doubleton_eq_left : forall u v w : T, ❴u; v❵ = ❴u; w❵ <-> v = w.
Proof.
move=> u v w.
rewrite /iff ; split ; last by move->.
(* we prove the hard case: {u, v} = {u, w} -> v = w *)
move=> uvisuw.
apply/eqP.
move: (set22 u v) => H1.
rewrite uvisuw in_set2 in H1.
case/orP: H1 => [visu | // ].
rewrite -!(eqP visu) pair_absorb in uvisuw.
move: (set22 v w) => H2.
by rewrite eq_sym -in_set1 uvisuw.
Qed.
Lemma doubleton_eq_right : forall u v w : T, ❴u; w❵ = ❴v; w❵ <-> u = v.
Proof.
move=> u v w.
rewrite (pair_commute u w) (pair_commute v w).
exact: doubleton_eq_left.
Qed.
Lemma doubleton_eq_iff : forall u v w x: T, ❴u; v❵ = ❴w; x❵ <->
((u = w /\ v = x) \/ (u = x /\ v = w)).
Proof.
move=> u v w x.
rewrite /iff ; split ; last first.
(* first case : <- *)
case => [ [uisw visx] | [uisx visw] ].
by rewrite uisw visx.
by rewrite uisx visw pair_commute.
(* second case : -> *)
move=> uviswx.
move: (set21 u v) => uinwx.
rewrite uviswx in_set2 in uinwx.
case/orP: uinwx => [/eqP uisw|/eqP uisx].
left ; split => //.
move: (doubleton_eq_left w v x) => [dbl_eq_left _].
apply: dbl_eq_left.
by rewrite -[in X in X = _] uisw.
right ; split => //.
move: (doubleton_eq_right v w x) => [dbl_eq_right _].
apply: dbl_eq_right.
rewrite -[in X in X = _] uisx -uviswx.
exact: pair_commute.
Qed.
Lemma pair_neq_card2 : forall u v : T, (u <> v) <-> #|❴u; v❵| = 2.
Proof.
move=> u v.
rewrite /iff ; split.
(* first case: -> *)
move=> uneqv.
rewrite cardsU !cards1.
by rewrite (set_pair_disjoint uneqv) cards0.
(* second case: <- *)
move=> eis2 ueqv.
by rewrite ueqv (pair_absorb v) cards1 in eis2.
Qed.
Lemma pair_card2_exists : forall S : {set T}, #|S| = 2 -> exists u v : T, u <> v /\ S = ❴u; v❵.
Proof.
move=> S Sis2.
(* we first extract an element u *)
have: exists u : T, u ∈ S by apply/set0Pn ; rewrite -card_gt0 Sis2 ltn0Sn.
move=> [u uine].
exists u.
have Sminusuis1: #|S :\: ❴u❵| == 1.
rewrite (cardsD1 u S) uine in Sis2.
by rewrite -(eqn_add2l 1) Sis2.
(* then, an element v *)
have: exists v : T, v ∈ (S :\: ❴u❵).
by apply/set0Pn ; rewrite -card_gt0 (eqP Sminusuis1) ltn0Sn.
move=> [v vinSminusu].
exists v.
rewrite in_setD1 in vinSminusu.
move: vinSminusu => /andP [-/eqP vnequ vinS].
split ; [ exact: not_eq_sym vnequ | ].
apply/eqP.
rewrite eq_sym eqEcard.
apply/andP ; split.
apply/subsetP => x xinuv.
rewrite in_set2 in xinuv.
case/orP: xinuv => [xisu|xisv].
by move/eqP: xisu ->.
by move/eqP: xisv ->.
rewrite pair_commute.
move: vnequ.
rewrite (pair_neq_card2 v u) => vucard2.
by rewrite vucard2 Sis2 /=.
Qed.
End Preliminaries2.
(**********************************************************************************)
Section Neighborhoods_definitions.
Variable G : sgraph.
Definition open_neigh : G -> {set G} := fun u => ❴v | sedge u v❵.
Local Notation "N( x )" := (open_neigh x) (at level 0, x at level 99).
Definition closed_neigh : G -> {set G} := fun u => N(u) :|: ❴u❵.
Local Notation "N[ x ]" := (closed_neigh x) (at level 0, x at level 99).
Definition cl_sedge : G -> G -> bool := fun u v => (u -- v) || (u == v).
Definition edge_set_pred : {set G} -> Prop :=
fun e => (#|e| = 2) /\ forall u v : G, e = ❴u; v❵ -> (u -- v).
Definition edge_set_predb : pred {set G} :=
fun e => (#|e| == 2) && [forall u, forall v, (e == ❴u; v❵) ==> (u -- v) ].
Definition edge_set := ❴e | edge_set_predb e❵.
Definition isolate_graph := edge_set = ∅.
Definition deg : G -> nat := fun v => #|N(v)|.
Variable D : {set G}.
Definition open_neigh_set : {set G} := ⋃(w in G | w ∈ D) N(w).
Definition closed_neigh_set : {set G} := ⋃(w in G | w ∈ D) N[w].
End Neighborhoods_definitions.
Notation "N( G ; x )" := (@open_neigh G x) (at level 0, G at level 99, x at level 99).
Notation "N[ G ; x ]" := (@closed_neigh G x) (at level 0, G at level 99, x at level 99).
Notation "N( x )" := (open_neigh x) (at level 0, x at level 99, only parsing).
Notation "N[ x ]" := (closed_neigh x) (at level 0, x at level 99, only parsing).
Notation "x -*- y" := (cl_sedge x y) (at level 30).
Notation "V( G )" := (setT : {set G}) (at level 0, G at level 99).
Notation "E( G )" := (@edge_set G) (at level 0, G at level 99).
Notation "NS( G ; D )" := (@open_neigh_set G D) (at level 0, G at level 99, D at level 99).
Notation "NS( D )" := (open_neigh_set D) (at level 0, D at level 99).
Notation "NS[ G ; D ]" := (@closed_neigh_set G D) (at level 0, G at level 99, D at level 99).
Notation "NS[ D ]" := (closed_neigh_set D) (at level 0, D at level 99).
Global Arguments deg : clear implicits.
(**********************************************************************************)
Section Basic_Facts_Neighborhoods.
Variable G : sgraph.
Lemma sg_opneigh : forall u v : G, u -- v = (u ∈ N(v)).
Proof. move=> u v ; by rewrite /open_neigh in_set sg_sym. Qed.
Lemma clsg_clneigh : forall u v : G, u -*- v = (u ∈ N[v]).
Proof.
move=> u v.
rewrite /closed_neigh in_set in_set1.
apply: orb_id2r => _.
exact: sg_opneigh.
Qed.
Lemma cl_sg_sym : symmetric (@cl_sedge G). (* cl_sedge u v = cl_sedge v u *)
Proof. rewrite /symmetric /cl_sedge /closed_neigh => x y ; by rewrite sg_sym eq_sym. Qed.
Lemma cl_sg_refl : reflexive (@cl_sedge G). (* cl_sedge u u = true *)
Proof. rewrite /reflexive /cl_sedge /closed_neigh => u ; by rewrite eq_refl orbT. Qed.
Lemma edges_size_two : forall e : {set G}, e ∈ E(G) -> #|e| = 2.
Proof. move=> e ; rewrite /edge_set in_set => /andP [eis2 _] ; exact: eqP eis2. Qed.
Proposition edge_setP : forall e : {set G}, reflect (edge_set_pred e) (edge_set_predb e).
Proof.
move=> e.
rewrite /edge_set_pred /edge_set_predb.
apply: (iffP andP).
(* first case: bool to Prop *)
move=> [/eqP eis2 /forallP H1].
split ; [exact: eis2 | ].
move=> u v.
move: (H1 u) => /forallP /(_ v) /implyP => H2.
by move/eqP.
(* second case: Prop to bool *)
move=> [/eqP eis2 H2].
split ; [exact: eis2 | ].
apply/forallP => u.
apply/forallP => v.
move: ((H2 u) v) => H3.
apply/implyP.
by move/eqP.
Qed.
Proposition sg_in_edge_set : forall u v : G, u -- v <-> ❴u; v❵ ∈ E(G).
Proof.
move=> u v.
rewrite /edge_set in_set.
rewrite /iff ; split.
(* case: -> *)
move=> adjuv.
apply/edge_setP.
rewrite /edge_set_pred.
split.
rewrite -pair_neq_card2.
move: (negbT (sg_edgeNeq adjuv)).
by move/eqP.
move=> u' v'.
rewrite doubleton_eq_iff.
case=> [ [uisu' visv'] | [uisv' visu'] ].
by rewrite -uisu' -visv'.
by rewrite -uisv' -visu' sg_sym.
(* case: <- *)
move/edge_setP.
rewrite /edge_set_pred => [ [_ ] ].
by move=> /(_ u v) ->.
Qed.
Proposition sg_isolate_graph : forall u v : G, isolate_graph G -> u -- v = false.
Proof.
move=> u v.
rewrite /isolate_graph.
move/eqP.
apply: contraTF => adjuv.
apply/set0Pn.
exists ❴u; v❵.
rewrite /edge_set in_set.
apply/edge_setP.
rewrite /edge_set_pred.
split.
rewrite -(pair_neq_card2 u v) => /eqP.
by rewrite sg_edgeNeq.
move=> u' v'.
rewrite doubleton_eq_iff.
elim=> [ [uisu' visv'] | [uisv' visu'] ].
by rewrite -uisu' -visv'.
by rewrite -uisv' -visu' sg_sym.
Qed.
Proposition deg_isolate_graph : forall v : G, isolate_graph G -> deg G v = 0.
Proof.
move=> v i_graph.
rewrite /deg /open_neigh.
apply/eqP.
rewrite cards_eq0 -subset0.
apply/subsetP => x.
rewrite inE in_set0.
by rewrite sg_isolate_graph.
Qed.
Variables D1 D2 : {set G}.
Proposition D_in_closed_neight_set : D1 ⊆ NS[D1].
Proof.
apply/subsetP => x xinD1.
rewrite /closed_neigh_set /closed_neigh.
apply/bigcupP.
exists x.
by rewrite xinD1.
by rewrite in_setU in_set1 eq_refl orbT.
Qed.
Proposition dominated_belongs_to_open_neigh_set : forall u v : G, u ∈ D1 -> u -- v -> v ∈ NS(D1).
Proof.
move=> u v uinD1 adjuv.
rewrite /open_neigh_set.
apply/bigcupP.
exists u.
apply/andP ; split=> [// | //].
by rewrite /open_neigh in_set.
Qed.
Proposition open_neigh_set_subset_closed_neigh_set : NS(D1) ⊆ NS[D1].
Proof.
apply/subsetP => u.
rewrite /open_neigh_set /closed_neigh_set.
move/bigcupP.
elim=> v /andP [_ vinD1] uinNv.
apply/bigcupP.
exists v => [// | ].
by rewrite /closed_neigh in_setU uinNv orTb.
Qed.
Proposition dominated_belongs_to_closed_neigh_set : forall u v : G, u ∈ D1 -> u -- v -> v ∈ NS[D1].
Proof.
move=> u v uinD1 adjuv.
apply: (subsetP open_neigh_set_subset_closed_neigh_set v).
exact: dominated_belongs_to_open_neigh_set adjuv.
Qed.
Proposition closed_neigh_set_subset : D1 ⊆ D2 -> NS[D1] ⊆ NS[D2].
Proof.
move=> D1subD2.
rewrite /closed_neigh_set.
apply/subsetP => x /bigcupP.
elim=> i /andP [_ iinD1] xinNi.
apply/bigcupP.
exists i.
apply/andP ; split=> //.
exact: subsetP D1subD2 i iinD1.
exact: xinNi.
Qed.
End Basic_Facts_Neighborhoods.
(**********************************************************************************)
Variable G : sgraph.
Definition open_neigh : G -> {set G} := fun u => ❴v | sedge u v❵.
Local Notation "N( x )" := (open_neigh x) (at level 0, x at level 99).
Definition closed_neigh : G -> {set G} := fun u => N(u) :|: ❴u❵.
Local Notation "N[ x ]" := (closed_neigh x) (at level 0, x at level 99).
Definition cl_sedge : G -> G -> bool := fun u v => (u -- v) || (u == v).
Definition edge_set_pred : {set G} -> Prop :=
fun e => (#|e| = 2) /\ forall u v : G, e = ❴u; v❵ -> (u -- v).
Definition edge_set_predb : pred {set G} :=
fun e => (#|e| == 2) && [forall u, forall v, (e == ❴u; v❵) ==> (u -- v) ].
Definition edge_set := ❴e | edge_set_predb e❵.
Definition isolate_graph := edge_set = ∅.
Definition deg : G -> nat := fun v => #|N(v)|.
Variable D : {set G}.
Definition open_neigh_set : {set G} := ⋃(w in G | w ∈ D) N(w).
Definition closed_neigh_set : {set G} := ⋃(w in G | w ∈ D) N[w].
End Neighborhoods_definitions.
Notation "N( G ; x )" := (@open_neigh G x) (at level 0, G at level 99, x at level 99).
Notation "N[ G ; x ]" := (@closed_neigh G x) (at level 0, G at level 99, x at level 99).
Notation "N( x )" := (open_neigh x) (at level 0, x at level 99, only parsing).
Notation "N[ x ]" := (closed_neigh x) (at level 0, x at level 99, only parsing).
Notation "x -*- y" := (cl_sedge x y) (at level 30).
Notation "V( G )" := (setT : {set G}) (at level 0, G at level 99).
Notation "E( G )" := (@edge_set G) (at level 0, G at level 99).
Notation "NS( G ; D )" := (@open_neigh_set G D) (at level 0, G at level 99, D at level 99).
Notation "NS( D )" := (open_neigh_set D) (at level 0, D at level 99).
Notation "NS[ G ; D ]" := (@closed_neigh_set G D) (at level 0, G at level 99, D at level 99).
Notation "NS[ D ]" := (closed_neigh_set D) (at level 0, D at level 99).
Global Arguments deg : clear implicits.
(**********************************************************************************)
Section Basic_Facts_Neighborhoods.
Variable G : sgraph.
Lemma sg_opneigh : forall u v : G, u -- v = (u ∈ N(v)).
Proof. move=> u v ; by rewrite /open_neigh in_set sg_sym. Qed.
Lemma clsg_clneigh : forall u v : G, u -*- v = (u ∈ N[v]).
Proof.
move=> u v.
rewrite /closed_neigh in_set in_set1.
apply: orb_id2r => _.
exact: sg_opneigh.
Qed.
Lemma cl_sg_sym : symmetric (@cl_sedge G). (* cl_sedge u v = cl_sedge v u *)
Proof. rewrite /symmetric /cl_sedge /closed_neigh => x y ; by rewrite sg_sym eq_sym. Qed.
Lemma cl_sg_refl : reflexive (@cl_sedge G). (* cl_sedge u u = true *)
Proof. rewrite /reflexive /cl_sedge /closed_neigh => u ; by rewrite eq_refl orbT. Qed.
Lemma edges_size_two : forall e : {set G}, e ∈ E(G) -> #|e| = 2.
Proof. move=> e ; rewrite /edge_set in_set => /andP [eis2 _] ; exact: eqP eis2. Qed.
Proposition edge_setP : forall e : {set G}, reflect (edge_set_pred e) (edge_set_predb e).
Proof.
move=> e.
rewrite /edge_set_pred /edge_set_predb.
apply: (iffP andP).
(* first case: bool to Prop *)
move=> [/eqP eis2 /forallP H1].
split ; [exact: eis2 | ].
move=> u v.
move: (H1 u) => /forallP /(_ v) /implyP => H2.
by move/eqP.
(* second case: Prop to bool *)
move=> [/eqP eis2 H2].
split ; [exact: eis2 | ].
apply/forallP => u.
apply/forallP => v.
move: ((H2 u) v) => H3.
apply/implyP.
by move/eqP.
Qed.
Proposition sg_in_edge_set : forall u v : G, u -- v <-> ❴u; v❵ ∈ E(G).
Proof.
move=> u v.
rewrite /edge_set in_set.
rewrite /iff ; split.
(* case: -> *)
move=> adjuv.
apply/edge_setP.
rewrite /edge_set_pred.
split.
rewrite -pair_neq_card2.
move: (negbT (sg_edgeNeq adjuv)).
by move/eqP.
move=> u' v'.
rewrite doubleton_eq_iff.
case=> [ [uisu' visv'] | [uisv' visu'] ].
by rewrite -uisu' -visv'.
by rewrite -uisv' -visu' sg_sym.
(* case: <- *)
move/edge_setP.
rewrite /edge_set_pred => [ [_ ] ].
by move=> /(_ u v) ->.
Qed.
Proposition sg_isolate_graph : forall u v : G, isolate_graph G -> u -- v = false.
Proof.
move=> u v.
rewrite /isolate_graph.
move/eqP.
apply: contraTF => adjuv.
apply/set0Pn.
exists ❴u; v❵.
rewrite /edge_set in_set.
apply/edge_setP.
rewrite /edge_set_pred.
split.
rewrite -(pair_neq_card2 u v) => /eqP.
by rewrite sg_edgeNeq.
move=> u' v'.
rewrite doubleton_eq_iff.
elim=> [ [uisu' visv'] | [uisv' visu'] ].
by rewrite -uisu' -visv'.
by rewrite -uisv' -visu' sg_sym.
Qed.
Proposition deg_isolate_graph : forall v : G, isolate_graph G -> deg G v = 0.
Proof.
move=> v i_graph.
rewrite /deg /open_neigh.
apply/eqP.
rewrite cards_eq0 -subset0.
apply/subsetP => x.
rewrite inE in_set0.
by rewrite sg_isolate_graph.
Qed.
Variables D1 D2 : {set G}.
Proposition D_in_closed_neight_set : D1 ⊆ NS[D1].
Proof.
apply/subsetP => x xinD1.
rewrite /closed_neigh_set /closed_neigh.
apply/bigcupP.
exists x.
by rewrite xinD1.
by rewrite in_setU in_set1 eq_refl orbT.
Qed.
Proposition dominated_belongs_to_open_neigh_set : forall u v : G, u ∈ D1 -> u -- v -> v ∈ NS(D1).
Proof.
move=> u v uinD1 adjuv.
rewrite /open_neigh_set.
apply/bigcupP.
exists u.
apply/andP ; split=> [// | //].
by rewrite /open_neigh in_set.
Qed.
Proposition open_neigh_set_subset_closed_neigh_set : NS(D1) ⊆ NS[D1].
Proof.
apply/subsetP => u.
rewrite /open_neigh_set /closed_neigh_set.
move/bigcupP.
elim=> v /andP [_ vinD1] uinNv.
apply/bigcupP.
exists v => [// | ].
by rewrite /closed_neigh in_setU uinNv orTb.
Qed.
Proposition dominated_belongs_to_closed_neigh_set : forall u v : G, u ∈ D1 -> u -- v -> v ∈ NS[D1].
Proof.
move=> u v uinD1 adjuv.
apply: (subsetP open_neigh_set_subset_closed_neigh_set v).
exact: dominated_belongs_to_open_neigh_set adjuv.
Qed.
Proposition closed_neigh_set_subset : D1 ⊆ D2 -> NS[D1] ⊆ NS[D2].
Proof.
move=> D1subD2.
rewrite /closed_neigh_set.
apply/subsetP => x /bigcupP.
elim=> i /andP [_ iinD1] xinNi.
apply/bigcupP.
exists i.
apply/andP ; split=> //.
exact: subsetP D1subD2 i iinD1.
exact: xinNi.
Qed.
End Basic_Facts_Neighborhoods.
(**********************************************************************************)
Section Remove_edge.
Variable G : sgraph.
Variables u v : G.
Hypothesis adjuv : u -- v.
Let sedge' (x y : G) := if (x ∈ ❴u; v❵) && (y ∈ ❴u; v❵) then false else sedge x y.
Let sg_sym' : symmetric sedge'.
Proof.
rewrite /symmetric /sedge' => x y.
case: ifP ; case: ifP => // ; rewrite andbC.
by move->.
by move->.
by rewrite sg_sym.
Qed.
Let sg_irrefl' : irreflexive sedge'.
Proof. rewrite /irreflexive /sedge' => x ; case: ifP => // ; by rewrite sg_irrefl. Qed.
Definition G_minus_uv := SGraph sg_sym' sg_irrefl'.
Lemma sg_uv_false : sedge' u v = false.
Proof. by rewrite /sedge' set21 set22. Qed.
Lemma sg_xy_sg : forall x y : G, x ∉ ❴u; v❵ \/ y ∉ ❴u; v❵ -> sedge' x y = sedge x y.
Proof.
rewrite /sedge' => x y ; case.
case: ifP => //.
move=> /andP [xinuv _] ; by rewrite xinuv.
move=> ynotinuv ; by rewrite (negbTE ynotinuv) andbF.
Qed.
Lemma sg_implies_sg : forall x y : G, sedge' x y -> sedge x y.
Proof. rewrite /sedge' => x y ; by case: ifP => //. Qed.
Proposition edge_set_minus_uv : E(G_minus_uv) = E(G) :\: ❴❴u; v❵❵.
Proof.
apply/eqP.
rewrite eqEsubset.
apply/andP ; split.
(* we first prove E(G_minus_uv) in E(G) - {{u,v}} *)
apply/subsetP => e.
rewrite /edge_set !in_set.
move/edge_setP => [eis2 /= H1].
apply/andP ; split.
have: (e == ❴u; v❵) ==> sedge' u v.
apply/implyP => /eqP eisuv.
by rewrite (H1 u v eisuv).
apply: contraL => eisuv.
by rewrite eisuv sg_uv_false.
apply/edge_setP.
split => //.
move=> x y eisxy.
move: ((H1 x y) eisxy) => /=.
exact: sg_implies_sg.
(* now, we prove E(G) - {{u,v}} in E(G_minus_uv) *)
apply/subsetP => e.
rewrite in_setD in_set1 !in_set => /andP [eisnotuv /edge_setP [eis2 H2] ].
apply/edge_setP.
rewrite /edge_set_pred /=.
split => //.
move=> x y eisxy.
rewrite sg_xy_sg.
exact: H2 x y eisxy.
rewrite !in_set.
apply/orP.
move: eisnotuv.
rewrite eisxy.
apply: contraR.
move=> H3.
apply/eqP.
rewrite doubleton_eq_iff.
rewrite negb_or !negbK in H3.
move: (sg_edgeNeq (H2 x y eisxy)) => xisnoty.
move: H3 => /andP [xisuorv yisuorv].
case/orP: xisuorv => [/eqP xisu | /eqP xisv].
left ; split => // ; case/orP: yisuorv => [/eqP yisu | /eqP yisv] ; [ | by []].
by rewrite xisu yisu eq_refl in xisnoty.
right ; split => // ; case/orP: yisuorv => [/eqP yisu | /eqP yisv] ; [by [] | ].
by rewrite xisv yisv eq_refl in xisnoty.
Qed.
Proposition subset_opneigh_minus_uv : forall w : G, N(G_minus_uv; w) ⊆ N(G; w).
Proof.
move=> w.
apply/subsetP => x.
rewrite /open_neigh !in_set /=.
exact: sg_implies_sg.
Qed.
Definition give_adj_uv (w : G) := if w == u then v else u.
Lemma give_adj_uv_u : give_adj_uv u = v.
Proof. by rewrite /give_adj_uv eq_refl. Qed.
Lemma give_adj_uv_v : give_adj_uv v = u.
Proof. rewrite /give_adj_uv ; case: ifP => // ; by move/eqP->. Qed.
Lemma op_neigh_minus_uv_empty : forall w : G, w ∈ ❴u; v❵ ->
N(G_minus_uv; w) :&: ❴give_adj_uv w❵ = ∅.
Proof.
move=> w wisuv.
rewrite in_set in wisuv.
apply/setP => x.
apply/setIP.
rewrite in_set0 !in_set1.
elim=> H1 xisv.
move: H1.
rewrite (eqP xisv) /open_neigh in_set.
apply/negP.
case/orP: wisuv => [wisu|wisv].
rewrite in_set1 in wisu.
by rewrite (eqP wisu) give_adj_uv_u /= sg_uv_false.
rewrite in_set1 in wisv.
by rewrite (eqP wisv) give_adj_uv_v /= sg_sym' sg_uv_false.
Qed.
Lemma op_neigh_minus_uv0: forall w : G, w ∉ ❴u; v❵ -> N(G; w) = N(G_minus_uv; w).
Proof.
move=> w wnotuv.
apply/eqP.
rewrite eqEsubset.
apply/andP ; split ; last exact: subset_opneigh_minus_uv.
apply/subsetP => x.
rewrite /open_neigh !in_set /= => adjwx.
rewrite sg_xy_sg //.
by left.
Qed.
Proposition deg_minus_uv0 : forall w : G, w ∉ ❴u; v❵ -> deg G w = deg G_minus_uv w.
Proof.
move=> w wnotuv.
rewrite /deg.
apply: eq_card.
by rewrite (op_neigh_minus_uv0 wnotuv).
Qed.
Lemma op_neigh_minus_uv1: forall w : G, w ∈ ❴u; v❵ ->
N(G; w) = N(G_minus_uv; w) :|: ❴give_adj_uv w❵.
Proof.
move=> w wisuv.
rewrite in_set in wisuv.
(* first, we prove that v ∈ N(G,u) and viceversa *)
have adjinNw : give_adj_uv w ∈ N(G; w).
rewrite /open_neigh in_set.
case/orP: wisuv => [wisu|wisv].
rewrite in_set1 in wisu.
by rewrite (eqP wisu) give_adj_uv_u.
rewrite in_set1 in wisv.
by rewrite (eqP wisv) give_adj_uv_v sg_sym.
(* next, we prove N(G,w) == N(G,w) cup {give_adj_uv w} *)
have H1: N(G; w) == N(G; w) :|: ❴give_adj_uv w❵.
rewrite eqEsubset.
apply/andP ; split.
rewrite -[in X in X ⊆ _](setU0 N(G; w)) setUS //.
exact: sub0set.
apply/subsetP => x H2.
rewrite in_setU in H2.
case/orP: H2 => [// | xisadjw].
rewrite in_set1 in xisadjw.
move/eqP: xisadjw ->.
exact: adjinNw.
(* finally, we prove the main statement *)
apply/eqP.
rewrite eqEsubset.
apply/andP ; split ; last first.
(* first subset: N(G_minus_uv; w) cup {give_adj_uv w} in N(G; w) *)
rewrite (eqP H1) setSU //.
exact: subset_opneigh_minus_uv.
(* second subset: N( G; w) in N(G_minus_uv; w) cup {give_adj_uv w} *)
apply/subsetP => x.
rewrite /open_neigh !in_set sg_in_edge_set => adjwx.
case H3: (x == give_adj_uv w) ; [ exact: orbT | ].
rewrite orbF.
rewrite sg_in_edge_set edge_set_minus_uv in_setD in_set1.
apply/andP ; split=> [ | // ].
move: (negbT H3).
apply: contra.
case/orP: wisuv => [wisu|wisv].
(* case when w is u *)
rewrite in_set1 in wisu.
move/eqP: wisu->.
move/eqP.
rewrite doubleton_eq_left give_adj_uv_u.
by move->.
rewrite in_set1 in wisv.
move/eqP: wisv->.
move/eqP.
rewrite (pair_commute u v) doubleton_eq_left give_adj_uv_v.
by move->.
Qed.
Proposition deg_minus_uv1 : deg G u = (deg G_minus_uv u) + 1.
Proof.
move: (set21 u v) => uinuv.
rewrite /deg.
have H1: N(G; u) == N(G_minus_uv; u) :|: ❴v❵
by rewrite -give_adj_uv_u (op_neigh_minus_uv1 uinuv).
rewrite (eqP H1) cardsU cards1.
have H2: N(G_minus_uv; u) :&: ❴v❵ == ∅
by rewrite -give_adj_uv_u (op_neigh_minus_uv_empty uinuv).
by rewrite (eqP H2) cards0 subn0.
Qed.
Proposition deg_minus_uv2 : deg G v = (deg G_minus_uv v) + 1.
Proof.
move: (set22 u v) => vinuv.
rewrite /deg.
have H1: N(G; v) == N(G_minus_uv; v) :|: ❴u❵
by rewrite -give_adj_uv_v (op_neigh_minus_uv1 vinuv).
rewrite (eqP H1) cardsU cards1.
have H2: N(G_minus_uv; v) :&: ❴u❵ == ∅
by rewrite -give_adj_uv_v (op_neigh_minus_uv_empty vinuv).
by rewrite (eqP H2) cards0 subn0.
Qed.
End Remove_edge.
(**********************************************************************************)
Section Sum_degrees_eq_twice_edges.
Lemma VeqVminusepluse : forall (G : sgraph) (e : {set G}), e ∈ E(G) -> V(G) = (V(G) :\: e) :|: e.
Proof. move=> G e einE ; apply: set_minus_union ; exact: subsetT. Qed.
Theorem sumdeg_2E : forall G : sgraph, 2 * #|E(G)| = Σ(w in V(G)) deg G w.
Proof.
(* first, we shape the statement *)
suff: forall (n : nat) (G : sgraph), #|E(G)| = n -> 2 * n = Σ(w in G | w ∈ V(G)) deg G w.
move=> newstat G ; by move: (newstat #|E(G)| G erefl)->.
move=> n ; elim/nat_ind: n => [G | m IH].
(* base case *)
move=> /eqP Eempty.
rewrite cards_eq0 -/isolate_graph in Eempty.
apply/eqP.
rewrite muln0 eq_sym sum_nat_eq0.
apply/forall_inP => i iinV.
apply/eqP.
by rewrite deg_isolate_graph // /isolate_graph (eqP Eempty).
(* inductive case: first, we obtain an edge e = {u,v} *)
move=> G Emplus1.
rewrite mulnC mulSn mulnC addnC.
have existsedge: exists e : {set G}, e ∈ E(G).
apply/set0Pn.
by rewrite -card_gt0 Emplus1 ltn0Sn.
elim: existsedge => [e einE].
move: (pair_card2_exists (edges_size_two einE)) => [u [v [uneqv eisuv]]].
(* now, we create some useful elements *)
set Gruv := G_minus_uv u v.
have uvinE: ❴u; v❵ ∈ E(G) by rewrite -eisuv einE.
have uvsubE: ❴❴u; v❵❵ ⊆ E(G) by rewrite sub1set uvinE.
have H1: #|E(G) :\: ❴❴u; v❵❵| = m
by rewrite cardsD -(subset_inter uvsubE) cards1 Emplus1 subSS subn0.
(* here, we manipulate the inductive hypothesis *)
have IHG: 2 * m = Σ(w in Gruv | w ∈ V(Gruv) :\: e) deg Gruv w + deg Gruv u + deg Gruv v.
rewrite (IH Gruv) ; last by rewrite edge_set_minus_uv H1.
rewrite (eq_bigl (fun w => w ∈ (V(Gruv) :\: e) :|: e)) ; last first.
move=> w ; apply/eqP ; by rewrite -(VeqVminusepluse einE).
rewrite sum_disjoint_union ; last exact: set_minus_disjoint.
rewrite [in X in _ + X = _] eisuv.
rewrite [in X in _ + X = _] sum_disjoint_union ; last exact: set_pair_disjoint.
rewrite !sum_singleton addnA.
apply/eqP ; by rewrite !eqn_add2r.
(* next, we manipulate the original inductive case *)
rewrite (eq_bigl (fun w => w ∈ (V(G) :\: e) :|: e)) ; last first.
move=> w ; by rewrite -(VeqVminusepluse einE).
rewrite sum_disjoint_union ; last exact: set_minus_disjoint.
rewrite [in X in _ = _ + X] eisuv.
rewrite [in X in _ = _ + X] sum_disjoint_union ; last exact: set_pair_disjoint.
rewrite !sum_singleton addnA.
(* finally, we apply the inductive hypothesis *)
rewrite IHG.
move: uvinE ; rewrite -sg_in_edge_set => adjuv.
rewrite (deg_minus_uv1 adjuv) (deg_minus_uv2 adjuv) -/Gruv.
rewrite !addnA.
rewrite -[in X in _ = X + _] addnA.
rewrite [in X in _ = _ + X + _] addnC.
rewrite addnA.
rewrite -[in X in _ = X] addnA.
apply/eqP ; rewrite eqn_add2r ; apply/eqP.
rewrite [in X in _ = X] (eq_bigr (fun w => deg Gruv w)) //.
move=> w.
rewrite in_setD => /andP [_ /andP [wnotine _] ].
rewrite eisuv in wnotine.
exact: deg_minus_uv0.
Qed.
End Sum_degrees_eq_twice_edges.
Variable G : sgraph.
Variables u v : G.
Hypothesis adjuv : u -- v.
Let sedge' (x y : G) := if (x ∈ ❴u; v❵) && (y ∈ ❴u; v❵) then false else sedge x y.
Let sg_sym' : symmetric sedge'.
Proof.
rewrite /symmetric /sedge' => x y.
case: ifP ; case: ifP => // ; rewrite andbC.
by move->.
by move->.
by rewrite sg_sym.
Qed.
Let sg_irrefl' : irreflexive sedge'.
Proof. rewrite /irreflexive /sedge' => x ; case: ifP => // ; by rewrite sg_irrefl. Qed.
Definition G_minus_uv := SGraph sg_sym' sg_irrefl'.
Lemma sg_uv_false : sedge' u v = false.
Proof. by rewrite /sedge' set21 set22. Qed.
Lemma sg_xy_sg : forall x y : G, x ∉ ❴u; v❵ \/ y ∉ ❴u; v❵ -> sedge' x y = sedge x y.
Proof.
rewrite /sedge' => x y ; case.
case: ifP => //.
move=> /andP [xinuv _] ; by rewrite xinuv.
move=> ynotinuv ; by rewrite (negbTE ynotinuv) andbF.
Qed.
Lemma sg_implies_sg : forall x y : G, sedge' x y -> sedge x y.
Proof. rewrite /sedge' => x y ; by case: ifP => //. Qed.
Proposition edge_set_minus_uv : E(G_minus_uv) = E(G) :\: ❴❴u; v❵❵.
Proof.
apply/eqP.
rewrite eqEsubset.
apply/andP ; split.
(* we first prove E(G_minus_uv) in E(G) - {{u,v}} *)
apply/subsetP => e.
rewrite /edge_set !in_set.
move/edge_setP => [eis2 /= H1].
apply/andP ; split.
have: (e == ❴u; v❵) ==> sedge' u v.
apply/implyP => /eqP eisuv.
by rewrite (H1 u v eisuv).
apply: contraL => eisuv.
by rewrite eisuv sg_uv_false.
apply/edge_setP.
split => //.
move=> x y eisxy.
move: ((H1 x y) eisxy) => /=.
exact: sg_implies_sg.
(* now, we prove E(G) - {{u,v}} in E(G_minus_uv) *)
apply/subsetP => e.
rewrite in_setD in_set1 !in_set => /andP [eisnotuv /edge_setP [eis2 H2] ].
apply/edge_setP.
rewrite /edge_set_pred /=.
split => //.
move=> x y eisxy.
rewrite sg_xy_sg.
exact: H2 x y eisxy.
rewrite !in_set.
apply/orP.
move: eisnotuv.
rewrite eisxy.
apply: contraR.
move=> H3.
apply/eqP.
rewrite doubleton_eq_iff.
rewrite negb_or !negbK in H3.
move: (sg_edgeNeq (H2 x y eisxy)) => xisnoty.
move: H3 => /andP [xisuorv yisuorv].
case/orP: xisuorv => [/eqP xisu | /eqP xisv].
left ; split => // ; case/orP: yisuorv => [/eqP yisu | /eqP yisv] ; [ | by []].
by rewrite xisu yisu eq_refl in xisnoty.
right ; split => // ; case/orP: yisuorv => [/eqP yisu | /eqP yisv] ; [by [] | ].
by rewrite xisv yisv eq_refl in xisnoty.
Qed.
Proposition subset_opneigh_minus_uv : forall w : G, N(G_minus_uv; w) ⊆ N(G; w).
Proof.
move=> w.
apply/subsetP => x.
rewrite /open_neigh !in_set /=.
exact: sg_implies_sg.
Qed.
Definition give_adj_uv (w : G) := if w == u then v else u.
Lemma give_adj_uv_u : give_adj_uv u = v.
Proof. by rewrite /give_adj_uv eq_refl. Qed.
Lemma give_adj_uv_v : give_adj_uv v = u.
Proof. rewrite /give_adj_uv ; case: ifP => // ; by move/eqP->. Qed.
Lemma op_neigh_minus_uv_empty : forall w : G, w ∈ ❴u; v❵ ->
N(G_minus_uv; w) :&: ❴give_adj_uv w❵ = ∅.
Proof.
move=> w wisuv.
rewrite in_set in wisuv.
apply/setP => x.
apply/setIP.
rewrite in_set0 !in_set1.
elim=> H1 xisv.
move: H1.
rewrite (eqP xisv) /open_neigh in_set.
apply/negP.
case/orP: wisuv => [wisu|wisv].
rewrite in_set1 in wisu.
by rewrite (eqP wisu) give_adj_uv_u /= sg_uv_false.
rewrite in_set1 in wisv.
by rewrite (eqP wisv) give_adj_uv_v /= sg_sym' sg_uv_false.
Qed.
Lemma op_neigh_minus_uv0: forall w : G, w ∉ ❴u; v❵ -> N(G; w) = N(G_minus_uv; w).
Proof.
move=> w wnotuv.
apply/eqP.
rewrite eqEsubset.
apply/andP ; split ; last exact: subset_opneigh_minus_uv.
apply/subsetP => x.
rewrite /open_neigh !in_set /= => adjwx.
rewrite sg_xy_sg //.
by left.
Qed.
Proposition deg_minus_uv0 : forall w : G, w ∉ ❴u; v❵ -> deg G w = deg G_minus_uv w.
Proof.
move=> w wnotuv.
rewrite /deg.
apply: eq_card.
by rewrite (op_neigh_minus_uv0 wnotuv).
Qed.
Lemma op_neigh_minus_uv1: forall w : G, w ∈ ❴u; v❵ ->
N(G; w) = N(G_minus_uv; w) :|: ❴give_adj_uv w❵.
Proof.
move=> w wisuv.
rewrite in_set in wisuv.
(* first, we prove that v ∈ N(G,u) and viceversa *)
have adjinNw : give_adj_uv w ∈ N(G; w).
rewrite /open_neigh in_set.
case/orP: wisuv => [wisu|wisv].
rewrite in_set1 in wisu.
by rewrite (eqP wisu) give_adj_uv_u.
rewrite in_set1 in wisv.
by rewrite (eqP wisv) give_adj_uv_v sg_sym.
(* next, we prove N(G,w) == N(G,w) cup {give_adj_uv w} *)
have H1: N(G; w) == N(G; w) :|: ❴give_adj_uv w❵.
rewrite eqEsubset.
apply/andP ; split.
rewrite -[in X in X ⊆ _](setU0 N(G; w)) setUS //.
exact: sub0set.
apply/subsetP => x H2.
rewrite in_setU in H2.
case/orP: H2 => [// | xisadjw].
rewrite in_set1 in xisadjw.
move/eqP: xisadjw ->.
exact: adjinNw.
(* finally, we prove the main statement *)
apply/eqP.
rewrite eqEsubset.
apply/andP ; split ; last first.
(* first subset: N(G_minus_uv; w) cup {give_adj_uv w} in N(G; w) *)
rewrite (eqP H1) setSU //.
exact: subset_opneigh_minus_uv.
(* second subset: N( G; w) in N(G_minus_uv; w) cup {give_adj_uv w} *)
apply/subsetP => x.
rewrite /open_neigh !in_set sg_in_edge_set => adjwx.
case H3: (x == give_adj_uv w) ; [ exact: orbT | ].
rewrite orbF.
rewrite sg_in_edge_set edge_set_minus_uv in_setD in_set1.
apply/andP ; split=> [ | // ].
move: (negbT H3).
apply: contra.
case/orP: wisuv => [wisu|wisv].
(* case when w is u *)
rewrite in_set1 in wisu.
move/eqP: wisu->.
move/eqP.
rewrite doubleton_eq_left give_adj_uv_u.
by move->.
rewrite in_set1 in wisv.
move/eqP: wisv->.
move/eqP.
rewrite (pair_commute u v) doubleton_eq_left give_adj_uv_v.
by move->.
Qed.
Proposition deg_minus_uv1 : deg G u = (deg G_minus_uv u) + 1.
Proof.
move: (set21 u v) => uinuv.
rewrite /deg.
have H1: N(G; u) == N(G_minus_uv; u) :|: ❴v❵
by rewrite -give_adj_uv_u (op_neigh_minus_uv1 uinuv).
rewrite (eqP H1) cardsU cards1.
have H2: N(G_minus_uv; u) :&: ❴v❵ == ∅
by rewrite -give_adj_uv_u (op_neigh_minus_uv_empty uinuv).
by rewrite (eqP H2) cards0 subn0.
Qed.
Proposition deg_minus_uv2 : deg G v = (deg G_minus_uv v) + 1.
Proof.
move: (set22 u v) => vinuv.
rewrite /deg.
have H1: N(G; v) == N(G_minus_uv; v) :|: ❴u❵
by rewrite -give_adj_uv_v (op_neigh_minus_uv1 vinuv).
rewrite (eqP H1) cardsU cards1.
have H2: N(G_minus_uv; v) :&: ❴u❵ == ∅
by rewrite -give_adj_uv_v (op_neigh_minus_uv_empty vinuv).
by rewrite (eqP H2) cards0 subn0.
Qed.
End Remove_edge.
(**********************************************************************************)
Section Sum_degrees_eq_twice_edges.
Lemma VeqVminusepluse : forall (G : sgraph) (e : {set G}), e ∈ E(G) -> V(G) = (V(G) :\: e) :|: e.
Proof. move=> G e einE ; apply: set_minus_union ; exact: subsetT. Qed.
Theorem sumdeg_2E : forall G : sgraph, 2 * #|E(G)| = Σ(w in V(G)) deg G w.
Proof.
(* first, we shape the statement *)
suff: forall (n : nat) (G : sgraph), #|E(G)| = n -> 2 * n = Σ(w in G | w ∈ V(G)) deg G w.
move=> newstat G ; by move: (newstat #|E(G)| G erefl)->.
move=> n ; elim/nat_ind: n => [G | m IH].
(* base case *)
move=> /eqP Eempty.
rewrite cards_eq0 -/isolate_graph in Eempty.
apply/eqP.
rewrite muln0 eq_sym sum_nat_eq0.
apply/forall_inP => i iinV.
apply/eqP.
by rewrite deg_isolate_graph // /isolate_graph (eqP Eempty).
(* inductive case: first, we obtain an edge e = {u,v} *)
move=> G Emplus1.
rewrite mulnC mulSn mulnC addnC.
have existsedge: exists e : {set G}, e ∈ E(G).
apply/set0Pn.
by rewrite -card_gt0 Emplus1 ltn0Sn.
elim: existsedge => [e einE].
move: (pair_card2_exists (edges_size_two einE)) => [u [v [uneqv eisuv]]].
(* now, we create some useful elements *)
set Gruv := G_minus_uv u v.
have uvinE: ❴u; v❵ ∈ E(G) by rewrite -eisuv einE.
have uvsubE: ❴❴u; v❵❵ ⊆ E(G) by rewrite sub1set uvinE.
have H1: #|E(G) :\: ❴❴u; v❵❵| = m
by rewrite cardsD -(subset_inter uvsubE) cards1 Emplus1 subSS subn0.
(* here, we manipulate the inductive hypothesis *)
have IHG: 2 * m = Σ(w in Gruv | w ∈ V(Gruv) :\: e) deg Gruv w + deg Gruv u + deg Gruv v.
rewrite (IH Gruv) ; last by rewrite edge_set_minus_uv H1.
rewrite (eq_bigl (fun w => w ∈ (V(Gruv) :\: e) :|: e)) ; last first.
move=> w ; apply/eqP ; by rewrite -(VeqVminusepluse einE).
rewrite sum_disjoint_union ; last exact: set_minus_disjoint.
rewrite [in X in _ + X = _] eisuv.
rewrite [in X in _ + X = _] sum_disjoint_union ; last exact: set_pair_disjoint.
rewrite !sum_singleton addnA.
apply/eqP ; by rewrite !eqn_add2r.
(* next, we manipulate the original inductive case *)
rewrite (eq_bigl (fun w => w ∈ (V(G) :\: e) :|: e)) ; last first.
move=> w ; by rewrite -(VeqVminusepluse einE).
rewrite sum_disjoint_union ; last exact: set_minus_disjoint.
rewrite [in X in _ = _ + X] eisuv.
rewrite [in X in _ = _ + X] sum_disjoint_union ; last exact: set_pair_disjoint.
rewrite !sum_singleton addnA.
(* finally, we apply the inductive hypothesis *)
rewrite IHG.
move: uvinE ; rewrite -sg_in_edge_set => adjuv.
rewrite (deg_minus_uv1 adjuv) (deg_minus_uv2 adjuv) -/Gruv.
rewrite !addnA.
rewrite -[in X in _ = X + _] addnA.
rewrite [in X in _ = _ + X + _] addnC.
rewrite addnA.
rewrite -[in X in _ = X] addnA.
apply/eqP ; rewrite eqn_add2r ; apply/eqP.
rewrite [in X in _ = X] (eq_bigr (fun w => deg Gruv w)) //.
move=> w.
rewrite in_setD => /andP [_ /andP [wnotine _] ].
rewrite eisuv in wnotine.
exact: deg_minus_uv0.
Qed.
End Sum_degrees_eq_twice_edges.