PADEC - Coq Library

Library Padec.Model.Topologies.Ring_topology

A Framework for Certified Self-Stabilization
PADEC Coq Library

March 2017

Global imports

From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import ZArith.
From Coq Require Import Lia.

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:

a predecessor function Pred to go one step backward on the ring
a successor function Succ to go one step forward on the ring
a distance function Dist which counts the number of (clockwise) steps between any two elements in the ring.

Convention:

Dist increments (if it can) with Succ
Dist decrements (if it can) with Pred

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

a equivalence on A, considered as the equality on the elements of A and
that each function (Pred, Succ, Dist) is compatible w.r.t. this relation.

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:

(base case) it holds at some element x
(induction step) if it holds somewhere, let say at element y,

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_all_ind:
    forall (P: A -> A -> Prop) (P_compat: Proper pequiv P),
      (forall n, P n n ) ->
      (forall m n, ~ m == n ->
                   forall n', Between (Succ m) n' n ->
                              P n' n -> P (Pred n') n ) ->
    forall m n, P m 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:

the first one constrains the network to be a unidirectional ring, namely it should have a ring topology (as defined above) on nodes and the Pred function should correspond to existing channels
the second one adds the constraint of being rooted: the definition simply assumes a particular node to be the root.

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

the channel that goes to the predecessor in the ring; this is given by function ring_pred_channel
and whether it is the root; this is given by function ring_is_root.

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.