PADEC
Coq Library
Tools
PADEC - Coq Library

Library Padec.Model.Ring_topology

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 CoLoR Require ListUtil.
From Padec Require Import SetoidUtil.
From Padec Require Import ListUtils.
From Padec Require Import NatUtils.
From Padec Require Import ZUtils.
From Padec Require Import FoldRight.
From Padec Require Import RelModel.
From Padec Require Import Algorithm.
From Padec Require Import Count.

Set Implicit Arguments.
Open Scope nat_scope.

Ring Topology

A ring topology on elements of type A is defined using the following functions:
Convention:
Note that the aforementioned functions are total hence every element of A is covered by the structure which is indeed a ring.
The definition is setoid-compatible, hence it requires

Class Ring_Topology {A} `{SA: Setoid A}: Type :=
  mkRing {
      Pred: A -> A;
      Succ: A -> A;
      Dist: A -> A -> nat;
      Pred_compat:> Proper fequiv Pred;
      Succ_compat:> Proper fequiv Succ;
      Dist_compat:> Proper fequiv Dist;
      Pred_Succ_inv: forall x y, Succ x == y <-> x == Pred y;
      Dist_refl: forall x y, Dist x y = 0 <-> x == y;
      Dist_Succ_r: forall x y,
          Dist x (Succ y) = 1 + Dist x y \/ Dist x (Succ y) = 0;
      Dist_Pred_l: forall x y,
          Dist (Pred x) y = 1 + Dist x y \/ Dist (Pred x) y = 0
    }.

Section With_Ring_Topology.

  Context {A} `{Rt: Ring_Topology A}.

  Instance A_equiv: Equivalence equiv := setoid_equiv.

The equality on A is decidable
  Lemma equiv_dec: Decider equiv.

Straightforward Properties about Pred, Succ and Dist on a Ring

  Lemma Dist_self: forall x, Dist x x = 0.

  Lemma Pred_Succ: forall (x: A), Pred (Succ x) == x.

  Lemma Succ_Pred: forall (x: A), Succ (Pred x) == x.

  Lemma Pred_injective: forall x y, Pred x == Pred y -> x == y.

  Lemma Succ_injective: forall x y, Succ x == Succ y -> x == y.

  Lemma Dist_Succ_l: forall x y, Dist x y = 1 + Dist (Succ x) y \/
                                 Dist x y = 0.

  Lemma Dist_Pred_r: forall x y, Dist x y = 1 + Dist x (Pred y) \/
                                 Dist x y = 0.

  Lemma Dist_Succ: forall x y, Dist x y = Dist (Succ x) (Succ y).

  Lemma Dist_Pred: forall x y, Dist x y = Dist (Pred x) (Pred y).

Ring size

The ring size is computed by one ring traversal, going backward or equivalently forward. The equivalence between those two definitions is proved below.
To be able to count, the ring_size function requires to fix a node (the origin / 0 for counting) but we show that the result (Ring_size) is the same whatever be this node (see Ring_size_invariant).
  Definition Ring_size (x: A): nat := S (Dist (Succ x) x).
  Definition Ring_size' (x: A): nat := S (Dist x (Pred x)).

  Instance Ring_size_compat: Proper pequiv Ring_size.

  Lemma Ring_size_pos: forall x, Ring_size x > 0.

  Lemma Ring_size_invariant: forall (x y: A), Ring_size x = Ring_size y.

  Lemma Ring_size_alt: forall (x y: A), Ring_size x = Ring_size' y.

  Instance Ring_size'_compat: Proper pequiv Ring_size'.

Interative Tools (power) on Ring Topology


  Lemma power_Succ_Pred:
    forall (k: nat) (x y: A),
      power _ Succ k x == y <-> x == power _ Pred k y.

  Lemma Dist_power_Succ:
    forall (k: nat) (x y: A), Dist x y = k -> power _ Succ k x == y.

  Lemma Dist_power_Pred:
    forall (k: nat) (x y: A), Dist x y = k -> x == power _ Pred k y.

  Lemma power_Succ_Pred':
    forall (p q: A) d, Pred (power _ Succ d q) ==
                       power _ Succ d (Pred q).

  Lemma power_Pred_Succ':
    forall (p q: A) d, Succ (power _ Pred d q) ==
                       power _ Pred d (Succ q).

  Lemma Succ_nilpotent: forall x y,
      power _ Succ (Ring_size y) x == x.

  Lemma Pred_nilpotent: forall x y,
      power _ Pred (Ring_size y) x == x.

  Lemma Succ_modulo: forall (k: nat) x y,
      power _ Succ k x == power _ Succ (k mod (Ring_size y)) x.

  Lemma Pred_modulo: forall (k: nat) x y,
      power _ Pred k x == power _ Pred (k mod (Ring_size y)) x.

  Lemma Dist_unique: forall x1 x2 y1 y2,
      Dist x1 y1 = Dist x2 y2 -> (equiv x1 x2 <-> equiv y1 y2).

Inductive Schema on the ring:

to prove a property P on every element of the ring, prove that: then it also holds at the successor (Succ y)
The same Lemma exists with Pred.
  Lemma Ring_Succ_ind: forall (P: A -> Prop),
      Proper pequiv P ->
      forall x, P x -> (forall y, P y -> P (Succ y)) -> forall z, P z.

  Lemma Ring_Pred_ind: forall (P: A -> Prop),
      Proper pequiv P ->
      forall x, P x -> (forall y, P y -> P (Pred y)) -> forall z, P z.

Ring made of a unique element (properties for Pred and Succ)

  Lemma Degenerate_ring_Succ:
    forall x, Succ x == x <-> forall y, equiv y x.

  Lemma Degenerate_ring_Pred:
    forall x, x == Pred x <-> forall y, equiv x y.

  Lemma Degenerate_ring_one:
    forall x, Ring_size x = 1 -> forall y n, y == n.

Non degenerated ring
  Lemma Non_Degenerated_Succ:
    forall x, ~ Succ x == x -> forall y, ~ Succ y == y.

  Lemma Non_Degenerated_Pred:
    forall x, ~ Pred x == x -> forall y, ~ Pred y == y.

  Lemma Non_Degenerated_size_Succ:
    forall x, Ring_size x > 1 -> forall y, ~ y == Succ y.

  Lemma Non_Degenerated_size_Pred:
    forall x, Ring_size x > 1 -> forall y, ~ y == Pred y.

  Lemma Dist_add_Ring_size:
    forall x y z, x == y \/ Ring_size z = Dist x y + Dist y x .

Between

Given 3 elements x y z, Between x y z provides the order of the element x y z on the ring, following the successors
Between forbids to perform a full traversal, namely, x and z should not be the same element of the ring, unless y is also equal to x and z.
  Definition Between (x y z: A): Prop := Dist x y + Dist y z = Dist x z.

  Instance Between_compat: Proper pequiv Between.

  Lemma Between_dec:
    forall x y z, {Between x y z} + {~Between x y z}.

  Lemma Between_Succ:
    forall x y z, Between x y z <-> Between (Succ x) (Succ y) (Succ z).

  Lemma Between_Pred:
    forall x y z, Between x y z <-> Between (Pred x) (Pred y) (Pred z).

  Lemma Between_eq:
    forall x y z, Between x y z -> (x == z <-> (x == y /\ y == z)).

  Lemma Between_strict:
    forall x y z, Between x y z -> ~x == z \/ x == y /\ y == z.

  Lemma Between_circ:
    forall x y z, Between x y z -> x == y \/ Between y z x.

  Lemma Between_eq_l:
    forall x y z, x == y -> Between x y z.

  Lemma Between_eq_r:
    forall x y z, y == z -> Between x y z.

  Lemma Between_self:
    forall x y, Between x y x <-> x == y.

  Lemma Between_self_l:
    forall x y, Between x x y.

  Lemma Between_self_r:
    forall y z, Between y z z.

  Lemma Between_self_lr:
    forall x, Between x x x.

  Lemma Between_Succ_l:
    forall x y z, Between x y z ->
                  x == y \/ Between (Succ x) y z.

  Lemma Between_Pred_l:
    forall x y z, Between x y z ->
                  Pred x == z \/ Between (Pred x) y z.

  Lemma Between_Succ_m:
    forall x y z, Between x y z ->
                  y == z \/ Between x (Succ y) z.

  Lemma Between_Pred_m:
    forall x y z, Between x y z ->
                  x == y \/ Between x (Pred y) z.

  Lemma Between_Succ_r:
    forall x y z, Between x y z ->
                  x == Succ z \/ Between x y (Succ z).

  Lemma Between_Pred_r:
    forall x y z, Between x y z ->
                  y == z \/ Between x y (Pred z).

  Lemma Between_dist_le_l:
    forall x y z, Dist x y <= Dist x z <-> Between x y z.

  Lemma Between_dist_le_r:
    forall x y z, Dist y z <= Dist x z <-> Between x y z.

  Lemma Between_alt_l:
    forall x y z, Between x y z \/ Between x z y.

  Lemma Between_alt_r:
    forall x y z, Between x y z \/ Between y x z.

  Lemma Between_alt_m:
    forall x y z, x == z \/ Between x y z \/ Between z y x.

  Lemma all_Between_Succ: forall x y, Between (Succ x) y x.

  Lemma all_Between_Pred: forall x y, Between x y (Pred x).

  Lemma Between_rewrite_l:
    forall x y, y == x -> forall z t, Between x z t -> Between y z t.

  Lemma Between_rewrite_m:
    forall x y, y == x -> forall z t, Between z x t -> Between z y t.

  Lemma Between_rewrite_r:
    forall x y, y == x -> forall z t, Between z t x -> Between z t y.

  Lemma Dist_lt_Ring_size: forall r x y, Dist x y < Ring_size r.

  Lemma Between_not_Succ_m:
    forall x y, ~ x == Succ y -> ~ Between x (Succ y) y.

  Lemma Between_not_Pred_m:
    forall x y, ~ x == Pred y -> ~ Between y (Pred y) x.

  Lemma Between_not_Pred_l:
    forall x y, ~ x == y -> ~ Between x y (Pred y).

  Lemma Between_not_Succ_r:
    forall x y, ~ x == y -> ~ Between (Succ x) x y.


  Lemma Between_Succ_ind:
    forall (P: A -> Prop) (P_compat: Proper pequiv P),
    forall p q,
      P p ->
      (forall n', Between p n' (Pred q) -> P n' -> P (Succ n')) ->
      forall n, Between p n q -> P n.

  Lemma Dist_Pred_full:
    forall x, forall y, Dist y (Pred y) = Ring_size x - 1.

  Lemma Dist_Succ_full:
    forall x, forall y, Dist (Succ y) y = Ring_size x - 1.

  Lemma Between_trans1:
    forall y a b c, Between b a y -> Between (Succ y) a c ->
                    Between b c y.

  Lemma Between_Pred_ind:
    forall (P: A -> Prop) (P_compat: Proper pequiv P),
    forall p q,
      P q ->
      (forall n', Between (Succ p) n' q -> P n' -> P (Pred n')) ->
      forall n, Between p n q -> P n.

  Lemma Between_trans2:
    forall a b n x,
      Between a n b -> Between a x n -> Between a x b.

  Lemma Between_trans3:
    forall a b n x,
      Between a n b -> Between n x b -> Between a x b.

  Lemma Between_trans4:
    forall a b n x,
      Between a n b -> Between n x b -> Between a n x.

  Lemma power_Succ_Dist_mod:
    forall (k: nat) x y z,
      power _ Succ k x == y <-> Dist x y = k mod (Ring_size z).

  Lemma power_Pred_Dist_mod:
    forall (k: nat) x y z,
      x == power _ Pred k y <-> Dist x y = k mod (Ring_size z).

  Lemma Between_alt_m_bis:
    forall x y z, ~ Succ x == x -> ~ x == Succ z ->
                  Between x y z ->
                  ~ Between (Succ z) y (Pred x).

List of the ring elements

Build the list of n elements of the ring, starting from element x
  Fixpoint traversal_Succ (n: nat) (x: A): list A :=
    match n with | 0 => nil | S p => x :: (traversal_Succ p (Succ x)) end.

  Fixpoint traversal_Pred (n: nat) (x: A): list A :=
    match n with | 0 => nil | S p => x :: (traversal_Pred p (Pred x)) end.

  Lemma traversal_Succ_compat:
    Proper (eq ==> equiv ==> eqlistA equiv) traversal_Succ.

  Lemma traversal_Succ_compat_equiv:
    Proper (eq ==> equiv ==> equivlistA equiv) traversal_Succ.

  Lemma traversal_Pred_compat:
    Proper (eq ==> equiv ==> eqlistA equiv) traversal_Pred.

  Lemma traversal_Pred_compat_equiv:
    Proper (eq ==> equiv ==> equivlistA equiv) traversal_Pred.

  Lemma traversal_Succ_app:
    forall x (k: nat),
      eqlistA equiv (traversal_Succ (S k) x)
              ((traversal_Succ k x)++(power _ Succ k x)::nil).

  Lemma traversal_Succ_Pred_rev:
    forall x (k: nat),
      eqlistA equiv (traversal_Succ k x)
              (rev (traversal_Pred k (power _ Succ k (Pred x)))).

  Lemma traversal_Pred_Succ_rev:
    forall x (k: nat),
      eqlistA equiv (traversal_Pred k x)
              (rev (traversal_Succ k (power _ Pred k (Succ x)))).

  Lemma traversal_Succ_Pred_equiv:
    forall x (k: nat),
      equivlistA equiv (traversal_Succ k x)
                 (traversal_Pred k (power _ Succ k (Pred x))).

  Lemma traversal_Pred_Succ_equiv:
    forall x (k: nat),
      equivlistA equiv (traversal_Pred k x)
                 (traversal_Succ k (power _ Pred k (Succ x))).

  Lemma traversal_Succ_Dist_Between:
    forall x y z,
      InA equiv y (traversal_Succ (S (Dist x z)) x) <-> Between x y z.

  Lemma traversal_Pred_Dist_Between:
    forall x y z,
      InA equiv y (traversal_Pred (S (Dist x z)) z) <-> Between x y z.

The list traversal_Succ of length Ring_Size (and from any element) contains no repeat, but exactly every element in A. This is also true for traversal_Pred.
  Lemma traversal_Succ_full_no_repeat:
    forall x y, NoDupA equiv (traversal_Succ (Ring_size x) y).

  Lemma traversal_Succ_full_all:
    forall x y z, InA equiv z (traversal_Succ (Ring_size x) y).

  Lemma traversal_Pred_full_no_repeat:
    forall x y, NoDupA equiv (traversal_Pred (Ring_size x) y).

  Lemma traversal_Pred_full_all:
    forall x y z, InA equiv z (traversal_Pred (Ring_size x) y).

Traversal Between
  Definition traversal_Between (p q: A): list A :=
    traversal_Succ (1 + (Dist p q)) p.

  Lemma traversal_Between_def:
    forall p q,
      traversal_Between p q = p :: if equiv_dec p q then nil
                                   else traversal_Between (Succ p) q.

  Lemma traversal_Between_rev:
    forall p q, traversal_Between p q ==
                rev (traversal_Pred (1 + (Dist p q)) q).

  Lemma traversal_Between_def_rev:
    forall p q,
      traversal_Between p q == (if equiv_dec p q then nil
                                else traversal_Between p (Pred q)) ++ q::nil.
  Lemma traversal_Between_self:
    forall p, traversal_Between p p = p::nil.

  Instance traversal_Between_compat: Proper pequiv traversal_Between.

  Lemma traversal_Between_Between:
    forall p q n, InA equiv n (traversal_Between p q) <-> Between p n q.

  Lemma traversal_Between_app:
    forall p q,
      ~ q == Pred q -> ~ p == q ->
      forall n, Between p n (Pred q) ->
                traversal_Between p q ==
                traversal_Between p n ++ traversal_Between (Succ n) q.

  Lemma traversal_Between_app':
    forall p q,
      ~ q == Pred q -> ~ p == q ->
      forall n, Between (Succ p) n q ->
                traversal_Between p q ==
                traversal_Between p (Pred n) ++ traversal_Between n q.

Decomposition of a slice of nodes.
The result comes directly from traversal_Between_app, traversal_Between_def and traversal_Between_def_rev.
  Lemma decomp_list:
    forall r, ~ Succ r == r ->
              forall a b x,
                Between a x b ->
                traversal_Between a b ==
                (if equiv_dec x a then nil else traversal_Between a (Pred x))
                  ++
                  x ::
                  (if equiv_dec x b
                   then nil else traversal_Between (Succ x) b).
Ring_fold_Succ applies f_acc to every element of the ring from a
  Definition Ring_fold_Succ (T: Type) (a: A) (init: T) (f_acc: A -> T -> T) :=
    fold_right f_acc init (traversal_Succ (Ring_size a) a).

  Definition Ring_fold_Pred (T: Type) (a: A) (init: T) (f_acc: A -> T -> T) :=
    fold_right f_acc init (traversal_Pred (Ring_size a) a).

  Global Instance Ring_fold_Pred_compat {T: Type} {PT: PartialSetoid T}:
    Proper pequiv (Ring_fold_Pred (T := T)).

  Global Instance Ring_fold_Succ_compat {T: Type} {PT: PartialSetoid T}:
    Proper pequiv (Ring_fold_Succ (T := T)).

The number of elements in A (i.e. in the ring) is exactly given

by Ring_size
  Lemma Ring_elements_card:
    forall x, Num_Card Same A (Ring_size x).

  Definition Between_fold
             (T: Type) (init: T) (f_acc: A -> T -> T)
             (p q: A): T :=
    fold_right f_acc init (traversal_Between p q).

  Instance Between_fold_compat: forall (T: Type) {PT: PartialSetoid T},
      Proper pequiv (Between_fold (T := T)).

  Lemma fold_Between_Ring:
    forall (T: Type) {PT: PartialSetoid T}
           (init: T) (pi: Proper pequiv init)
           (f_acc: A -> T -> T)
           (f_acc_compat: Proper fequiv f_acc),
    forall p, Ring_fold_Succ p init f_acc
                             =~=
                             Between_fold init f_acc p (Pred p).

End With_Ring_Topology.

Ring Network

Given a network, this section provides two definitions:
Section Ring_Network.

  Variable (Chans: Channels)
           (Net: Network).

  Class Unidirectional_Ring_Network :=
    mkURN {
        URN_topo :> Ring_Topology (A:=Node);
        URN_pred_channel : Node -> Channel;
        URN_pred_channel_compat :> Proper fequiv URN_pred_channel;
        URN_channels: forall x y,
            Pred x == y <-> is_channel x (URN_pred_channel x) y
      }.

  Class Rooted_Unidirectional_Ring_Network :=
    mkRURN {
        RURN_URN :> Unidirectional_Ring_Network;
        RURN_root: Node;
      }.

End Ring_Network.

Ring Algorithm

We define a property which provides the assumption for an algorithm to run on a rooted ring network,i.e., the state of every node should contain
Section Ring_Algorithm.

  Definition Ring_Network_assumption {Chans: Channels}
             (Net: Network)
             (RURN: Rooted_Unidirectional_Ring_Network Net)
             (ring_is_root: Node -> bool)
             (ring_pred_channel: Node -> Channel): Prop :=
    (forall n,
        ring_is_root n = true <-> n == RURN_root (Net := Net))
    /\
    (forall n, is_channel n (ring_pred_channel n) (Pred n)).

  Instance Ring_Network_assumption_compat:
    forall {Chans: Channels} Net
           (RURN: Rooted_Unidirectional_Ring_Network Net),
      Proper fequiv (Ring_Network_assumption RURN).

End Ring_Algorithm.

Ring instance

We prove that the class Ring_Topology is inhabited. We build the ring on Z/kZ, of size k
Section Ring_instance.

  Open Scope Z_scope.
  Variable (k: Z) (k_pos: k > 0).
  Notation eqk := (eqk k).

  Instance Zmodk_Setoid :Setoid Z :=
    {| equiv := eqk; setoid_equiv := eqk_equiv k_pos |}.

  Program Definition ring: Ring_Topology :=
    {| Pred := (fun x => x - 1);
       Succ := (fun x => x + 1);
       Dist :=
         (fun x y =>
            if gtk_dec k x y then Z.to_nat(k - x mod k + y mod k)
            else Z.to_nat (y mod k - x mod k)
         )
    |}.







  Lemma ring_size_k:
    forall x, Ring_size (Rt:=ring) x = Z.to_nat k.

  Close Scope Z_scope.

End Ring_instance.

Unset Implicit Arguments.
Close Scope signature_scope.
Close Scope nat_scope.