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.
From Coq Require Import Inclusion.
From Coq Require Import RelationPairs.

#### Local Imports

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

# Termination for KClustering Algorithm: Alpha Steps Only

This part shows termination of the algorithm when considering alpha safe steps only. Actually, it shows safe inclusion required by the rest of the proof:
alpha_safe_incl := (forall g g', Alpha_SafeStep g' g -> ltM (Pot_alpha g') (Pot_alpha g)

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 direct child has moved
3) Proof (down path induction + 2)): if a node becomes enabled, one of its descedant 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) conclude that the algorithm terminates
=> Use results from P_Q_Termination
• proof of local criterion: see 3)
• proof of global criterion: see 4)

Section KClustering_Alpha_Termination.

## Channel and network

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

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

Let k_pos := k_pos.

Variable (root: Node).

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 (g: Env) (pg: Proper pequiv g)
(span_tree: spanning_tree root (Par_part g) /\
Symmetric_Network_assumption Net (fun n => KCpeers (g n)) (fun n => KCreverse (g n))).

Local (of a node) alpha-potential is defined using the depth of the node in the spanning tree Note that this definition requires that the spanning tree exists indeed. This is the reason why termination can not be shown without the assumption of a safe environment.

#### depth in the tree

Program Fixpoint depth (env: Env) (n: N) (W: Acc (is_tree_parent_of env) n) {struct W}: nat := Datatypes.S match W with Acc_intro h => match (tree_parent env n) as op return (eqoptionA eqN op (tree_parent env n)) -> nat with | None => fun _ => 0%nat | Some p => fun e => (@depth env p (h p e)) end (Equivalence_Reflexive (tree_parent env n)) end.
Definition depth_ (par:Node -> option Channel) (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_part_compat pg) (proj1 span_tree) n).

Alpha-Potential of a node: 0 if not alpha-enabled, else tree depth
Definition potential (n: Node): nat :=
if alpha_enabled_bb g 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 (A:=Node -> nat ))
(Env::nil)
(pequiv,tt)
(inl (fun g => Proper fequiv g)
::inl (fun g => spanning_tree root (Par_part g)
/\
Symmetric_Network_assumption
Net (fun n => KCpeers (g n))
(fun n => KCreverse (g n))
)
::nil)) depth.

Lemma potential_compat:
Proper (respectful_dep_param
(pequiv (A:=Node -> nat ))
(Env::nil)
(pequiv,tt)
(inl (fun g => Proper fequiv g)
::inl (fun g => spanning_tree root (Par_part g)
/\
Symmetric_Network_assumption
Net (fun n => KCpeers (g n))
(fun n => KCreverse (g n))
)
::nil)) potential.

End Potential_Compatibility.

Section Depth_Properties.

Variable (g: Env) (pg: Proper pequiv g)
(span_tree: spanning_tree root (Par_part g) /\
Symmetric_Network_assumption
Net (fun n => KCpeers (g n))
(fun n => KCreverse (g n))).

Lemma depth_gt_0: forall (n: Node), gt (depth pg span_tree 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_part g) n child ->
depth pg span_tree child = Datatypes.S (depth pg span_tree n).

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

End Depth_Properties.

## Results for one alpha step of execution

Section With_Step.

The alpha step
Variable (g g': Env)
(pg: Proper pequiv g) (pg': Proper pequiv g')
(step: Step g' g)
(alpha_step: alpha_step_b g' g = true)
(span_tree: spanning_tree root (Par_part g)
/\
Symmetric_Network_assumption
Net (fun n => KCpeers (g n))
(fun n => KCreverse (g n)))
(span_tree': spanning_tree root (Par_part g')
/\
Symmetric_Network_assumption
Net (fun n => KCpeers (g' n))
(fun n => KCreverse (g' n))).

Lemma Local_Children_Unchanged:
forall n,
equivlistA equiv (Local_Children (KCpeers (g n)) (lPar (local_env g n))
(KCreverse (g n)))
(Local_Children (KCpeers (g' n)) (lPar (local_env g' n))
(KCreverse (g' n))).

### Any new variables only depends on children alpha-moves

New Alphas of Children only depends on children alpha-moves
Lemma ChildrenAlphas_only_depends_on_children:
forall (n: Node),
(forall (child: Node),
is_tree_parent_of (Par_part g) n child
->
alpha (g child) = alpha (g' child))
-> equivlistA
equiv (ChildrenAlphas (g n) (local_env g n))
(ChildrenAlphas (g' n) (local_env g' n)).

Lemma MinATall_only_depends_on_children:
forall (n: Node),
(forall (child: Node),
is_tree_parent_of (Par_part g) n child
-> alpha (g child) = alpha (g' child)) ->
MinATall (g n) (local_env g n) = MinATall (g' n) (local_env g' n).

New Alphas only depends on children alpha-moves
Lemma NewAlpha_only_depends_on_children:
forall (n: Node),
(forall (child: Node),
is_tree_parent_of (Par_part g) n child
-> alpha (g child) = alpha (g' child))
-> NewAlpha (g n) (local_env g n) =
NewAlpha (g' n) (local_env g' n).

The states after firing an alpha-RUN only depends on children moves
Lemma alpha_RUN_only_depends_on_children:
forall (n: Node),
eqS (g n) (g' n) ->
alpha_enabled_bb g n = true ->
(forall (child: Node),
is_tree_parent_of (Par_part g) n child
-> alpha (g child) = alpha (g' child))
->
(RUN g n) == (RUN g' n).

Lemma alpha_step_effect:
forall n, alpha (g' n) = NewAlpha (g n) (local_env g n)
\/ alpha (g' n) = alpha (g n).

When a node that was disabled becomes enabled, one of its child has actually moved.
Lemma enabled_child_has_moved:
forall (n: Node) (H: alpha_enabled_bb g n = false)
(H': alpha_enabled_bb g' n = true),
exists (child: Node),
(is_tree_parent_of (Par_part g) n child) /\
(alpha (g child)) <> (alpha (g' child)).

When a node has actually moved while none of its children moved, it is no more enabled at next configuration.
Lemma node_has_moved_but_no_child:
forall n, alpha (g n) <> alpha (g' n)
-> (forall child, is_tree_parent_of (Par_part g) n child
-> alpha (g child) = alpha (g' child))
-> alpha_enabled_bb g' n = false.

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

### Alpha-Termination Proof

Section Alpha_Termination.

Definition alpha_potential
(sg: sig (Pspanning_tree root)) (n: Node): nat :=
potential (proj1 (proj2_sig sg)) (proj2 (proj2_sig sg)) n.

Global Instance alpha_potential_compat:
Proper fequiv alpha_potential.

Alpha-Termination
Notation ltM := (@MultisetNat.MSetOrd.MultisetLT gt).
Notation Pot_alpha := (Pot alpha_potential).

Theorem alpha_safe_inclusion:
inclusion (Alpha_SafeStep (root := root)) (ltM @@ Pot_alpha).

End Alpha_Termination.

End KClustering_Alpha_Termination.

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