(* Domination 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 basics.
Set Implicit Arguments.
Unset Strict Implicit.
Section Domination_Theory.
Variable G : sgraph.
(* A "Vertex Set Property" has the following fields:
vsprop : the property as a Prop-predicate over sets
vsbool : the property as a bool-predicate over sets
vsrefl : the reflection between the previous definitions
vsinhb : an inhabitant satisfying vsprop
vspinh : the proof that vsinh satisfy vsprop *)
Record vsproperty := VertexSetProperty {
vsprop :> {set G} -> Prop ;
vsbool : pred {set G} ;
vsrefl : forall D : {set G}, reflect (vsprop D) (vsbool D) ;
vsinhb : {set G} ;
vspinh : vsprop vsinhb
}.
(**********************************************************************************)
Section Stable_Set.
Variable S : {set G}.
Definition p_stable : Prop := forall u v : G, u ∈ S -> v ∈ S -> ~ (u -- v).
Definition pb_stable : bool := NS(S) :&: S == ∅.
Lemma stable_refl : reflect p_stable [forall u : G, forall v : G, (u ∈ S) ==> (v ∈ S) ==> ~~ (u -- v)].
Proof.
rewrite /p_stable.
apply: (iffP forallP).
move=> H1 u v uinS vinS.
move/forallP: (H1 u) => H2.
apply/negP.
by rewrite (implyP ((implyP (H2 v)) uinS) vinS).
move=> H2 u.
apply/forallP => v.
apply/implyP => uinS.
apply/implyP => vinS.
apply/negP.
exact: H2.
Qed.
Lemma stableP : reflect p_stable pb_stable.
Proof.
rewrite /pb_stable.
apply: introP.
(* first case: -> *)
rewrite eqEsubset => /andP [NScapSsub0 _].
rewrite /p_stable => u v uinS vinS adjuv.
have vinNScapS: v ∈ (NS(S) :&: S).
move: (dominated_belongs_to_open_neigh_set uinS adjuv) => vinNS.
by rewrite in_setI vinNS vinS.
move: (subsetP NScapSsub0 v vinNScapS).
by rewrite in_set0.
(* second case: <- *)
move/set0Pn.
elim=> u.
rewrite in_setI => [/andP[uinNS uinS] ].
move/bigcupP: uinNS.
elim=> v /andP[_ vinS].
rewrite -sg_opneigh => adjuv.
move=> /(_ u v).
rewrite uinS vinS => /(_ isT isT).
contradiction.
Qed.
End Stable_Set.
Proposition st_empty : p_stable ∅.
Proof. rewrite /p_stable => u v ; rewrite in_set0 //. Qed.
Definition stable := @VertexSetProperty p_stable pb_stable stableP ∅ st_empty.
(**********************************************************************************)
Section Dominating_Set.
Variable D : {set G}.
Definition p_dominating : Prop := forall v : G, v ∉ D -> exists u : G, u ∈ D /\ u -- v.
Definition pb_dominating : bool := V(G) == NS[D].
Theorem dominatingP : reflect p_dominating pb_dominating.
Proof.
rewrite /p_dominating /pb_dominating.
apply: (iffP eqP).
(* first case: -> *)
move=> /eqP VisND v vnotinD.
move/eqP: VisND (in_setT v) -> => /bigcupP.
elim=> [x /andP [_ xinD] vinNx].
rewrite /closed_neigh in_setU /open_neigh in_set in vinNx.
case/orP: vinNx => [adjxv|visx].
exists x.
by split=> [// | //].
rewrite in_set1 in visx.
rewrite -(eqP visx) in xinD.
move: (negP vnotinD).
contradiction.
(* second case: <- *)
move=> H1.
apply/eqP.
rewrite eqEsubset subsetT andbT.
(* it is enough to prove V(G) ⊆ ND *)
apply/subsetP => x.
move: (set_minus_union (subsetT D)) ->.
rewrite in_setU.
case/orP ; [ | apply/subsetP ; exact: D_in_closed_neight_set].
(* case when x ∉ D *)
move: (H1 x) => H2.
rewrite in_setD => /andP [xnotinD _].
elim: (H2 xnotinD) => u [uinD adjux].
exact: dominated_belongs_to_closed_neigh_set uinD adjux.
Qed.
End Dominating_Set.
Proposition dom_VG : p_dominating V(G).
Proof.
apply/dominatingP.
rewrite /pb_dominating eqEsubset subsetT andbT.
exact: D_in_closed_neight_set.
Qed.
Definition dominating := @VertexSetProperty p_dominating pb_dominating dominatingP V(G) dom_VG.
(**********************************************************************************)
Section Private_vertices.
Variable D : {set G}.
Definition private_set : G -> {set G} := fun v => N[v] :\: NS[D :\: ❴v❵].
Definition private : G -> G -> Prop := fun w v => v -*- w /\ (forall u : G, u ∈ D -> u -*- w -> u = v).
Definition privateb : G -> G -> bool := fun w v => w ∈ private_set v.
Theorem privateP : forall v w : G, reflect (private v w) (privateb v w).
Proof.
move=> v w.
rewrite /private /privateb /private_set in_setD /closed_neigh_set.
apply: (iffP andP) ; last first.
(* first case: <- *)
move=> [vdomw H1].
split ; [ | by rewrite -clsg_clneigh cl_sg_sym ].
(* we prove that w is not in ND - {v} *)
apply/bigcupP.
elim=> x /andP [_ xinDminusv] winNx.
move: (H1 x) => H2.
rewrite cl_sg_sym in H2.
rewrite in_setD in xinDminusv.
move: xinDminusv => /andP [xnotv xinD].
rewrite -clsg_clneigh in winNx.
move: (H2 xinD winNx) => xisv.
move: xnotv.
by rewrite in_set => /eqP.
(* second case: -> *)
move=> [wnotincup winNv].
split ; [ by rewrite cl_sg_sym clsg_clneigh | ].
(* we prove that any vertex in D such that it dominates w, then it must be v *)
move=> u uinD udomw.
apply/eqP.
move: wnotincup.
apply: contraR => unotv.
apply/bigcupP.
exists u.
apply/andP ; split=> //.
rewrite in_setD in_set.
apply/andP ; split=> [// | //].
by rewrite -clsg_clneigh cl_sg_sym.
Qed.
End Private_vertices.
Arguments private_set : clear implicits.
Arguments private : clear implicits.
Arguments privateb : clear implicits.
Arguments privateP : clear implicits.
(**********************************************************************************)
Section Irredundant_Set.
Variable D : {set G}.
Definition p_irredundant : Prop := forall v : G, v ∈ D -> exists w : G, private D w v.
Definition pb_irredundant : bool := [forall v : G, (v ∈ D) ==> (private_set D v != ∅)].
Lemma irredundantP : reflect p_irredundant pb_irredundant.
Proof.
rewrite /p_irredundant /pb_irredundant.
apply: (iffP forallP).
move=> irr v vinD.
move/set0Pn: (implyP (irr v) vinD).
elim=> w /privateP winpriv.
by exists w.
move=> irr v.
apply/implyP => vinD.
apply/set0Pn.
elim: (irr v vinD) => w winpriv.
exists w.
by apply/privateP.
Qed.
End Irredundant_Set.
Proposition irr_empty : p_irredundant ∅.
Proof. rewrite /p_irredundant => v ; by rewrite in_set0. Qed.
Definition irredundant := @VertexSetProperty p_irredundant pb_irredundant irredundantP ∅ irr_empty.
(**********************************************************************************)
Variable S : {set G}.
Definition p_stable : Prop := forall u v : G, u ∈ S -> v ∈ S -> ~ (u -- v).
Definition pb_stable : bool := NS(S) :&: S == ∅.
Lemma stable_refl : reflect p_stable [forall u : G, forall v : G, (u ∈ S) ==> (v ∈ S) ==> ~~ (u -- v)].
Proof.
rewrite /p_stable.
apply: (iffP forallP).
move=> H1 u v uinS vinS.
move/forallP: (H1 u) => H2.
apply/negP.
by rewrite (implyP ((implyP (H2 v)) uinS) vinS).
move=> H2 u.
apply/forallP => v.
apply/implyP => uinS.
apply/implyP => vinS.
apply/negP.
exact: H2.
Qed.
Lemma stableP : reflect p_stable pb_stable.
Proof.
rewrite /pb_stable.
apply: introP.
(* first case: -> *)
rewrite eqEsubset => /andP [NScapSsub0 _].
rewrite /p_stable => u v uinS vinS adjuv.
have vinNScapS: v ∈ (NS(S) :&: S).
move: (dominated_belongs_to_open_neigh_set uinS adjuv) => vinNS.
by rewrite in_setI vinNS vinS.
move: (subsetP NScapSsub0 v vinNScapS).
by rewrite in_set0.
(* second case: <- *)
move/set0Pn.
elim=> u.
rewrite in_setI => [/andP[uinNS uinS] ].
move/bigcupP: uinNS.
elim=> v /andP[_ vinS].
rewrite -sg_opneigh => adjuv.
move=> /(_ u v).
rewrite uinS vinS => /(_ isT isT).
contradiction.
Qed.
End Stable_Set.
Proposition st_empty : p_stable ∅.
Proof. rewrite /p_stable => u v ; rewrite in_set0 //. Qed.
Definition stable := @VertexSetProperty p_stable pb_stable stableP ∅ st_empty.
(**********************************************************************************)
Section Dominating_Set.
Variable D : {set G}.
Definition p_dominating : Prop := forall v : G, v ∉ D -> exists u : G, u ∈ D /\ u -- v.
Definition pb_dominating : bool := V(G) == NS[D].
Theorem dominatingP : reflect p_dominating pb_dominating.
Proof.
rewrite /p_dominating /pb_dominating.
apply: (iffP eqP).
(* first case: -> *)
move=> /eqP VisND v vnotinD.
move/eqP: VisND (in_setT v) -> => /bigcupP.
elim=> [x /andP [_ xinD] vinNx].
rewrite /closed_neigh in_setU /open_neigh in_set in vinNx.
case/orP: vinNx => [adjxv|visx].
exists x.
by split=> [// | //].
rewrite in_set1 in visx.
rewrite -(eqP visx) in xinD.
move: (negP vnotinD).
contradiction.
(* second case: <- *)
move=> H1.
apply/eqP.
rewrite eqEsubset subsetT andbT.
(* it is enough to prove V(G) ⊆ ND *)
apply/subsetP => x.
move: (set_minus_union (subsetT D)) ->.
rewrite in_setU.
case/orP ; [ | apply/subsetP ; exact: D_in_closed_neight_set].
(* case when x ∉ D *)
move: (H1 x) => H2.
rewrite in_setD => /andP [xnotinD _].
elim: (H2 xnotinD) => u [uinD adjux].
exact: dominated_belongs_to_closed_neigh_set uinD adjux.
Qed.
End Dominating_Set.
Proposition dom_VG : p_dominating V(G).
Proof.
apply/dominatingP.
rewrite /pb_dominating eqEsubset subsetT andbT.
exact: D_in_closed_neight_set.
Qed.
Definition dominating := @VertexSetProperty p_dominating pb_dominating dominatingP V(G) dom_VG.
(**********************************************************************************)
Section Private_vertices.
Variable D : {set G}.
Definition private_set : G -> {set G} := fun v => N[v] :\: NS[D :\: ❴v❵].
Definition private : G -> G -> Prop := fun w v => v -*- w /\ (forall u : G, u ∈ D -> u -*- w -> u = v).
Definition privateb : G -> G -> bool := fun w v => w ∈ private_set v.
Theorem privateP : forall v w : G, reflect (private v w) (privateb v w).
Proof.
move=> v w.
rewrite /private /privateb /private_set in_setD /closed_neigh_set.
apply: (iffP andP) ; last first.
(* first case: <- *)
move=> [vdomw H1].
split ; [ | by rewrite -clsg_clneigh cl_sg_sym ].
(* we prove that w is not in ND - {v} *)
apply/bigcupP.
elim=> x /andP [_ xinDminusv] winNx.
move: (H1 x) => H2.
rewrite cl_sg_sym in H2.
rewrite in_setD in xinDminusv.
move: xinDminusv => /andP [xnotv xinD].
rewrite -clsg_clneigh in winNx.
move: (H2 xinD winNx) => xisv.
move: xnotv.
by rewrite in_set => /eqP.
(* second case: -> *)
move=> [wnotincup winNv].
split ; [ by rewrite cl_sg_sym clsg_clneigh | ].
(* we prove that any vertex in D such that it dominates w, then it must be v *)
move=> u uinD udomw.
apply/eqP.
move: wnotincup.
apply: contraR => unotv.
apply/bigcupP.
exists u.
apply/andP ; split=> //.
rewrite in_setD in_set.
apply/andP ; split=> [// | //].
by rewrite -clsg_clneigh cl_sg_sym.
Qed.
End Private_vertices.
Arguments private_set : clear implicits.
Arguments private : clear implicits.
Arguments privateb : clear implicits.
Arguments privateP : clear implicits.
(**********************************************************************************)
Section Irredundant_Set.
Variable D : {set G}.
Definition p_irredundant : Prop := forall v : G, v ∈ D -> exists w : G, private D w v.
Definition pb_irredundant : bool := [forall v : G, (v ∈ D) ==> (private_set D v != ∅)].
Lemma irredundantP : reflect p_irredundant pb_irredundant.
Proof.
rewrite /p_irredundant /pb_irredundant.
apply: (iffP forallP).
move=> irr v vinD.
move/set0Pn: (implyP (irr v) vinD).
elim=> w /privateP winpriv.
by exists w.
move=> irr v.
apply/implyP => vinD.
apply/set0Pn.
elim: (irr v vinD) => w winpriv.
exists w.
by apply/privateP.
Qed.
End Irredundant_Set.
Proposition irr_empty : p_irredundant ∅.
Proof. rewrite /p_irredundant => v ; by rewrite in_set0. Qed.
Definition irredundant := @VertexSetProperty p_irredundant pb_irredundant irredundantP ∅ irr_empty.
(**********************************************************************************)
Section MaxMin_sets.
Variable p : vsproperty.
Variable D : {set G}.
Let pb := vsbool p.
Let pP := vsrefl p.
Definition maximal : Prop := p D /\ (forall F : {set G}, D ⊂ F -> ~ p F).
Definition minimal : Prop := p D /\ (forall F : {set G}, F ⊂ D -> ~ p F).
Definition maximalb : bool := maxset pb D.
Definition minimalb : bool := minset pb D.
Lemma maximalP : reflect maximal maximalb.
Proof.
have imP: forall F : {set G}, reflect (D ⊂ F -> ~ p F) ((D ⊂ F) ==> ~~ (pb F)).
move=> F.
apply: (iffP implyP).
move=> H1 DproperF /pP pF ; by move: (negP (H1 DproperF)).
move=> H1 DproperF ; apply/pP ; by move: (H1 DproperF).
(* now, we prove the main statement *)
rewrite /maximal /maximalb.
apply: (iffP idP).
(* case <- *)
move=> /maxsetP [/pP pD H2].
split => //.
move=> F.
apply/imP.
rewrite implybN /proper.
apply/implyP => pbF.
rewrite negb_and -implybE negbK.
apply/implyP => DsubF.
by move: (H2 F pbF DsubF)->.
(* case -> *)
move=> [/pP pbD H3].
apply/maxsetP.
split => //.
move=> F pbF DsubF.
apply/eqP ; rewrite eqEsubset.
apply/andP ; split => [ |//].
move/imP: (H3 F).
by rewrite implybN pbF implyTb /proper DsubF andTb negbK.
Qed.
Lemma minimalP : reflect minimal minimalb.
Proof.
have imP: forall F : {set G}, reflect (F ⊂ D -> ~ p F) ((F ⊂ D) ==> ~~ (pb F)).
move=> F.
apply: (iffP implyP).
move=> H1 FproperD /pP pF ; by move: (negP (H1 FproperD)).
move=> H1 FproperD ; apply/pP ; by move: (H1 FproperD).
(* now, we prove the main statement *)
rewrite /minimal /minimalb.
apply: (iffP idP).
(* case <- *)
move=> /minsetP [/pP pD H2].
split => //.
move=> F.
apply/imP.
rewrite implybN /proper.
apply/implyP => pbF.
rewrite negb_and -implybE negbK.
apply/implyP => FsubD.
by move: (H2 F pbF FsubD)->.
(* case -> *)
move=> [/pP pbD H3].
apply/minsetP.
split => //.
move=> F pbF FsubD.
apply/eqP ; rewrite eqEsubset.
apply/andP ; split => //.
move/imP: (H3 F).
by rewrite implybN pbF implyTb /proper FsubD andTb negbK.
Qed.
End MaxMin_sets.
(**********************************************************************************)
Section MaxMin_sets_existence.
Variable p : vsproperty.
Variable D : {set G}.
Let pb := vsbool p.
Let pP := vsrefl p.
Let F := vsinhb p.
Let pF := vspinh p.
(* here, pbF is the proof that F satisfy the bool-predicate version of the property *)
Let pbF : pb F.
Proof. exact/pP. Qed.
Definition ex_maximal : {set G} := s2val (maxset_exists pbF).
Definition ex_minimal : {set G} := s2val (minset_exists pbF).
Lemma maximal_exists : maximal p ex_maximal.
Proof.
apply/(maximalP p ex_maximal).
rewrite /maximalb /ex_maximal.
exact: s2valP (maxset_exists pbF).
Qed.
Lemma minimal_exists : minimal p ex_minimal.
Proof.
apply/(minimalP p ex_minimal).
rewrite /minimalb /ex_minimal.
exact: s2valP (minset_exists pbF).
Qed.
End MaxMin_sets_existence.
(**********************************************************************************)
Section Independence_system_definitions.
Variable p : vsproperty.
Definition hereditary : Prop :=
forall D F : {set G}, F ⊆ D -> p D -> p F.
Definition superhereditary : Prop :=
forall D F : {set G}, D ⊆ F -> p D -> p F.
End Independence_system_definitions.
(**********************************************************************************)
Section Independence_system_properties.
(* if D is dominating, any supraset of D is also dominating *)
Proposition dom_superhereditary : superhereditary dominating.
Proof.
rewrite /superhereditary /p_dominating.
move=> D F DsubF Ddom v vnotinF.
have vinVminusF: v ∈ (V(G) :\: F) by rewrite in_setD in_setT andbT.
move: (subsetP (setDS setT DsubF)).
move=> /(_ v vinVminusF) => vinVminusD.
rewrite in_setD in_setT andbT in vinVminusD.
elim: (Ddom v vinVminusD) => w [winD adjwv].
exists w.
split=> [ | //].
exact: (subsetP DsubF) w winD.
Qed.
(* if D is irredundant, any subset of D is also irredundant *)
Proposition irr_hereditary : hereditary irredundant.
Proof.
rewrite /hereditary /p_irredundant.
move=> D F FsubD Dirr v vinF.
move: (subsetP FsubD v vinF) => vinD.
elim: (Dirr v vinD) => x xprivv.
exists x.
move: xprivv.
rewrite /private => [ [vdomx H1] ].
split => //.
move=> u uinF udomx.
move: (subsetP FsubD u uinF) => uinD.
exact: H1 u uinD udomx.
Qed.
(* if D is stable, any subset of D is also stable *)
Proposition st_hereditary : hereditary stable.
Proof.
rewrite /hereditary /p_stable.
move=> D F FsubD Dstable u v uinF vinF.
move: (subsetP FsubD u uinF) => uinD.
move: (subsetP FsubD v vinF) => vinD.
exact: Dstable u v uinD vinD.
Qed.
Variable p : vsproperty.
Variable D : {set G}.
(* Alternative definition of maximal set of a hereditary property *)
Theorem maximal_altdef : hereditary p ->
(maximal p D <-> (p D /\ (forall v : G, v ∉ D -> ~ p (D :|: ❴v❵)))).
Proof.
move=> p_hereditary.
rewrite /maximal /iff ; split.
(* first case: -> *)
move=> [pD H1].
split=> //.
move=> v vnotinD.
apply: (H1 (D :|: ❴v❵)).
(* it is enough to prove that D ⊂ D cup {v} *)
rewrite properUl //.
apply/negP => vsubD.
move: ((subsetP vsubD) v).
rewrite in_set1 eq_refl => vinD.
move: vnotinD.
apply/negP.
by rewrite negbK vinD.
(* second case: <- *)
move=> [pD H2].
split=> //.
move=> F /properP [DsubF].
elim=> v vinF vnotinD.
move: (H2 v vnotinD) => nopDminusv pF.
have DcupvsubF: D :|: ❴v❵ ⊆ F.
apply/subsetP => x.
rewrite in_setU.
case/orP => [ |xisv].
exact: (subsetP DsubF).
rewrite in_set1 in xisv.
by move/eqP: xisv ->.
move: p_hereditary.
rewrite /hereditary => /(_ F (D :|: ❴v❵) DcupvsubF pF).
contradiction.
Qed.
(* Alternative definition of minimal set of a superhereditary property *)
Theorem minimal_altdef : superhereditary p ->
(minimal p D <-> (p D /\ (forall v : G, v ∈ D -> ~ p (D :\: ❴v❵)))).
Proof.
move=> p_superhereditary.
rewrite /minimal /iff ; split.
(* first case: -> *)
move=> [pD H1].
split=> //.
move=> v vinD.
apply: (H1 (D :\: ❴v❵)).
by rewrite properD1.
(* second case: <- *)
move=> [pD H2].
split=> //.
move=> F /properP [FsubD].
elim=> v vinD vnotinF.
move: ((H2 v) vinD) => nopDminusv pF.
have FsubDminusv: F ⊆ D :\: ❴v❵.
apply/subsetP => x xinF.
rewrite in_setD (subsetP FsubD x xinF) andbT.
move: vnotinF.
apply: contra => xisv.
rewrite in_set1 in xisv.
by move/eqP: xisv <-.
move: p_superhereditary.
rewrite /superhereditary => /(_ F (D :\: ❴v❵) FsubDminusv pF).
contradiction.
Qed.
End Independence_system_properties.
(**********************************************************************************)
Variable p : vsproperty.
Variable D : {set G}.
Let pb := vsbool p.
Let pP := vsrefl p.
Definition maximal : Prop := p D /\ (forall F : {set G}, D ⊂ F -> ~ p F).
Definition minimal : Prop := p D /\ (forall F : {set G}, F ⊂ D -> ~ p F).
Definition maximalb : bool := maxset pb D.
Definition minimalb : bool := minset pb D.
Lemma maximalP : reflect maximal maximalb.
Proof.
have imP: forall F : {set G}, reflect (D ⊂ F -> ~ p F) ((D ⊂ F) ==> ~~ (pb F)).
move=> F.
apply: (iffP implyP).
move=> H1 DproperF /pP pF ; by move: (negP (H1 DproperF)).
move=> H1 DproperF ; apply/pP ; by move: (H1 DproperF).
(* now, we prove the main statement *)
rewrite /maximal /maximalb.
apply: (iffP idP).
(* case <- *)
move=> /maxsetP [/pP pD H2].
split => //.
move=> F.
apply/imP.
rewrite implybN /proper.
apply/implyP => pbF.
rewrite negb_and -implybE negbK.
apply/implyP => DsubF.
by move: (H2 F pbF DsubF)->.
(* case -> *)
move=> [/pP pbD H3].
apply/maxsetP.
split => //.
move=> F pbF DsubF.
apply/eqP ; rewrite eqEsubset.
apply/andP ; split => [ |//].
move/imP: (H3 F).
by rewrite implybN pbF implyTb /proper DsubF andTb negbK.
Qed.
Lemma minimalP : reflect minimal minimalb.
Proof.
have imP: forall F : {set G}, reflect (F ⊂ D -> ~ p F) ((F ⊂ D) ==> ~~ (pb F)).
move=> F.
apply: (iffP implyP).
move=> H1 FproperD /pP pF ; by move: (negP (H1 FproperD)).
move=> H1 FproperD ; apply/pP ; by move: (H1 FproperD).
(* now, we prove the main statement *)
rewrite /minimal /minimalb.
apply: (iffP idP).
(* case <- *)
move=> /minsetP [/pP pD H2].
split => //.
move=> F.
apply/imP.
rewrite implybN /proper.
apply/implyP => pbF.
rewrite negb_and -implybE negbK.
apply/implyP => FsubD.
by move: (H2 F pbF FsubD)->.
(* case -> *)
move=> [/pP pbD H3].
apply/minsetP.
split => //.
move=> F pbF FsubD.
apply/eqP ; rewrite eqEsubset.
apply/andP ; split => //.
move/imP: (H3 F).
by rewrite implybN pbF implyTb /proper FsubD andTb negbK.
Qed.
End MaxMin_sets.
(**********************************************************************************)
Section MaxMin_sets_existence.
Variable p : vsproperty.
Variable D : {set G}.
Let pb := vsbool p.
Let pP := vsrefl p.
Let F := vsinhb p.
Let pF := vspinh p.
(* here, pbF is the proof that F satisfy the bool-predicate version of the property *)
Let pbF : pb F.
Proof. exact/pP. Qed.
Definition ex_maximal : {set G} := s2val (maxset_exists pbF).
Definition ex_minimal : {set G} := s2val (minset_exists pbF).
Lemma maximal_exists : maximal p ex_maximal.
Proof.
apply/(maximalP p ex_maximal).
rewrite /maximalb /ex_maximal.
exact: s2valP (maxset_exists pbF).
Qed.
Lemma minimal_exists : minimal p ex_minimal.
Proof.
apply/(minimalP p ex_minimal).
rewrite /minimalb /ex_minimal.
exact: s2valP (minset_exists pbF).
Qed.
End MaxMin_sets_existence.
(**********************************************************************************)
Section Independence_system_definitions.
Variable p : vsproperty.
Definition hereditary : Prop :=
forall D F : {set G}, F ⊆ D -> p D -> p F.
Definition superhereditary : Prop :=
forall D F : {set G}, D ⊆ F -> p D -> p F.
End Independence_system_definitions.
(**********************************************************************************)
Section Independence_system_properties.
(* if D is dominating, any supraset of D is also dominating *)
Proposition dom_superhereditary : superhereditary dominating.
Proof.
rewrite /superhereditary /p_dominating.
move=> D F DsubF Ddom v vnotinF.
have vinVminusF: v ∈ (V(G) :\: F) by rewrite in_setD in_setT andbT.
move: (subsetP (setDS setT DsubF)).
move=> /(_ v vinVminusF) => vinVminusD.
rewrite in_setD in_setT andbT in vinVminusD.
elim: (Ddom v vinVminusD) => w [winD adjwv].
exists w.
split=> [ | //].
exact: (subsetP DsubF) w winD.
Qed.
(* if D is irredundant, any subset of D is also irredundant *)
Proposition irr_hereditary : hereditary irredundant.
Proof.
rewrite /hereditary /p_irredundant.
move=> D F FsubD Dirr v vinF.
move: (subsetP FsubD v vinF) => vinD.
elim: (Dirr v vinD) => x xprivv.
exists x.
move: xprivv.
rewrite /private => [ [vdomx H1] ].
split => //.
move=> u uinF udomx.
move: (subsetP FsubD u uinF) => uinD.
exact: H1 u uinD udomx.
Qed.
(* if D is stable, any subset of D is also stable *)
Proposition st_hereditary : hereditary stable.
Proof.
rewrite /hereditary /p_stable.
move=> D F FsubD Dstable u v uinF vinF.
move: (subsetP FsubD u uinF) => uinD.
move: (subsetP FsubD v vinF) => vinD.
exact: Dstable u v uinD vinD.
Qed.
Variable p : vsproperty.
Variable D : {set G}.
(* Alternative definition of maximal set of a hereditary property *)
Theorem maximal_altdef : hereditary p ->
(maximal p D <-> (p D /\ (forall v : G, v ∉ D -> ~ p (D :|: ❴v❵)))).
Proof.
move=> p_hereditary.
rewrite /maximal /iff ; split.
(* first case: -> *)
move=> [pD H1].
split=> //.
move=> v vnotinD.
apply: (H1 (D :|: ❴v❵)).
(* it is enough to prove that D ⊂ D cup {v} *)
rewrite properUl //.
apply/negP => vsubD.
move: ((subsetP vsubD) v).
rewrite in_set1 eq_refl => vinD.
move: vnotinD.
apply/negP.
by rewrite negbK vinD.
(* second case: <- *)
move=> [pD H2].
split=> //.
move=> F /properP [DsubF].
elim=> v vinF vnotinD.
move: (H2 v vnotinD) => nopDminusv pF.
have DcupvsubF: D :|: ❴v❵ ⊆ F.
apply/subsetP => x.
rewrite in_setU.
case/orP => [ |xisv].
exact: (subsetP DsubF).
rewrite in_set1 in xisv.
by move/eqP: xisv ->.
move: p_hereditary.
rewrite /hereditary => /(_ F (D :|: ❴v❵) DcupvsubF pF).
contradiction.
Qed.
(* Alternative definition of minimal set of a superhereditary property *)
Theorem minimal_altdef : superhereditary p ->
(minimal p D <-> (p D /\ (forall v : G, v ∈ D -> ~ p (D :\: ❴v❵)))).
Proof.
move=> p_superhereditary.
rewrite /minimal /iff ; split.
(* first case: -> *)
move=> [pD H1].
split=> //.
move=> v vinD.
apply: (H1 (D :\: ❴v❵)).
by rewrite properD1.
(* second case: <- *)
move=> [pD H2].
split=> //.
move=> F /properP [FsubD].
elim=> v vinD vnotinF.
move: ((H2 v) vinD) => nopDminusv pF.
have FsubDminusv: F ⊆ D :\: ❴v❵.
apply/subsetP => x xinF.
rewrite in_setD (subsetP FsubD x xinF) andbT.
move: vnotinF.
apply: contra => xisv.
rewrite in_set1 in xisv.
by move/eqP: xisv <-.
move: p_superhereditary.
rewrite /superhereditary => /(_ F (D :\: ❴v❵) FsubDminusv pF).
contradiction.
Qed.
End Independence_system_properties.
(**********************************************************************************)
Section Relations_between_stable_dominating_irredundant_sets.
Variable D : {set G}.
(* A stable set D is maximal iff D is stable and dominating
* See Prop. 3.5 of Fundamentals of Domination *)
Theorem maximal_st_iff_st_dom : maximal stable D <-> (stable D /\ dominating D).
Proof.
rewrite maximal_altdef // ; last exact: st_hereditary.
rewrite /dominating /iff ; split ; last first.
(* first case: <- *)
move=> [Dst Ddom].
split=> //.
move=> v vnotinD.
rewrite /stable => Dcupvstable.
elim: (Ddom v vnotinD) => u [uinD adjuv].
have uinDplusv : u ∈ (D :|: ❴v❵) by rewrite in_setU uinD orTb.
have vinDplusv : v ∈ (D :|: ❴v❵) by rewrite in_setU in_set1 eq_refl orbT.
move: ((Dcupvstable u v) uinDplusv vinDplusv).
contradiction.
(* second case: -> *)
move=> [Dst Dmaximal].
split => //.
(* we know that D is a maximal stable set and we need to prove that, for each v ∈ V(G)-D,
* there must be an u ∈ D adjacent to v. *)
move=> v vnotinD.
move: (Dmaximal v vnotinD) => /stable_refl.
rewrite negb_forall => /existsP ; elim=> x.
rewrite negb_forall => /existsP ; elim=> w.
rewrite !implybE !negb_or => /andP [xinDplusv /andP [winDplusv adjxw] ].
rewrite in_setU negbK in xinDplusv.
rewrite in_setU negbK in winDplusv.
rewrite negbK in adjxw.
case/orP: xinDplusv.
case/orP: winDplusv.
(* case 1: w and x are from the stable set -> contradiction *)
move=> winD xinD.
move: Dst.
rewrite /stable.
move=> /(_ x w xinD winD) => noadjxw.
contradiction.
(* case 2: w=v and x is from the stable set *)
rewrite in_set1 => /eqP wisv xinD.
exists x.
split=> //.
by rewrite -wisv.
case/orP: winDplusv.
(* case 3: x=v and w is from the stable set *)
rewrite in_set1 => winD /eqP xisv.
exists w.
split=> //.
by rewrite sg_sym -xisv.
(* case 4: x=v and w=v -> contradiction *)
rewrite !in_set1 => /eqP wisv /eqP xisv.
by rewrite xisv wisv sg_irrefl in adjxw.
Qed.
(* A maximal stable set is minimal dominating
* See Prop. 3.6 of Fundamentals of Domination *)
Theorem maximal_st_is_minimal_dom : maximal stable D -> minimal dominating D.
Proof.
rewrite maximal_st_iff_st_dom.
move=> [Dst Ddom].
rewrite minimal_altdef // ; last exact: dom_superhereditary.
split=> //.
move=> v vinD.
rewrite /dominating => /(_ v).
rewrite in_setD vinD andbT negbK in_set1 (eq_refl v) => /(_ isT).
elim=> x.
rewrite in_setD.
move=> [/andP [xneqv xinD] adjxv].
rewrite in_set in xneqv.
(* we have found an edge (x,v) in D, but D is stable -> contradiction *)
move: Dst.
rewrite /stable.
move=> /(_ x v) => /(_ xinD vinD).
contradiction.
Qed.
(* A dominating set D is minimal iff D is dominating and irredundant
* See Prop. 3.8 of Fundamentals of Domination *)
Theorem minimal_dom_iff_dom_irr : minimal dominating D <-> dominating D /\ irredundant D.
Proof.
rewrite minimal_altdef // ; last exact: dom_superhereditary.
rewrite /irredundant /iff ; split ; last first.
(* first case: <- *)
move=> [Ddom Dirr].
split=> //.
move=> v vinD.
rewrite /dominating => Dminusvdom.
(* v has a private vertex u so D-{v} can not be dominating since it can not dominate u *)
elim: (Dirr v vinD) => u.
rewrite /private => [ [vdomu privvu] ].
case: (boolP (u ∈ (D :\ v))).
(* case u in D-{v} *)
move/setD1P => [/eqP uneqv uinD].
move: (privvu u uinD (cl_sg_refl u)).
contradiction.
(* case u notin D-{v} *)
move=> unotinDminusv.
elim: (Dminusvdom u unotinDminusv) => w [winDminusv adjwu].
rewrite in_setD in_set1 in winDminusv.
move: winDminusv => /andP [/eqP wneqv winD].
have wdomu: w -*- u by rewrite /cl_sedge adjwu orTb.
move: (privvu w winD wdomu).
contradiction.
(* second case: -> *)
move=> [Ddom Dminimal].
split => //.
move=> v vinD.
move: (Dminimal v vinD) => /dominatingP.
rewrite /pb_dominating eq_sym eqEproper negb_and subsetT orFb negbK.
move=> /properP [ _ ].
elim=> w _ wnotinNDminusv.
move: (in_setT w).
move/dominatingP: Ddom.
rewrite /pb_dominating => /eqP ->.
move=> winND.
exists w.
apply/privateP.
rewrite /privateb /private_set in_setD wnotinNDminusv andTb.
move: winND.
rewrite /closed_neigh_set.
move/bigcupP.
elim=> x /andP [_ xinD] winNx.
(* the unique x that dominates u is v, other vertex leads to a contradiction *)
case: (boolP (v == x)) ; [ by move/eqP-> | ].
move=> visnotx.
have xinDminusv: x ∈ D :\: ❴v❵ by rewrite in_setD in_set1 eq_sym visnotx andTb xinD.
rewrite -clsg_clneigh cl_sg_sym /cl_sedge in winNx.
move/negP: wnotinNDminusv.
case/orP: winNx => [adjxw | xeqw].
(* case when x is adjacent to w *)
move: (dominated_belongs_to_closed_neigh_set xinDminusv adjxw).
contradiction.
(* case when x = w *)
move: (subsetP (D_in_closed_neight_set (D :\: ❴v❵)) x xinDminusv).
move/eqP: xeqw<-.
contradiction.
Qed.
(* A minimal dominating set is maximal irredundant
* See Prop. 3.9 of Fundamentals of Domination *)
Theorem minimal_dom_is_maximal_irr : minimal dominating D -> maximal irredundant D.
Proof.
rewrite minimal_dom_iff_dom_irr.
move=> [Ddom Dirr].
rewrite maximal_altdef // ; last exact: irr_hereditary.
split=> //.
move=> v vnotinD.
rewrite /irredundant => /(_ v).
rewrite in_setU in_set1 (eq_refl v) orbT => /(_ isT).
elim=> x.
(* we have found a private vertex x of v in D cup {v}, but D is already dominating x -> contradiction *)
rewrite /private => [ [vdomx] ].
case: (boolP (x ∈ D)) => [xinD | xnotinD].
(* case when x is in D (x dominates itself) *)
have xinDcupv: x ∈ D :|: ❴v❵ by rewrite in_setU xinD orTb.
move=> /(_ x xinDcupv).
rewrite cl_sg_refl => /(_ isT).
move=> xeqv ; move/negP: vnotinD ; rewrite -xeqv ; contradiction.
(* case when x is not in D (some u in D dominates x) *)
move: Ddom.
rewrite /dominating => /(_ x xnotinD).
elim=> u [uinD adjux].
have uinDcupv: u ∈ D :|: ❴v❵ by rewrite in_setU uinD orTb.
move=> /(_ u uinDcupv).
rewrite /cl_sedge adjux orTb => /(_ isT).
move=> xeqv ; move/negP: vnotinD ; rewrite -xeqv ; contradiction.
Qed.
End Relations_between_stable_dominating_irredundant_sets.
(**********************************************************************************)
Section Existence_of_stable_dominating_irredundant_sets.
(* Definitions of "stable and dominating", "minimal dominating" and "maximal irredundant" sets *)
Definition p_st_dom := (fun D : {set G} => stable D /\ dominating D).
Definition pb_st_dom := (fun D : {set G} => pb_stable D && pb_dominating D).
Definition p_min_dom := minimal dominating.
Definition pb_min_dom := minimalb dominating.
Definition p_max_irr := maximal irredundant.
Definition pb_max_irr := maximalb irredundant.
(* Some reflection lemmas *)
Lemma st_domP: forall D : {set G}, reflect (p_st_dom D) (pb_st_dom D).
Proof.
move=> D.
rewrite /p_st_dom /pb_st_dom.
apply: (iffP andP).
by move=> [/stableP pb_st /dominatingP pb_dom].
by move=> [/stableP p_st /dominatingP p_dom].
Qed.
Lemma min_domP: forall D : {set G}, reflect (p_min_dom D) (pb_min_dom D).
Proof. move=> D ; rewrite /p_min_dom /pb_min_dom ; apply/minimalP. Qed.
Lemma max_irrP: forall D : {set G}, reflect (p_max_irr D) (pb_max_irr D).
Proof. move=> D ; rewrite /p_max_irr /pb_max_irr ; apply/maximalP. Qed.
(* Inhabitants that are "maximal stable", "minimal dominating" and "maximal irredundant" + proofs *)
Definition inhb_st_dom := ex_maximal stable.
Definition inhb_min_dom := ex_minimal dominating.
Definition inhb_max_irr := ex_maximal irredundant.
Lemma pinh_st_dom : p_st_dom inhb_st_dom.
Proof.
have: maximal stable inhb_st_dom by exact: maximal_exists.
by rewrite /p_st_dom maximal_st_iff_st_dom.
Qed.
Lemma pinh_min_dom : p_min_dom inhb_min_dom.
Proof. exact: minimal_exists. Qed.
Lemma pinh_max_irr : p_max_irr inhb_max_irr.
Proof. exact: maximal_exists. Qed.
End Existence_of_stable_dominating_irredundant_sets.
Definition st_dom := @VertexSetProperty p_st_dom pb_st_dom st_domP inhb_st_dom pinh_st_dom.
Definition min_dom := @VertexSetProperty p_min_dom pb_min_dom min_domP inhb_min_dom pinh_min_dom.
Definition max_irr := @VertexSetProperty p_max_irr pb_max_irr max_irrP inhb_max_irr pinh_max_irr.
(**********************************************************************************)
Variable D : {set G}.
(* A stable set D is maximal iff D is stable and dominating
* See Prop. 3.5 of Fundamentals of Domination *)
Theorem maximal_st_iff_st_dom : maximal stable D <-> (stable D /\ dominating D).
Proof.
rewrite maximal_altdef // ; last exact: st_hereditary.
rewrite /dominating /iff ; split ; last first.
(* first case: <- *)
move=> [Dst Ddom].
split=> //.
move=> v vnotinD.
rewrite /stable => Dcupvstable.
elim: (Ddom v vnotinD) => u [uinD adjuv].
have uinDplusv : u ∈ (D :|: ❴v❵) by rewrite in_setU uinD orTb.
have vinDplusv : v ∈ (D :|: ❴v❵) by rewrite in_setU in_set1 eq_refl orbT.
move: ((Dcupvstable u v) uinDplusv vinDplusv).
contradiction.
(* second case: -> *)
move=> [Dst Dmaximal].
split => //.
(* we know that D is a maximal stable set and we need to prove that, for each v ∈ V(G)-D,
* there must be an u ∈ D adjacent to v. *)
move=> v vnotinD.
move: (Dmaximal v vnotinD) => /stable_refl.
rewrite negb_forall => /existsP ; elim=> x.
rewrite negb_forall => /existsP ; elim=> w.
rewrite !implybE !negb_or => /andP [xinDplusv /andP [winDplusv adjxw] ].
rewrite in_setU negbK in xinDplusv.
rewrite in_setU negbK in winDplusv.
rewrite negbK in adjxw.
case/orP: xinDplusv.
case/orP: winDplusv.
(* case 1: w and x are from the stable set -> contradiction *)
move=> winD xinD.
move: Dst.
rewrite /stable.
move=> /(_ x w xinD winD) => noadjxw.
contradiction.
(* case 2: w=v and x is from the stable set *)
rewrite in_set1 => /eqP wisv xinD.
exists x.
split=> //.
by rewrite -wisv.
case/orP: winDplusv.
(* case 3: x=v and w is from the stable set *)
rewrite in_set1 => winD /eqP xisv.
exists w.
split=> //.
by rewrite sg_sym -xisv.
(* case 4: x=v and w=v -> contradiction *)
rewrite !in_set1 => /eqP wisv /eqP xisv.
by rewrite xisv wisv sg_irrefl in adjxw.
Qed.
(* A maximal stable set is minimal dominating
* See Prop. 3.6 of Fundamentals of Domination *)
Theorem maximal_st_is_minimal_dom : maximal stable D -> minimal dominating D.
Proof.
rewrite maximal_st_iff_st_dom.
move=> [Dst Ddom].
rewrite minimal_altdef // ; last exact: dom_superhereditary.
split=> //.
move=> v vinD.
rewrite /dominating => /(_ v).
rewrite in_setD vinD andbT negbK in_set1 (eq_refl v) => /(_ isT).
elim=> x.
rewrite in_setD.
move=> [/andP [xneqv xinD] adjxv].
rewrite in_set in xneqv.
(* we have found an edge (x,v) in D, but D is stable -> contradiction *)
move: Dst.
rewrite /stable.
move=> /(_ x v) => /(_ xinD vinD).
contradiction.
Qed.
(* A dominating set D is minimal iff D is dominating and irredundant
* See Prop. 3.8 of Fundamentals of Domination *)
Theorem minimal_dom_iff_dom_irr : minimal dominating D <-> dominating D /\ irredundant D.
Proof.
rewrite minimal_altdef // ; last exact: dom_superhereditary.
rewrite /irredundant /iff ; split ; last first.
(* first case: <- *)
move=> [Ddom Dirr].
split=> //.
move=> v vinD.
rewrite /dominating => Dminusvdom.
(* v has a private vertex u so D-{v} can not be dominating since it can not dominate u *)
elim: (Dirr v vinD) => u.
rewrite /private => [ [vdomu privvu] ].
case: (boolP (u ∈ (D :\ v))).
(* case u in D-{v} *)
move/setD1P => [/eqP uneqv uinD].
move: (privvu u uinD (cl_sg_refl u)).
contradiction.
(* case u notin D-{v} *)
move=> unotinDminusv.
elim: (Dminusvdom u unotinDminusv) => w [winDminusv adjwu].
rewrite in_setD in_set1 in winDminusv.
move: winDminusv => /andP [/eqP wneqv winD].
have wdomu: w -*- u by rewrite /cl_sedge adjwu orTb.
move: (privvu w winD wdomu).
contradiction.
(* second case: -> *)
move=> [Ddom Dminimal].
split => //.
move=> v vinD.
move: (Dminimal v vinD) => /dominatingP.
rewrite /pb_dominating eq_sym eqEproper negb_and subsetT orFb negbK.
move=> /properP [ _ ].
elim=> w _ wnotinNDminusv.
move: (in_setT w).
move/dominatingP: Ddom.
rewrite /pb_dominating => /eqP ->.
move=> winND.
exists w.
apply/privateP.
rewrite /privateb /private_set in_setD wnotinNDminusv andTb.
move: winND.
rewrite /closed_neigh_set.
move/bigcupP.
elim=> x /andP [_ xinD] winNx.
(* the unique x that dominates u is v, other vertex leads to a contradiction *)
case: (boolP (v == x)) ; [ by move/eqP-> | ].
move=> visnotx.
have xinDminusv: x ∈ D :\: ❴v❵ by rewrite in_setD in_set1 eq_sym visnotx andTb xinD.
rewrite -clsg_clneigh cl_sg_sym /cl_sedge in winNx.
move/negP: wnotinNDminusv.
case/orP: winNx => [adjxw | xeqw].
(* case when x is adjacent to w *)
move: (dominated_belongs_to_closed_neigh_set xinDminusv adjxw).
contradiction.
(* case when x = w *)
move: (subsetP (D_in_closed_neight_set (D :\: ❴v❵)) x xinDminusv).
move/eqP: xeqw<-.
contradiction.
Qed.
(* A minimal dominating set is maximal irredundant
* See Prop. 3.9 of Fundamentals of Domination *)
Theorem minimal_dom_is_maximal_irr : minimal dominating D -> maximal irredundant D.
Proof.
rewrite minimal_dom_iff_dom_irr.
move=> [Ddom Dirr].
rewrite maximal_altdef // ; last exact: irr_hereditary.
split=> //.
move=> v vnotinD.
rewrite /irredundant => /(_ v).
rewrite in_setU in_set1 (eq_refl v) orbT => /(_ isT).
elim=> x.
(* we have found a private vertex x of v in D cup {v}, but D is already dominating x -> contradiction *)
rewrite /private => [ [vdomx] ].
case: (boolP (x ∈ D)) => [xinD | xnotinD].
(* case when x is in D (x dominates itself) *)
have xinDcupv: x ∈ D :|: ❴v❵ by rewrite in_setU xinD orTb.
move=> /(_ x xinDcupv).
rewrite cl_sg_refl => /(_ isT).
move=> xeqv ; move/negP: vnotinD ; rewrite -xeqv ; contradiction.
(* case when x is not in D (some u in D dominates x) *)
move: Ddom.
rewrite /dominating => /(_ x xnotinD).
elim=> u [uinD adjux].
have uinDcupv: u ∈ D :|: ❴v❵ by rewrite in_setU uinD orTb.
move=> /(_ u uinDcupv).
rewrite /cl_sedge adjux orTb => /(_ isT).
move=> xeqv ; move/negP: vnotinD ; rewrite -xeqv ; contradiction.
Qed.
End Relations_between_stable_dominating_irredundant_sets.
(**********************************************************************************)
Section Existence_of_stable_dominating_irredundant_sets.
(* Definitions of "stable and dominating", "minimal dominating" and "maximal irredundant" sets *)
Definition p_st_dom := (fun D : {set G} => stable D /\ dominating D).
Definition pb_st_dom := (fun D : {set G} => pb_stable D && pb_dominating D).
Definition p_min_dom := minimal dominating.
Definition pb_min_dom := minimalb dominating.
Definition p_max_irr := maximal irredundant.
Definition pb_max_irr := maximalb irredundant.
(* Some reflection lemmas *)
Lemma st_domP: forall D : {set G}, reflect (p_st_dom D) (pb_st_dom D).
Proof.
move=> D.
rewrite /p_st_dom /pb_st_dom.
apply: (iffP andP).
by move=> [/stableP pb_st /dominatingP pb_dom].
by move=> [/stableP p_st /dominatingP p_dom].
Qed.
Lemma min_domP: forall D : {set G}, reflect (p_min_dom D) (pb_min_dom D).
Proof. move=> D ; rewrite /p_min_dom /pb_min_dom ; apply/minimalP. Qed.
Lemma max_irrP: forall D : {set G}, reflect (p_max_irr D) (pb_max_irr D).
Proof. move=> D ; rewrite /p_max_irr /pb_max_irr ; apply/maximalP. Qed.
(* Inhabitants that are "maximal stable", "minimal dominating" and "maximal irredundant" + proofs *)
Definition inhb_st_dom := ex_maximal stable.
Definition inhb_min_dom := ex_minimal dominating.
Definition inhb_max_irr := ex_maximal irredundant.
Lemma pinh_st_dom : p_st_dom inhb_st_dom.
Proof.
have: maximal stable inhb_st_dom by exact: maximal_exists.
by rewrite /p_st_dom maximal_st_iff_st_dom.
Qed.
Lemma pinh_min_dom : p_min_dom inhb_min_dom.
Proof. exact: minimal_exists. Qed.
Lemma pinh_max_irr : p_max_irr inhb_max_irr.
Proof. exact: maximal_exists. Qed.
End Existence_of_stable_dominating_irredundant_sets.
Definition st_dom := @VertexSetProperty p_st_dom pb_st_dom st_domP inhb_st_dom pinh_st_dom.
Definition min_dom := @VertexSetProperty p_min_dom pb_min_dom min_domP inhb_min_dom pinh_min_dom.
Definition max_irr := @VertexSetProperty p_max_irr pb_max_irr max_irrP inhb_max_irr pinh_max_irr.
(**********************************************************************************)
Section Weighted_Sets.
Variable weight : G -> nat.
Hypothesis positive_weights : forall v : G, weight v > 0.
Variable p : vsproperty.
Variable D : {set G}.
Definition weight_set : {set G} -> nat := fun S => Σ(v in G | v ∈ S) weight v.
Lemma weight_set_natural : forall A : {set G}, weight_set A >= 0.
Proof. move=> A ; exact: leq0n. Qed.
Lemma empty_set_zero_weight : D = ∅ <-> weight_set D = 0.
Proof.
rewrite /iff ; split.
(* first case: -> *)
move=> Dempty.
rewrite /weight_set.
move: Dempty ->.
exact: sum_empty.
(* second case: <- *)
move=> /eqP weightzero.
apply/eqP.
move: weightzero.
apply: contraLR => /set0Pn.
elim=> x xinD.
rewrite /weight_set.
rewrite (eq_bigl (fun v => v ∈ ((D :\: ❴x❵) :|: ❴x❵))) ; last first.
move=> i ; by rewrite [in X in X = _](set_minus_union1 xinD).
rewrite lt0n_neq0 //.
(* now, we need to prove that the summation over (D - {x}) cup {x} is positive *)
rewrite sum_disjoint_union ; last by rewrite set_minus_disjoint.
rewrite sum_singleton addnC ltn_addr => [// | ].
exact: positive_weights x.
Qed.
Lemma subsets_weight : forall A B : {set G}, A ⊆ B -> weight_set A <= weight_set B.
Proof.
move=> A B AsubB.
rewrite /weight_set.
rewrite [in X in _ <= X](eq_bigl (fun v => v ∈ ((B :\: A) :|: A))) ; last first.
move=> i ; by rewrite [in X in X = _](set_minus_union AsubB).
rewrite (sum_disjoint_union weight (set_minus_disjoint B A)).
exact: leq_addl.
Qed.
Lemma proper_sets_weight : forall A B : {set G}, A ⊂ B -> weight_set A < weight_set B.
Proof.
move=> A B /properP [AsubB].
elim=> x xinB xnotinA.
(* we prove that indeed A ⊆ B - {x} *)
have AinBminusx: A ⊆ B :\: ❴x❵.
apply/subsetP => v vinA.
move: (subsetP AsubB v vinA) => vinB.
apply/setD1P.
split=> [ | //].
move: xnotinA.
apply: contra => visx.
by move/eqP: visx <-.
move: (subsets_weight AinBminusx) => wAleqwBminusx.
suff wBminusxleqwB: weight_set (B :\: ❴x❵) < weight_set B.
exact: leq_ltn_trans wAleqwBminusx wBminusxleqwB.
(* it is enough to prove weight_set (B - {x}) < weight_set B *)
rewrite /weight_set.
rewrite [in X in _ < X](eq_bigl (fun v => v ∈ ((B :\: ❴x❵) :|: ❴x❵))) ; last first.
move=> i ; by rewrite [in X in X = _](set_minus_union1 xinB).
rewrite sum_disjoint_union ; last exact: set_minus_disjoint.
rewrite sum_singleton.
rewrite -[in X in X < _](addn0 (Σ(v in G | v ∈ (B :\: ❴x❵)) weight v)).
rewrite ltn_add2l.
exact: positive_weights x.
Qed.
Definition maximum : Prop := p D /\ (forall F : {set G}, p F -> weight_set F <= weight_set D).
Definition minimum : Prop := p D /\ (forall F : {set G}, p F -> weight_set D <= weight_set F).
Proposition maximum_is_maximal : maximum -> maximal p D.
Proof.
rewrite /maximum /maximal => [ [pD Dmaximum] ].
split=> //.
move=> F DproperF pF.
move: (Dmaximum F pF) => wFleqwD.
move: (proper_sets_weight DproperF).
rewrite ltnNge => /negP nowFleqwD.
contradiction.
Qed.
Proposition minimum_is_minimal : minimum -> minimal p D.
Proof.
rewrite /minimum /minimal => [ [pD Dminimum] ].
split=> //.
move=> F FproperD pF.
move: (Dminimum F pF) => wDleqwF.
move: (proper_sets_weight FproperD).
rewrite ltnNge => /negP nowDleqwF.
contradiction.
Qed.
End Weighted_Sets.
(**********************************************************************************)
Section Argument_weighted_sets.
Variable weight : G -> nat.
Variable p : vsproperty.
Let pb := vsbool p.
Let pP := vsrefl p.
Let F := vsinhb p.
Let pF := vspinh p.
Let pbF : pb F.
Proof. exact/pP. Qed.
Definition maximum_set : {set G} := [arg max_(D > F | pb D) weight_set weight D].
Definition minimum_set : {set G} := [arg min_(D < F | pb D) weight_set weight D].
Lemma maximum_set_p : p maximum_set.
Proof. apply/pP ; rewrite /maximum_set ; by case: (arg_maxP (fun D => weight_set weight D) pbF). Qed.
Lemma minimum_set_p : p minimum_set.
Proof. apply/pP ; rewrite /minimum_set ; by case: (arg_minP (fun D => weight_set weight D) pbF). Qed.
Lemma maximum_set_welldefined : maximum weight p maximum_set.
Proof.
rewrite /maximum_set.
case: (arg_maxP (fun D => weight_set weight D) pbF).
move=> D pD H1.
rewrite /maximum.
split ; [ by apply/pP | ].
move=> D'.
move: (H1 D') => H2.
move/pP.
exact: H2.
Qed.
Lemma minimum_set_welldefined : minimum weight p minimum_set.
Proof.
rewrite /minimum_set.
case: (arg_minP (fun D => weight_set weight D) pbF).
move=> D pD H1.
rewrite /minimum.
split ; [ by apply/pP | ].
move=> D'.
move: (H1 D') => H2.
move/pP.
exact: H2.
Qed.
End Argument_weighted_sets.
(**********************************************************************************)
Section Weighted_domination_parameters.
Variable weight : G -> nat.
Hypothesis positive_weights : forall v : G, weight v > 0.
(* Sets of minimum/maximum weight *)
Let minimum_maximal_irr : {set G} := minimum_set weight max_irr.
Let minimum_dom : {set G} := minimum_set weight dominating.
Let minimum_st_dom : {set G} := minimum_set weight st_dom.
Let maximum_st : {set G} := maximum_set weight stable.
Let maximum_minimal_dom : {set G} := maximum_set weight min_dom.
Let maximum_irr : {set G} := maximum_set weight irredundant.
(* Definitions of parameters: basically, they measure the weight of the previous sets *)
Definition ir_w : nat := weight_set weight minimum_maximal_irr.
Definition gamma_w : nat := weight_set weight minimum_dom.
Definition ii_w : nat := weight_set weight minimum_st_dom.
Definition alpha_w : nat := weight_set weight maximum_st.
Definition Gamma_w : nat := weight_set weight maximum_minimal_dom.
Definition IR_w : nat := weight_set weight maximum_irr.
(* Weighted version of the Cockayne-Hedetniemi domination chain. *)
Theorem ir_w_leq_gamma_w : ir_w <= gamma_w.
Proof.
(* we generate "set_is_min" which says that any maximal irredundant F has weight >= ir(G) *)
move: (minimum_set_welldefined weight max_irr).
rewrite /minimum => [ [_ set_is_min] ].
(* we provides an F that is minimal dominating *)
set F := minimum_dom.
move: (minimum_set_welldefined weight dominating) => Fminimum_dom.
rewrite -/minimum_dom -/F in Fminimum_dom.
move: (minimum_is_minimal positive_weights Fminimum_dom) => Fminimal_dom.
(* and, therefore, F is maximal irredundant *)
move: (minimal_dom_is_maximal_irr Fminimal_dom) => Fmaximal_irr.
by move: (set_is_min F Fmaximal_irr).
Qed.
Theorem gamma_w_leq_ii_w : gamma_w <= ii_w.
Proof.
(* we generate "set_is_min" which says that any dominating set F has weight >= gamma_w(G) *)
move: (minimum_set_welldefined weight dominating).
rewrite /minimum => [ [_ set_is_min] ].
(* we provides a dominating F (not matter if F is stable too) *)
set F := minimum_st_dom.
move: (minimum_set_p weight st_dom).
rewrite -/minimum_st_dom -/F /p_st_dom.
move=> [_ Fdom].
by move: (set_is_min F Fdom).
Qed.
Theorem ii_w_leq_alpha_w : ii_w <= alpha_w.
Proof.
(* we generate "set_is_max" which says that any stable set F has weight <= alpha_w(G) *)
move: (maximum_set_welldefined weight stable).
rewrite /maximum => [ [_ set_is_max] ].
(* we provides a stable F (not matter if F is dominating too) *)
set F := minimum_st_dom.
move: (minimum_set_p weight st_dom).
rewrite -/minimum_st_dom -/F /p_st_dom.
move=> [Fst _].
by move: (set_is_max F Fst).
Qed.
Theorem alpha_w_leq_Gamma_w : alpha_w <= Gamma_w.
Proof.
(* we generate "set_is_max" which says that any minimal dom. set F has weight <= Gamma_w(G) *)
move: (maximum_set_welldefined weight min_dom).
rewrite /maximum => [ [_ set_is_max] ].
(* we provides an F that F maximal stable ... *)
set F := maximum_st.
move: (maximum_set_welldefined weight stable) => Fmaximum_st.
rewrite -/maximum_st -/F in Fmaximum_st.
move: (maximum_is_maximal positive_weights Fmaximum_st) => Fmaximal_st.
(* and, therefore, F is minimal dominating *)
move: (maximal_st_is_minimal_dom Fmaximal_st) => Fminimal_dom.
by move: (set_is_max F Fminimal_dom).
Qed.
Theorem Gamma_w_leq_IR_w : Gamma_w <= IR_w.
Proof.
(* we generate "set_is_max" which says that any irredundant F has weight <= IR_w(G) *)
move: (maximum_set_welldefined weight irredundant).
rewrite /maximum => [ [_ set_is_max] ].
(* we provides an F that is maximal irredundant *)
set F := maximum_minimal_dom.
move: (maximum_set_p weight min_dom).
rewrite -/maximum_minimal_dom -/F /p_min_dom.
move=> Fminimal_dom.
move: (minimal_dom_is_maximal_irr Fminimal_dom).
(* in particular, it only matters if F is irredundant *)
rewrite /maximal.
move=> [Firr _].
by move: (set_is_max F Firr).
Qed.
End Weighted_domination_parameters.
Arguments ir_w : clear implicits.
Arguments gamma_w : clear implicits.
Arguments ii_w : clear implicits.
Arguments alpha_w : clear implicits.
Arguments Gamma_w : clear implicits.
Arguments IR_w : clear implicits.
(**********************************************************************************)
Variable weight : G -> nat.
Hypothesis positive_weights : forall v : G, weight v > 0.
Variable p : vsproperty.
Variable D : {set G}.
Definition weight_set : {set G} -> nat := fun S => Σ(v in G | v ∈ S) weight v.
Lemma weight_set_natural : forall A : {set G}, weight_set A >= 0.
Proof. move=> A ; exact: leq0n. Qed.
Lemma empty_set_zero_weight : D = ∅ <-> weight_set D = 0.
Proof.
rewrite /iff ; split.
(* first case: -> *)
move=> Dempty.
rewrite /weight_set.
move: Dempty ->.
exact: sum_empty.
(* second case: <- *)
move=> /eqP weightzero.
apply/eqP.
move: weightzero.
apply: contraLR => /set0Pn.
elim=> x xinD.
rewrite /weight_set.
rewrite (eq_bigl (fun v => v ∈ ((D :\: ❴x❵) :|: ❴x❵))) ; last first.
move=> i ; by rewrite [in X in X = _](set_minus_union1 xinD).
rewrite lt0n_neq0 //.
(* now, we need to prove that the summation over (D - {x}) cup {x} is positive *)
rewrite sum_disjoint_union ; last by rewrite set_minus_disjoint.
rewrite sum_singleton addnC ltn_addr => [// | ].
exact: positive_weights x.
Qed.
Lemma subsets_weight : forall A B : {set G}, A ⊆ B -> weight_set A <= weight_set B.
Proof.
move=> A B AsubB.
rewrite /weight_set.
rewrite [in X in _ <= X](eq_bigl (fun v => v ∈ ((B :\: A) :|: A))) ; last first.
move=> i ; by rewrite [in X in X = _](set_minus_union AsubB).
rewrite (sum_disjoint_union weight (set_minus_disjoint B A)).
exact: leq_addl.
Qed.
Lemma proper_sets_weight : forall A B : {set G}, A ⊂ B -> weight_set A < weight_set B.
Proof.
move=> A B /properP [AsubB].
elim=> x xinB xnotinA.
(* we prove that indeed A ⊆ B - {x} *)
have AinBminusx: A ⊆ B :\: ❴x❵.
apply/subsetP => v vinA.
move: (subsetP AsubB v vinA) => vinB.
apply/setD1P.
split=> [ | //].
move: xnotinA.
apply: contra => visx.
by move/eqP: visx <-.
move: (subsets_weight AinBminusx) => wAleqwBminusx.
suff wBminusxleqwB: weight_set (B :\: ❴x❵) < weight_set B.
exact: leq_ltn_trans wAleqwBminusx wBminusxleqwB.
(* it is enough to prove weight_set (B - {x}) < weight_set B *)
rewrite /weight_set.
rewrite [in X in _ < X](eq_bigl (fun v => v ∈ ((B :\: ❴x❵) :|: ❴x❵))) ; last first.
move=> i ; by rewrite [in X in X = _](set_minus_union1 xinB).
rewrite sum_disjoint_union ; last exact: set_minus_disjoint.
rewrite sum_singleton.
rewrite -[in X in X < _](addn0 (Σ(v in G | v ∈ (B :\: ❴x❵)) weight v)).
rewrite ltn_add2l.
exact: positive_weights x.
Qed.
Definition maximum : Prop := p D /\ (forall F : {set G}, p F -> weight_set F <= weight_set D).
Definition minimum : Prop := p D /\ (forall F : {set G}, p F -> weight_set D <= weight_set F).
Proposition maximum_is_maximal : maximum -> maximal p D.
Proof.
rewrite /maximum /maximal => [ [pD Dmaximum] ].
split=> //.
move=> F DproperF pF.
move: (Dmaximum F pF) => wFleqwD.
move: (proper_sets_weight DproperF).
rewrite ltnNge => /negP nowFleqwD.
contradiction.
Qed.
Proposition minimum_is_minimal : minimum -> minimal p D.
Proof.
rewrite /minimum /minimal => [ [pD Dminimum] ].
split=> //.
move=> F FproperD pF.
move: (Dminimum F pF) => wDleqwF.
move: (proper_sets_weight FproperD).
rewrite ltnNge => /negP nowDleqwF.
contradiction.
Qed.
End Weighted_Sets.
(**********************************************************************************)
Section Argument_weighted_sets.
Variable weight : G -> nat.
Variable p : vsproperty.
Let pb := vsbool p.
Let pP := vsrefl p.
Let F := vsinhb p.
Let pF := vspinh p.
Let pbF : pb F.
Proof. exact/pP. Qed.
Definition maximum_set : {set G} := [arg max_(D > F | pb D) weight_set weight D].
Definition minimum_set : {set G} := [arg min_(D < F | pb D) weight_set weight D].
Lemma maximum_set_p : p maximum_set.
Proof. apply/pP ; rewrite /maximum_set ; by case: (arg_maxP (fun D => weight_set weight D) pbF). Qed.
Lemma minimum_set_p : p minimum_set.
Proof. apply/pP ; rewrite /minimum_set ; by case: (arg_minP (fun D => weight_set weight D) pbF). Qed.
Lemma maximum_set_welldefined : maximum weight p maximum_set.
Proof.
rewrite /maximum_set.
case: (arg_maxP (fun D => weight_set weight D) pbF).
move=> D pD H1.
rewrite /maximum.
split ; [ by apply/pP | ].
move=> D'.
move: (H1 D') => H2.
move/pP.
exact: H2.
Qed.
Lemma minimum_set_welldefined : minimum weight p minimum_set.
Proof.
rewrite /minimum_set.
case: (arg_minP (fun D => weight_set weight D) pbF).
move=> D pD H1.
rewrite /minimum.
split ; [ by apply/pP | ].
move=> D'.
move: (H1 D') => H2.
move/pP.
exact: H2.
Qed.
End Argument_weighted_sets.
(**********************************************************************************)
Section Weighted_domination_parameters.
Variable weight : G -> nat.
Hypothesis positive_weights : forall v : G, weight v > 0.
(* Sets of minimum/maximum weight *)
Let minimum_maximal_irr : {set G} := minimum_set weight max_irr.
Let minimum_dom : {set G} := minimum_set weight dominating.
Let minimum_st_dom : {set G} := minimum_set weight st_dom.
Let maximum_st : {set G} := maximum_set weight stable.
Let maximum_minimal_dom : {set G} := maximum_set weight min_dom.
Let maximum_irr : {set G} := maximum_set weight irredundant.
(* Definitions of parameters: basically, they measure the weight of the previous sets *)
Definition ir_w : nat := weight_set weight minimum_maximal_irr.
Definition gamma_w : nat := weight_set weight minimum_dom.
Definition ii_w : nat := weight_set weight minimum_st_dom.
Definition alpha_w : nat := weight_set weight maximum_st.
Definition Gamma_w : nat := weight_set weight maximum_minimal_dom.
Definition IR_w : nat := weight_set weight maximum_irr.
(* Weighted version of the Cockayne-Hedetniemi domination chain. *)
Theorem ir_w_leq_gamma_w : ir_w <= gamma_w.
Proof.
(* we generate "set_is_min" which says that any maximal irredundant F has weight >= ir(G) *)
move: (minimum_set_welldefined weight max_irr).
rewrite /minimum => [ [_ set_is_min] ].
(* we provides an F that is minimal dominating *)
set F := minimum_dom.
move: (minimum_set_welldefined weight dominating) => Fminimum_dom.
rewrite -/minimum_dom -/F in Fminimum_dom.
move: (minimum_is_minimal positive_weights Fminimum_dom) => Fminimal_dom.
(* and, therefore, F is maximal irredundant *)
move: (minimal_dom_is_maximal_irr Fminimal_dom) => Fmaximal_irr.
by move: (set_is_min F Fmaximal_irr).
Qed.
Theorem gamma_w_leq_ii_w : gamma_w <= ii_w.
Proof.
(* we generate "set_is_min" which says that any dominating set F has weight >= gamma_w(G) *)
move: (minimum_set_welldefined weight dominating).
rewrite /minimum => [ [_ set_is_min] ].
(* we provides a dominating F (not matter if F is stable too) *)
set F := minimum_st_dom.
move: (minimum_set_p weight st_dom).
rewrite -/minimum_st_dom -/F /p_st_dom.
move=> [_ Fdom].
by move: (set_is_min F Fdom).
Qed.
Theorem ii_w_leq_alpha_w : ii_w <= alpha_w.
Proof.
(* we generate "set_is_max" which says that any stable set F has weight <= alpha_w(G) *)
move: (maximum_set_welldefined weight stable).
rewrite /maximum => [ [_ set_is_max] ].
(* we provides a stable F (not matter if F is dominating too) *)
set F := minimum_st_dom.
move: (minimum_set_p weight st_dom).
rewrite -/minimum_st_dom -/F /p_st_dom.
move=> [Fst _].
by move: (set_is_max F Fst).
Qed.
Theorem alpha_w_leq_Gamma_w : alpha_w <= Gamma_w.
Proof.
(* we generate "set_is_max" which says that any minimal dom. set F has weight <= Gamma_w(G) *)
move: (maximum_set_welldefined weight min_dom).
rewrite /maximum => [ [_ set_is_max] ].
(* we provides an F that F maximal stable ... *)
set F := maximum_st.
move: (maximum_set_welldefined weight stable) => Fmaximum_st.
rewrite -/maximum_st -/F in Fmaximum_st.
move: (maximum_is_maximal positive_weights Fmaximum_st) => Fmaximal_st.
(* and, therefore, F is minimal dominating *)
move: (maximal_st_is_minimal_dom Fmaximal_st) => Fminimal_dom.
by move: (set_is_max F Fminimal_dom).
Qed.
Theorem Gamma_w_leq_IR_w : Gamma_w <= IR_w.
Proof.
(* we generate "set_is_max" which says that any irredundant F has weight <= IR_w(G) *)
move: (maximum_set_welldefined weight irredundant).
rewrite /maximum => [ [_ set_is_max] ].
(* we provides an F that is maximal irredundant *)
set F := maximum_minimal_dom.
move: (maximum_set_p weight min_dom).
rewrite -/maximum_minimal_dom -/F /p_min_dom.
move=> Fminimal_dom.
move: (minimal_dom_is_maximal_irr Fminimal_dom).
(* in particular, it only matters if F is irredundant *)
rewrite /maximal.
move=> [Firr _].
by move: (set_is_max F Firr).
Qed.
End Weighted_domination_parameters.
Arguments ir_w : clear implicits.
Arguments gamma_w : clear implicits.
Arguments ii_w : clear implicits.
Arguments alpha_w : clear implicits.
Arguments Gamma_w : clear implicits.
Arguments IR_w : clear implicits.
(**********************************************************************************)
Section Unweighted_Sets.
Variable p : vsproperty.
Variable D : {set G}.
Definition ones : (G -> nat) := (fun _ => 1).
Definition maximum_card : Prop := p D /\ (forall F : {set G}, p F -> #|F| <= #|D|).
Definition minimum_card : Prop := p D /\ (forall F : {set G}, p F -> #|D| <= #|F|).
Lemma card_weight_1 : forall S : {set G}, #|S| = weight_set ones S.
Proof. move=> S ; by rewrite /weight_set /ones sum1_card. Qed.
Lemma maximum1 : maximum_card <-> maximum ones p D.
Proof.
rewrite /maximum /maximum_card /iff.
split=> [ [pD H1] | [pD H2 ] ].
split=> [ // | F pF ] ; rewrite -!card_weight_1 ; exact: H1.
split=> [ // | F pF ] ; rewrite !card_weight_1 ; exact: H2.
Qed.
Lemma minimum1 : minimum_card <-> minimum ones p D.
Proof.
rewrite /minimum /minimum_card /iff.
split=> [ [pD H1] | [pD H2 ] ].
split=> [ // | F pF ] ; rewrite -!card_weight_1 ; exact: H1.
split=> [ // | F pF ] ; rewrite !card_weight_1 ; exact: H2.
Qed.
Proposition maximum_card_is_maximal : maximum_card -> maximal p D.
Proof. rewrite maximum1 ; exact: maximum_is_maximal. Qed.
Proposition minimum_card_is_minimal : minimum_card -> minimal p D.
Proof. rewrite minimum1 ; exact: minimum_is_minimal. Qed.
End Unweighted_Sets.
Arguments ones : clear implicits.
(**********************************************************************************)
Section Argument_unweighted_sets.
Variable p : vsproperty.
Let pb := vsbool p.
Let pP := vsrefl p.
Let F := vsinhb p.
Let pF := vspinh p.
Let pbF : pb F.
Proof. exact/pP. Qed.
Definition maximum_set_card : {set G} := [arg max_(D > F | pb D) #|D|].
Definition minimum_set_card : {set G} := [arg min_(D < F | pb D) #|D|].
Lemma max_card_weight_1 : #|maximum_set_card| = #|maximum_set ones p|.
Proof.
rewrite /maximum_set_card.
case: (arg_maxP (fun D : {set G} => #|D|) pbF).
move=> D1 pbD1 H1.
rewrite /maximum_set.
case: (arg_maxP (fun D => weight_set ones D) pbF).
move=> D2 pbD2 H2.
apply/eqP ; rewrite eqn_leq ; apply/andP ; split.
move: (H2 D1 pbD1).
by rewrite -!card_weight_1.
exact: H1 D2 pbD2.
Qed.
Lemma min_card_weight_1 : #|minimum_set_card| = #|minimum_set ones p|.
Proof.
rewrite /minimum_set_card.
case: (arg_minP (fun D : {set G} => #|D|) pbF).
move=> D1 pbD1 H1.
rewrite /minimum_set.
case: (arg_minP (fun D => weight_set ones D) pbF).
move=> D2 pbD2 H2.
apply/eqP ; rewrite eqn_leq ; apply/andP ; split.
exact: H1 D2 pbD2.
move: (H2 D1 pbD1).
by rewrite -!card_weight_1.
Qed.
End Argument_unweighted_sets.
(**********************************************************************************)
Section Classic_domination_parameters.
(* Sets of minimum/maximum cardinal *)
Let minimum_maximal_irr : {set G} := minimum_set_card max_irr.
Let minimum_dom : {set G} := minimum_set_card dominating.
Let minimum_st_dom : {set G} := minimum_set_card st_dom.
Let maximum_st : {set G} := maximum_set_card stable.
Let maximum_minimal_dom : {set G} := maximum_set_card min_dom.
Let maximum_irr : {set G} := maximum_set_card irredundant.
(* Definitions of classic parameters *)
Definition ir : nat := #|minimum_maximal_irr|.
Definition gamma : nat := #|minimum_dom|.
Definition ii : nat := #|minimum_st_dom|.
Definition alpha : nat := #|maximum_st|.
Definition Gamma : nat := #|maximum_minimal_dom|.
Definition IR : nat := #|maximum_irr|.
(* Conversion between classic and weighted parameters *)
Lemma ir_is_ir1 : ir = ir_w ones.
Proof.
rewrite /ir /ir_w /minimum_maximal_irr (min_card_weight_1 max_irr).
exact: card_weight_1.
Qed.
Lemma gamma_is_gamma1 : gamma = gamma_w ones.
Proof.
rewrite /gamma /gamma_w /minimum_dom (min_card_weight_1 dominating).
exact: card_weight_1.
Qed.
Lemma ii_is_ii1 : ii = ii_w ones.
Proof.
rewrite /ii /ii_w /minimum_st_dom (min_card_weight_1 st_dom).
exact: card_weight_1.
Qed.
Lemma alpha_is_alpha1 : alpha = alpha_w ones.
Proof.
rewrite /alpha /alpha_w /maximum_st (max_card_weight_1 stable).
exact: card_weight_1.
Qed.
Lemma Gamma_is_Gamma1 : Gamma = Gamma_w ones.
Proof.
rewrite /Gamma /Gamma_w /maximum_minimal_dom (max_card_weight_1 min_dom).
exact: card_weight_1.
Qed.
Lemma IR_is_IR1 : IR = IR_w ones.
Proof.
rewrite /IR /IR_w /maximum_irr (max_card_weight_1 irredundant).
exact: card_weight_1.
Qed.
(* Classic Cockayne-Hedetniemi domination chain. *)
Corollary ir_leq_gamma : ir <= gamma.
Proof. by rewrite ir_is_ir1 gamma_is_gamma1 ir_w_leq_gamma_w. Qed.
Corollary gamma_leq_ii : gamma <= ii.
Proof. by rewrite gamma_is_gamma1 ii_is_ii1 gamma_w_leq_ii_w. Qed.
Corollary ii_leq_alpha : ii <= alpha.
Proof. by rewrite ii_is_ii1 alpha_is_alpha1 ii_w_leq_alpha_w. Qed.
Corollary alpha_leq_Gamma : alpha <= Gamma.
Proof. by rewrite alpha_is_alpha1 Gamma_is_Gamma1 alpha_w_leq_Gamma_w. Qed.
Corollary Gamma_leq_IR : Gamma <= IR.
Proof. by rewrite Gamma_is_Gamma1 IR_is_IR1 Gamma_w_leq_IR_w. Qed.
End Classic_domination_parameters.
End Domination_Theory.
(* Clear implicit arguments for modules used by dom.v *)
Global Arguments private_set : clear implicits.
Global Arguments private : clear implicits.
Global Arguments privateb : clear implicits.
Global Arguments privateP : clear implicits.
Global Arguments ir_w : clear implicits.
Global Arguments gamma_w : clear implicits.
Global Arguments ii_w : clear implicits.
Global Arguments alpha_w : clear implicits.
Global Arguments Gamma_w : clear implicits.
Global Arguments IR_w : clear implicits.
Global Arguments ones : clear implicits.
Global Arguments ir : clear implicits.
Global Arguments gamma : clear implicits.
Global Arguments ii : clear implicits.
Global Arguments alpha : clear implicits.
Global Arguments Gamma : clear implicits.
Global Arguments IR : clear implicits.
Variable p : vsproperty.
Variable D : {set G}.
Definition ones : (G -> nat) := (fun _ => 1).
Definition maximum_card : Prop := p D /\ (forall F : {set G}, p F -> #|F| <= #|D|).
Definition minimum_card : Prop := p D /\ (forall F : {set G}, p F -> #|D| <= #|F|).
Lemma card_weight_1 : forall S : {set G}, #|S| = weight_set ones S.
Proof. move=> S ; by rewrite /weight_set /ones sum1_card. Qed.
Lemma maximum1 : maximum_card <-> maximum ones p D.
Proof.
rewrite /maximum /maximum_card /iff.
split=> [ [pD H1] | [pD H2 ] ].
split=> [ // | F pF ] ; rewrite -!card_weight_1 ; exact: H1.
split=> [ // | F pF ] ; rewrite !card_weight_1 ; exact: H2.
Qed.
Lemma minimum1 : minimum_card <-> minimum ones p D.
Proof.
rewrite /minimum /minimum_card /iff.
split=> [ [pD H1] | [pD H2 ] ].
split=> [ // | F pF ] ; rewrite -!card_weight_1 ; exact: H1.
split=> [ // | F pF ] ; rewrite !card_weight_1 ; exact: H2.
Qed.
Proposition maximum_card_is_maximal : maximum_card -> maximal p D.
Proof. rewrite maximum1 ; exact: maximum_is_maximal. Qed.
Proposition minimum_card_is_minimal : minimum_card -> minimal p D.
Proof. rewrite minimum1 ; exact: minimum_is_minimal. Qed.
End Unweighted_Sets.
Arguments ones : clear implicits.
(**********************************************************************************)
Section Argument_unweighted_sets.
Variable p : vsproperty.
Let pb := vsbool p.
Let pP := vsrefl p.
Let F := vsinhb p.
Let pF := vspinh p.
Let pbF : pb F.
Proof. exact/pP. Qed.
Definition maximum_set_card : {set G} := [arg max_(D > F | pb D) #|D|].
Definition minimum_set_card : {set G} := [arg min_(D < F | pb D) #|D|].
Lemma max_card_weight_1 : #|maximum_set_card| = #|maximum_set ones p|.
Proof.
rewrite /maximum_set_card.
case: (arg_maxP (fun D : {set G} => #|D|) pbF).
move=> D1 pbD1 H1.
rewrite /maximum_set.
case: (arg_maxP (fun D => weight_set ones D) pbF).
move=> D2 pbD2 H2.
apply/eqP ; rewrite eqn_leq ; apply/andP ; split.
move: (H2 D1 pbD1).
by rewrite -!card_weight_1.
exact: H1 D2 pbD2.
Qed.
Lemma min_card_weight_1 : #|minimum_set_card| = #|minimum_set ones p|.
Proof.
rewrite /minimum_set_card.
case: (arg_minP (fun D : {set G} => #|D|) pbF).
move=> D1 pbD1 H1.
rewrite /minimum_set.
case: (arg_minP (fun D => weight_set ones D) pbF).
move=> D2 pbD2 H2.
apply/eqP ; rewrite eqn_leq ; apply/andP ; split.
exact: H1 D2 pbD2.
move: (H2 D1 pbD1).
by rewrite -!card_weight_1.
Qed.
End Argument_unweighted_sets.
(**********************************************************************************)
Section Classic_domination_parameters.
(* Sets of minimum/maximum cardinal *)
Let minimum_maximal_irr : {set G} := minimum_set_card max_irr.
Let minimum_dom : {set G} := minimum_set_card dominating.
Let minimum_st_dom : {set G} := minimum_set_card st_dom.
Let maximum_st : {set G} := maximum_set_card stable.
Let maximum_minimal_dom : {set G} := maximum_set_card min_dom.
Let maximum_irr : {set G} := maximum_set_card irredundant.
(* Definitions of classic parameters *)
Definition ir : nat := #|minimum_maximal_irr|.
Definition gamma : nat := #|minimum_dom|.
Definition ii : nat := #|minimum_st_dom|.
Definition alpha : nat := #|maximum_st|.
Definition Gamma : nat := #|maximum_minimal_dom|.
Definition IR : nat := #|maximum_irr|.
(* Conversion between classic and weighted parameters *)
Lemma ir_is_ir1 : ir = ir_w ones.
Proof.
rewrite /ir /ir_w /minimum_maximal_irr (min_card_weight_1 max_irr).
exact: card_weight_1.
Qed.
Lemma gamma_is_gamma1 : gamma = gamma_w ones.
Proof.
rewrite /gamma /gamma_w /minimum_dom (min_card_weight_1 dominating).
exact: card_weight_1.
Qed.
Lemma ii_is_ii1 : ii = ii_w ones.
Proof.
rewrite /ii /ii_w /minimum_st_dom (min_card_weight_1 st_dom).
exact: card_weight_1.
Qed.
Lemma alpha_is_alpha1 : alpha = alpha_w ones.
Proof.
rewrite /alpha /alpha_w /maximum_st (max_card_weight_1 stable).
exact: card_weight_1.
Qed.
Lemma Gamma_is_Gamma1 : Gamma = Gamma_w ones.
Proof.
rewrite /Gamma /Gamma_w /maximum_minimal_dom (max_card_weight_1 min_dom).
exact: card_weight_1.
Qed.
Lemma IR_is_IR1 : IR = IR_w ones.
Proof.
rewrite /IR /IR_w /maximum_irr (max_card_weight_1 irredundant).
exact: card_weight_1.
Qed.
(* Classic Cockayne-Hedetniemi domination chain. *)
Corollary ir_leq_gamma : ir <= gamma.
Proof. by rewrite ir_is_ir1 gamma_is_gamma1 ir_w_leq_gamma_w. Qed.
Corollary gamma_leq_ii : gamma <= ii.
Proof. by rewrite gamma_is_gamma1 ii_is_ii1 gamma_w_leq_ii_w. Qed.
Corollary ii_leq_alpha : ii <= alpha.
Proof. by rewrite ii_is_ii1 alpha_is_alpha1 ii_w_leq_alpha_w. Qed.
Corollary alpha_leq_Gamma : alpha <= Gamma.
Proof. by rewrite alpha_is_alpha1 Gamma_is_Gamma1 alpha_w_leq_Gamma_w. Qed.
Corollary Gamma_leq_IR : Gamma <= IR.
Proof. by rewrite Gamma_is_Gamma1 IR_is_IR1 Gamma_w_leq_IR_w. Qed.
End Classic_domination_parameters.
End Domination_Theory.
(* Clear implicit arguments for modules used by dom.v *)
Global Arguments private_set : clear implicits.
Global Arguments private : clear implicits.
Global Arguments privateb : clear implicits.
Global Arguments privateP : clear implicits.
Global Arguments ir_w : clear implicits.
Global Arguments gamma_w : clear implicits.
Global Arguments ii_w : clear implicits.
Global Arguments alpha_w : clear implicits.
Global Arguments Gamma_w : clear implicits.
Global Arguments IR_w : clear implicits.
Global Arguments ones : clear implicits.
Global Arguments ir : clear implicits.
Global Arguments gamma : clear implicits.
Global Arguments ii : clear implicits.
Global Arguments alpha : clear implicits.
Global Arguments Gamma : clear implicits.
Global Arguments IR : clear implicits.