PADEC
Coq Library
Tools
PADEC - Coq Library

Library Padec.KDomSet.KDomSet_alpha

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.

Local Imports

From Padec Require Import OptionUtil.
From Padec Require Import ZUtils.
From Padec Require Import ListUtils.
From Padec Require Import SetoidUtil.
From Padec Require Import FoldRight.
From Padec Require Import Algorithm.
From Padec Require Import Spanning_Tree.
From Padec Require Import KDomSet_specification.

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

Definition of alpha and its computation

Section KDomSet_Alpha.

  Context {Chans: Channels} {Net: Symmetric_Network}.

  Context {KDP: KDomSet_parameters}.
  Let k_pos := k_pos.

Functions used for the computation of alpha

  Section Local_Alpha_Definition.

    Definition Local_ChildrenAlphas
               (peers: list Channel)
               (peer_Par: Channel -> option Channel)
               (reply: Channel -> Channel)
               (peer_alpha: Channel -> option Z): list Z :=
      map_filter peer_alpha (Local_Children peers peer_Par reply).

    Global Instance Local_ChildrenAlphas_compat:
      Proper (equivlistA equiv ==> fequiv ==> fequiv ==> fequiv
                         ==> equivlistA eq) Local_ChildrenAlphas.

    Notation alpha_peer :=
      (fun (alpha: Node -> Z) n => (fun c => option_map alpha (peer n c))).
    Instance alpha_peer_compat: Proper fequiv alpha_peer.

    Definition ChildrenAlphas (Par: Node -> option Channel)
               (alpha: Node -> Z) (n: Node): list Z :=
      map_filter (alpha_peer alpha n) (Children Par n).

    Global Instance ChildrenAlphas_compat:
      Proper (fequiv ==> fequiv ==> equiv ==> equivlistA eq) ChildrenAlphas.

    Notation Par_peer :=
      (fun (Par: Node -> option Channel) (n: Node) =>
         (fun c: Channel => match (peer n c) with
                              None => None | Some x => Par x end)).
    Instance Par_peer_compat:
      Proper (fequiv ==> equiv ==> equiv ==> equiv) Par_peer.

    Lemma ChildrenAlphas_equiv:
      forall Par alpha n,
        Proper fequiv Par -> Proper fequiv alpha ->
        eqlistA
          eq (Local_ChildrenAlphas
                (peers n) (Par_peer Par n) (reverse n) (alpha_peer alpha n))
          (ChildrenAlphas Par alpha n).

    Definition _IsShort _alpha := (_alpha <? k).
    Global Instance _IsShort_compat: Proper fequiv _IsShort.

    Definition _IsTall _alpha := (_alpha >=? k).
    Global Instance _IsTall_compat: Proper fequiv _IsTall.

    Definition ShortAlphas (peers: list Channel)
               (peer_Par: Channel -> option Channel)
               (reply: Channel -> Channel)
               (peer_alpha: Channel -> option Z): list Z :=
      List.filter _IsShort
                  (Local_ChildrenAlphas peers peer_Par reply peer_alpha).

    Global Instance ShortAlphas_compat:
      Proper (equivlistA equiv ==> fequiv ==>
                         fequiv ==> fequiv ==> equivlistA eq) ShortAlphas.

    Definition TallAlphas (peers: list Channel)
               (peer_Par: Channel -> option Channel)
               (reply: Channel -> Channel)
               (peer_alpha: Channel -> option Z): list Z
      := List.filter _IsTall (Local_ChildrenAlphas peers
                                                   peer_Par reply peer_alpha).

    Global Instance TallAlphas_compat:
      Proper (equivlistA equiv ==> fequiv ==>
                         fequiv ==> fequiv ==> equivlistA eq) TallAlphas.

    Definition MaxAShort (peers: list Channel)
               (peer_Par: Channel -> option Channel)
               (reply: Channel -> Channel)
               (peer_alpha: Channel -> option Z): Z :=
      List.fold_right Z.max (-1) (ShortAlphas peers peer_Par reply peer_alpha).

    Global Instance MaxAShort_compat:
      Proper (equivlistA equiv ==> fequiv ==>
                         fequiv ==> fequiv ==> eq) MaxAShort.

    Definition MinATall (peers: list Channel)
               (peer_Par: Channel -> option Channel)
               (reply: Channel -> Channel)
               (peer_alpha: Channel -> option Z): Z
      := List.fold_right
           Z.min (2 * k + 1) (TallAlphas peers peer_Par reply peer_alpha).

    Global Instance MinATall_compat:
      Proper (equivlistA equiv ==> fequiv ==> fequiv ==> fequiv ==> eq) MinATall.

    Definition Local_NewAlpha (peers: list Channel)
               (peer_Par: Channel -> option Channel)
               (reply: Channel -> Channel)
               (peer_alpha: Channel -> option Z): Z :=
      if Z_le_gt_dec (MaxAShort peers peer_Par reply peer_alpha
                      + MinATall peers peer_Par reply peer_alpha + 2)
                     (2 * k) then
        MinATall peers peer_Par reply peer_alpha + 1
      else
        MaxAShort peers peer_Par reply peer_alpha + 1.

    Global Instance Local_NewAlpha_compat:
      Proper (equivlistA equiv ==> fequiv ==>
                         fequiv ==> fequiv ==> eq) Local_NewAlpha.

    Definition NewAlpha (Par: Node -> option Channel)
               (alpha: Node -> Z) (p: Node): Z :=
      let tall := List.filter _IsTall (ChildrenAlphas Par alpha p) in
      let short := List.filter _IsShort (ChildrenAlphas Par alpha p) in
      let min := List.fold_right Z.min (2 * k + 1) tall in
      let max := List.fold_right Z.max (-1) short in
      if Z_le_gt_dec (max + min + 2) (2 * k)
      then min + 1 else max + 1.

    Lemma NewAlpha_equiv:
      forall Par alpha n,
        Proper fequiv Par -> Proper fequiv alpha ->
        Local_NewAlpha
          (peers n)
          (fun c => match (peer n c) with None => None | Some x => Par x end)
          (reverse n)
          (fun c => option_map alpha (peer n c))
        =
        NewAlpha Par alpha n.

    Global Instance NewAlpha_compat: Proper fequiv NewAlpha.

  End Local_Alpha_Definition.

  Section Other_Alpha_Definition.

    Definition enabled_alpha_b (Par: Node -> option Channel)
               (alpha: Node -> Z) (p: Node): bool :=
      if Z.eqb (alpha p) (NewAlpha Par alpha p) then false else true.

    Global Instance enabled_alpha_b_compat: Proper fequiv enabled_alpha_b.

    Definition enabled_alpha (Par: Node -> option Channel)
               (alpha: Node -> Z) (p: Node): Prop :=
      enabled_alpha_b Par alpha p = true.

    Global Instance enabled_alpha_compat: Proper fequiv enabled_alpha.

    Definition IsShort (alpha: Node -> Z) (p: Node): bool := _IsShort (alpha p).

    Global Instance IsShort_compat: Proper fequiv IsShort.

    Definition IsTall (alpha: Node -> Z) (p: Node): bool := _IsTall (alpha p).

    Global Instance IsTall_compat: Proper fequiv IsTall.

    Notation eqCob := (dec2b (A := option Channel)
                             (eqoptionA_dec Channel_dec)).
    Instance eqCob_compat:
      Proper (equiv (A := option Channel) ==> equiv (A := option Channel)
                    ==> eq) eqCob.

    Definition IsRoot (Par: Node -> option Channel) (p: Node) :=
      eqCob (Par p) None.

    Lemma IsRoot_is_root_equiv:
      is_root =~= (fun Par p => IsRoot Par p = true).

    Global Instance IsRoot_compat: Proper fequiv IsRoot.

    Definition kDominator (Par: Node -> option Channel)
               (alpha: Node -> Z) (p: Node) :=
      orb (Z.eqb (alpha p) k) (andb (IsShort alpha p) (IsRoot Par p)).

    Global Instance kDominator_compat: Proper fequiv kDominator.

  End Other_Alpha_Definition.

  Section Short_Or_Tall.

    Variable (alpha: Node -> Z).

    Lemma short_or_tall:
      forall (n: Node), {IsShort alpha n = true} + {IsTall alpha n = true}.

  End Short_Or_Tall.

alpha is always between 0 and 2k

  Section Range_of_alpha.

    Lemma new_alpha_0_2k:
      forall Par alpha n, 0 <= NewAlpha Par alpha n <= 2*k.

  End Range_of_alpha.

Local properties of alpha, based on is_tree_parent

  Section Alpha_Local_Properties.

    Variable (Par: Node -> option Channel)
             (Par_compat: Proper fequiv Par)
             (alpha: Node -> Z)
             (alpha_compat: Proper fequiv alpha).

    Lemma InA_ChildrenAlphas:
      forall (n: Node) (a: Z),
        (exists (m: Node), is_tree_parent_of Par n m /\ alpha m = a)
        <-> InA eq a (ChildrenAlphas Par alpha n).

  End Alpha_Local_Properties.

End KDomSet_Alpha.

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