PADEC
Coq Library
Tools
PADEC - Coq Library

Library Padec.Dijkstra.Dijkstra_sum_dist

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 Bool.
From Coq Require Import Omega.
From Coq Require Import Lia.

Local Imports

From Padec Require Import Stream.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Exec.
From Padec Require Import Ring_topology.
From Padec Require Import Dijkstra_algo.
From Padec Require Import Dijkstra_common.
From Padec Require Import Self_Stabilization.
From Padec Require Import Steps.
From Padec Require Import NatUtils.
From Padec Require Import SetoidUtil.
From Padec Require Import Count.
From Padec Require All_In.
From Padec Require FoldRight.
From Padec Require Import ListUtils.


Set Implicit Arguments.
Open Scope nat_scope.

Diskstra's first token ring algorithm

Potential sum_dist

/contains:/ Definitions and results about sum_dist
/assumes:/ Parameter k>1; the network is a unidirectional rooted ring;

Section Dijkstra_sum_dist.

  Context {Chans: Channels}
          {Net: Network}
          {RURN: Rooted_Unidirectional_Ring_Network Net}
          {DP: Dijkstra_parameters}.

  Notation Algo := Dijkstra_algo.
  Notation Root := (RURN_root (Net := Net)).
  Notation Ring := (URN_topo (Net := Net)).


  Notation N := (Ring_size Root).

The ring contains at least 3 nodes
  Hypothesis HN4: N >= 4.

Definitions for the sum of distances to the root of every

token holder. We define sum_dist which is the complete sum and then sd which is a partial sum computed on a given slice of the ring.
accumulation function
  Notation f_dtok g :=
    (fun n acc => acc + if Token_dec g n then Dist n Root else 0).

  Lemma f_dtok_compat: Proper pequiv (fun g => f_dtok g).

sum_dist: sum of distances to the root of every token holder.
  Definition sum_dist := (fun g => Ring_fold_Pred Root 0 (f_dtok g)).

  Instance sum_dist_compat: Proper pequiv sum_dist.

sd: partial sum computed on a given slice of the ring
  Definition sd := (fun g p q => Between_fold
                                   0 (f_dtok g) p q).

  Instance sd_compat:
    Proper (pequiv ==> equiv ==> equiv ==> eq) sd.

Tools about sd

to reduce or split the slice on which sd is computed
  Lemma sd_Succ:
    forall g p q,
      sd g p q = (if Token_dec g p then Dist p Root else 0) +
                 if Node_dec p q then 0 else sd g (Succ p) q.

  Lemma sd_Pred:
    forall g (pg: Proper pequiv g) p q,
      sd g p q = (if Token_dec g q then Dist q Root else 0) +
                 if Node_dec p q then 0 else sd g p (Pred q).

  Lemma sd_cut:
    forall g (pg: Proper pequiv g) p q,
    forall n, Between p n q -> ~ n == q ->
              sd g p q = sd g p n + sd g (Succ n) q.

  Lemma sd_one:
    forall g x, sd g x x = if Token_dec g x then Dist x Root else 0.

decomposition for sd that exihibits the value of a given node in the slice.
  Lemma sd_decomp:
    forall g (pg: Proper pequiv g),
    forall a b x,
      Between a x b ->
      sd g a b =
      (if Node_dec x a then 0 else sd g a (Pred x)) +
      (if Token_dec g x then Dist x Root else 0) +
      (if Node_dec x b then 0 else sd g (Succ x) b).

Relation between sd and sum_dist

  Lemma sum_dist_sd:
    forall g (pg: Proper pequiv g) x, sum_dist g = sd g x (Pred x).

  Lemma sum_dist_sd_Root:
    forall g (pg: Proper pequiv g),
      sum_dist g = sd g (Succ Root) (Pred Root).

Tools for sd (at most) decreasing

When no node obtains a token in some slice, then the sum of the slice does not increase (proof by induction on the list of the nodes in the slice)
  Lemma sd_no_increase:
    forall g g',
    forall a b,
      (forall n, Between a n b -> Token g' n -> Token g n)
      -> sd g' a b <= sd g a b.

When no node obtains a token, but at least one loses a token, sd decreases
  Lemma sd_decrease:
    forall g (pg: Proper pequiv g) g' (pg': Proper pequiv g'),
    forall a b,
      (forall n, Between a n b -> Token g' n -> Token g n) ->
      (exists n, ~ n == Root /\
                 Between a n b /\ Token g n /\ ~ Token g' n) ->
      sd g' a b < sd g a b.

  Lemma Dist_increases:
    forall a b n, ~ a == Pred b -> Between a n b -> ~ n == b ->
                  ~ n == a -> Dist b a < Dist n a.

In a slice, where no node obtains a token but the last one, if some node inbetween actually loses a token, then sd decrease.
  Lemma sd_decrease2:
    forall g (pg: Proper pequiv g) g' (pg': Proper pequiv g'),
    forall a b,
      Between Root a (Pred b) ->
      ~ Token g b -> Token g' b ->
      (forall n, Between a n (Pred b) -> Token g' n -> Token g n) ->
      (exists n, ~ n == Root /\
                 Between a n (Pred b) /\ Token g n /\ ~ Token g' n) ->
      sd g' a b < sd g a b.

LO

We build the list of non-root nodes that obtain a token during a step from g to g'. Note that this list is built traversing the node from (Succ Root) to (Pred Root) in the reverse order.

token_obtained

We say that a node obtains a token during a step from g to g' when it does not hold a token in g, but holds one in g'.
  Definition token_obtained g' g :=
    (fun n =>
       if Token_dec g n then false
       else if Token_dec g' n then true
            else false).

  Lemma token_obtained_true:
    forall g' g n, token_obtained g' g n = true <->
                   ~ Token g n /\ Token g' n.

  Lemma token_obtained_false:
    forall g' g n, token_obtained g' g n = false <->
                   (Token g' n -> Token g n).

  Instance token_obtained_compat: Proper pequiv token_obtained.

LO

  Definition LO g' g :=
    filter (token_obtained g' g)
           (rev (traversal_Between (Succ Root) (Pred Root))).

Note that for every node x in LO, x itself does not move, its predecessor Pred x moves, and its successor Succ x either does not move or else loses its token (since it copies x's value and this value remains constant in the step).
  Lemma TO_Pred_moves:
    forall g' g n, Assume g -> Step g' g ->
                   token_obtained g' g n = true ->
                   has_moved_b g' g (Pred n) = true.

  Lemma TO_not_move:
    forall g' g n, Assume g -> Step g' g ->
                   token_obtained g' g n = true ->
                   has_moved_b g' g n = false.

  Lemma TO_not_Succ:
    forall g' g n, Assume g -> Step g' g ->
                   ~ Root == Succ n ->
                   token_obtained g' g n = true ->
                   has_moved_b g' g (Succ n) = false \/
                   ~ Token g' (Succ n).

Tools for LO decomposition

We first define tools for LO decomposition. We consider the case when LO contains at least one element and then the case of at least two (consecutive) elements.

If LO contains at least an element:

LO can be decomposed as l ++ x ++ l' where x is a node and l and l' are lists. Then, we have: Those results come directly from the definitions and the assumption N>=3.
  Lemma LO_decomp_tokO_:
    forall g' g (pg': Proper pequiv g') (pg: Proper pequiv g),
    forall a b l x l',
      filter (token_obtained g' g)
             (rev (traversal_Between a b)) == l ++ x :: l' ->
      token_obtained g' g x = true.

  Lemma LO_decomp_tokO:
    forall g' g (pg': Proper pequiv g') (pg: Proper pequiv g),
    forall l x l', LO g' g == l ++ x :: l' ->
                   token_obtained g' g x = true.

  Lemma LO_decomp_B:
    forall g' g (pg': Proper pequiv g') (pg: Proper pequiv g),
    forall l x l', LO g' g == l ++ x :: l' ->
                   Between (Succ Root) x (Pred Root).

  Lemma LO_decomp_notRoot:
    forall g' g (pg': Proper pequiv g') (pg: Proper pequiv g),
    forall l x l', LO g' g == l ++ x :: l' -> ~ x == Root.
As there is no duplicate in a traversal list of node, if LO is split into 3 parts (l, x, l') then l and l' are the results of the filtering operation on the list before x, resp. after x.
  Lemma LO_decomp_decomp:
    forall g' g (pg': Proper pequiv g') (pg: Proper pequiv g),
    forall a b l x l',
      filter (token_obtained g' g)
             (rev (traversal_Between a b)) == l ++ x :: l' ->
      filter (token_obtained g' g)
             (rev (if Node_dec x b then nil else
                     traversal_Between (Succ x) b)) == l /\
      filter (token_obtained g' g)
             (rev (if Node_dec x a then nil else
                     traversal_Between a (Pred x))) == l'.
Particular case of the considered element being Succ Root to prove this result, we directly apply LO_decomp_decomp
  Lemma LO_decomp_first:
    forall g' g (pg': Proper pequiv g') (pg: Proper pequiv g),
    forall l x l', LO g' g == l ++ x :: l' -> x == Succ Root ->
                   l' == nil.

Particular case of the considered element being Pred Root to prove this result, we directly apply LO_decomp_decomp
  Lemma LO_decomp_last:
    forall g' g (pg': Proper pequiv g') (pg: Proper pequiv g),
    forall l x l', LO g' g == l ++ x :: l' -> x == Pred Root -> l == nil.

If LO contains at least two elements:

LO can be decomposed as l ++ x :: y :: l' where x and y are nodes and l and l' are lists. The 4 last results come directly from the definitions and the assumption N>=3.
  Lemma LO_decomp_successive_:
    forall g' g (ass: Assume g) (step: Step g' g),
    forall a b x y l ll,
      filter (token_obtained g' g)
             (rev (traversal_Between a b)) == l ++ x :: y :: ll ->
      ~ x == Succ y.

  Lemma LO_decomp_successive:
    forall g' g (ass: Assume g) (step: Step g' g),
    forall x y l ll, LO g' g == l ++ x :: (y :: ll) ->
                     ~ x == Succ y.

  Lemma LO_decomp_successive_first:
    forall g' g (pg': Proper pequiv g') (pg: Proper pequiv g),
    forall x y l ll, LO g' g == l ++ x :: (y :: ll) ->
                     ~ x == Succ Root.

  Lemma LO_decomp_successive_last:
    forall g' g (pg': Proper pequiv g') (pg: Proper pequiv g),
    forall x y l ll, LO g' g == l ++ x :: (y :: ll) ->
                     ~ y == Pred Root.

Again, as there is no duplicate in a traversal list of nodes, if LO is split into 4 parts (l, x, y, l') then l and l' are the results of the filtering operation on the list before x, resp. after y, and the filtering operation on the list after x and before y returns an empty list.
  Lemma LO_decomp_successive_decomp:
    forall g' g (ass: Assume g) (step: Step g' g),
    forall a b l x y l',
      filter (token_obtained g' g)
             (rev (traversal_Between a b)) == l ++ x :: y :: l' ->
      filter (token_obtained g' g)
             (rev (if Node_dec x b then nil else
                     traversal_Between (Succ x) b)) == l /\
      filter (token_obtained g' g)
             (rev (if Node_dec y a then nil else
                     traversal_Between a (Pred y))) == l' /\
      filter (token_obtained g' g)
             (rev (traversal_Between (Succ y) (Pred x))) == nil.

  Lemma LO_decomp_successive_1:
    forall g' g (pg': Proper pequiv g') (pg: Proper pequiv g),
    forall x y l ll,
      LO g' g == l ++ x :: y :: ll -> ~ x == y.

Order between the two consecutive elements of LO to prove this result, we directly apply LO_decomp_decomp
  Lemma LO_decomp_successive_Bl:
    forall g' g (ass: Assume g) (step: Step g' g),
    forall x y l ll, LO g' g == l ++ x :: (y :: ll) ->
                     Between (Succ Root) y (Pred x).

Order between the two consecutive elements of LO to prove this result, we directly apply LO_decomp_decomp
  Lemma LO_decomp_successive_Br:
    forall g' g (pg': Proper pequiv g') (pg: Proper pequiv g),
    forall x y l ll, LO g' g == l ++ x :: (y :: ll) ->
                     Between (Succ y) x (Pred Root).

  Lemma LO_decomp_successive_Bl':
    forall g' g (ass: Assume g) (step: Step g' g),
    forall x y l ll, LO g' g == l ++ x :: (y :: ll) ->
                     Between Root (Succ y) (Pred x).

3) Remark: in any slice of the ring between two

consecutive elements of LO (resp in the first slice, before flo) (resp in the last slice after llo), no node obtains a token, hence sd computed on this slice does not increase.

Results for Remark 3

  Lemma _no_TO_2cases:
    forall g g' (ass: Assume g) (step: Step g' g),
      let flo := match LO g' g with nil => Root | a::l => a end in
      ~ flo == Pred Root ->
      forall n, Between (Succ flo) n (Pred Root) ->
                Token g' n -> Token g n.
  Lemma LO_nil_no_TO:
    forall g g' (ass: Assume g) (step: Step g' g),
      LO g' g = nil ->
      forall n, Between (Succ Root) n (Pred Root) ->
                Token g' n -> Token g n.
  Lemma fist_slice_no_TO:
    forall g g' (ass: Assume g) (step: Step g' g) flo l,
      LO g' g = flo :: l -> ~ flo == Pred Root ->
      forall n, Between (Succ flo) n (Pred Root) ->
                Token g' n -> Token g n.

  Lemma last_slice_no_TO:
    forall g' g (ass: Assume g) (step: Step g' g) llo l,
      LO g' g == l ++ llo :: nil -> ~ Succ Root == llo ->
      forall n, Between (Succ Root) n (Pred llo) ->
                Token g' n -> Token g n.
  Lemma mid_slice_no_TO:
    forall g' g (ass: Assume g) (step: Step g' g) x y l ll,
      LO g' g == l ++ x :: y :: ll ->
      forall n, Between (Succ y) n (Pred x) ->
                Token g' n -> Token g n.

Lemma witness

The proof is mainly an induction on LO. It mainly relies the idea that for every node n in LO (and even if LO is empty) we can find a witness node which loses a token and is farther than n from the root.
Lemma witness: in a slice m - n of nodes, if n moves, then either m moves and holds a token in g' or there exits a node l between m and n which loses its token.
Lemma witness is proven by induction on m using an induction schema of Between. For the base case, (the property has to be proven for n), n moves. Hence, either it loses its token or keeps it; both cases prove the base case. At each induction step, either we already found the witness node or the current node moves and keeps the token. By two_tokens_moves, we obtain that the predecessor of the current node also moves, hence as in the base case, both cases are proven whatever be the fact that the node keeps its token or not.
  Lemma witness:
    forall g' g (ass: Assume g) (step: Step g' g),
    forall m n,
      has_moved_b g' g n = true ->
      (Token g' m /\ has_moved_b g' g m = true) \/
      (exists x, Between m x n /\ Token g x /\ ~ Token g' x).

Case: LO is nil.

We already have "<=" using the remark above. During the step,
  Lemma sd_decr_LO_nil_RM:
    forall g g' (ass: Assume g) (step: Step g' g),
      LO g' g = nil ->
      has_moved_b g' g Root = true -> sum_dist g' <= sum_dist g.

  Lemma sd_decr_LO_nil:
    forall g g' (ass: Assume g) (step: Step g' g),
      LO g' g = nil ->
      has_moved_b g' g Root = false -> sum_dist g' < sum_dist g.

The rest of the proof is done by an induction on LO. It

relies on the idea that for every node n in LO we can find a witness node which loses a token and is farther than n from the root.
For; the first slice of nodes, Succ flo - Pred Root we have <=.
  Lemma sd_first_slice:
    forall g g' (ass: Assume g) (step: Step g' g) flo l,
      LO g' g = flo :: l -> ~ flo == Pred Root ->
      sd g' (Succ flo) (Pred Root) <= sd g (Succ flo) (Pred Root).

For every slice of nodes Succ y - x, since Pred x moves, and Succ y either does not move or else loses its token, Lemma witness applied on Succ y - Pred x exhibit a witness node which is farther than x the root and makes sd decrease on the slice.
  Lemma sd_mid_slice:
    forall g g' (ass: Assume g) (step: Step g' g) l x y ll,
      LO g' g == l ++ x :: y :: ll ->
      sd g' (Succ y) x < sd g (Succ y) x.

For the last slice Succ Root - llo, if Succ Root

moves and still holds a token, then the root moves. This is the case with no witness when sd increases by at most N - 1 = Dist (Succ Root) Root in the slice. Otherwise, Lemma witness applies to Succ Root - Pred llo and exhibits a witness node which is farther than llo from the root and makes sd decrease on the slice.
  Lemma sd_last_slice:
    forall g g' (ass: Assume g) (step: Step g' g) l llo,
      LO g' g == l ++ llo :: nil ->
      if has_moved_b g' g Root then
        sd g' (Succ Root) llo <= sd g (Succ Root) llo + N - 1
      else
        sd g' (Succ Root) llo < sd g (Succ Root) llo.

Results on all the slices:

Assuming LO not nil. We compute sd on the slice from Succ Root to flo. It either increases by at most N-1 when the root moves and decreases otherwise.
The proof is done by induction on LO, proving that sd computed from sd to every element in LO follows the above property. Induction step uses Lemmas sd_mid_slice and sd_last_slice.
  Lemma sd_mid_last_slices:
    forall g g' (ass: Assume g) (step: Step g' g) flo l,
      LO g' g = flo :: l ->
      if has_moved_b g' g Root then
        sd g' (Succ Root) flo <= sd g (Succ Root) flo + N - 1
      else
        sd g' (Succ Root) flo < sd g (Succ Root) flo.

Lemma sum_dist_evolves

Case LO is nil: sd_decr_LO_nil and sd_decr_LO_nil_RM provide the result.
Case LO not nil: sd_mid_last_slices and sd_first_slice provide the result.
  Lemma sum_dist_evolves:
    forall g g', Assume g -> Step g' g ->
                 if has_moved_b g' g Root then
                   sum_dist g' <= sum_dist g + N - 1
                 else
                   sum_dist g' < sum_dist g.

Bound on sum_dist

sum_dist is maximal when every node holds a token, maximum given by the sum of distances (induction on the slice on which sum_dist is computed)
  Lemma sum_dist_bound:
    forall g, Proper pequiv g -> 2 * sum_dist g <= N * (N - 1).

Technical lemma to handle particular cases for small values

of N, exhbit the weight of two token holders in sum_dist
Induction on the list of nodes (given by (traversal_Pred N Root)) if the liste contains both n1 and n2 then res >= Dist n1 Root + Dist n2 Root else if the list contains n1 then res >= Dist n1 Root else if the list contains n2 then res >= Dist n2 Root
  Lemma minus2:
    forall g (pg: Proper pequiv g)
           n1 n2,
      ~ n1 == n2 -> Token g n1 -> Token g n2 ->
      sum_dist g >= Dist n1 Root + Dist n2 Root.


End Dijkstra_sum_dist.

Unset Implicit Arguments.
Close Scope nat_scope.