(* Some examples
* 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 basics dom.
Set Implicit Arguments.
Unset Strict Implicit.
(**********************************************************************************)
Section Weighted_complete.
Variable G : sgraph.
Variable weight : G -> nat.
Hypothesis positive_weights : forall v : G, weight v > 0.
Variable h : G.
Let wh : nat := weight h.
Hypothesis h_heaviest : forall v : G, weight v <= wh.
Hypothesis complete_graph : forall u v : G, u <> v -> u -- v.
(* we propose the singleton S={h} *)
Let S : {set G} := ❴h❵.
Lemma S_is_stable : stable G S.
Proof.
rewrite /stable /S => u v uinS vinS.
rewrite in_set1 in uinS.
rewrite in_set1 in vinS.
move/eqP: uinS ->.
move/eqP: vinS ->.
by rewrite sg_irrefl.
Qed.
Lemma S_weights_wh : weight_set weight S = wh.
Proof. by rewrite /S /weight_set sum_singleton. Qed.
(* we prove that parameters alpha_w, Gamma_w and IR_w are equal to w(h) *)
Lemma wh_leq_alpha_w : wh <= alpha_w G weight.
Proof.
move: (maximum_set_welldefined weight (stable G)).
rewrite /maximum => [ [_ set_is_max] ].
move: (set_is_max S S_is_stable).
by rewrite /alpha_w S_weights_wh.
Qed.
Lemma irr_size_1 : forall D : {set G}, irredundant G D -> #|D| <= 1.
Proof.
move=> D Dirr.
move/irredundantP: Dirr.
apply: contraLR.
rewrite -ltnNge => Dgt1.
(* we first extract an element u *)
have: exists u : G, u ∈ D by apply/set0Pn ; rewrite -card_gt0 (leq_ltn_trans (leqnSn 0) Dgt1).
elim=> [u uinD].
have Dminusugt0: 0 < #|D :\: ❴u❵| by rewrite (cardsD1 u D) uinD /= in Dgt1.
(* then, an element v *)
have: exists v : G, v ∈ (D :\: ❴u❵) by apply/set0Pn ; rewrite -card_gt0 Dminusugt0.
elim=> v vinDminusu.
(* now, we prove that D can not be irredundant *)
rewrite /pb_irredundant negb_forall.
apply/existsP.
exists u.
rewrite uinD /= negbK /private_set.
(* in particular, that Nu-ND-{u} is empty *)
suff: ~ (exists x : G, x ∈ N[u] :\: NS[D :\ u]) by move/set0Pn.
move=> existsx.
elim: existsx => x.
rewrite in_setD => [ /andP [/negP xnotinNDu _] ].
case: (boolP (v==x)) => [/eqP veqx | /eqP vneqx].
(* we separate in two cases: v = x ... *)
move: (subsetP (D_in_closed_neight_set (D :\ u)) v vinDminusu).
rewrite veqx.
contradiction.
(* ... and v <> x, i.e. x is adjacent to v *)
move: (complete_graph vneqx) => adjvx.
move: (dominated_belongs_to_closed_neigh_set vinDminusu adjvx).
contradiction.
Qed.
Lemma IR_w_leq_wh : IR_w G weight <= wh.
Proof.
set D := @maximum_set G weight (irredundant G).
move: (maximum_set_welldefined weight (irredundant G)).
rewrite /maximum -/D => [ [Dirr _] ].
have Dleq1: #|D| = 0 \/ #|D| = 1.
move: (irr_size_1 Dirr).
case: #|D| ; [by left | ].
move=> m ; rewrite /leq subSS subn0 => /eqP mis0.
right ; by rewrite mis0.
case: Dleq1.
(* case when D is empty *)
move/eqP ; rewrite cards_eq0 ; move/eqP.
rewrite (empty_set_zero_weight (weight:=weight)) /IR_w -/D.
by move->.
exact: positive_weights.
(* case when D is a singleton *)
move/eqP/cards1P.
elim=> v Disv.
by rewrite /IR_w -/D Disv /weight_set sum_singleton h_heaviest.
Qed.
Theorem alpha_w_eq_wh : alpha_w G weight = wh.
Proof.
apply/eqP.
rewrite eqn_leq wh_leq_alpha_w andbT.
exact: (leq_trans (leq_trans (@alpha_w_leq_Gamma_w G weight positive_weights)
(@Gamma_w_leq_IR_w G weight)) IR_w_leq_wh).
Qed.
Theorem Gamma_w_eq_wh : Gamma_w G weight = wh.
Proof.
apply/eqP.
rewrite eqn_leq.
apply/andP ; split.
exact: (leq_trans (@Gamma_w_leq_IR_w G weight) IR_w_leq_wh).
by rewrite -alpha_w_eq_wh alpha_w_leq_Gamma_w.
Qed.
Theorem IR_w_eq_wh : IR_w G weight = wh.
Proof.
apply/eqP.
rewrite eqn_leq.
apply/andP ; split.
exact: IR_w_leq_wh.
by rewrite -Gamma_w_eq_wh Gamma_w_leq_IR_w.
Qed.
End Weighted_complete.
(**********************************************************************************)
Section Unweighted_complete.
Variable G : sgraph.
Variable h : G.
Hypothesis complete_graph : forall u v : G, u <> v -> u -- v.
(* now, we now prove that, for the unweighted case, all parameters equal 1 *)
Let weight := ones G.
Let positive_weights : forall v : G, weight v > 0.
Proof. by []. Qed.
Let h_heaviest : forall v : G, weight v <= weight h.
Proof. by []. Qed.
Let S : {set G} := ❴h❵.
Lemma S_is_maximal_irredundant : maximal (irredundant G) S.
Proof.
rewrite /maximal ; split.
(* first, we prove that S is irredundant *)
rewrite /irredundant /S /private => v vinS.
exists v.
split ; [ exact: cl_sg_refl | ].
move=> u uinS _.
rewrite in_set1 in uinS.
move/eqP: uinS ->.
rewrite in_set1 in vinS.
by move/eqP: vinS ->.
(* next, that S is maximal *)
move=> F.
rewrite properEcard /S cards1 ltnNge => /andP [_ /negP Fgt1].
move=> Firr ; move: (irr_size_1 complete_graph Firr).
contradiction.
Qed.
Lemma ir_geq_1 : 1 <= ir G.
Proof.
set D := @minimum_set G weight (max_irr G).
rewrite /ir (min_card_weight_1 (max_irr G)) -/D card_gt0.
apply/eqP.
move=> Dempty.
move: (minimum_set_welldefined weight (max_irr G)).
rewrite /minimum -/D => [ [Dmaxirr _] ].
move: Dmaxirr.
rewrite Dempty /p_max_irr /maximal => [ [_] ].
move=> /(_ S).
rewrite proper0 -card_gt0 cards1 (leqnn 1) => /(_ isT).
move: (S_is_maximal_irredundant).
rewrite /maximal => [ [Sirr _] ].
contradiction.
Qed.
Lemma IR_leq_1 : IR G <= 1.
Proof.
set D := @maximum_set G weight (irredundant G).
move: (maximum_set_welldefined weight (irredundant G)).
rewrite /maximum -/D => [ [Dirr _] ].
move: (irr_size_1 complete_graph Dirr).
by rewrite /IR (max_card_weight_1 (irredundant G)) -/D.
Qed.
Theorem ir_eq_1 : ir G = 1.
Proof.
apply/eqP.
rewrite eqn_leq ir_geq_1 andbT.
exact: (leq_trans (leq_trans (leq_trans (leq_trans (leq_trans (ir_leq_gamma G) (gamma_leq_ii G))
(ii_leq_alpha G)) (alpha_leq_Gamma G)) (Gamma_leq_IR G)) IR_leq_1).
Qed.
Theorem gamma_eq_1 : gamma G = 1.
Proof.
apply/eqP.
rewrite eqn_leq.
apply/andP ; split.
exact: (leq_trans (leq_trans (leq_trans (leq_trans (gamma_leq_ii G) (ii_leq_alpha G))
(alpha_leq_Gamma G)) (Gamma_leq_IR G)) IR_leq_1).
by rewrite -ir_eq_1 ir_leq_gamma.
Qed.
Theorem ii_eq_1 : ii G = 1.
Proof.
apply/eqP.
rewrite eqn_leq.
apply/andP ; split.
exact: (leq_trans (leq_trans (leq_trans (ii_leq_alpha G) (alpha_leq_Gamma G))
(Gamma_leq_IR G)) IR_leq_1).
by rewrite -gamma_eq_1 gamma_leq_ii.
Qed.
Theorem alpha_eq_1 : alpha G = 1.
Proof.
apply/eqP.
rewrite eqn_leq.
apply/andP ; split.
exact: (leq_trans (leq_trans (alpha_leq_Gamma G) (Gamma_leq_IR G)) IR_leq_1).
by rewrite -ii_eq_1 ii_leq_alpha.
Qed.
Theorem Gamma_eq_1 : Gamma G = 1.
Proof.
apply/eqP.
rewrite eqn_leq.
apply/andP ; split.
exact: (leq_trans (Gamma_leq_IR G) IR_leq_1).
by rewrite -alpha_eq_1 alpha_leq_Gamma.
Qed.
Theorem IR_eq_1 : IR G = 1.
Proof.
apply/eqP.
rewrite eqn_leq.
apply/andP ; split.
exact: IR_leq_1.
by rewrite -Gamma_eq_1 Gamma_leq_IR.
Qed.
End Unweighted_complete.
(**********************************************************************************)
Section Example.
Variable n : nat.
Hypothesis ngt0 : n > 0.
(* Kn is the complete graph of vertices {0, 1, ..., n-1} *)
Definition Kn : sgraph.
Proof.
refine {| svertex := ordinal_finType (n.-1).+1 ;
sedge := (fun x y => x != y)
|}.
(* sedge is symmetric *)
rewrite /symmetric => x y ; f_equal ; exact: eq_sym.
(* sedge is irreflexive *)
rewrite /irreflexive => x ; apply: negbTE ; by rewrite negbK eq_refl.
Defined.
(* Each vertex v receives weight v+1, and h=n-1 is the heaviest *)
Let weight : Kn -> nat := fun x => x.+1.
Let positive_weights : forall v : Kn, weight v > 0.
Proof. by []. Qed.
Let h : Kn := ord_max.
Let max_weights : forall v : Kn, weight v <= weight h.
Proof. by case. Qed.
Let complete_graph : forall u v : Kn, u <> v -> u -- v.
Proof. move=> u v uneqv ; rewrite /sedge /= ; by apply/eqP. Qed.
(* For instance, let's prove that Gamma_w(Kn) = n and Gamma(Kn) = 1 *)
Example Gamma_w_Kn_eq_n : Gamma_w Kn weight = n.
Proof.
move: (Gamma_w_eq_wh positive_weights max_weights complete_graph)->.
by rewrite /weight (prednK ngt0).
Qed.
Example Gamma_Kn_eq_1 : Gamma Kn = 1.
Proof. by move: (Gamma_eq_1 h complete_graph)->. Qed.
End Example.
Variable G : sgraph.
Variable weight : G -> nat.
Hypothesis positive_weights : forall v : G, weight v > 0.
Variable h : G.
Let wh : nat := weight h.
Hypothesis h_heaviest : forall v : G, weight v <= wh.
Hypothesis complete_graph : forall u v : G, u <> v -> u -- v.
(* we propose the singleton S={h} *)
Let S : {set G} := ❴h❵.
Lemma S_is_stable : stable G S.
Proof.
rewrite /stable /S => u v uinS vinS.
rewrite in_set1 in uinS.
rewrite in_set1 in vinS.
move/eqP: uinS ->.
move/eqP: vinS ->.
by rewrite sg_irrefl.
Qed.
Lemma S_weights_wh : weight_set weight S = wh.
Proof. by rewrite /S /weight_set sum_singleton. Qed.
(* we prove that parameters alpha_w, Gamma_w and IR_w are equal to w(h) *)
Lemma wh_leq_alpha_w : wh <= alpha_w G weight.
Proof.
move: (maximum_set_welldefined weight (stable G)).
rewrite /maximum => [ [_ set_is_max] ].
move: (set_is_max S S_is_stable).
by rewrite /alpha_w S_weights_wh.
Qed.
Lemma irr_size_1 : forall D : {set G}, irredundant G D -> #|D| <= 1.
Proof.
move=> D Dirr.
move/irredundantP: Dirr.
apply: contraLR.
rewrite -ltnNge => Dgt1.
(* we first extract an element u *)
have: exists u : G, u ∈ D by apply/set0Pn ; rewrite -card_gt0 (leq_ltn_trans (leqnSn 0) Dgt1).
elim=> [u uinD].
have Dminusugt0: 0 < #|D :\: ❴u❵| by rewrite (cardsD1 u D) uinD /= in Dgt1.
(* then, an element v *)
have: exists v : G, v ∈ (D :\: ❴u❵) by apply/set0Pn ; rewrite -card_gt0 Dminusugt0.
elim=> v vinDminusu.
(* now, we prove that D can not be irredundant *)
rewrite /pb_irredundant negb_forall.
apply/existsP.
exists u.
rewrite uinD /= negbK /private_set.
(* in particular, that Nu-ND-{u} is empty *)
suff: ~ (exists x : G, x ∈ N[u] :\: NS[D :\ u]) by move/set0Pn.
move=> existsx.
elim: existsx => x.
rewrite in_setD => [ /andP [/negP xnotinNDu _] ].
case: (boolP (v==x)) => [/eqP veqx | /eqP vneqx].
(* we separate in two cases: v = x ... *)
move: (subsetP (D_in_closed_neight_set (D :\ u)) v vinDminusu).
rewrite veqx.
contradiction.
(* ... and v <> x, i.e. x is adjacent to v *)
move: (complete_graph vneqx) => adjvx.
move: (dominated_belongs_to_closed_neigh_set vinDminusu adjvx).
contradiction.
Qed.
Lemma IR_w_leq_wh : IR_w G weight <= wh.
Proof.
set D := @maximum_set G weight (irredundant G).
move: (maximum_set_welldefined weight (irredundant G)).
rewrite /maximum -/D => [ [Dirr _] ].
have Dleq1: #|D| = 0 \/ #|D| = 1.
move: (irr_size_1 Dirr).
case: #|D| ; [by left | ].
move=> m ; rewrite /leq subSS subn0 => /eqP mis0.
right ; by rewrite mis0.
case: Dleq1.
(* case when D is empty *)
move/eqP ; rewrite cards_eq0 ; move/eqP.
rewrite (empty_set_zero_weight (weight:=weight)) /IR_w -/D.
by move->.
exact: positive_weights.
(* case when D is a singleton *)
move/eqP/cards1P.
elim=> v Disv.
by rewrite /IR_w -/D Disv /weight_set sum_singleton h_heaviest.
Qed.
Theorem alpha_w_eq_wh : alpha_w G weight = wh.
Proof.
apply/eqP.
rewrite eqn_leq wh_leq_alpha_w andbT.
exact: (leq_trans (leq_trans (@alpha_w_leq_Gamma_w G weight positive_weights)
(@Gamma_w_leq_IR_w G weight)) IR_w_leq_wh).
Qed.
Theorem Gamma_w_eq_wh : Gamma_w G weight = wh.
Proof.
apply/eqP.
rewrite eqn_leq.
apply/andP ; split.
exact: (leq_trans (@Gamma_w_leq_IR_w G weight) IR_w_leq_wh).
by rewrite -alpha_w_eq_wh alpha_w_leq_Gamma_w.
Qed.
Theorem IR_w_eq_wh : IR_w G weight = wh.
Proof.
apply/eqP.
rewrite eqn_leq.
apply/andP ; split.
exact: IR_w_leq_wh.
by rewrite -Gamma_w_eq_wh Gamma_w_leq_IR_w.
Qed.
End Weighted_complete.
(**********************************************************************************)
Section Unweighted_complete.
Variable G : sgraph.
Variable h : G.
Hypothesis complete_graph : forall u v : G, u <> v -> u -- v.
(* now, we now prove that, for the unweighted case, all parameters equal 1 *)
Let weight := ones G.
Let positive_weights : forall v : G, weight v > 0.
Proof. by []. Qed.
Let h_heaviest : forall v : G, weight v <= weight h.
Proof. by []. Qed.
Let S : {set G} := ❴h❵.
Lemma S_is_maximal_irredundant : maximal (irredundant G) S.
Proof.
rewrite /maximal ; split.
(* first, we prove that S is irredundant *)
rewrite /irredundant /S /private => v vinS.
exists v.
split ; [ exact: cl_sg_refl | ].
move=> u uinS _.
rewrite in_set1 in uinS.
move/eqP: uinS ->.
rewrite in_set1 in vinS.
by move/eqP: vinS ->.
(* next, that S is maximal *)
move=> F.
rewrite properEcard /S cards1 ltnNge => /andP [_ /negP Fgt1].
move=> Firr ; move: (irr_size_1 complete_graph Firr).
contradiction.
Qed.
Lemma ir_geq_1 : 1 <= ir G.
Proof.
set D := @minimum_set G weight (max_irr G).
rewrite /ir (min_card_weight_1 (max_irr G)) -/D card_gt0.
apply/eqP.
move=> Dempty.
move: (minimum_set_welldefined weight (max_irr G)).
rewrite /minimum -/D => [ [Dmaxirr _] ].
move: Dmaxirr.
rewrite Dempty /p_max_irr /maximal => [ [_] ].
move=> /(_ S).
rewrite proper0 -card_gt0 cards1 (leqnn 1) => /(_ isT).
move: (S_is_maximal_irredundant).
rewrite /maximal => [ [Sirr _] ].
contradiction.
Qed.
Lemma IR_leq_1 : IR G <= 1.
Proof.
set D := @maximum_set G weight (irredundant G).
move: (maximum_set_welldefined weight (irredundant G)).
rewrite /maximum -/D => [ [Dirr _] ].
move: (irr_size_1 complete_graph Dirr).
by rewrite /IR (max_card_weight_1 (irredundant G)) -/D.
Qed.
Theorem ir_eq_1 : ir G = 1.
Proof.
apply/eqP.
rewrite eqn_leq ir_geq_1 andbT.
exact: (leq_trans (leq_trans (leq_trans (leq_trans (leq_trans (ir_leq_gamma G) (gamma_leq_ii G))
(ii_leq_alpha G)) (alpha_leq_Gamma G)) (Gamma_leq_IR G)) IR_leq_1).
Qed.
Theorem gamma_eq_1 : gamma G = 1.
Proof.
apply/eqP.
rewrite eqn_leq.
apply/andP ; split.
exact: (leq_trans (leq_trans (leq_trans (leq_trans (gamma_leq_ii G) (ii_leq_alpha G))
(alpha_leq_Gamma G)) (Gamma_leq_IR G)) IR_leq_1).
by rewrite -ir_eq_1 ir_leq_gamma.
Qed.
Theorem ii_eq_1 : ii G = 1.
Proof.
apply/eqP.
rewrite eqn_leq.
apply/andP ; split.
exact: (leq_trans (leq_trans (leq_trans (ii_leq_alpha G) (alpha_leq_Gamma G))
(Gamma_leq_IR G)) IR_leq_1).
by rewrite -gamma_eq_1 gamma_leq_ii.
Qed.
Theorem alpha_eq_1 : alpha G = 1.
Proof.
apply/eqP.
rewrite eqn_leq.
apply/andP ; split.
exact: (leq_trans (leq_trans (alpha_leq_Gamma G) (Gamma_leq_IR G)) IR_leq_1).
by rewrite -ii_eq_1 ii_leq_alpha.
Qed.
Theorem Gamma_eq_1 : Gamma G = 1.
Proof.
apply/eqP.
rewrite eqn_leq.
apply/andP ; split.
exact: (leq_trans (Gamma_leq_IR G) IR_leq_1).
by rewrite -alpha_eq_1 alpha_leq_Gamma.
Qed.
Theorem IR_eq_1 : IR G = 1.
Proof.
apply/eqP.
rewrite eqn_leq.
apply/andP ; split.
exact: IR_leq_1.
by rewrite -Gamma_eq_1 Gamma_leq_IR.
Qed.
End Unweighted_complete.
(**********************************************************************************)
Section Example.
Variable n : nat.
Hypothesis ngt0 : n > 0.
(* Kn is the complete graph of vertices {0, 1, ..., n-1} *)
Definition Kn : sgraph.
Proof.
refine {| svertex := ordinal_finType (n.-1).+1 ;
sedge := (fun x y => x != y)
|}.
(* sedge is symmetric *)
rewrite /symmetric => x y ; f_equal ; exact: eq_sym.
(* sedge is irreflexive *)
rewrite /irreflexive => x ; apply: negbTE ; by rewrite negbK eq_refl.
Defined.
(* Each vertex v receives weight v+1, and h=n-1 is the heaviest *)
Let weight : Kn -> nat := fun x => x.+1.
Let positive_weights : forall v : Kn, weight v > 0.
Proof. by []. Qed.
Let h : Kn := ord_max.
Let max_weights : forall v : Kn, weight v <= weight h.
Proof. by case. Qed.
Let complete_graph : forall u v : Kn, u <> v -> u -- v.
Proof. move=> u v uneqv ; rewrite /sedge /= ; by apply/eqP. Qed.
(* For instance, let's prove that Gamma_w(Kn) = n and Gamma(Kn) = 1 *)
Example Gamma_w_Kn_eq_n : Gamma_w Kn weight = n.
Proof.
move: (Gamma_w_eq_wh positive_weights max_weights complete_graph)->.
by rewrite /weight (prednK ngt0).
Qed.
Example Gamma_Kn_eq_1 : Gamma Kn = 1.
Proof. by move: (Gamma_eq_1 h complete_graph)->. Qed.
End Example.