PADEC
Coq Library
Toc
Tools
PADEC - Coq Library

Library Padec.BFS.BFS_unfair_bis

A Framework for Certified Self-Stabilization
PADEC Coq Library

Global Imports

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

Local Imports

From Padec Require Import SetoidUtil.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Exec.
From Padec Require Import Self_Stabilization.
From Padec Require Import BFS_algo_bis.
From Padec Require Import BFS_common_bis.
From Padec Require Import Graph_Diameter.
From Padec Require Import Min_list.
From Padec Require Import Count.
From Padec Require Import WellfoundedUtil.
From Padec Require Import P_Q_Termination.


Open Scope nat_scope.
Set Implicit Arguments.

BFS: Proof of convergence with an unfair daemon


Section BFS_unfair.

  Context {Chans: Channels}
          {Net: Network}
          {Graph_assumption: BFS_Assume}
          {Graph_network_assumption: Graph_Network_matching}.

  Existing Instance G_compat.

  Notation Algo := (BFS_algo).
  Notation Env := (Env (Net := Net) (Algo := Algo)).
  Notation Step := (Step (Net := Net) (Algo := Algo)).

  Existing Instance BFS_RO_assumption.

Tools on Graph

More tools on graph, developped for this use case
  Section Tools_on_Graph.

    Lemma flat_map_InA:
      forall (A B : Type) (SA: Setoid A) (SB: Setoid B) (f : A -> list B) (pf: Proper pequiv f)
             (l : list A) (y : B),
        InA equiv y (flat_map f l) <->
          (exists x : A, InA equiv x l /\ InA equiv y (f x)).

    Definition all_pair_of_nodes: list (Node * Node) :=
      flat_map (fun a =>
                  map (fun b => (a, b)) all_nodes) all_nodes.

    Lemma all_pair_of_nodes_prop:
      forall ab, InA equiv ab all_pair_of_nodes.

    Definition all_edges: list (Node * Node) :=
      filter (fun ab => if G_dec (fst ab) (snd ab) then true else false)
      all_pair_of_nodes.

    Lemma all_edges_prop:
      forall a b, InA equiv (a, b) all_edges <-> G a b.

End Tools_on_Graph.


Non-root d-actions

This section is restricted to non-root d-actions This means that the d-value of the root remains constant and at least one node modifies its d-value. Note taht other nodes may change their par-value.
  Section non_root_d_actions_only.

Definition of Step' (non-root d-step) and some direct properties

    Definition d_has_moved (g' g: Env) n := d (g' n) <> d (g n).

    Lemma d_has_moved_compat: Proper pequiv d_has_moved.

    Lemma d_has_moved_dec: forall g' g n,
        {d_has_moved g' g n}+{~d_has_moved g' g n}.

    Lemma d_has_moved_false: forall g' g n,
        ~d_has_moved g' g n -> d (g' n) = d (g n).

    Lemma d_has_moved_has_moved_b: forall g' g n,
        d_has_moved g' g n -> has_moved_b g' g n = true.

    Lemma d_has_moved_dec_compat:
      forall g1' g2' (eg': g1' =~= g2') g1 g2 (eg: g1 =~= g2) u1 u2 (eu: u1 == u2),
        (if d_has_moved_dec g1' g1 u1 then true else false) =
          (if d_has_moved_dec g2' g2 u2 then true else false).

    Definition Step': relation Env :=
      fun g' g => Step g' g
                  /\ d (g Root) = d (g' Root)
                  /\ exists n, d_has_moved g' g n.

    Instance Step'_compat: Proper fequiv Step'.

    Lemma Step'_proper_l:
      forall g g': Env, Step' g' g -> Proper pequiv g'.

    Lemma Step'_proper_r:
      forall g g': Env, Step' g' g -> Proper pequiv g.

    Lemma step'_noRoot:
      forall g g', Step' g' g ->
                   forall p, d_has_moved g' g p -> ~p == Root.

    Lemma step'_move:
      forall g (i: Assume g) g',
        Step' g' g ->
        forall p,
          d_has_moved g' g p ->
          d (g' p) = Dist_p (map S (dist_Neigh g p)).

    Lemma step'_move2:
      forall g (i: Assume g) g',
        Step' g' g ->
        forall p,
          d_has_moved g' g p ->
          (exists q, G p q /\ S (d (g q)) = d (g' p)) /\
            (forall q, G p q -> S (d (g q)) >= d (g' p)).

Definition of the interval of d-values

During an execution the d-value will remain in some interval of values which can be computed and depends on the initial configuration.

The minimum d-value for a node and for all nodes: hbot and hmin

node }
We can prove that for any d-step, g -d-> g' we have: If an execution starts with the initial configuration ginit, (hmin ginit) is a lower bound for all d-values (for all nodes) that will be reached during the execution.
hb is a tool to represent hbot when applied to (fun u => d (g u)) (see Definition); it has been introduced to prove it is monotonic and idempot.
    Definition hb (h: Node -> nat) (n: Node): nat :=
      Min_list (h Root) (map h all_nodes).

    Lemma hb_compat: Proper pequiv hb.

    Lemma hb_const: forall h n1 n2, hb h n1 = hb h n2.

    Definition InfEq (h h': Node -> nat): Prop := forall n, h n <= h' n.

    Lemma hb_monotonic: forall h h', InfEq h h' -> InfEq (hb h) (hb h').

    Lemma hb_idempotent: forall h, Proper pequiv h -> hb h =~= hb (hb h).

    Definition hbot (g: Env) (n: Node): nat := hb (fun u => d (g u)) n.

    Lemma hbot_compat: Proper pequiv hbot.

    Lemma list_d_g_prop:
      forall (g: Env) (pg: Proper pequiv g) dd,
        InA equiv dd (map (fun u => d (g u)) all_nodes)
        <-> exists n, dd = d (g n).

    Lemma hbot_prop: forall g (pg: Proper pequiv g) n, hbot g n <= d (g n).

    Definition hmin (g: Env): nat := hbot g Root.

    Lemma hmin_compat: Proper pequiv hmin.

    Lemma hmin_hbot: forall g n, hmin g = hbot g n.

    Lemma hmin_monotonic:
      forall g g', InfEq (hbot g) (hbot g') -> hmin g <= hmin g'.

    Lemma technical_Dist_p0:
      forall (f: Node -> nat) u l,
        Dist_p (map f (u :: l)) = Min_list (f u) (map f l).

    Lemma technical_Dist_p:
      forall (f: Node -> nat) u,
        ~u == Root ->
        exists nu lnu,
          Neigh u = nu :: lnu /\
            Dist_p (map f (Neigh u)) = Min_list (f nu) (map f lnu).

    Lemma technical_Dist_p':
      forall (g: Env) u,
        ~u == Root ->
        exists neigh lneigh,
          dist_Neigh g u = neigh :: lneigh
          /\ Dist_p (dist_Neigh g u) = Min_list neigh lneigh.

    Lemma hmin_bound:
      forall g (i: Assume g) g', Step' g' g ->
                                 forall u, hmin g <= d (g' u).

    Lemma hbot_bound:
      forall g (i: Assume g) g', Step' g' g ->
                   forall u, hbot g u <= d (g' u).

    Lemma hbot_progress:
      forall g (i: Assume g) g', Step' g' g ->
                   forall n, hbot g n <= hbot g' n.

    Lemma hmin_progress:
      forall g (i: Assume g) g', Step' g' g ->
                   hmin g <= hmin g'.

The maximum d-value for a node and for all nodes: htop and hmax

Note that the definition of htop os recursive and requires the filtering of neighbors of n at some distance to the root. We introduce those tools to be able to define htop.
We can prove that for any d-step, g -d-> g' we have: If an execution starts with the initial configuration ginit, (hmin ginit) is an upper bound for all d-values (for all nodes) that will be reached during the execution.

    Notation dist := (dist G_compat G_dec Connected all_nodes_prop (DA := Node_dec)).
Distance to the root and some properties
    Definition rank (n: Node): nat := dist n Root.
    Lemma rank_compat: Proper pequiv rank.

    Lemma rank_pos:
      forall u, rank u > 0 -> exists v, G u v /\ S (rank v) = rank u.

    Lemma rank_not_root: forall u, u == Root <-> rank u = 0.

neighbors at some rank
    Definition neigh_rank u r :=
      filter (fun v =>
                if G_dec u v then
                  if Nat.eq_dec (S (rank v)) r then true
                  else false
                else false) all_nodes.

    Lemma neigh_rank_compat: Proper fequiv neigh_rank.

    Lemma neigh_rank_spec':
      forall u r v, InA equiv v (neigh_rank u r) <-> G u v /\ S (rank v) = r.

    Lemma neigh_rank_spec:
      forall u v, InA equiv v (neigh_rank u (rank u)) <->
                      G u v /\ S (rank v) = rank u.

    Lemma neigh_rank_not_nil:
      forall u, rank u > 0 -> neigh_rank u (rank u) <> nil.

    Lemma neigh_rank_incl:
      forall u r, inclA equiv (neigh_rank u r) (Neigh u).

As hb, ht is introduced to be able to prove the idempotent and monotonic property
    Fixpoint ht' (h: Node -> nat) (n: Node) (rn: nat): nat :=
      match rn with
      | 0 => h n
      | S rv =>
          match neigh_rank n rn with
          | nil => h n
          | a::nrnk =>
              max
                (h n)
                (S (Min_list (ht' h a rv)
                     (map (fun v => (ht' h v rv)) nrnk)))
          end
      end.

    Lemma ht'_compat: Proper fequiv ht'.

    Definition ht (h: Node -> nat) (n: Node): nat := ht' h n (rank n).

    Lemma ht_compat: Proper pequiv ht.

    Lemma ht_monotonic: forall h h', InfEq h h' -> InfEq (ht h) (ht h').

    Lemma ht_idempotent: forall h, Proper pequiv h -> ht h =~= ht (ht h).

    Definition htop (g: Env) (n: Node): nat := ht (fun u => d (g u)) n.

    Lemma htop_compat: Proper fequiv htop.

    Lemma htop_bound: forall g u, d (g u) <= htop g u.

    Lemma htop_bound_step:
      forall g (i: Assume g) g', Step' g' g ->
                                 forall u, d (g' u) <= htop g u.

    Lemma htop_progress:
      forall g (i: Assume g) g', Step' g' g ->
                   forall n, htop g n >= htop g' n.

    Definition hmax: Env -> nat :=
      fun g =>
        fold_right max
          (htop g Root) (map (fun n => htop g n) all_nodes).

    Lemma hmax_compat: Proper fequiv hmax.

    Lemma hmax_prop: forall g (pg: Proper pequiv g) n, htop g n <= hmax g.

    Lemma hmax_progress:
      forall g (i: Assume g) g', Step' g' g -> hmax g >= hmax g'.

    Lemma hbot_htop:
      forall g (pg: Proper pequiv g) u, hbot g u <= htop g u.

    Lemma hmin_hmax: forall g (pg: Proper pequiv g), hmin g <= hmax g.

    Lemma hmax_monotonic:
      forall g g', InfEq (htop g) (htop g') -> hmax g <= hmax g'.


Smooth and non-smooth edges: definitions and direct properties

The potential function that is used to prove convergence is based on counting the number of smooth and non-smooth edges
Given a configuration g, pictures) when |d(g u) - d(g v)| <= 1

    Definition red (g: Env) (u v: Node): Prop :=
      d (g u) >= d (g v) + 2 \/ d (g v) >= d (g u) + 2.

    Lemma red_compat: Proper pequiv red.

    Lemma red_sym: forall g u v, red g u v <-> red g v u.

    Lemma red_dec: forall g u v, {red g u v} + {~red g u v}.

    Definition blue (g: Env) (u v: Node): Prop :=
      d (g u) <= d (g v) + 1 /\ d (g v) <= d (g u) + 1.

    Lemma blue_compat: Proper pequiv blue.

    Lemma blue_sym: forall g u v, blue g u v <-> blue g v u.

    Lemma red_not_blue: forall g u v, red g u v <-> ~blue g u v.

    Lemma blue_not_red: forall g u v, blue g u v <-> ~red g u v.

    Lemma blue_dec: forall g u v, {blue g u v} + {~blue g u v}.

The RANK of an edge is the minimum d-value taken between the two d-values of its nodes
    Definition RANK (g: Env) (u v: Node): nat := min (d (g u)) (d (g v)).

    Lemma RANK_compat: Proper pequiv RANK.

    Lemma RANK_sym: forall g u v, RANK g u v = RANK g v u.

    Lemma RANK_spec: forall g u v R,
        R = RANK g u v <->
          d (g u) <= d (g v) /\ R = d (g u) \/
            d (g v) <= d (g u) /\ R = d (g v).

    Definition edge_moves :=
      (fun g' g u v => d_has_moved g' g u \/ d_has_moved g' g v).

    Lemma edge_moves_compat: Proper pequiv edge_moves.

    Lemma edge_moves_dec:
      forall g' g u v, {edge_moves g' g u v}+{~edge_moves g' g u v}.

    Lemma edge_moves_dec_compat:
      forall g1' g2' (eg': g1' =~= g2') g1 g2 (eg: g1 =~= g2) u1 u2 (eu: u1 == u2) v1 v2 (ev: v1 == v2),
        (if edge_moves_dec g1' g1 u1 v1 then true else false) =
          (if edge_moves_dec g2' g2 u2 v2 then true else false).

    Lemma edge_moves_sym:
      forall g' g u v, edge_moves g' g u v == edge_moves g' g v u.

    Lemma edge_moves_false_d:
      forall g' g (st: Step' g' g) u v,
        ~edge_moves g' g u v -> d (g u) = d (g' u) /\ d (g v) = d (g' v).

For an edge, when none of its nodes moves, its smoothness does not change
    Lemma edge_moves_false_red:
      forall g' g (st: Step' g' g) u v,
        ~edge_moves g' g u v -> ( red g u v <-> red g' u v ).

    Lemma edge_moves_false_blue:
      forall g' g (st: Step' g' g) u v,
        ~edge_moves g' g u v -> ( blue g u v <-> blue g' u v ).

    Lemma edge_moves_false_RANK:
      forall g' g (st: Step' g' g) u v,
        ~edge_moves g' g u v -> RANK g u v = RANK g' u v.

During a d-step, either a red edge moves or every moving edge are blue
    Lemma exists_red_move_dec:
      forall g' g (st: Step' g' g),
        {exists u v, G u v /\ red g u v /\ edge_moves g' g u v}
        +
          {forall u v, G u v -> edge_moves g' g u v -> blue g u v}.

The following lemma allows to pick a neighbor node of y, called x, s.t. the edge is red and x is below y (smaller d) ; if this is not possible, this means that every node linked to y with a red edge is above y (greater d).
    Lemma red_below_dec:
      forall g (pg: Proper pequiv g) y,
        {x | G y x /\ red g y x /\ RANK g y x = d (g x)}
        +
          {forall z, G y z -> red g y z -> RANK g y z = d (g y)}.

The list of red edges that move during the step g -d-> g'
    Definition red_move_list (g' g: Env): list (Node * Node) :=
      filter
        (fun uv =>
           if red_dec g (fst uv) (snd uv) then
             if edge_moves_dec g' g (fst uv) (snd uv) then true else false
        else false)
        all_edges.

    Lemma red_move_list_prop:
      forall g' (pg': Proper pequiv g')
             g (pg: Proper pequiv g),
      forall u v,
        InA equiv (u, v) (red_move_list g' g) <->
          G u v /\ red g u v /\ edge_moves g' g u v.

Bound definition: the bound is the minimum RANK (i.e. the minimum d-value) among the red moving edges This definition is meaningless when no red moving edge exits - see assumptions uv_red and uv_moves below

    Notation RANK' := (fun (g: Env) (uv: Node * Node) => RANK g (fst uv) (snd uv)).

    Lemma RANK'_compat: Proper pequiv RANK'.

    Definition bound (g' g: Env) (u v: Node): nat :=
      Min_list (RANK g u v) (map (RANK' g) (red_move_list g' g)).

    Lemma bound_spec:
      forall g g' (st: Step' g' g)
             u v (Guv: G u v) (uv_red: red g u v)
             (uv_moves: edge_moves g' g u v) b,
        b = bound g' g u v <->
          (forall x y, G x y -> edge_moves g' g x y -> red g x y ->
                     b <= RANK g x y) /\
            exists x y, G x y /\ edge_moves g' g x y /\ red g x y /\
                        b = RANK g x y.

    Lemma bound_prop_forall:
      forall g g' (st: Step' g' g)
             u v (Guv: G u v) (uv_red: red g u v)
             (uv_moves: edge_moves g' g u v),
      forall x y, G x y -> edge_moves g' g x y ->
                  red g x y ->
                  bound g' g u v <= RANK g x y.

    Lemma bound_prop_exists:
      forall g g' (st: Step' g' g)
             u v (Guv: G u v) (uv_red: red g u v)
             (uv_moves: edge_moves g' g u v),
      exists x y, G x y /\ edge_moves g' g x y /\
                    red g x y /\
                    bound g' g u v = RANK g x y.

    Lemma bound_inf:
      forall g g' (st: Step' g' g)
             u v (Guv: G u v) (uv_red: red g u v)
             (uv_moves: edge_moves g' g u v),
        hmin g <= bound g' g u v.

    Lemma bound_sup:
      forall g g' (st: Step' g' g)
             u v (Guv: G u v) (uv_red: red g u v)
             (uv_moves: edge_moves g' g u v),
        bound g' g u v <= hmax g.

First Case: when the moving edges are blue exclusively


    Lemma blue_edge:
      forall g u v,
        G u v -> blue g u v -> d (g v) + 1 = d (g u)
                               \/ d (g v) = d (g u)
                               \/ d (g v) = d (g u) + 1.

    Lemma blue_node_moves:
      forall g (i: Assume g) g' (st: Step' g' g) u,
        d_has_moved g' g u ->
        (forall v, G u v -> blue g u v) ->
        (
          ( d (g' u) = d (g u) + 1 /\
                (exists v, G u v /\ d (g v) = d (g u)) /\
                forall v, G u v -> d (g v) >= d (g u) )
          \/ ( d (g' u) = d (g u) + 2 /\
                 (exists v, G u v /\ d (g v) = d (g u) + 1) /\
                 forall v, G u v -> d (g v) = d (g u) + 1 )
        ).

First Case: when the moving edges are blue exclusively,
    Lemma only_blue_moving_1:
      forall g (i: Assume g) g' (st: Step' g' g),
        (forall u v, G u v -> edge_moves g' g u v -> blue g u v)
        ->
          forall u v, G u v -> (red g' u v <-> red g u v).

First Case: when the moving edges are blue exclusively,
    Lemma only_blue_moving_2:
      forall g g' (st: Step' g' g),
        (forall u v, G u v -> edge_moves g' g u v -> blue g u v)
        ->
          forall u v, G u v -> red g u v ->
                      RANK g' u v = RANK g u v.


First Case: when the moving edges are blue exclusively,
   Lemma only_blue_moving_3:
      forall g (i: Assume g) g' (st: Step' g' g),
        (forall u v, G u v -> edge_moves g' g u v -> blue g u v)
        ->
          forall u, d_has_moved g' g u -> d (g' u) > d (g u).

First Case: when the moving edges are blue exclusively,
    Lemma only_blue_moving_edge_set:
      forall g (i: Assume g) g' (st: Step' g' g),
        (forall u v, G u v -> edge_moves g' g u v -> blue g u v)
        ->
        forall k, forall u v (huv: G u v),
          (red g u v /\ RANK g u v = k)
          <->
            (red g' u v /\ RANK g' u v = k).

Second Case: when at least one red edge moves

    Lemma red_moving_1:
      forall g g' (st: Step' g' g)
             u v (Guv: G u v) (uv_red: red g u v)
             (uv_moves: edge_moves g' g u v),
      forall x y, G x y -> red g x y ->
                  RANK g x y < bound g' g u v ->
                  (RANK g' x y = RANK g x y /\ red g' x y).

    Lemma red_moving_23:
      forall g (i: Assume g) g' (st: Step' g' g)
             u v (Guv: G u v) (uv_red: red g u v)
             (uv_moves: edge_moves g' g u v),
      forall x y, G x y -> red g' x y ->
                  RANK g' x y <= bound g' g u v ->
                  RANK g' x y = RANK g x y /\ red g x y.

    Lemma red_moving_2:
      forall g (i: Assume g) g' (st: Step' g' g)
             u v (Guv: G u v) (uv_red: red g u v)
             (uv_moves: edge_moves g' g u v),
      forall x y, G x y -> red g' x y ->
                  RANK g' x y < bound g' g u v ->
                  RANK g' x y = RANK g x y /\ red g x y.

    Lemma red_moving_3:
      forall g (i: Assume g) g' (st: Step' g' g)
             u v (Guv: G u v) (uv_red: red g u v)
             (uv_moves: edge_moves g' g u v),
      forall x y, G x y -> red g' x y ->
                  RANK g' x y = bound g' g u v ->
                  RANK g' x y = RANK g x y /\ red g x y.

There exists a red edge with RANK equal to the bound at g If this edge is still red at g', then its RANK has increased
    Lemma red_moving_4:
      forall g (i: Assume g) g' (st: Step' g' g)
             u v (Guv: G u v) (uv_red: red g u v)
             (uv_moves: edge_moves g' g u v),
      exists x y, G x y /\ red g x y /\
                    RANK g x y = bound g' g u v /\
                    (red g' x y -> RANK g' x y > RANK g x y).

Second Case: when at least one red edge moves
Consequence on the set of red edges: forall k, 1. if k < bound, then the set of red edges of RANK k is unchanged 2. if k = bound, then the set of red edges of RANK k at g' is included in the set of red edges of RANK k at g 3. there exists a red edge of RANK equal to the bound at g: if this edge is still red at g', then its RANK has increased
    Lemma red_moving_edge_set_1:
      forall g (i: Assume g) g' (st: Step' g' g)
             (u v: Node) (Guv: G u v) (uv_red: red g u v)
             (uv_moves: edge_moves g' g u v),
      forall k, k < bound g' g u v ->
                forall x y (hxy: G x y),
                  (red g x y /\ RANK g x y = k)
                  <->
                    (red g' x y /\ RANK g' x y = k).

    Lemma red_moving_edge_set_2:
      forall g (i: Assume g) g' (st: Step' g' g)
             (u v: Node) (Guv: G u v) (uv_red: red g u v)
             (uv_moves: edge_moves g' g u v),
      forall k, k = bound g' g u v ->
                forall u v (huv: G u v),
                  (red g' u v /\ RANK g' u v = k) ->
                  (red g u v /\ RANK g u v = k).

    Lemma red_moving_edge_set_3:
      forall g (i: Assume g) g' (st: Step' g' g)
             (u v: Node) (Guv: G u v) (uv_red: red g u v)
             (uv_moves: edge_moves g' g u v),
      exists x y,
        G x y /\ red g x y /\ RANK g x y = bound g' g u v /\
          (red g' x y -> RANK g' x y > bound g' g u v).

Potential definition <xi, sigma>

where As the d-values of an execution are ranging from (hmin ginit) to (hmax ginit) (ginit being the initial configuration), we use this interval for the index of the xi vector.
Namely:

(xi g) at h = { x y, G x y /\ red g x y /\

Rank g x y = h } k from (hmin ginit) to (hmax ginit)

sigma g = sum{u in V} d (g u)

(xi g) at h is represented as a predicate on pairs of nodes:
    Definition xi_at_h g h :=
      fun xy => G (fst xy) (snd xy) /\ red g (fst xy) (snd xy) /\
                  RANK g (fst xy) (snd xy) = h.

    Lemma xi_at_h_compat: Proper pequiv xi_at_h.

    Lemma xi_at_h_dec: forall g h xy, xi_at_h g h xy \/ ~xi_at_h g h xy.

Vector of predicates xi
    Definition xi min max g :=
      build_ (fun h => xi_at_h g (max - h)) (max + 1 - min).

    Lemma xi_hd:
      forall min max g,
        min <= max -> hd (fun _=>True) (xi min max g) = xi_at_h g min.

    Lemma xi_compat: Proper pequiv xi.

    Lemma xi_length: forall min max g, length (xi min max g) = max + 1 - min.

Getters on xi: on index h, to obtain (xi_at_h g h) (see Lemma xi_spec)
    Program Definition get_xi (min max: nat) (g: Env)
      h (hm: min <= h) (hM: h <= max)
      :=
      @get _ (xi min max g) (h - min) _.

    Lemma xi_spec:
      forall (min max: nat) g h (hm: min <= h) (hM: h <= max),
        get_xi g hm hM = xi_at_h g h.

    Definition get_xi' (min max: nat) (g: Env) h :=
      nth (h - min) (xi min max g) (fun _ => True).

    Lemma xi_spec':
      forall (min max: nat) g h (hm: min <= h) (hM: h <= max),
        get_xi' min max g h = xi_at_h g h.

Sigma: sum of d-values on all nodes
    Definition sigma (g: Env): nat :=
      fold_right Nat.add 0 (map (fun v => d (g v)) all_nodes).

    Lemma sigma_compat: Proper pequiv sigma.

    Lemma sigma_monotonic:
      forall (g g': Env),
        (forall n, d (g n) <= d (g' n)) -> sigma g <= sigma g'.

    Lemma sigma_monotonic':
      forall (g g': Env) (pg: Proper pequiv g) (pg': Proper pequiv g'),
        (forall n, d (g n) <= d (g' n)) ->
        (exists n, d (g n) < d (g' n)) -> sigma g < sigma g'.

Maximal value for sigma
    Lemma sigma_bound:
      forall g B,
        (forall n, d (g n) <= B) -> sigma g <= B * (length all_nodes).

One D-Step

We now fix one d-step and express the observation made on smooth and non-smooth edges to obtain properties on xi and sigma
    Section with_one_step.

      Variable (g g': Env) (st: Step' g' g) (i: Assume g).
      Notation pg' := (Step'_proper_l st).
      Notation pg := (Step'_proper_r st).

When only blue edges move, xi is left unchanged from one configuration to the next.
      Lemma only_blue_xi:
        forall (min max: nat),
        (forall u v, G u v -> edge_moves g' g u v -> blue g u v) ->
        xi min max g =~= xi min max g'.

When only blue edges move, sigma increases from one configuration to the next.
      Lemma only_blue_sigma:
        (forall u v, G u v -> edge_moves g' g u v -> blue g u v) ->
        sigma g < sigma g'.

When at least on red edge moves, we consider the predicate of xi at index (bound). This predicate is smaller (strict inclusion) at g' than at g.
      Lemma red_moves_witness:
        forall min max (hm: min <= hmin g) (hM: hmax g <= max),
        forall (u v: Node) (Guv: G u v)
               (uv_red: red g u v) (uv_moves: edge_moves g' g u v),

        incl _ (get_xi' min max g' (bound g' g u v))
          (get_xi' min max g (bound g' g u v)).

When at least on red edge moves, we consider any predicate of xi at index smaller than bound. Such a predicate is "left unchanged" from g to g'.
      Lemma red_moves_preserve:
        forall min max (hm: min <= hmin g) (hM: hmax g <= max),
        forall (u v: Node) (Guv: G u v)
               (uv_red: red g u v) (uv_moves: edge_moves g' g u v),

          forall k, min <= k < bound g' g u v ->
                    get_xi' min max g k =~= get_xi' min max g' k.

    End with_one_step.

The three previous lemma are enough to obtain the convergence property for DStep, i.e. (Acc DStep ginit).
The following formalizes this conclusion.

Ordering xi

We build the ordering relation on xi by:
Equality on predicates on pairs of nodes (meant for edges): equivalence of predicates
    Definition eqPred: relation (Node * Node -> Prop) :=
      pequiv (A := Node * Node -> Prop).

Order on predicates on pairs of nodes (meant for edges): inclusion, i.e. "strict implies"
    Definition ltPred: relation (Node * Node -> Prop) :=
      (fun p q => incl _ p q).

    Lemma ltPred_proper_l: forall a b, ltPred a b -> a =~= a.

    Lemma ltPred_compat: Proper pequiv ltPred.

Order on list of predicate on pairs of nodes (edges): the lexicographic order based on the previous order and equality on predicates
    Definition ltlexPred: relation (list (Node * Node -> Prop)) :=
      fun a b => Proper pequiv a /\ lexico_lists eqPred ltPred a b.

    Lemma ltlexPred_proper_l: forall a b, ltlexPred a b -> a =~= a.

    Lemma ltlexPred_compat: Proper pequiv ltlexPred.

This lexicographic order is well-founded, since the ordering on predicates is well-founded; indeed, predicate applies on finite sets.
    Lemma ltlexPred_Acc: forall x, Acc ltlexPred x.

The entire relation: it compares two configurations g' < g iff (xi g', sigma g') <lex (xi g, sigma g)
where <lex is the lexicographic order made of
    Definition relEnv hmin hmax (g' g: Env): Prop :=
      (lexico_pairs (eqlistA eqPred) ltlexPred
         (fun n m : nat => m < n <= hmax * (length all_nodes)))
        (xi hmin hmax g', sigma g')
        (xi hmin hmax g, sigma g).

    Lemma relEnv_compat: Proper pequiv relEnv.


The relation Dstep is well-founded (when restricted to

well-formed (Assume, Proper pequiv) configurations.
    Lemma Step'_Acc:
      forall g, Assume g -> Proper pequiv g -> Acc Step' g.
  End non_root_d_actions_only.

  Section other_actions.


Well-formed configurations:
    Definition safeBFS :=
      (fun g: Env => Proper pequiv g /\ Assume g).

Par-Step: we show that the relation Step restricted to steps

where only par-actions are executed is well-founded.
    Definition StepPar :=
      (fun g' g => Step g' g /\ forall n, d (g n) = d (g' n)).

    Definition par_enabled_b :=
      (fun g n =>
         if Node_dec n Root then false
         else
           if Nat.eq_dec (d (g n)) (Dist_p (map S (dist_Neigh g n))) then
             if Nat.eq_dec (d (g n)) (S (d (g (Par g n))))
             then false
             else true
           else false
      ).

    Lemma par_enabled_b_compat: Proper pequiv par_enabled_b.

    Lemma par_enabled_b_true:
      forall g n,
        Proper pequiv g -> Assume g ->
        par_enabled_b g n = true -> enabled_b g n = true.

A node that executes a par-action is not the root.
    Lemma StepPar_nonRoot:
      forall g' g (i: Assume g) (st: StepPar g' g) n,
        has_moved_b g' g n = true -> ~n == Root.

technical - when executing a par-action, the d-value is well-set.
    Lemma StepPar_hm1:
      forall g' g (i: Assume g) (st: StepPar g' g) n,
        has_moved_b g' g n = true ->
        d (g n) = Dist_p (map S (dist_Neigh g n)).

technical - when executing a par-action, the d-value of the parent cannot provide the d-value of the node (before the par-action).
    Lemma StepPar_hm2:
      forall g' g (i: Assume g) (st: StepPar g' g) n,
        has_moved_b g' g n = true -> d (g n) <> S (d (g (Par g n))).

technical
    Lemma StepPar_Dist_p_const:
      forall g' g n, StepPar g' g ->
      Dist_p (map S (dist_Neigh g n)) = Dist_p (map S (dist_Neigh g' n)).

A node which is par-enabled and does not execute remains par-enabled.
    Lemma StepPar_en_nhm:
      forall g' g n, Assume g -> StepPar g' g ->
                     par_enabled_b g n = true ->
                     has_moved_b g' g n = false ->
                     par_enabled_b g' n = true.

A node that executes during a par-Step was par-enabled before the step and is no more par-enabled after the step.
    Lemma StepPar_hm:
      forall g' g n, Assume g -> StepPar g' g ->
                     has_moved_b g' g n = true ->
                     par_enabled_b g n = true /\ par_enabled_b g' n = false.

A node which is par-disabled before a par-Step remains par-disabled after this step.
    Lemma StepPar_dis:
      forall g' g n, Assume g -> StepPar g' g ->
                     par_enabled_b g n = false ->
                     par_enabled_b g' n = false.

We show that Par-Step is a well-founded order using a potential function This potential simply counts the number of nodes which are enabled for a par-action. Using the previous observations, this number decreases by at least one at each par-Step.
    Definition par_potential (g: Env) (n: Node): nat :=
      if par_enabled_b g n then 1%nat
      else 0%nat.

    Notation ltM := (@MultisetNat.MSetOrd.MultisetLT gt).
    Notation Pot_par := (Pot (fun sg => par_potential (proj1_sig sg))).

    Notation TransPar :=
      (fun sg' sg: sig safeBFS =>
         forall n, d (proj1_sig sg n) = d (proj1_sig sg' n)).

    Lemma Par_pot_decreases:
      forall sg' sg, safeQStep TransPar sg' sg ->
                     ltM (Pot_par sg') (Pot_par sg).

Par-Step is a well-founded order
    Lemma StepPar_wf: well_founded (safeQStep TransPar).

Root-Step: we now consider steps where the root executes.

This relation is (trivially) well-founded, since once the root has executed, it can no more execute.
    Notation TransRoot :=
      (fun sg' sg: sig safeBFS =>
         has_moved_b (proj1_sig sg') (proj1_sig sg) Root = true).

    Lemma StepRoot_wf: well_founded (safeQStep TransRoot).

The D-step relation is well-founded (using the same formalism as

for Par-Step and Root-Step).
    Notation Trans' :=
      (fun sg' sg: sig safeBFS =>
         d (proj1_sig sg Root) = d (proj1_sig sg' Root) /\
           (exists n, d_has_moved (proj1_sig sg') (proj1_sig sg) n)).

    Lemma safeStep'_wf: well_founded (safeQStep Trans').

    Lemma Trans'_dec: forall sg' sg,
        {Trans' sg' sg} + {~Trans' sg' sg}.

    Lemma TransRoot_dec: forall sg' sg,
        {TransRoot sg' sg} + {~TransRoot sg' sg}.

    Lemma TransPar_dec: forall sg' sg,
        {TransPar sg' sg} + {~TransPar sg' sg}.

A Step is either a D-step, a root-step or a Par-Step.

    Lemma TransAll:
      forall sg' sg,
        Trans' sg' sg \/ TransRoot sg' sg \/ TransPar sg' sg.

    Lemma TransPar_default:
      forall sg' sg, ~Trans' sg' sg -> ~TransRoot sg' sg ->
                     TransPar sg' sg.

(xi, sigma) is left unchanged by a par-Step.
    Lemma Par_xi_sigma_unchanged:
      forall g' g,
        Step g' g -> (forall n, d (g n) = d (g' n)) ->
        forall hm hM,
          (xi hm hM g, sigma g) =~= (xi hm hM g', sigma g').

Relation Step is well-founded

    Lemma Step_Acc:
      forall g, Assume g -> Proper pequiv g -> Acc Step g.
  End other_actions.


Convergence: eventually a legitimate (terminal) configuration is

reached with an unfair daemon
  Theorem BFS_convergence:
    Self_Stabilization.convergence BFS_RO_assumption
      Fairness.unfair_daemon terminal.

End BFS_unfair.

Unset Implicit Arguments.
Close Scope nat_scope.
You can change colors, if you wish ;)