PADEC
Coq Library
Tools
PADEC - Coq Library

Library Padec.KClustering.KClustering_count

A Framework for Certified Self-Stabilization
PADEC Coq Library

Global Imports

From Coq Require Import ZArith.
From Coq Require Import Lia.
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 Spanning_Tree.
From Padec Require Import KClustering_specification.
From Padec Require Import KClustering_algo.
From Padec Require Import KClustering_def_termination.
From Padec Require Import KClustering_correctness_alpha.

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}.

  Existing Instance KC_Stable.
  Existing Instance OrdChans.

  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).

Dominating Heads

Two kinds:
  Definition DomHeads := { n: Node | kDominator g n = true }.

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

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

  Instance RegDomHead_compat: Proper fequiv RegDomHead.

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 ->
                    RegHeadAncestor m h -> RegHeadAncestor n h.

  Instance RegHeadAncestor_compat:
    Proper fequiv RegHeadAncestor.

  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 (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: if root is short:
    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 KClustering_count.

Close Scope Z_scope.
Unset Implicit Arguments.