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.

# Termination for K-Dominating Set Algorithm

1) Define Potential of a node: 0 if not enabled, else tree depth signature: node->env -> nat
NB: depth for root == 1
2) Proof: if a node becomes enabled, one of its child has moved
3) Proof (down path induction + 2)): if a node becomes enabled, one of its descendant has become disabled
assumption: downpaths are finite (to be proved elsewhere)
4) Proof: there is always a node whose activation has changed (potential of this node passed from >0 to 0) (induction on down path)
5) Using 3) and multiset theorem (P_Q_Termination.v) concludes that the algorithm terminates
=> Use results from P_Q_Termination
• proof of local criterion: see 3)
• proof of global criterion: see 4)
Section KDomSet_Termination.

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

Section Potential_Definition.

## Potential of a node:

0 if not enabled, else depth of the node in the spanning tree.
Note that this definition requires that the spanning tree exists. This is the reason why termination cannot be shown without the assumption on safe configurations.

Variable (root: Node).
Variable (Par: Node -> option Channel).
Variable (span_tree: spanning_tree root Par)
(Par_compat: Proper fequiv Par).

depth in the tree
Definition depth_ (n: Node)
(W: Acc (is_tree_parent_of Par) n): nat :=
@Fix_F Node (is_tree_parent_of Par) (fun _ => nat)
(fun (x: Node)
(f_rec: forall y: Node, is_tree_parent_of Par y x -> nat) =>
Datatypes.S
(match (tree_parent Par x) as op return
(op == (tree_parent Par x)) -> nat
with
| None => fun _ => 0%nat
| Some y => fun e => (f_rec y e)
end (Equivalence_Reflexive (tree_parent Par x)))
) n W.

Definition depth (n: Node): nat := depth_ (WF_par Par_compat span_tree n).

Potential of a node: 0 if not enabled, else depth
Definition potential (alpha: Node -> Z) (n: Node): nat :=
if (enabled_alpha_b Par alpha n) then (depth n) else 0%nat.

End Potential_Definition.

Section Potential_Compatibility.

Lemma depth__compat:
(Proper (respectful_dep_param (equiv (A:=nat))
((Node -> option Channel)::Node::nil)
(pequiv,(equiv,tt))
(inl (fun par n => Acc (is_tree_parent_of par) n)::nil)) depth_).

Lemma depth_compat:
Proper (respectful_dep_param pequiv
(Node::(Node -> option Channel)::nil)
(equiv,(pequiv,tt))
( inl (fun r p => spanning_tree r p)
::
inl (fun r p => Proper fequiv p)
::
nil)) depth.

Lemma potential_compat:
Proper (respectful_dep_param pequiv
(Node::(Node -> option Channel)::nil)
(equiv,(pequiv,tt))
( inl (fun r p => spanning_tree r p)
::
inl (fun r p => Proper fequiv p)
::
nil)) potential.

End Potential_Compatibility.

Section Potential_Properties.

Variable (root: Node).
Variable (Par: Node -> option Channel).
Variable (span_tree: spanning_tree root Par)
(Par_compat: Proper fequiv Par).

Lemma depth_gt_0: forall (n: Node), gt (depth span_tree Par_compat n) 0.

Any node which is down-linked to another has smaller depth than the first one.
Lemma deeper_depth_step:
forall (n: Node) (child: Node),
is_tree_parent_of Par n child ->
depth span_tree
Par_compat child = Datatypes.S (depth span_tree Par_compat n).

Lemma deeper_depth:
forall (p: list Node) (n: Node) (d: Node),
~ (n == d) -> directed_tree_path Par n p d ->
(depth span_tree Par_compat n < depth span_tree Par_compat d)%nat.

End Potential_Properties.

## Results for one step of execution

Section With_Step.

Variable (root: Node).

Variable (Par: Node -> option Channel) (Par': Node -> option Channel).
Variable (Par_same: Par =~= Par') (span: spanning_tree root Par).
Variable (Par_compat: Proper fequiv Par)
(Par'_compat: Proper fequiv Par')
(span': spanning_tree root Par').
Variable (alpha: Node -> Z) (alpha': Node -> Z).
Variable (alpha_compat: Proper fequiv alpha)
(alpha'_compat: Proper fequiv alpha')
(step_ok: forall n, alpha' n = NewAlpha Par alpha n \/
alpha' n = alpha n)
(progress: exists n, alpha n <> alpha' n).

New Children alphas only depends on children moves
New Alphas only depends on children moves
When a node that was disabled becomes enabled, one of its child has actually moved.
When a node has actually moved while none of its children moved, it is no more enabled at next configuration.
When a node has moved, but is still enabled at next configuration, it has a child that actually also moved.
When a node actually moved, it is down-linked (in the spanning tree) to a node which was enabled and became disabled.
When a node that was disabled becomes enabled at next configuration, it is down-linked (in the spanning tree) to a node which was enabled and becomes disabled.

### 4) Proof:

there is always a node that becomes disabled after a step (potential of this node passed from >0 to 0) (induction on down path)
Within a valid step, there exists a node that was enabled but becomes disabled

### 5) Using 3) and multiset theorem (Termination.v,

Wf_Algo_Multiset) conclude that the algorithm terminates
• proof of local criterion: see 3)
• proof of global criterion: see 4)

Local Criterion

## Global Criterion

Lemma kHopDom_global_criterion:
exists n, potential span' Par'_compat alpha' n <>
potential span Par_compat alpha n.

End Potential_termination_criteria.
End With_Step.

End KDomSet_Termination.

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