Coq Library
Tools
PADEC - Coq Library

#### Global Imports

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

#### Local Imports

From Padec Require Import NatUtils.
From Padec Require Import OptionUtil.
From Padec Require Import SetoidUtil.
From Padec Require Import Count.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Tree_topology.
From Padec Require Import KDomSet_algo_tree_topology.

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.

Channel and Network definitions
Context {Chans: Channels}
{Net: Network}
{DTN: Down_Tree_Network Net}
{KDP: KDomSet_parameters}.
Let k_pos := k_pos.

Notation Tree := (DTN_topo (Net := Net)).
Context {SPAN: is_spanning _ Tree}.

Notation Algo := KDom_algo.
Notation Env := (Env (Net := Net) (Algo := KDom_algo)).

Assumptions on Inputs
Variable (env: Env) (env_compat: Proper pequiv env)
(hassume: Assume env)
(final: terminal env).

Two kinds:
• the regular one (with alpha equals k)
• (maybe) the root
Notation kDominator := (kDominator env).
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 (env p) = k.

Definition RegDomHeads := { n: Node | RegDomHead n }.

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 (env n) >= k -> HasTallAncestor n
| HTA_parent:
forall m n, isParent 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 (env h) = k -> RegHeadAncestor n h
| RHA_parent:
forall m n h, isParent m n -> alpha (env n) <> k ->
RegHeadAncestor m h -> RegHeadAncestor n h.

Section with_cardinals.

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

Variable (card_DH: nat)
(Hcard_DH: Num_Card Same DomHeads card_DH).

Variable (card_RDH: nat)
(Hcard_RDH: Num_Card Same RegDomHeads card_RDH).

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 (env (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:
forall x: Node,
(( 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 :
forall x: Node,
(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) :
forall x: Node,
(card_N - 1 >= (Datatypes.S (Z.to_nat k)) * (card_DH - 1))%nat.

Theorem counting_theorem_non_empty:
forall x: Node,
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.

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.