Coq Library
PADEC - Coq Library

Library Padec.KClustering.KClustering_pcl_termination

A Framework for Certified Self-Stabilization
PADEC Coq Library

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

From Padec Require Import SetoidUtil.
From Padec Require Import OptionUtil.
From Padec Require Import ZUtils.
From Padec Require Import ListUtils.
From Padec Require Import RelationA.
From Padec Require Import FoldRight.
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_alpha_termination.
From Padec Require Import P_Q_Termination.

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

Termination for KClustering Algorithm: Parent Cluster Steps Only

This part shows termination of the algorithm when considering Pcl safe steps only. Actually, it shows safe inclusion required by the rest of the proof:
pcl_safe_incl := (forall g g', Pcl_SafeStep g' g -> ltM (Pot_pcl g') (Pot_pcl g)

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

PCL Potential

  Definition pcl_potential (sg: sig (Pspanning_tree root)) (n: Node): nat :=
    if pcl_enabled_bb (proj1_sig sg) n then 1%nat else 0%nat.

  Global Instance pcl_potential_compat: Proper fequiv pcl_potential.

Results with a PCL step

  Section With_Pcl_Step.

    Variable (g g': Env)
             (pg: Proper pequiv g) (pg': Proper pequiv g')
             (step: Step g' g)
             (pcl_step: pcl_step_b g' g = true)
             (span_tree: spanning_tree root (Par_part g) /\
                           Net (fun n => KCpeers (g n))
                           (fun n => KCreverse (g n)))
             (span_tree': spanning_tree root (Par_part g') /\
                            Net (fun n => KCpeers (g' n))
                            (fun n => KCreverse (g' n))).

    Lemma pcl_no_alpha_enabled_when_move:
      forall n, has_moved_b g' g n = true -> alpha_enabled_bb g n = false.

    Lemma exists_pcl_move:
      exists n, has_moved_b g' g n = true /\ pcl_enabled_bb g n = true.

    Lemma pcl_alpha_unchanged:
      forall n, alpha (g n) = alpha (g' n).

    Lemma pcl_NewParCl_unchanged_:
      (forall n, alpha (g n) = alpha (g' n)) ->
      forall n,
        NewparCl (g n) (local_env g n) == NewparCl (g' n) (local_env g' n).

    Lemma pcl_NewParCl_unchanged:
      forall n,
        NewparCl (g n) (local_env g n) == NewparCl (g' n) (local_env g' n).

    Lemma alpha_enabled_unchanged_pcl:
      forall n, alpha_enabled_bb g n = alpha_enabled_bb g' n.

    Lemma pcl_becomes_disabled:
      forall n, pcl_enabled_bb g n = true
                -> has_moved_b g' g n = true
                -> pcl_enabled_bb g' n = false.

    Lemma pcl_no_move:
      forall n, pcl_enabled_bb g n = false -> parCl (g' n) == parCl (g n).

    Lemma pcl_stays_disabled:
      forall n, pcl_enabled_bb g n = false -> pcl_enabled_bb g' n = false.

  End With_Pcl_Step.

PCL Criteria

  Section Pcl_Termination_Criteria.

    Variable (sg sg': sig (Pspanning_tree root))
             (step: Pcl_SafeStep sg' sg).

    Lemma Pcl_step_b: pcl_step_b (proj1_sig sg') (proj1_sig sg) = true.
    Lemma Pcl_step: Step (proj1_sig sg') (proj1_sig sg).

    Lemma global_pcl_criterium:
      exists n, pcl_potential sg n <> pcl_potential sg' n.

    Lemma local_pcl_criterium:
      forall n,
        (pcl_potential sg n) <> (pcl_potential sg' n) ->
        gt (pcl_potential sg n) (pcl_potential sg' n).

  End Pcl_Termination_Criteria.

PCL Termination

  Section Pcl_Termination.

    Notation ltM := (@MultisetNat.MSetOrd.MultisetLT gt).
    Notation Pot_pcl := (Pot pcl_potential).

    Lemma pcl_safe_inclusion:
      inclusion (Pcl_SafeStep (root := root)) (ltM @@ Pot_pcl).

  End Pcl_Termination.

End KClustering_Pcl_Termination.

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