PADEC - Coq Library
Library Padec.Model.Topologies.Tree_topology
A Framework for Certified Self-Stabilization
PADEC Coq Library
- March 2017
- first author: Benjamin Collet
Global imports
From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import ZArith.
From Coq Require Import Lia.
From Coq Require Import SetoidClass.
From Coq Require Import ZArith.
From Coq Require Import Lia.
Local imports
From Padec Require Import SetoidUtil.
From Padec Require Import OptionUtil.
From Padec Require Import NatUtils.
From Padec Require Import ListUtils.
From Padec Require Import FoldRight.
From Padec Require Import RelModel.
From Padec Require Import Algorithm.
From Padec Require Import RelationA.
Open Scope nat_scope.
Open Scope signature.
Global Instance proj1_sig_compat {A} `{SA: Setoid A} (P: A -> Prop): Proper pequiv (@proj1_sig _ P).
Lemma app_cons_equivlist {A: Type} (eqA: relation A):
forall a l1 l2, equivlistA eqA (l1 ++ a::l2) (a:: l1 ++ l2).
Lemma fold_right_map {A: Type} {SA: Setoid A}:
forall (f: A -> A -> A) (f_compat: Proper pequiv f)
(g: A -> A)
(l: list A) x
(commute1: forall a, f (g a) x == g (f a x))
(commute2: forall a b, f (g a) (g b) == g (f a b)),
l <> nil -> fold_right f x (map g l) == g (fold_right f x l).
Lemma fold_right_max_ge:
forall l x, fold_right max x l >= x.
Lemma fold_right_max_ge2:
forall l x, l <> nil -> forall y, In y l -> fold_right max x l >= y.
Lemma fold_right_max_exact:
forall l a, l <> nil -> In a l ->
(forall b, In b l -> b <= a) ->
a = fold_right max 0 l.
Section Max_All_In.
Variable (A: Type) (SA: PartialSetoid A)
(eqA_dec: Decider (pequiv (A := A)))
(all: list A) (all_prop: forall a, InA pequiv a all)
(f: A -> nat) (f_compat: Proper pequiv f).
Lemma arg_max: all <> nil -> { max | forall y, f max >= f y}.
End Max_All_In.
Section Power_option.
Variable (A: Type).
Definition opt_bind (f: A -> option A): option A -> option A :=
fun x => match x with
None => None
| Some x => f x
end.
Global Instance opt_bind_compat eqA:
Proper ((eqA ==> eqoptionA eqA) ==> eqoptionA eqA ==> eqoptionA eqA) opt_bind.
Definition power_opt (f: A -> option A) (n: nat): A -> option A :=
fun x => power (opt_bind f) n (Some x).
Global Instance power_opt_compat eqA:
Proper ((eqA ==> eqoptionA eqA) ==> @eq nat ==> eqA ==> eqoptionA eqA) power_opt.
Lemma power_opt_0: forall f x, power_opt f 0 x = Some x.
Lemma power_opt_None: forall f n, power (opt_bind f) n None = None.
Lemma S_power_opt: forall f n x,
power_opt f (S n) x = (opt_bind f) (power_opt f n x).
Lemma power_opt_S: forall f n x,
power_opt f (S n) x = opt_bind (power_opt f n) (f x).
Lemma power_opt_add: forall f n p x,
power_opt f (n + p) x = opt_bind (power_opt f n) (power_opt f p x).
Lemma power_opt_mult: forall f n p x,
power_opt f (n * p) x = power_opt (power_opt f n) p x.
End Power_option.
From Padec Require Import OptionUtil.
From Padec Require Import NatUtils.
From Padec Require Import ListUtils.
From Padec Require Import FoldRight.
From Padec Require Import RelModel.
From Padec Require Import Algorithm.
From Padec Require Import RelationA.
Open Scope nat_scope.
Open Scope signature.
Global Instance proj1_sig_compat {A} `{SA: Setoid A} (P: A -> Prop): Proper pequiv (@proj1_sig _ P).
Lemma app_cons_equivlist {A: Type} (eqA: relation A):
forall a l1 l2, equivlistA eqA (l1 ++ a::l2) (a:: l1 ++ l2).
Lemma fold_right_map {A: Type} {SA: Setoid A}:
forall (f: A -> A -> A) (f_compat: Proper pequiv f)
(g: A -> A)
(l: list A) x
(commute1: forall a, f (g a) x == g (f a x))
(commute2: forall a b, f (g a) (g b) == g (f a b)),
l <> nil -> fold_right f x (map g l) == g (fold_right f x l).
Lemma fold_right_max_ge:
forall l x, fold_right max x l >= x.
Lemma fold_right_max_ge2:
forall l x, l <> nil -> forall y, In y l -> fold_right max x l >= y.
Lemma fold_right_max_exact:
forall l a, l <> nil -> In a l ->
(forall b, In b l -> b <= a) ->
a = fold_right max 0 l.
Section Max_All_In.
Variable (A: Type) (SA: PartialSetoid A)
(eqA_dec: Decider (pequiv (A := A)))
(all: list A) (all_prop: forall a, InA pequiv a all)
(f: A -> nat) (f_compat: Proper pequiv f).
Lemma arg_max: all <> nil -> { max | forall y, f max >= f y}.
End Max_All_In.
Section Power_option.
Variable (A: Type).
Definition opt_bind (f: A -> option A): option A -> option A :=
fun x => match x with
None => None
| Some x => f x
end.
Global Instance opt_bind_compat eqA:
Proper ((eqA ==> eqoptionA eqA) ==> eqoptionA eqA ==> eqoptionA eqA) opt_bind.
Definition power_opt (f: A -> option A) (n: nat): A -> option A :=
fun x => power (opt_bind f) n (Some x).
Global Instance power_opt_compat eqA:
Proper ((eqA ==> eqoptionA eqA) ==> @eq nat ==> eqA ==> eqoptionA eqA) power_opt.
Lemma power_opt_0: forall f x, power_opt f 0 x = Some x.
Lemma power_opt_None: forall f n, power (opt_bind f) n None = None.
Lemma S_power_opt: forall f n x,
power_opt f (S n) x = (opt_bind f) (power_opt f n x).
Lemma power_opt_S: forall f n x,
power_opt f (S n) x = opt_bind (power_opt f n) (f x).
Lemma power_opt_add: forall f n p x,
power_opt f (n + p) x = opt_bind (power_opt f n) (power_opt f p x).
Lemma power_opt_mult: forall f n p x,
power_opt f (n * p) x = power_opt (power_opt f n) p x.
End Power_option.
Tree Topology
A tree topology on elements of type A is defined as: begin given- a parent function Parent: it represents going one step closer to the root of the tree
- a distance to lowest common ancestor function Dist_LCA: it counts the number of steps to get to a common ancestor
- a relation on A, considered as the equality on the elements of A and
- that each function (Parent, Dist_LCA) is compatible wrt this relation.
Class Tree_Topology {A} `{SA:Setoid A}: Type :=
mkTree {
Parent: A -> option A;
Dist_LCA: A -> A -> nat;
Parent_compat:> Proper fequiv Parent;
Dist_LCA_compat:> Proper fequiv Dist_LCA;
isParent x y := Parent y == Some x;
isRoot x := Parent x == None;
isAncestor x y := Dist_LCA x y = 0;
Dist_LCA_refl: forall x y,
x == y <-> Dist_LCA x y = 0 /\ Dist_LCA y x = 0;
Dist_LCA_root: forall x y, isRoot x -> isAncestor x y;
Dist_LCA_Parent: forall x Px,
isParent Px x <-> Dist_LCA x Px = 1 /\ Dist_LCA Px x = 0;
Dist_LCA_Parent_l: forall x y Px,
isParent Px x -> Dist_LCA Px y = pred (Dist_LCA x y);
Dist_LCA_Parent_r: forall x y Py,
isParent Py y -> ~(isAncestor y x) -> Dist_LCA x y = Dist_LCA x Py;
Dist_LCA_Parent_r_ancestor: forall x y Py,
isParent Py y -> isAncestor y x -> Dist_LCA x y + 1 = Dist_LCA x Py;
all_nodes: list A;
all_nodes_prop: forall n, InA equiv n all_nodes;
}.
Section With_Tree_Topology.
Context {A} `{Tt: Tree_Topology A}.
Instance A_equiv: Equivalence equiv := setoid_equiv.
Lemma eqA_dec: Decider equiv.
Instance isParent_compat: Proper pequiv (@isParent A SA Tt).
Instance isRoot_compat: Proper pequiv isRoot.
Instance isAncestor_compat: Proper pequiv (@isAncestor A SA Tt).
Lemma Dist_LCA_self: forall x, Dist_LCA x x = 0.
Lemma Dist_LCA_Parent_l_not_ancestor: forall x y Px,
isParent Px x -> ~isAncestor x y -> Dist_LCA x y = Dist_LCA Px y + 1.
Lemma isParent_dec: forall x y, {isParent x y} + {~isParent x y}.
Lemma has_Parent_dec: forall x, {y | Parent x == Some y} + {Parent x == None}.
Lemma isParent_unique:
forall x y z, isParent x y -> isParent z y -> x == z.
Lemma isParent_notsym: forall x y, isParent x y -> ~isParent y x.
Lemma isParent_notid: forall x y, isParent x y -> ~ x == y.
Lemma isParent_notsym_isAncestor: forall x y, isParent x y -> ~isAncestor y x.
Lemma isAncestor_dec: forall x y, {isAncestor x y} + {~isAncestor x y}.
Lemma isAncestor_inherit: forall x Px y, isParent Px x -> isAncestor x y -> isAncestor Px y.
Lemma isAncestor_down_inherit:
forall x y Py, isParent Py y -> isAncestor x y -> ~x == y ->
isAncestor x Py.
Lemma isAncestor_Parent: forall x Px, isParent Px x -> isAncestor Px x.
Lemma isAncestor_refl: forall x, isAncestor x x.
Lemma isAncestor_antisym: forall x y,
isAncestor x y -> isAncestor y x -> x == y.
Lemma isAncestor_trans: forall x y z, isAncestor x y -> isAncestor y z -> isAncestor x z.
Lemma uniq_root: forall x y, isRoot x -> isRoot y -> x == y.
Lemma Parent_non_id: forall x y, isParent x y -> ~ x == y.
Lemma have_common_ancestor: forall x y, { a | isAncestor a x /\ isAncestor a y}.
Definition emptyTree := all_nodes = nil.
Lemma not_emptyTree: forall x: A, ~emptyTree.
Lemma emptyTree_root: { r | isRoot r } + { emptyTree }.
Definition getRoot (x: A): {r: A | isRoot r}.
Lemma getRoot_same: forall x y, getRoot x == getRoot y.
Instance getRoot_compat: Proper pequiv getRoot.
Definition isChild x y := Parent x == Some y.
Definition isSibling x y := Parent x == Parent y.
Definition isChild_b :=
(fun x y => if eqoptionA_dec eqA_dec (Parent x) (Some y)
then true else false).
Definition Children x :=
filter (fun cx => isChild_b cx x) all_nodes.
Definition isLeaf x := equivlistA equiv (Children x) nil.
Instance isChild_compat: Proper pequiv isChild.
Instance isSibling_compat: Proper pequiv isSibling.
Instance isChild_b_compat: Proper pequiv isChild_b.
Instance Children_compat:
Proper (equiv ==> equivlistA equiv) Children.
Instance isLeaf_compat: Proper pequiv isLeaf.
Lemma isChild_b_isChild:
forall x y, isChild_b x y = true <-> isChild x y.
Lemma isChild_b_isChild_false:
forall x y, isChild_b x y = false <-> ~isChild x y.
Lemma isChild_b_isParent:
forall x y, isChild_b x y = true <-> isParent y x.
Lemma isChild_isParent:
forall x y, isChild x y <-> isParent y x.
Lemma in_children:
forall x Px, isParent Px x <-> InA equiv x (Children Px).
Lemma childrent_not_nil:
forall x Px, isParent Px x -> ~ equivlistA equiv (Children Px) nil.
Lemma exists_child:
forall x y, Dist_LCA y x > 0 -> Dist_LCA x y = 0 ->
~ equivlistA equiv (Children x) nil.
Lemma two_children:
forall x y z, isChild y x -> isChild z x -> ~ y == z ->
~isAncestor y z.
Lemma Leaf_isAncestor:
forall x y, isLeaf x -> isAncestor x y -> x == y.
Lemma nonLeaf:
forall x, ~isLeaf x -> exists c, isParent x c.
Definition isAncestor_b x y :=
if (Nat.eq_dec 0 (Dist_LCA x y)) then true else false.
Instance isAncestor_b_compat: Proper pequiv isAncestor_b.
Lemma isAncestor_b_isAncestor:
forall x y, isAncestor_b x y = true <-> isAncestor x y.
Lemma isAncestor_b_isAncestor_false:
forall x y, isAncestor_b x y = false <-> ~isAncestor x y.
Lemma isAncestor_b_isParent:
forall x y, isParent x y -> isAncestor_b x y = true.
Definition Height x :=
fold_right max
0
(map (fun y => Dist_LCA y x)
(filter (fun y => isAncestor_b x y) all_nodes)).
Instance Height_compat: Proper pequiv Height.
Lemma max0: forall a b, max a b = 0 -> a = 0 /\ b = 0.
Lemma Height_leaf: forall x, isLeaf x <-> Height x = 0.
Lemma noAncestor:
forall x y, isAncestor x y ->
forall a, ~isAncestor x a -> ~isAncestor y a.
Lemma ancestor_child_exists:
forall x a, ~ x == a -> isAncestor x a -> exists c, isParent x c /\ isAncestor c a.
Lemma Height_isParent:
forall x y, isParent x y -> Height x >= 1 + Height y.
Lemma Height_isParent_exists:
forall x, ~isLeaf x -> exists y, isParent x y /\ Height x = 1 + Height y.
Lemma Height_alt:
forall x, Height x =
fold_right max
0
(map (fun y => 1 + Height y) (Children x)).
Definition Depth (x: A): nat := Dist_LCA x (proj1_sig (getRoot x)).
Instance Depth_compat: Proper pequiv Depth.
mkTree {
Parent: A -> option A;
Dist_LCA: A -> A -> nat;
Parent_compat:> Proper fequiv Parent;
Dist_LCA_compat:> Proper fequiv Dist_LCA;
isParent x y := Parent y == Some x;
isRoot x := Parent x == None;
isAncestor x y := Dist_LCA x y = 0;
Dist_LCA_refl: forall x y,
x == y <-> Dist_LCA x y = 0 /\ Dist_LCA y x = 0;
Dist_LCA_root: forall x y, isRoot x -> isAncestor x y;
Dist_LCA_Parent: forall x Px,
isParent Px x <-> Dist_LCA x Px = 1 /\ Dist_LCA Px x = 0;
Dist_LCA_Parent_l: forall x y Px,
isParent Px x -> Dist_LCA Px y = pred (Dist_LCA x y);
Dist_LCA_Parent_r: forall x y Py,
isParent Py y -> ~(isAncestor y x) -> Dist_LCA x y = Dist_LCA x Py;
Dist_LCA_Parent_r_ancestor: forall x y Py,
isParent Py y -> isAncestor y x -> Dist_LCA x y + 1 = Dist_LCA x Py;
all_nodes: list A;
all_nodes_prop: forall n, InA equiv n all_nodes;
}.
Section With_Tree_Topology.
Context {A} `{Tt: Tree_Topology A}.
Instance A_equiv: Equivalence equiv := setoid_equiv.
Lemma eqA_dec: Decider equiv.
Instance isParent_compat: Proper pequiv (@isParent A SA Tt).
Instance isRoot_compat: Proper pequiv isRoot.
Instance isAncestor_compat: Proper pequiv (@isAncestor A SA Tt).
Lemma Dist_LCA_self: forall x, Dist_LCA x x = 0.
Lemma Dist_LCA_Parent_l_not_ancestor: forall x y Px,
isParent Px x -> ~isAncestor x y -> Dist_LCA x y = Dist_LCA Px y + 1.
Lemma isParent_dec: forall x y, {isParent x y} + {~isParent x y}.
Lemma has_Parent_dec: forall x, {y | Parent x == Some y} + {Parent x == None}.
Lemma isParent_unique:
forall x y z, isParent x y -> isParent z y -> x == z.
Lemma isParent_notsym: forall x y, isParent x y -> ~isParent y x.
Lemma isParent_notid: forall x y, isParent x y -> ~ x == y.
Lemma isParent_notsym_isAncestor: forall x y, isParent x y -> ~isAncestor y x.
Lemma isAncestor_dec: forall x y, {isAncestor x y} + {~isAncestor x y}.
Lemma isAncestor_inherit: forall x Px y, isParent Px x -> isAncestor x y -> isAncestor Px y.
Lemma isAncestor_down_inherit:
forall x y Py, isParent Py y -> isAncestor x y -> ~x == y ->
isAncestor x Py.
Lemma isAncestor_Parent: forall x Px, isParent Px x -> isAncestor Px x.
Lemma isAncestor_refl: forall x, isAncestor x x.
Lemma isAncestor_antisym: forall x y,
isAncestor x y -> isAncestor y x -> x == y.
Lemma isAncestor_trans: forall x y z, isAncestor x y -> isAncestor y z -> isAncestor x z.
Lemma uniq_root: forall x y, isRoot x -> isRoot y -> x == y.
Lemma Parent_non_id: forall x y, isParent x y -> ~ x == y.
Lemma have_common_ancestor: forall x y, { a | isAncestor a x /\ isAncestor a y}.
Definition emptyTree := all_nodes = nil.
Lemma not_emptyTree: forall x: A, ~emptyTree.
Lemma emptyTree_root: { r | isRoot r } + { emptyTree }.
Definition getRoot (x: A): {r: A | isRoot r}.
Lemma getRoot_same: forall x y, getRoot x == getRoot y.
Instance getRoot_compat: Proper pequiv getRoot.
Definition isChild x y := Parent x == Some y.
Definition isSibling x y := Parent x == Parent y.
Definition isChild_b :=
(fun x y => if eqoptionA_dec eqA_dec (Parent x) (Some y)
then true else false).
Definition Children x :=
filter (fun cx => isChild_b cx x) all_nodes.
Definition isLeaf x := equivlistA equiv (Children x) nil.
Instance isChild_compat: Proper pequiv isChild.
Instance isSibling_compat: Proper pequiv isSibling.
Instance isChild_b_compat: Proper pequiv isChild_b.
Instance Children_compat:
Proper (equiv ==> equivlistA equiv) Children.
Instance isLeaf_compat: Proper pequiv isLeaf.
Lemma isChild_b_isChild:
forall x y, isChild_b x y = true <-> isChild x y.
Lemma isChild_b_isChild_false:
forall x y, isChild_b x y = false <-> ~isChild x y.
Lemma isChild_b_isParent:
forall x y, isChild_b x y = true <-> isParent y x.
Lemma isChild_isParent:
forall x y, isChild x y <-> isParent y x.
Lemma in_children:
forall x Px, isParent Px x <-> InA equiv x (Children Px).
Lemma childrent_not_nil:
forall x Px, isParent Px x -> ~ equivlistA equiv (Children Px) nil.
Lemma exists_child:
forall x y, Dist_LCA y x > 0 -> Dist_LCA x y = 0 ->
~ equivlistA equiv (Children x) nil.
Lemma two_children:
forall x y z, isChild y x -> isChild z x -> ~ y == z ->
~isAncestor y z.
Lemma Leaf_isAncestor:
forall x y, isLeaf x -> isAncestor x y -> x == y.
Lemma nonLeaf:
forall x, ~isLeaf x -> exists c, isParent x c.
Definition isAncestor_b x y :=
if (Nat.eq_dec 0 (Dist_LCA x y)) then true else false.
Instance isAncestor_b_compat: Proper pequiv isAncestor_b.
Lemma isAncestor_b_isAncestor:
forall x y, isAncestor_b x y = true <-> isAncestor x y.
Lemma isAncestor_b_isAncestor_false:
forall x y, isAncestor_b x y = false <-> ~isAncestor x y.
Lemma isAncestor_b_isParent:
forall x y, isParent x y -> isAncestor_b x y = true.
Definition Height x :=
fold_right max
0
(map (fun y => Dist_LCA y x)
(filter (fun y => isAncestor_b x y) all_nodes)).
Instance Height_compat: Proper pequiv Height.
Lemma max0: forall a b, max a b = 0 -> a = 0 /\ b = 0.
Lemma Height_leaf: forall x, isLeaf x <-> Height x = 0.
Lemma noAncestor:
forall x y, isAncestor x y ->
forall a, ~isAncestor x a -> ~isAncestor y a.
Lemma ancestor_child_exists:
forall x a, ~ x == a -> isAncestor x a -> exists c, isParent x c /\ isAncestor c a.
Lemma Height_isParent:
forall x y, isParent x y -> Height x >= 1 + Height y.
Lemma Height_isParent_exists:
forall x, ~isLeaf x -> exists y, isParent x y /\ Height x = 1 + Height y.
Lemma Height_alt:
forall x, Height x =
fold_right max
0
(map (fun y => 1 + Height y) (Children x)).
Definition Depth (x: A): nat := Dist_LCA x (proj1_sig (getRoot x)).
Instance Depth_compat: Proper pequiv Depth.
Any node which is down-linked to another has smaller depth than the first one.
Lemma deeper_Depth_step:
forall a child, isParent a child -> Depth child = Depth a + 1.
Lemma deeper_Depth:
forall a b, ~ a == b -> isAncestor a b -> Depth a < Depth b.
forall a child, isParent a child -> Depth child = Depth a + 1.
Lemma deeper_Depth:
forall a b, ~ a == b -> isAncestor a b -> Depth a < Depth b.
Induction Schema
in a subtree T: T is identified by its root rT,
a node n is in T iff isAncestor rT n
Lemma subtree_down_induction:
forall (P: A -> Prop) (P_compat: Proper pequiv P) (rT: A),
P rT ->
(forall n, isAncestor rT n ->
P n -> forall c, InA equiv c (Children n) -> P c) ->
forall n, isAncestor rT n -> P n.
Lemma tree_down_induction:
forall (P: A -> Prop) (P_compat: Proper pequiv P) (rT: A),
isRoot rT -> P rT ->
(forall n, P n -> forall c, InA equiv c (Children n) -> P c) ->
forall n, P n.
Lemma path_down_induction:
forall (P: A -> Prop) (P_compat: Proper pequiv P)
(Q: A -> Prop) (Q_compat: Proper pequiv Q) (Q_classical: forall a, {Q a} + {~Q a}),
(forall m, P m -> ~ Q m ->
exists c, InA equiv c (Children m) /\
(P c \/ Q c)) ->
forall n, P n -> exists d, isAncestor n d /\ Q d.
Lemma tr_d:
forall p q,
transitive_closure (fun x y => Some x == Parent y) p q
-> Dist_LCA q p > 0.
Lemma no_loop:
forall p,
~ transitive_closure (fun x y => Some x == Parent y) p p.
End With_Tree_Topology.
Tree Network
Given a network, this section provides the definition that constrains the network to be endowed with a rooted spanning tree, namely it should have a tree topology (as defined above) on nodes and the Parent function should correspond to channels The tree is bidirectionnal.Set Implicit Arguments.
Section Tree_Network.
Variable (Chans: Channels).
Definition is_spanning (Net: Network)
(topo: Tree_Topology (A := Node)): Prop :=
equivlistA equiv (Algorithm.all_nodes (Network := Net))
(@all_nodes _ _ topo).
Class Up_Tree_Network (Net: Network) :=
mkUTN {
UTN_topo:> Tree_Topology (A := Node);
UTN_parent: Node -> option Channel;
UTN_parent_compat:> Proper fequiv UTN_parent;
UTN_channels_ok:
forall x c, UTN_parent x == Some c ->
exists y, is_channel x c y;
UTN_parent_ok:
forall x y, Parent x == Some y <->
exists c, UTN_parent x == Some c /\
is_channel x c y;
UTN_root_ok:
forall x, Parent x == None <-> UTN_parent x == None
}.
Class Down_Tree_Network (Net: Network) :=
mkDTN {
DTN_topo:> Tree_Topology (A := Node);
DTN_root: Node -> bool;
DTN_root_compat:> Proper fequiv DTN_root;
DTN_children: Node -> list Channel;
DTN_children_compat:> Proper fequiv DTN_children;
DTN_channels_ok:
forall c y, InA equiv c (DTN_children y) ->
exists x, is_channel y c x;
DTN_children_ok:
forall x y, Parent x == Some y <->
exists c, InA equiv c (DTN_children y) /\
is_channel y c x;
DTN_root_ok:
forall x, Parent x == None <-> DTN_root x = true
}.
Class Tree_Network (Net: Symmetric_Network) :=
mkTN {
TN_topo:> Tree_Topology (A := Node);
TN_parent: Node -> option Channel;
TN_parent_compat:> Proper fequiv TN_parent;
TN_children: Node -> list Channel;
TN_children_compat:> Proper fequiv TN_children;
TN_channels_parent_ok:
forall x c, TN_parent x == Some c ->
exists y, is_channel x c y;
TN_channels_children_ok:
forall c y, InA equiv c (TN_children y) ->
exists x, is_channel y c x;
TN_parent_children_ok:
forall x y,
Parent x == Some y <->
exists c, TN_parent x == Some c /\
InA equiv (reverse x c) (TN_children y) /\
is_channel x c y;
TN_root_ok:
forall x, Parent x == None <-> TN_parent x == None
}.
End Tree_Network.
Tree Algorithm
We define what is an algorithm that computes on a spanning tree network: the state of every node should contain the channels defined by the spanning rooted tree network. Those information should be read-only.
Section Tree_Algorithm.
Definition Up_Tree_Network_assumption {Chans: Channels}
(Net: Network)
(UTN: Up_Tree_Network Net)
(tree_parent: Node -> option Channel): Prop :=
tree_parent =~= UTN_parent (Net := Net).
Definition Down_Tree_Network_assumption {Chans: Channels}
(Net: Network)
(DTN: Down_Tree_Network Net)
(tree_children: Node -> list Channel)
(tree_root: Node -> bool): Prop :=
(equiv ==> equivlistA equiv) tree_children (DTN_children (Net := Net)) /\
tree_root =~= DTN_root (Net := Net).
Definition Tree_Network_assumption {Chans: Channels}
(Net: Symmetric_Network)
(TN: Tree_Network Net)
(tree_parent: Node -> option Channel)
(tree_children: Node -> list Channel): Prop :=
tree_parent =~= TN_parent (Net := Net) /\
(equiv ==> equivlistA equiv) tree_children (TN_children (Net := Net)).
Instance Up_Tree_Network_assumption_compat:
forall {Chans: Channels} Net
(UTN: Up_Tree_Network Net),
Proper fequiv (Up_Tree_Network_assumption UTN).
Instance Down_Tree_Network_assumption_compat:
forall {Chans: Channels} Net
(DTN: Down_Tree_Network Net),
Proper ((equiv ==> equivlistA equiv) ==> fequiv ==> equiv)
(Down_Tree_Network_assumption DTN).
Instance Tree_Network_assumption_compat:
forall {Chans: Channels} Net
(TN: Tree_Network Net),
Proper (fequiv ==> (equiv ==> equivlistA equiv) ==> equiv)
(Tree_Network_assumption TN).
End Tree_Algorithm.
Unset Implicit Arguments.
Close Scope nat_scope.
Close Scope signature.
Definition Up_Tree_Network_assumption {Chans: Channels}
(Net: Network)
(UTN: Up_Tree_Network Net)
(tree_parent: Node -> option Channel): Prop :=
tree_parent =~= UTN_parent (Net := Net).
Definition Down_Tree_Network_assumption {Chans: Channels}
(Net: Network)
(DTN: Down_Tree_Network Net)
(tree_children: Node -> list Channel)
(tree_root: Node -> bool): Prop :=
(equiv ==> equivlistA equiv) tree_children (DTN_children (Net := Net)) /\
tree_root =~= DTN_root (Net := Net).
Definition Tree_Network_assumption {Chans: Channels}
(Net: Symmetric_Network)
(TN: Tree_Network Net)
(tree_parent: Node -> option Channel)
(tree_children: Node -> list Channel): Prop :=
tree_parent =~= TN_parent (Net := Net) /\
(equiv ==> equivlistA equiv) tree_children (TN_children (Net := Net)).
Instance Up_Tree_Network_assumption_compat:
forall {Chans: Channels} Net
(UTN: Up_Tree_Network Net),
Proper fequiv (Up_Tree_Network_assumption UTN).
Instance Down_Tree_Network_assumption_compat:
forall {Chans: Channels} Net
(DTN: Down_Tree_Network Net),
Proper ((equiv ==> equivlistA equiv) ==> fequiv ==> equiv)
(Down_Tree_Network_assumption DTN).
Instance Tree_Network_assumption_compat:
forall {Chans: Channels} Net
(TN: Tree_Network Net),
Proper (fequiv ==> (equiv ==> equivlistA equiv) ==> equiv)
(Tree_Network_assumption TN).
End Tree_Algorithm.
Unset Implicit Arguments.
Close Scope nat_scope.
Close Scope signature.