Coq Library
Tools

Global imports
From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import ZArith.
From Coq Require Import Bool.

Local imports

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

# Correctness of the K-Dominating Set algorithm

Once a terminal configuration is reached, we prove that the variables draw a k-dominating set
Section KDomSet_Correctness.

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

Notation alphas_ :=
(fun (env: Env) n => alphas (children_states (env n) (local_env env n))).

Notation new_alpha_ := (fun env n => new_alpha (alphas_ env n)).

## Correctness

Section Final_kDomSet.

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

Variable (final: forall (n: Node), enabled_b env n = false).

Lemma same: forall (n: Node), alpha (env n) = new_alpha_ env n.

Definition is_kDom_path := chain (is_kDom_edge env).

Lemma tall_has_path_to_root:
forall (n: Node) (i: nat),
alpha (env n) = k + Z_of_nat i ->
exists (r: Node),
kDominator env r = true /\
exists (p: list Node), (is_kDom_path r p n).

forall (n: Node) (i: nat),
alpha (env n) = k + Z_of_nat i ->
(exists (r: Node),
kDominator env r = true /\
exists (p: list Node), (is_kDom_path r p n)).

Lemma tall_is_kDominated:
forall (n: Node) (i: nat),
alpha (env n) = k + Z_of_nat i ->
forall r p, is_kDom_path r p n -> (length p <= i)%nat.

Lemma tall_k:
forall (n: Node),
_IsTall (alpha (env n)) = true ->
exists (i: nat), alpha (env n) = k + Z.of_nat i.

Lemma short_k:
forall (n: Node),
_IsShort (alpha (env n)) = true ->
exists (i: nat), (Z.of_nat i < k)%Z /\
alpha (env n) = k - 1 - Z.of_nat i.

Lemma alpha_monotonic_small:
forall (n m: Node),
isParent m n ->
_IsShort (alpha (env n)) = true ->
alpha (env m) >= alpha (env n) + 1.

forall (i: nat) (n: Node),
alpha (env n) = k - Z.of_nat i ->
(exists (r: Node),
kDominator env r = true /\
exists (p: list Node), (is_kDom_path r p n)).

Lemma short_is_kDominated:
forall (i: nat) (n: Node),
alpha (env n) = k - Z.of_nat i ->
forall r p, is_kDom_path r p n -> (length p <= i)%nat.

forall (n: Node), exists (r: Node),
kDominator env r = true /\
exists (p: list Node), (is_kDom_path r p n).

Lemma any_is_kDominated:
forall (n: Node),
forall r p, is_kDom_path r p n -> Z.of_nat (length p) <= k.

Lemma that proves correctness: Any node is linked to dom_set head through a path of length smaller than k
Definition IsInkDomSet (k: Z) (root: Node) (n: Node): Prop :=
kDominator env root = true /\
exists p, (is_kDom_path root p n) /\ (Z_of_nat (length p) <= k)%Z.

Lemma any_is_in_kDom_set:
forall (n: Node), exists (r: Node), IsInkDomSet k r n.

End Final_kDomSet.

## Correctness

Section Correctness.

Definition kDominator_ (g: Env) (n: Node): Prop :=
kDominator g n = true.

Theorem kdom_set_at_terminal:
forall (g: Env),
Assume g -> terminal g -> kDOM kDominator_ g (k := k).

Lemma kDOM_partial_correctness:
P_correctness KDom_RO_assumption (kDOM kDominator_ (k := k)).

End Correctness.

End KDomSet_Correctness.

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