PADEC - Coq Library

Library Padec.Model.Rounds_inductive_def

A Framework for Certified Self-Stabilization
PADEC Coq Library

Jun 2017

Global Imports

From Coq Require Import SetoidList.
From Coq Require Import Bool.
From Coq Require Import PeanoNat.
From Coq Require Import Lia.
From Coq Require Import RelationPairs.
From Coq Require Import SetoidClass.

Local Imports

From Padec Require Import WellfoundedUtil.
From Padec Require Import SetoidUtil.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Stream.
From Padec Require Import Simulation.
From Padec Require Import Exec.
From Padec Require Import Fairness.
From Padec Require Import ZUtils.
From Padec Require Import BoolSet.
From Padec Require Import RelationA.
From Padec Require Import ListUtils.

Open Scope nat_scope.
Open Scope signature_scope.
Set Implicit Arguments.

Rounds

In this section, we give tools to compute time complexity of an algorithm in terms of rounds. In particular, we compute the number of rounds to reach some predicate P.

Section Rounds.

  Context {Chans: Channels} {Net: Network} {Algo: Algorithm}.

  Notation zerob := (Nat.eqb 0).
  Notation not_zerob := (fun n => negb (Nat.eqb 0 n)).

Tools

The definitions for rounds use

sets of nodes that we model as Boolean set (see BoolSet)
activated nodes (i.e., nodes that execute during a step) and neutralized nodes (i.e., nodes that becomes disabled during a step without executing).

We first introduce tools about Boolean node sets and activated and neutralized nodes.

Tools to describe Node set as Boolean sets

  Notation NodeSet := (BoolSet (A:=Node)).
  Notation eqNodeSet := (eqBoolSet (eqA := (equiv (A:=Node)))).
  Notation leNodeSet := (leBoolSet (eqA := (equiv (A:=Node)))).
  Notation epsilon_NodeSet:=
    (epsilon_BoolSet (eqA := (equiv (A:=Node))) all_nodes_prop).

  Definition LeNodeSet U1 U2 :=
    Proper fequiv U1 /\ leNodeSet U1 U2 /\ Proper fequiv U2.

Tools for activated and neutralized nodes.

  Lemma UNSAT_shrinks (g: Env) (e: Exec) (U U': NodeSet)
        (pU: Proper fequiv U) (pg: Proper fequiv g)
        (pe: Proper pequiv e):
    eqNodeSet U' (diffBoolSet U (act_neut_b (s_cons g e))) ->
    forall n, U' n = true -> U n = true.

  Lemma UNSAT_enabled (g: Env) (e: Exec) (U U': NodeSet)
        (pU: Proper fequiv U) (pg: Proper fequiv g)
        (pe: Proper pequiv e):
    eqNodeSet U' (diffBoolSet U (act_neut_b (s_cons g e))) ->
    leNodeSet U (enabled_b g) ->
    leNodeSet U' (enabled_b (s_hd e)).

  Instance negb_compat: Proper fequiv negb.

  Instance leNodeSet_compat: Proper pequiv leNodeSet.

Definitions of Rounds

Predicate When_SAT is used to identified the end of the current round. It is further explain in the sequel via predicate This_round and Next_round which differs only by the instantiation of Boolean strict.

  Inductive When_SAT (strict: bool) (P: Exec -> Prop)
            (Q: Exec -> Prop): NodeSet -> Exec -> Prop :=
  | SAT_next_step: forall U g e,
      ~ P (s_cons g e) -> Q e ->
      ~ eqNodeSet U empty_BoolSet ->
      let U_ := diffBoolSet U (act_neut_b (s_cons g e)) in
      (if strict then eqNodeSet U_ empty_BoolSet else True ) ->
      When_SAT strict P Q U (s_cons g e)
  | SAT_later: forall U U' g e,
      ~ P (s_cons g e) -> ~ P e ->
      let U_ := diffBoolSet U (act_neut_b (s_cons g e)) in
      ~ eqNodeSet U_ empty_BoolSet -> eqNodeSet U' U_ ->
      When_SAT strict P Q U' e -> When_SAT strict P Q U (s_cons g e).

This_round P Q e:

Q is the predicate to be reached
P is the predicate to be maintained false all along the execution before (strict) it reaches Q

Hence This_round P P e represents the first time e reaches P. This should be achieved during the current round: it is computed using an inductive predicate which uses a set of /unsatisfied/ nodes, i.e. nodes that were unabled at the beginning of the round and have still not executed not been neutralized. We nont e = g0 g1 g2...,

we start at g0 with the set of unsatisfied nodes U0 as the enabled nodes at g0
at each step of e before reaching Q (hence in not P), U is refreshed by removing the nodes that either are executed or neutralized in the step: U1 = U0 - AN(0->1); U2 = U1 - AN(1->2) To remain in the same round the sets Ui should not be empty unless Q is reached.

Definition This_round (P Q: Exec -> Prop) e :=
When_SAT false P Q (enabled_b (s_hd e)) e.

Next_round P Q e:

Q is the predicate to be reached
P is the predicate to be maintained false all along the execution before (strict) it reaches Q

Next_round P Q is used to go through the current round until a new one can begin; Q will be instantiated as the predicate to be reached at the beginning of the next round. Next_round is computed using the same inductive predicate at This_round (but with Boolean strict set to true): again, we note e = g0 g1 g2... and

we start at g0 with the set of unsatisfied nodes U0 as the enabled nodes at g0
at each step of e before reaching Q (hence in not P), U is refreshed by removing the nodes that either are executed or neutralized in the step: U1 = U0 - AN(0->1); U2 = U1 - AN(1->2) To remain in the same round the sets Ui should not be empty unless Q is reached
when Q is reach, Ui should be empty so that a new round can start

Definition Next_round (P Q: Exec -> Prop) e :=
When_SAT true P Q (enabled_b (s_hd e)) e.

Note that When_SAT, hence both This_round and Next_round holds on the previous configuration before reaching Q. This allow to glue back together the current round and the next one. The particulat case when Q holds at e directly will be treated separately.

Hence, here comes the predicate to count the number of rounds to reach a predicate P. For an execution e, At_N_rounds N P e means: e reaches P in N rounds.

if N is null, then we should have P e
if N is one, then P should be reached during the current round, i.e., This_round P P e should hold
otherwise, N = N' + 1 with N' >0, hence we should have at least one round (computed using Next_round) and then seek P within N' round: Next_round P (At_N_rounds N' P) e

  Fixpoint At_N_rounds N (P: Exec -> Prop): Exec -> Prop :=
    match N with
      O => P
    | S N_ => (if zerob N_ then This_round P
               else Next_round P) (At_N_rounds N_ P)
    end.

Hence round complexity is expressed as some upper bound on At_N_rounds. P is the goal to be reached while Q restrict the execution among which we check the bound (usually it is set to: is_exec /\ Assume

  Definition Round_complexity (Q P: Exec -> Prop) (N: nat) :=
    forall exec, Q exec ->
                  exists n , n <= N /\ At_N_rounds n P exec.

Compatibility of the definitions

Compatibility for When_SAT, Next_round, This_round and Round_complexity

  Instance When_SAT_compat: Proper fequiv When_SAT.

  Instance Next_round_compat: Proper fequiv Next_round.

  Instance This_round_compat: Proper fequiv This_round.

  Instance At_N_rounds_compat: Proper fequiv At_N_rounds.

Compatibility for Round_complexity requires more assumption:

  Lemma Round_complexity_compat:
    forall n1 n2 (en: n1 == n2)
           P1 P2 (eP: fequiv P1 P2)
           (Q1 Q2: Exec -> Prop) (eQ: fequiv Q1 Q2)
           (hp1: forall e, Q1 e -> Proper pequiv e)
           (hp2: forall e, Q2 e -> Proper pequiv e),
      Round_complexity Q1 P1 n1 == Round_complexity Q2 P2 n2.

Properties based on At_N_rouds

Monotony wrt P and Q and strict: for every P P' Q Q' b b', P' -> P Q' -> Q b <= b': When_SAT b P Q U e -> When_SAT b' P' Q' U e

  Lemma When_SAT_monotonic:
    Proper (flip Bool.Bool.le ==> (pequiv ==> flip impl )
                 ==> (pequiv ==> impl ) ==> eqNodeSet
                 ==> pequiv ==> impl) When_SAT.

Relation between Next_round and This_round: for every P P' Q Q', P' -> P Q' -> Q: Next_round P Q e -> This_round P' Q' e

  Lemma Next_round_This_round :
    ((pequiv ==> flip impl ) ==> (pequiv ==> impl )
                            ==> pequiv ==> impl )
      Next_round This_round.

When_SAT implies Eventually

Lemma When_SAT_Eventually: forall P Q b UNSAT e,
When_SAT b P Q UNSAT e -> Eventually Q e.

When_SAT implies not P

  Lemma When_SAT_notP: forall P Q b UNSAT e,
      When_SAT b P Q UNSAT e -> ~P e.

  Lemma diff_not_empty:
    forall (s s': NodeSet),
      Proper eqNodeSet s -> Proper eqNodeSet s' ->
      ~ eqNodeSet (diffBoolSet s s') empty_BoolSet
      -> ~ eqNodeSet s empty_BoolSet.

  Lemma When_SAT_not_empty:
    forall P Q b U e (pU: Proper pequiv U) (pe: Proper pequiv e),
      When_SAT b P Q U e -> ~ eqNodeSet U empty_BoolSet.

The following property is direct from the definitions. Note nonetheless that: The converse is False.

  Lemma Next_round_S_until:
    forall N P e,
      Proper fequiv P -> Proper pequiv e ->
      Next_round P (At_N_rounds N P) e -> At_N_rounds (1+N) P e.

After (S N) rounds implies not P

Lemma After_SN_rounds_notP: forall N P e,
At_N_rounds (S N) P e -> ~P e.

At N rounds impls Eventually P

Lemma At_N_rounds_Eventually: forall N P e,
At_N_rounds N P e -> Eventually P e.

Progress Towards P

Simplfied assumption about an execution converging towards a goal P; if not yet reached, then there should be some enabled node(s).

  Definition progress_P (P: Exec -> Prop) (e: Exec): Prop :=
    Eventually P e ->
    Until (fun e => ~ eqNodeSet (enabled_b (s_hd e)) empty_BoolSet)
          P e.

  Lemma progress_P_is_exec:
    forall P (P_dec: Weak_Dec pequiv P) e,
      is_exec e -> progress_P P e.
  Lemma progress_P_contd:
    forall P e g, progress_P P (s_cons g e)
                  -> ~ P (s_cons g e) -> progress_P P e.

  Lemma progress_P_now:
    forall P e, progress_P P e -> Eventually P e -> ~ P e ->
                ~ eqNodeSet (enabled_b (s_hd e)) empty_BoolSet.

Round Properties

Conversely, Eventually P means that we can reach P within a finite number of rounds.

  Lemma Reachable_Rounds:
    forall P (P_dec: Weak_Dec pequiv P) e (pe: Proper pequiv e),
      Eventually P e -> progress_P P e ->
      exists N , At_N_rounds N P e.

At_N_rounds corresponds to a unique value

  Lemma At_N_Rounds_unique: forall P e N1 N2,
      Proper pequiv P -> Proper pequiv e ->
      At_N_rounds N1 P e ->
      At_N_rounds N2 P e -> N1 = N2.

  Lemma Eventually_When_SAT_At_N_rounds:
    forall P e N, Eventually (At_N_rounds N P) e -> Eventually P e.

  Lemma At_N_rounds_equiv:
    forall P Q (e: Exec), Always (fun e => P e <-> Q e) e ->
                          forall k, At_N_rounds k P e ->
                                    At_N_rounds k Q e.

Functional definition of Rounds,

as long as one can compute the reachability of the predicate.

count_rounds_aux assumes Finally P e (i.e. reachability of P can be computed); it uses a set of unsatisfied nodes, EN.

Either Finally tells that P is reached, hence one round
Or the set of unsatisfied is refreshed by removing moving or neutralized nodes. If this new set is empty, this starts a new round (add 1 and initialize the new set of unsatisfied with the enabled nodes of the current configuration) otherwise we go on the current round.

  Fixpoint count_rounds_aux (P: Exec -> Prop) (g: Env) (e: Exec)
           (UNSAT: Node -> bool) (F: Finally P e) : nat :=
    match F in Finally _ e_ return nat with
    | finally_now _ _ _ => 1

    | finally_not_yet g' e' F' =>
      let NEXT := diffBoolSet UNSAT (act_neut_b (s_cons g e)) in
      if EMPTY all_nodes NEXT
      then 1 + count_rounds_aux g' (enabled_b g') F'
      else count_rounds_aux g' NEXT F'
    end.

count_rounds provides the number of rounds to reach P. It compute the 0 case separately. Otherwise it uses count_rounds_aux and initialize the new set of unsatisfied with the enabled nodes of the initial configuration.

  Definition count_rounds
             (P: Exec -> Prop) (P_dec: Weak_Dec pequiv P)
             (e: Exec) (pe: Proper pequiv e)
             (he: Eventually P e): nat :=
    match (Eventually_Dec_Finally' P_dec pe he) in
          Finally _ e_ return nat with
    | finally_now _ _ _ => 0
    | finally_not_yet g' e' F' =>
      count_rounds_aux g' (enabled_b g') F'
    end.

  Lemma count_rounds_aux_S: forall P g e U (F: Finally P e),
      count_rounds_aux g U F <> 0.

  Theorem round_functional_equivalence:
    forall P (P_dec: Weak_Dec pequiv P) (P_compat: Proper pequiv P)
           e (pe: Proper pequiv e) (he: Eventually P e)
           (pP: progress_P P e) N,
      count_rounds P_dec pe he = N <-> At_N_rounds N P e.

Tools to cut an execution into pieces; each piece

corresponds to one round.

They can compute iteratively the partition of the execution into rounds: those tools allow to go through an execution round after round. Thus, we provide tools to access the first round of the execution. In addition and in the case, the first round is finite, those tools exhibit for the round its list of configurations. Such a list is called a prefix (of execution).

Infinite round

  CoInductive Infinite_first_round: (Node -> bool ) -> Exec -> Prop :=
    Infinite_First_round_ongoing: forall UNSAT1 U' g e,
      ~eqNodeSet UNSAT1 empty_BoolSet ->
      Proper eqNodeSet UNSAT1 ->
      let U_ := (diffBoolSet UNSAT1 (act_neut_b (s_cons g e))) in
      eqNodeSet U' U_ ->
      Infinite_first_round U' e ->
      Infinite_first_round UNSAT1 (s_cons g e).

  Definition infinite_first_round (e:Exec) :Prop :=
    Infinite_first_round (enabled_b (s_hd e)) e.

Finite rounds - first round: we define how to acces to the

first round of an execution, and its corresponding prefix

finite_first_round_contd e l c ensures that the first round of e is finite, plus the fact that:

l is the list of configurations at the beginning of e and represents the first round;
c is a suffix of e such that the second round begins at c
the concatenation of l and c (see Function cat_prefix) is

exactly e.

nb: l and c are proper are by definition.

  Inductive Finite_first_round_contd:
    (Node -> bool ) -> Exec -> list Env -> Exec -> Prop :=
  | Finite_First_round_done: forall U e lbeg contd,
      eqNodeSet U empty_BoolSet -> e =~= contd -> lbeg = nil ->
      Finite_first_round_contd U e lbeg contd
  | Finite_First_round_ongoing: forall U g gg e lbeg contd,
      ~ eqNodeSet U empty_BoolSet -> Proper eqNodeSet U ->
      let Udiff := (diffBoolSet U (act_neut_b (s_cons g e))) in
      Finite_first_round_contd Udiff e lbeg contd -> g =~= gg ->
      Finite_first_round_contd U (s_cons g e) (gg :: lbeg) contd.

  Definition no_round e: Prop :=
    eqNodeSet (enabled_b (s_hd e)) empty_BoolSet.

  Lemma terminal_no_round:
    forall e (pe: Proper pequiv e),
      no_round e <-> terminal (s_hd e).

  Definition finite_first_round_contd
             (e: Exec) (lbeg: list Env) (contd: Exec): Prop :=
    ~ no_round e /\
    Finite_first_round_contd (enabled_b (s_hd e)) e lbeg contd.

Finite rounds - after k rounds: we define how to acces to

the first k-th rounds of an execution, and the corresponding prefix.

after_k_rounds k e l c ensures that the first k rounds of e are finite, plus the fact that:

l is the list of configurations at the beginning of e and represents those k rounds;
c is a suffix of e such that the (k+1)-th round begins at c
the concatenation of l and c (see Function cat_prefix) is

exactly e.

nb: l and c are proper are by definition.

  Inductive after_k_rounds: nat -> Exec -> list Env -> Exec -> Prop :=
  | akr_0: forall e l c, e =~= c -> l =~= nil -> after_k_rounds 0 e l c
  | akr_more: forall k e l c cc l' lc,
      finite_first_round_contd e l' cc ->
      after_k_rounds k cc lc c ->
      l =~= l' ++ lc ->
      after_k_rounds (S k) e l c.

c is a suffix of e

  Lemma Ffrc_suffix:
    forall U e l c, Finite_first_round_contd U e l c ->
                    is_suffix e c.

  Lemma ffrc_suffix:
    forall e l c, finite_first_round_contd e l c -> is_suffix e c.

    Lemma akr_suffix:
    forall k (e: Exec) l c, after_k_rounds k e l c -> is_suffix e c.

List and suffix of executions are ensured to be pequiv:

  Lemma Ffrc_pequiv_suf:
    forall U e l c, Finite_first_round_contd U e l c ->
                    Proper pequiv c.

  Lemma ffrc_pequiv_suf:
    forall e l c, finite_first_round_contd e l c ->
                  Proper pequiv c.

  Lemma Ffrc_pequiv_list:
    forall l U e c, Proper pequiv e ->
                    Finite_first_round_contd U e l c ->
                    Proper pequiv l.

  Lemma ffrc_pequiv_list:
    forall e l c, Proper pequiv e ->
                  finite_first_round_contd e l c ->
                  Proper pequiv l.

  Lemma akr_pequiv_suf:
    forall k e l c, after_k_rounds k e l c -> Proper pequiv c.

  Lemma akr_pequiv_list:
    forall k e l c,
      Proper pequiv e ->
      after_k_rounds k e l c -> Proper pequiv l.

Compatibility

  Global Instance Finite_first_round_contd_compat:
    Proper pequiv Finite_first_round_contd.

  Instance no_round_compat: Proper pequiv no_round.

  Global Instance finite_first_round_contd_compat:
    Proper pequiv finite_first_round_contd.

  Instance after_k_rounds_compat: Proper pequiv after_k_rounds.

Inversion tools for finite_first_round_contd

  Lemma Ffrc_inv1:
    forall e U c, Finite_first_round_contd U e nil c ->
                  e =~= c /\ eqNodeSet U empty_BoolSet.

  Lemma Ffrc_inv2:
    forall e g l a U c,
      Finite_first_round_contd U (s_cons g e) (a :: l) c ->
      g =~= a /\
      ~ eqNodeSet U empty_BoolSet /\
      Proper eqNodeSet U /\
      Finite_first_round_contd
        (diffBoolSet U (act_neut_b (s_cons g e))) e l c.

  Lemma Ffrc_inv3:
    forall g l a U c,
      ~ Finite_first_round_contd U (s_one g) (a :: l) c.

  Lemma ffrc_inv1:
    forall e c, ~ finite_first_round_contd e nil c.

  Lemma ffrc_not_nil:
    forall e l c, finite_first_round_contd e l c -> l <> nil.

How to cat a prefix of execution (list of configurations)

and its suffix:

  Fixpoint cat_prefix (l: list Env) (e: Exec): Exec :=
    match l with nil => e
            | a :: ll => s_cons a (cat_prefix ll e) end.

  Instance cat_prefix_compat: Proper pequiv cat_prefix.
  Lemma cat_prefix_app:
    forall l ll e, cat_prefix (l ++ ll) e = cat_prefix l (cat_prefix ll e).

  Lemma cat_prefix_last:
    forall e b l,
      Proper pequiv e -> Proper pequiv b -> Proper pequiv l ->
      cat_prefix (l ++ b :: nil) e =~= cat_prefix l (s_cons b e).

  Lemma cat_prefix_proper_r:
    forall l c lc, cat_prefix l c =~= lc -> Proper pequiv c.

  Lemma cat_prefix_proper_l:
    forall l c lc, cat_prefix l c =~= lc -> Proper pequiv l.

  Lemma cat_prefix_app_eq:
    forall l a m b, l =~= m -> cat_prefix l a =~= cat_prefix m b ->
                    a =~= b.

  Lemma Forever_cat_prefix:
    forall P l e, Forever P (cat_prefix l e) -> Forever P e.

  Lemma is_suffix_cat_prefix:
    forall l (a b: Exec),
      is_suffix a b -> is_suffix (cat_prefix l a) b.

e is exactly the concatenation of l and c

  Lemma Ffrc_rebuild:
    forall l U e c,
      Proper pequiv e -> Finite_first_round_contd U e l c ->
      cat_prefix l c =~= e.

  Lemma ffrc_rebuild:
    forall e l c,
      Proper pequiv e -> finite_first_round_contd e l c ->
      cat_prefix l c =~= e.

  Lemma after_k_rounds_rebuild:
    forall k e l c,
      Proper pequiv e ->
      after_k_rounds k e l c -> cat_prefix l c =~= e.

The suffix of an execution is also an execution

  Lemma ffr_is_exec:
    forall (e: Exec) l c,
      is_exec e -> finite_first_round_contd e l c -> is_exec c.

Properties of prefix of execution (list of configurations)

check_list_ev_strict P l e means that

P eventually holds at some point in l
the definition is strict meaning before P holds, it does not hold

  Inductive check_list_ev_strict: (Exec -> Prop) -> list Env -> Exec -> Prop :=
    here: forall (P: Exec -> Prop) l c, P (cat_prefix l c) -> check_list_ev_strict P l c
  | further: forall P a l c, ~ P (cat_prefix (a :: l) c) ->
                             check_list_ev_strict P l c ->
                             check_list_ev_strict P (a :: l) c.

check_list_ev_strict P l e means that

P eventually holds at some point in l
the definition is not strict

  Inductive check_list_ev: (Exec -> Prop) -> list Env -> Exec -> Prop :=
    here_: forall (P: Exec -> Prop) l c, P (cat_prefix l c) -> check_list_ev P l c
  | further_: forall P a l c, check_list_ev P l c ->
                              check_list_ev P (a :: l) c.

check_list_al P l e means that

P holds at any configuration in l

  Inductive check_list_al: (Exec -> Prop) -> list Env -> Exec -> Prop :=
    end_: forall (P: Exec -> Prop) l c, l = nil ->
                                        check_list_al P l c
  | fur_: forall P a l c, check_list_al P l c ->
                          P (cat_prefix (a :: l) c) ->
                          check_list_al P (a :: l) c.

  Instance check_list_ev_strict_compat: Proper pequiv check_list_ev_strict.

  Instance check_list_ev_compat_impl:
    Proper ((pequiv ==> impl ) ==> pequiv ==> pequiv ==> impl) check_list_ev.

  Instance check_list_ev_compat: Proper pequiv check_list_ev.
  Instance check_list_al_compat: Proper pequiv check_list_al.

About check_list_al

  Lemma check_list_al_all:
    forall P l e, l <> nil -> check_list_al P l e -> P (cat_prefix l e).

  Lemma check_list_al_app_l:
    forall P l1 l2 e,
      check_list_al P (l1 ++ l2) e ->
      check_list_al P l1 (cat_prefix l2 e).

  Lemma check_list_al_app_r:
    forall P l1 l2 e,
      check_list_al P (l1 ++ l2) e ->
      check_list_al P l2 e.

About check_list_ev_strict and check_list_ev

  Lemma check_list_ev_strict_not_strict:
    forall P l e, check_list_ev_strict P l e -> check_list_ev P l e.

  Lemma check_list_ev_not_strict_strict:
    forall P l e
           (Pdec: Always (fun e => P e \/ ~P e) (cat_prefix l e)),
      check_list_ev P l e -> check_list_ev_strict P l e.

About check_list_ev

  Lemma check_list_ev_app:
    forall P a b e, check_list_ev P (a ++ b) e ->
                    check_list_al (fun e => ~P e) a (cat_prefix b e) ->
                    check_list_ev P b e.
  Lemma check_list_ev_app_r:
    forall P a b e, check_list_ev P b e ->
                    check_list_ev P (a ++ b) e.

  Lemma check_list_ev_app_l:
    forall P a b e, check_list_ev P a (cat_prefix b e) ->
                    check_list_ev P (a ++ b) e.

  Lemma check_list_ev_end:
    forall (P: Exec -> Prop) l e, P e -> check_list_ev P l e.

About check_list_ev_strict

When check_list_ev_strict P l c holds, this tools cuts l into two lists l1 and l2 such that

P never holds on l1
P holds at (cat_prefix l2 c).

  Lemma find_ev:
    forall P l c,
      check_list_ev_strict P l c ->
      exists l1 l2 ,
        l = l1 ++ l2 /\
        check_list_al (fun e => ~ P e) l1 (cat_prefix l2 c) /\
        P (cat_prefix l2 c).

Fundamental lemma when dealing with rounds:

when a node is enabled at the beginning of a round then it is activated or neutralized before the end of this round.

  Lemma round_en_act:
    forall e l b c,
      Proper pequiv e ->
      finite_first_round_contd e (l ++ b :: nil) c ->
      forall n,
        enabled_b (s_hd e) n = true ->
        check_list_ev_strict (fun e' => act_neut_b e' n = true) l (s_cons b c).

Relation between finite_first_round_contd and At_N_rounds

For an execution e,

if P holds at e then At_N_rounds 0 P e
otherwise, in case of finite first round, and if P is

eventually reached in this round then At_N_rounds 1 P e

otherwise we provide a lemma to prepare recursion:

Assume finite_first_round_contd e l c and Q c and P is never satisfied during the round, then Next_round P Q e

  Lemma At_N_rounds_0: forall e P, At_N_rounds 0 P e <-> P e.

  Lemma This_round_ffr:
    forall P (pc: Proper pequiv P) e (pe: Proper pequiv e) c l,
      ~ P e -> check_list_ev_strict P l c ->
      finite_first_round_contd e l c -> This_round P P e.
  Lemma At_N_rounds_1:
    forall P (pc: Proper pequiv P) e (pe: Proper pequiv e) c l,
      ~ P e -> check_list_ev_strict P l c ->
      finite_first_round_contd e l c -> At_N_rounds 1 P e.

  Lemma Next_round_ffr:
    forall P (pc: Proper pequiv P)
           (Q: Exec -> Prop) (qc: Proper pequiv Q)
           e (pe: Proper pequiv e) c l,
      Q c -> check_list_al (fun e => ~ P e) l c ->
      finite_first_round_contd e l c -> Next_round P Q e.
  Lemma Next_round_ffr_converse:
    forall P (pc: Proper pequiv P)
           (Q: Exec -> Prop) (qc: Proper pequiv Q)
           e (pe: Proper pequiv e),
      Next_round P Q e -> exists c l ,
        Q c /\ check_list_al (fun e => ~ P e) l c /\
        finite_first_round_contd e l c.

K Rounds

The definition of after_k_rounds, for (k+1) exhibits the first round and then the k next rounds. This definition copies the way At_N_rounds is defined. Nevertheless, in proof of round complexity, the induction is usually the other way round; namely, having letting pass k rounds, we reason about the last one (the (k+1)-th) and observe how properties about the last configurations have evolved.

Therefore, we provide tools to reverse the after_k_rounds definition:

if e starts with k rounds in l before c, and if c contains one

round ll before c', then e starts with (k+1) rounds in (l++ll) before c'

conversely, if e starts with (k+1) rounds l before c, then l can

be split into two parts l' and ll such that

e starts with k rounds l' before some execution c'

c' starts with a finite round ll before c.

similarly (but when looking for a target maybe reached before k

rounds), if e starts with (k+1) rounds (l1++l2) before c, then

some k'<=k rounds has elapsed on a prefix of l1

and a (k'+1)-th round can be found

  Lemma after_k_rounds_add:
    forall k l ll e c c', after_k_rounds k e l c ->
                          finite_first_round_contd c ll c' ->
                          after_k_rounds (S k) e (l ++ ll) c'.

  Lemma after_k_rounds_inv_rev:
    forall k e l c,
      Proper pequiv e ->
      after_k_rounds (S k) e l c ->
      exists l' ll c',
        l =~= l' ++ ll /\
        after_k_rounds k e l' c' /\
        finite_first_round_contd c' ll c.

  Lemma cut_akr:
    forall e c k l1 l2,
      Proper pequiv e ->
      after_k_rounds (S k) e (l1 ++ l2) c ->
      exists k' c' a la b lb ,
        k' <= k /\ l1 =~= la ++ a /\ l2 =~= b ++ lb /\
        after_k_rounds k' e la (cat_prefix (a ++ b) c') /\
        finite_first_round_contd (cat_prefix (a ++ b) c') (a ++ b) c'
        /\ (l1 <> nil -> a <> nil ).

Relation between finite_first_round_contd, after_k_rounds and

At_N_rounds

To prove At_N_rounds (k+1) P e, prove the following sufficient conditions: * e constains k rounds in l before c and never satifies P during l * c contains one round in l' before c' and satisfies P at some point in l'

Proving the exact number of rounds is usually very difficult and the results usually deals with upper bound. This is the aim of the following lemma.

To prove that there exists some k' <= k such that At_N_rounds k' P e, prove the following sufficient conditions: * e constains k rounds in l before c * e and satisfies P at some point in l nb: to get rid of the fact that the definition is strict (it would require strict eventuality), we require an additionnal assumption: Always (fun e => P e \/ ~P e) e, namely P is classical for e and all its suffices.

  Lemma At_N_rounds_ind_inf:
    forall k P (pc: Proper pequiv P)
           e (pe: Proper pequiv e) c l,
      after_k_rounds k e l c ->
      check_list_al (fun e => ~P e) l c -> ~ P c ->
      At_N_rounds 1 P c ->
      At_N_rounds (S k) P e.

  Lemma At_N_rounds_ind:
    forall k P (pc: Proper pequiv P)
           e (pe: Proper pequiv e) c c' l l',
      after_k_rounds k e l c ->
      check_list_al (fun e => ~P e) l c -> ~ P c ->
      finite_first_round_contd c l' c' ->
      check_list_ev_strict P l' c' ->
      At_N_rounds (S k) P e.
  Lemma At_N_rounds_ind_le:
    forall k P (pc: Proper pequiv P)
           e (pe: Proper pequiv e)
           (Pdec: Always (fun e => P e \/ ~P e) e)
           c l,
      after_k_rounds k e l c ->
      check_list_ev P l c ->
      exists k', k' <= k /\ At_N_rounds k' P e.

Relation between weaklyfair daemon and rounds

Properties for weakly execution:

for an execution, being weakly fair is equivalent to having all

its rounds finite.

if the execution is not already terminal at its first

configuration, then we can pick a finite first round

  Inductive Finite_first_round: (Node -> bool ) -> Exec -> Prop :=
  | Finite_First_round_done_: forall UNSAT e,
      eqNodeSet UNSAT empty_BoolSet ->
      Finite_first_round UNSAT e
  | Finite_First_round_ongoing_: forall UNSAT1 U' g e,
      ~eqNodeSet UNSAT1 empty_BoolSet ->
      Proper eqNodeSet UNSAT1 ->
      let U'_ := (diffBoolSet UNSAT1 (act_neut_b (s_cons g e))) in
      eqNodeSet U' U'_ ->
      Finite_first_round U' e ->
      Finite_first_round UNSAT1 (s_cons g e).

  Definition finite_first_round (e:Exec) :Prop :=
    Finite_first_round (enabled_b (s_hd e)) e.

  Lemma Finite_first_round_equiv:
    forall U (e: Exec) (pe: Proper pequiv e),
      Finite_first_round U e <->
      exists c l , Finite_first_round_contd U e l c.
  Lemma finite_first_round_equiv:
    forall e (pe: Proper pequiv e),
      finite_first_round e /\
      ~ eqNodeSet (enabled_b (s_hd e)) empty_BoolSet <->
      exists c l , finite_first_round_contd e l c.

  Definition all_rounds_finite (e:Exec) :Prop :=
    Always finite_first_round e.

  Lemma Weakly_fair_finite_rounds :
    forall e, Proper pequiv e ->
               weakly_fair e <-> all_rounds_finite e.

  Lemma weakly_fair_one_round:
    forall e, Proper pequiv e -> weakly_fair e ->
              ~ terminal (s_hd e) ->
              exists c l , finite_first_round_contd e l c.

At_N_rounds classical (when property is reachable)

  Lemma At_N_rounds_clas:
    forall P e k, Weak_Dec pequiv P -> Proper pequiv P ->
                  Eventually P e -> is_exec e ->
                  At_N_rounds k P e \/ ~At_N_rounds k P e.

*At_N_rounds* covariance

  Lemma When_SAT_cov:
    forall (P1 P2: Exec -> Prop) (Q1 Q2: Exec -> Prop)
           (pc2: Proper pequiv P2) (qc2: Proper pequiv Q2)
           e (pe: Proper pequiv e)
           (eP: Always (fun e => P2 e -> P1 e) e)
           (eQ: Always (fun e => Q1 e -> Q2 e) e)
           strict U,
      When_SAT strict P1 Q1 U e -> When_SAT strict P2 Q2 U e.

  Lemma This_round_cov:
    forall (P1 P2: Exec -> Prop)
           e (pe: Proper pequiv e)
           (eP: Always (fun e => P1 e -> P2 e) e)
           (d2: Always (fun c => P2 c \/ ~ P2 c) e),
      This_round P1 P1 e -> P2 e \/ This_round P2 P2 e.
  Lemma At_N_rounds_1_cov:
    forall (P1 P2: Exec -> Prop)
           e (pe: Proper pequiv e)
           (eP: Always (fun e => P1 e -> P2 e) e)
           (d2: Always (fun c => P2 c \/ ~ P2 c) e),
      At_N_rounds 1 P1 e -> P2 e \/ At_N_rounds 1 P2 e.

  Lemma Next_round_cov:
    forall (P1 P2: Exec -> Prop) (Q1 Q2: Exec -> Prop)
           e (pe: Proper pequiv e)
           (eP: Always (fun e => P1 e -> P2 e) e)
           (eQ: Always (fun e => Q2 e -> Q1 e) e)
           (d2: forall c, is_suffix e c -> P2 c \/ ~ P2 c),
      Next_round Q1 P1 e ->
      P2 e \/ This_round Q2 P2 e \/ Next_round Q2 P2 e.
  Lemma check_list_al_cc:
    forall Q (pq: Proper pequiv Q) l (pl: Proper pequiv l)
           ll c cc,
      check_list_al Q l c -> check_list_al Q ll cc ->
      c =~= cat_prefix ll cc -> check_list_al Q (l ++ ll) cc.

  Lemma find_round_list:
    forall k P (pc: Proper pequiv P) e (pe: Proper pequiv e),
      At_N_rounds (S k) P e ->
      exists l c , after_k_rounds k e l c /\
                  check_list_al (fun e => ~ P e) l c /\
                  At_N_rounds 1 P c.

  Lemma check_list_al_impl:
    forall (P1: Exec -> Prop) (P1c: Proper pequiv P1)
           (P2: Exec -> Prop) (eP: (pequiv ==> impl ) P1 P2)
           l (pl: Proper pequiv l) c (pc: Proper pequiv c)
           (d2: Always (fun c => P1 c \/ ~ P1 c)
                       (cat_prefix l c)),
      check_list_al P2 l c -> exists l' c',
        check_list_al P1 l' c' /\
        cat_prefix l c =~= cat_prefix l' c' /\
        ( l =~= l' \/ ~P1 c' ).

  Lemma At_N_rounds_cov:
    forall (P1: Exec -> Prop) (P1c: Proper pequiv P1)
           (P2: Exec -> Prop) (P2c: Proper pequiv P2)
           e (pe: Proper pequiv e)
           (d2: Always (fun c => P2 c \/ ~ P2 c) e) k1
           (impl2: Always (fun e => P1 e -> P2 e) e),
      At_N_rounds k1 P1 e ->
      exists k2 , k2 <= k1 /\ At_N_rounds k2 P2 e.

Compatibility for Round_complexity with implies:

  Lemma Round_complexity_compat_cov:
    forall n1 n2 (en: n1 == n2)
           (P1: Exec -> Prop) (P1c: Proper pequiv P1)
           (P2: Exec -> Prop) (P2c: Proper pequiv P2)
           (Q1: Exec -> Prop) (Q1c: Proper pequiv Q1)
           (Q2: Exec -> Prop) (Q2c: Proper pequiv Q2)
           (eQ: (pequiv ==> impl ) Q2 Q1)
           (eP: forall e, Q2 e -> Always (fun e => P1 e -> P2 e) e)
           (hp2: forall e, Q2 e -> Proper pequiv e)
           (d2: forall e, Q2 e -> Always (fun c => P2 c \/ ~ P2 c) e),
      Round_complexity Q1 P1 n1 -> Round_complexity Q2 P2 n2.

Proof Schema

Those tools are meant to help the proof designer in order to count the number of rounds, hence finite rounds (at least for all of them but the last one. This is why the tools focus on finite rounds.

First schema: progress by one round

P is the property which is obtained after n rounds
R is the property that should be satisfied after at most n+1 rounds

Obviously, the result requires that R is obtained from P after one more round. The property "(exists cc ll, finite_first_round_contd c ll cc /\ R cc)" contains two conditions

a progress condition, i.e. the existence of a next round
the fact that R can be reach from P in one round

  Lemma schema_one_round_progress:
    forall (P: Exec -> Prop) (R: Exec -> Prop) e n l c,
        after_k_rounds n e l c -> P c ->
        (exists cc ll , finite_first_round_contd c ll cc /\ R cc ) ->
        exists c' l', after_k_rounds (S n) e l' c' /\ R c'.

Corollary using At_N_rounds

  Lemma schema_one_round_progress':
    forall (P: Exec -> Prop) (R: Exec -> Prop) (Rc: Proper fequiv R)
           e (pe: Proper pequiv e)
           (clas: Always (fun e0 : Stream => R e0 \/ ~ R e0) e) n l c,
        after_k_rounds n e l c -> P c ->
        (exists cc ll , finite_first_round_contd c ll cc /\ R cc ) ->
        exists n', n' <= S n /\ At_N_rounds n' R e.

Induction Schema: progress by B rounds

  Lemma schema_round_induction:
    forall (Q: Exec -> Prop) (Qc: Proper pequiv Q)
           (P: nat -> Exec -> Prop) (Pc: Proper pequiv P)
           (B: nat) (e: Exec) (pe: Proper pequiv e),
      Always Q e ->
      (forall k, k <= B -> Always (fun e => P k e \/ ~ P k e) e ) ->
      (forall k, k <= B ->
                 Always (fun e => ~ P k e ->
                                  exists cc ll , finite_first_round_contd e ll cc) e ) ->
      P 0 e ->
      (forall k e l c, k < B ->
                       Q e -> P k e ->
                       finite_first_round_contd e l c -> P (S k) c )
      ->
      exists n c l , n <= B /\ after_k_rounds n e l c /\ P B c.

Corollary using At_N_rounds

  Lemma schema_round_induction':
    forall (Q: Exec -> Prop) (Qc: Proper pequiv Q)
           (P: nat -> Exec -> Prop) (Pc: Proper pequiv P)
           (B: nat) (e: Exec) (pe: Proper pequiv e),
      Always Q e ->
      (forall k, k <= B -> Always (fun e => P k e \/ ~ P k e) e ) ->
      (forall k, k <= B ->
                 Always (fun e => ~ P k e ->
                                  exists cc ll , finite_first_round_contd e ll cc) e ) ->
      P 0 e ->
      (forall k e l c, k < B ->
                       Q e -> P k e ->
                       finite_first_round_contd e l c -> P (S k) c )
      ->
      exists n , n <= B /\ At_N_rounds n (P B) e.

Schema of proofs - weakly fair daemon

  Lemma schema_round_induction_wf:
    forall (Q: Exec -> Prop) (Qc: Proper pequiv Q)
           (P: nat -> Exec -> Prop) (Pc: Proper pequiv P)
           (B: nat) (e: Exec) (pe: Proper pequiv e),
      Always Q e -> weakly_fair e ->
      (forall k, k <= B -> Always (fun e => P k e \/ ~ P k e) e ) ->
      (forall k, k <= B ->
                 Always (fun e => ~ P k e -> ~ terminal (s_hd e)) e ) ->
      P 0 e ->
      (forall k e l c, k < B ->
                       Q e -> P k e ->
                       finite_first_round_contd e l c -> P (S k) c )
      ->
      exists n c l , n <= B /\ after_k_rounds n e l c /\ P B c.

Corollary using At_N_rounds

  Lemma schema_round_induction_wf':
    forall (Q: Exec -> Prop) (Qc: Proper pequiv Q)
           (P: nat -> Exec -> Prop) (Pc: Proper pequiv P)
           (B: nat) (e: Exec) (pe: Proper pequiv e),
      Always Q e -> weakly_fair e ->
      (forall k, k <= B -> Always (fun e => P k e \/ ~ P k e) e ) ->
      (forall k, k <= B ->
                 Always (fun e => ~ P k e -> ~ terminal (s_hd e)) e ) ->
      P 0 e ->
      (forall k e l c, k < B ->
                       Q e -> P k e ->
                       finite_first_round_contd e l c -> P (S k) c )
      ->
      exists n , n <= B /\ At_N_rounds n (P B) e.

Relation between At_N_rounds and round extraction tools

At_N_rounds n P e <-> n = 0 /\ P e or n = S n' /\ after_k_rounds n' e l c /\ ~ P c /\ never P on l /\ either finite_first_round c l' c' /\ P in l' or infinite_first_round c /\ Eventually P on c

The last disjunction is not tractable. This characterization would be useless. We propose an inductive property to check the last disjunction; this property goes through the execution suffix c until reaching P, meanwhile it checks that the current round is not over.

  Inductive Check_P_in_First_Round (P: Exec -> Prop): NodeSet ->Exec -> Prop :=
  | CFR_stop: forall U e, P e -> Check_P_in_First_Round P U e
  | CFR_on: forall U g e,
      Check_P_in_First_Round P (diffBoolSet U (act_neut_b (s_cons g e))) e ->
      ~ eqNodeSet U empty_BoolSet ->
      Check_P_in_First_Round P U (s_cons g e).

  Instance Check_P_in_First_Round_compat: Proper pequiv Check_P_in_First_Round.

  Definition check_P_in_first_round P e :=
    ~ P e /\ Check_P_in_First_Round P (enabled_b (s_hd e)) e.

  Instance check_P_in_first_round_compat: Proper pequiv check_P_in_first_round.

  Lemma At_N_rounds_1_Check_P_First_Round:
    forall P (Pc: Proper pequiv P) (P_clas: forall e_, P e_ \/ ~ P e_)
           e (pe: Proper pequiv e),
      At_N_rounds 1 P e <-> check_P_in_first_round P e.

  Lemma At_N_rounds_charac:
    forall P (Pc: Proper pequiv P) (P_clas: forall e_, P e_ \/ ~ P e_)
           e (pe: Proper pequiv e) n,
      At_N_rounds n P e <->
      match n with
      | 0 => P e
      | S n' => exists l c , after_k_rounds n' e l c /\
                            check_list_al (fun e_ => ~ P e_) l c /\
                            check_P_in_first_round P c
      end.

End Rounds.