PADEC - Coq Library

Library Padec.Model.Topologies.Spanning_Tree

A Framework for Certified Self-Stabilization
PADEC Coq Library

Feb 2016

Global imports

From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import Bool.

Local imports

From Padec Require Import SetoidUtil.
From Padec Require Import OptionUtil.
From Padec Require Import ListUtils.
From Padec Require Import RelationA.
From Padec Require Import WellfoundedUtil.
From Padec Require Import FoldRight.
From Padec Require Import ZUtils.
From Padec Require Import Algorithm.

Open Scope signature_scope.
Set Implicit Arguments.

Spanning Tree:

Definition + properties

Section Spanning_Tree.

Defined on a network and on parent pointers (channels)

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

Definition of a spanning tree over the network

Section Is_Tree_Parent_Definition.

Variable (Par: Node -> option Channel).

Tools for spanning tree definition

    Definition tree_parent (x: Node): option Node :=
      option_rect (fun _ => option Node) (peer x) None (Par x).

    Definition is_tree_parent_of (x y: Node): Prop :=
      Some x == tree_parent y.

    Definition directed_tree_path := chain is_tree_parent_of.

    Definition is_tree_parent_or_child_of :=
      symmetric_closure is_tree_parent_of.

    Definition exists_tree_path :=
      reflexive_transitive_closure is_tree_parent_or_child_of.

  End Is_Tree_Parent_Definition.

  Section Is_Tree_Parent_Properties.

    Global Instance tree_parent_compat: Proper fequiv tree_parent.

    Global Instance is_tree_parent_of_compat:
      Proper fequiv is_tree_parent_of.

    Lemma is_tree_parent_of_dec:
      forall (Par: Node -> option Channel), Decider (is_tree_parent_of Par).

    Lemma is_tree_parent_unique:
      forall Par1 Par2,
        Par1 =~= Par2 ->
        forall x1 x2, x1 == x2 ->
                      forall y1 y2 ,
                        is_tree_parent_of Par1 y1 x1 ->
                        is_tree_parent_of Par2 y2 x2 ->
                        y1 == y2.

    Global Instance directed_tree_path_compat:
      Proper (fequiv ==> equiv ==> eqlistA equiv ==> equiv ==> iff)
             directed_tree_path.

  End Is_Tree_Parent_Properties.

  Section Spanning_Tree_Definition.

    Definition is_root (Par: Node -> option Channel) (n: Node): Prop :=
      Par n == None.

    Global Instance is_root_compat: Proper fequiv is_root.

Definition of a spanning tree

The following definition expresses that read-only variables (par: ROEnv) shape a spanning tree as a subgraph of network Net.

First, by construction, each node p has exactly at most one parent (par p).

Predicate parent_is_peer means that any link from p to (par p) is an existing channel in the network.

Predicates is_root_root and is_root_unique say that there exists a unique node root with no parent, i.e., with (par root) equals None.

Finally, predicate no_loop assumes that there is no loop following par pointers, namely, the transitive closure of par is not reflexive.

    Class spanning_tree (root: Node) (Par: Node -> option Channel): Prop :=
      {
        parent_is_peer:
          forall (n: Node) (c: Channel), Par n == Some c ->
                                         exists m , is_channel n c m;
        is_root_root: is_root Par root;
        is_root_unique:
          forall (n1 n2: Node), is_root Par n1 -> is_root Par n2 -> n1 == n2;
        no_loop: forall (p: Node),
            ~ transitive_closure (is_tree_parent_of Par) p p
      }.

Direct results on the spanning tree definition

Global Instance spanning_tree_compat: Proper fequiv spanning_tree.

the no_loop assumption of span_tree implies that is_tree_parent_of is a well-founded order (this will be used, later, for induction proof).

    Lemma WF_par:
      forall (root: Node) (Par: Node -> option Channel),
        Proper fequiv Par -> spanning_tree root Par ->
        well_founded (is_tree_parent_of Par).

the no_loop assumption of span_tree implies that is_tree_child_of, namely (flip is_tree_parent_of) is a well-founded order (this will be used, later, for induction proof).

    Lemma WF_child:
      forall (root: Node) (Par: Node -> option Channel),
        Proper fequiv Par -> spanning_tree root Par ->
        well_founded (flip (is_tree_parent_of Par)).

  End Spanning_Tree_Definition.

End Spanning_Tree.

Definition Spanning_Tree_Network_assumption {Chans: Channels}
           (Net: Network)
           (tested_par: Node -> option Channel): Prop :=
  exists root , spanning_tree root tested_par.

Global Instance Spanning_Tree_Network_assumption_compat:
  forall {Chans: Channels} Net,
    Proper fequiv (Spanning_Tree_Network_assumption Net).

Section Spanning_Tree_Symmetric_Network.

  Context {Chans: Channels} {Net: Symmetric_Network}.

  Section Spanning_Tree_Properties.

Algorithm father_dec computes

either the tree father with the associated proof
or a proof that the node is the root

    Lemma father_dec:
      forall (root: Node) (Par: Node -> option Channel),
        spanning_tree root Par ->
        forall (n: Node), {m | is_tree_parent_of Par m n } + {is_root Par n }.

    Lemma non_root_has_parent:
      forall (root: Node) (Par: Node -> option Channel),
        spanning_tree root Par ->
        forall (n: Node), ~is_root Par n ->
                          exists m , (is_tree_parent_of Par m n ).

    Lemma parent_is_peer_prop:
      forall (root: Node) (Par: Node -> option Channel),
        spanning_tree root Par ->
        forall (n child: Node), is_tree_parent_of Par n child
                                -> InA equiv child
                                       (map_filter (peer n) (peers n)).

    Lemma path_to_root:
      forall (root: Node) (Par: Node -> option Channel),
        Proper fequiv Par ->
        spanning_tree root Par ->
        forall (n: Node), exists (p: list Node ),
            (directed_tree_path Par root p n ).

  End Spanning_Tree_Properties.

Children defined using local information only

  Section Local_Children.

    Definition Local_IsChild (peers: list Channel)
               (peer_Par: Channel -> option Channel)
               (reply: Channel -> Channel)
               (c: Channel): bool :=
      option_rect (fun _ => bool)
                   (fun s => dec2b Channel_dec s (reply c))
                   false
                   (peer_Par c) .

    Definition Local_Children (peers: list Channel)
               (peer_Par: Channel -> option Channel)
               (reply: Channel -> Channel)
      := List.filter (Local_IsChild peers peer_Par reply) peers.

    Global Instance Local_IsChild_compat:
      Proper (equivlistA equiv ==> fequiv) Local_IsChild.

    Global Instance Local_Children_compat:
      Proper (equivlistA equiv ==> fequiv ==> fequiv
                         ==> equivlistA equiv) Local_Children.

    Lemma Local_IsChild_locality:
      forall ps1 ps2 lPar1 lPar2 rev1 rev2,
      forall c, InA equiv c ps1 -> lPar1 c == lPar2 c ->
                rev1 c == rev2 c ->
                Local_IsChild ps1 lPar1 rev1 c =
                Local_IsChild ps2 lPar2 rev2 c.

    Lemma Local_Children_locality:
      forall ps1 ps2 lPar1 lPar2 rev1 rev2,
        Proper fequiv lPar1 -> Proper fequiv lPar2 ->
        Proper fequiv rev1 -> Proper fequiv rev2 ->
        equivlistA equiv ps1 ps2 ->
        (forall c, InA equiv c ps1 -> lPar1 c == lPar2 c /\
                                      rev1 c == rev2 c ) ->
        equivlistA equiv (Local_Children ps1 lPar1 rev1)
                   (Local_Children ps2 lPar2 rev2).

  End Local_Children.

  Section Children.

    Definition IsChild (Par: Node -> option Channel)
               (n: Node) (c: Channel): bool :=
      Local_IsChild (peers n)
                    (fun c => match (peer n c) with None => None
                                               | Some x => Par x end)
                    (reverse n) c.

    Lemma Is_Child_is_tree_parent_of:
      forall Par n m,
        Proper fequiv Par ->
        ((exists c , Par m == Some c /\
                    IsChild Par n (reverse m c) = true /\
                    is_channel m c n )
         <-> is_tree_parent_of Par n m ).

    Global Instance IsChild_compat: Proper fequiv IsChild.

    Definition Children
               (Par: Node -> option Channel) (n: Node): list Channel :=
      List.filter (IsChild Par n) (peers n).

    Lemma Children_equiv:
      forall Par n,
        Proper fequiv Par ->
        eqlistA equiv (Children Par n)
                (Local_Children (peers n)
                                (fun c: Channel =>
                                   match (peer n c) with None => None
                                                    | Some x => Par x end)
                                (reverse n)).

    Global Instance Children_compat:
      Proper (fequiv ==> equiv ==> equivlistA equiv) Children.

    Lemma Children_inv:
      forall (Par: Node -> option Channel),
        Proper fequiv Par ->
        forall (n: Node) (c: Channel),
          InA equiv c (Children Par n) ->
          exists m , is_channel n c m /\ is_tree_parent_of Par n m.

    Lemma InA_Children:
      forall (Par: Node -> option Channel),
        Proper fequiv Par ->
        forall (n m: Node),
          is_tree_parent_of Par n m <->
          exists (c: Channel ), is_channel n c m /\
                               InA equiv c (Children Par n).

  End Children.

End Spanning_Tree_Symmetric_Network.

Unset Implicit Arguments.
Close Scope signature_scope.