Coq Library
Tools

#### Global Imports

From Coq Require Import Omega.
From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import RelationPairs.

#### Local Imports

Open Scope Z_scope.
Open Scope signature_scope.
Set Implicit Arguments.

# How Many Elements in the k-Hop-Dominating Set? Count the number

of elements in the dominating set (dominating heads) built by the algorithm.
We prove bounds on it.
Section KDomSet_count.

Context {Chans: Channels} {Net: Symmetric_Network}.
Context {KDP: KDomSet_parameters}.
Let k_pos := k_pos.

Assumptions on Inputs
Variable (Par: Node -> option Channel)
(Par_compat: Proper fequiv Par)
(alpha: Node -> Z)
(alpha_compat: Proper fequiv alpha).

Variable (root: Node)
(span_tree: spanning_tree root Par).

Variable (final: forall (n: Node), ~enabled_alpha Par alpha n).

Two kinds:
• the regular one (with alpha equals k)
• (maybe) the root
Notation kDominator := (kDominator Par alpha).
Definition DomHeads := { n: Node | kDominator n = true }.

Notation eqDH := (equiv (A := DomHeads)).

Regular Dominating Heads are nodes such that alpha = k
Definition RegDomHead p := (alpha p) = k.

Notation eqRDH := (equiv (A := RegDomHeads)).

Regular Nodes are those below a tall node: They cannot be in the dominating set of the short root (if short)

Inductive HasTallAncestor: Node -> Prop :=
| HTA_self: forall n, (alpha n) >= k -> HasTallAncestor n
| HTA_parent:
forall m n, is_tree_parent_of Par m n ->
HasTallAncestor m -> HasTallAncestor n.

Definition RegNode := { n: Node | HasTallAncestor n }.

Notation eqRN := (equiv (A := RegNode)).

Global Instance HasTallAncestor_compat: Proper fequiv HasTallAncestor.

Relation between a node and its closest ancestor s.t. alpha=k
Inductive RegHeadAncestor: Node -> Node -> Prop :=
| RHA_self: forall n h, n == h -> alpha h = k -> RegHeadAncestor n h
| RHA_parent:
forall m n h, is_tree_parent_of Par m n -> alpha n <> k ->

Section with_cardinals.

Variable (card_N: nat)
(Hcard_N: Num_Card Same Node card_N).

Variable (card_DH: nat)

Variable (card_RDH: nat)

Variable (card_RN: nat)
(Hcard_RN: Num_Card Same RegNode card_RN).

Rcount is an existence witness for a the cardinality result
Definition Rcount
(cpl: ltN (Datatypes.S (Z.to_nat k)) * RegDomHeads)
(rn: RegNode): Prop :=
Z.to_nat (alpha (proj1_sig rn)) = proj1_sig (fst cpl) /\
RegHeadAncestor (proj1_sig rn) (proj1_sig (snd cpl)).

count_ok every small index is present in every dominating set
Theorem simple_counting:
(card_RN >= (Datatypes.S (Z.to_nat k)) * card_RDH)%nat.

split_counting_cases if root is tall:
• all dominating heads are regular
• all nodes are regular (have a tall ancestor)
if root is short:
• all dominating heads are regular except the root
• at least one node is singular (namely the root)
Lemma split_counting_cases:
(( card_DH=card_RDH /\ card_N = card_RN ) \/
( card_DH = Datatypes.S card_RDH /\ card_N >= Datatypes.S card_RN))%nat.

Theorem counting_theorem_assuming_cardinals_exist :
(card_N - 1 >= (Datatypes.S (Z.to_nat k)) * (card_DH - 1))%nat.

End with_cardinals.

Theorem counting_theorem_
(card_N: nat)
(Hcard_N: Num_Card Same Node card_N)
(card_DH: nat)
(Hcard_DH: Num_Card Same DomHeads card_DH) :
(card_N - 1 >= (Datatypes.S (Z.to_nat k)) * (card_DH - 1))%nat.

Theorem counting_theorem:
exists (card_N: nat) (card_DH: nat),
Num_Card Same Node card_N /\ Num_Card Same DomHeads card_DH /\
(card_N - 1 >= (Datatypes.S (Z.to_nat k)) * (card_DH - 1))%nat.

End KDomSet_count.

Close Scope Z_scope.
Close Scope signature_scope.
Unset Implicit Arguments.