Coq Library
Tools

#### Global Imports

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

#### Local Imports

Open Scope Z_scope.
Set Implicit Arguments.

# How Many Elements in the cluster? Count the number of elements

in the cluster (cluster heads) built by the algorithm.
We prove bounds on it.
Section KClustering_count.

Channel interface definitions
Context {Chans: Channels} {Net: Symmetric_Network}
{KCP: KClustering_parameters} {KCT: KC_algo_tools}.

Notation Env := (Env (Algo := KC_algo)).

Let k_pos := k_pos.

Assumptions on Inputs
Variable (g: Env) (pg: Proper pequiv g).

Variable (root: Node)
(span_tree: spanning_tree root (Par_part g))
(sym: Symmetric_Network_assumption
Net (fun n => KCpeers (g n)) (fun n => KCreverse (g n))).

Variable (final_alpha:
forall (n: Node), alpha_enabled_bb g n = false).

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

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

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 (g n)) >= k -> HasTallAncestor n
| HTA_parent:
forall m n, is_tree_parent_of (Par_part g) m n ->
HasTallAncestor m -> HasTallAncestor n.

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

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 (g h)) = k -> RegHeadAncestor n h
| RHA_parent:
forall m n h, is_tree_parent_of (Par_part g) m n -> (alpha (g 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 (g (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 /\