PADEC - Coq Library
Library Padec.Model.Topologies.Graph_Diameter
*Certified Round Complexity of Self-Stabilizing Algorithms*
From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import ZArith.
From Coq Require Import Bool.
From Coq Require Import Lia.
From Coq Require Import SetoidClass.
From Coq Require Import ZArith.
From Coq Require Import Bool.
From Coq Require Import Lia.
From Padec Require Import OptionUtil.
From Padec Require Import SetoidUtil.
From Padec Require Import RelationA.
From Padec Require Import Count.
From Padec Require Import ListUtils.
From Padec Require Import All_In.
Open Scope nat_scope.
Open Scope signature_scope.
Set Implicit Arguments.
From Padec Require Import SetoidUtil.
From Padec Require Import RelationA.
From Padec Require Import Count.
From Padec Require Import ListUtils.
From Padec Require Import All_In.
Open Scope nat_scope.
Open Scope signature_scope.
Set Implicit Arguments.
finite set of vertices
Number of vertices
Use Count.Classical_set_Num_Card to obtain N
Notation HN_N := (Classical_set_Num_CardT DA _ all_here).
Definition N: nat := (proj1_sig HN_N).
Lemma HN: Num_Card Same A N.
Definition N: nat := (proj1_sig HN_N).
Lemma HN: Num_Card Same A N.
edges
undirected graph
path (non empty path):
(is_path x p y) means a path exists from x to y, made of the
consecutive nodes in (x :: p ++ y :: nil).
Definition is_path: A -> list A -> A -> Prop := (non_empty_chain G).
Lemma hd_app:
forall l (h: A) p, nil <> l -> hd h l = hd h (l ++ p).
Lemma hd_eq:
forall l (h1 h2: A), nil <> l -> hd h1 l = hd h2 l.
Lemma hd_eq':
forall l (h1 h2: A), nil <> l -> hd h1 l == hd h2 l.
Lemma rev_nil:
forall l: list A, nil = l <-> nil = rev l.
Global Instance hd_compat:
Proper (equiv ==> eqlistA equiv ==> equiv) (hd (A := A)).
Global Instance is_path_compat':
Proper (equiv ==> eqlistA (equiv) ==> pequiv) is_path.
Lemma is_path_cons:
forall p x xx y, is_path x (xx :: p) y -> is_path xx p y.
Lemma is_path_fst:
forall p x y, is_path x p y -> G x (hd y p).
Lemma is_path_cat:
forall p q x y z, is_path x p y -> is_path y q z ->
is_path x (p ++ y :: q) z.
Lemma hd_app:
forall l (h: A) p, nil <> l -> hd h l = hd h (l ++ p).
Lemma hd_eq:
forall l (h1 h2: A), nil <> l -> hd h1 l = hd h2 l.
Lemma hd_eq':
forall l (h1 h2: A), nil <> l -> hd h1 l == hd h2 l.
Lemma rev_nil:
forall l: list A, nil = l <-> nil = rev l.
Global Instance hd_compat:
Proper (equiv ==> eqlistA equiv ==> equiv) (hd (A := A)).
Global Instance is_path_compat':
Proper (equiv ==> eqlistA (equiv) ==> pequiv) is_path.
Lemma is_path_cons:
forall p x xx y, is_path x (xx :: p) y -> is_path xx p y.
Lemma is_path_fst:
forall p x y, is_path x p y -> G x (hd y p).
Lemma is_path_cat:
forall p q x y z, is_path x p y -> is_path y q z ->
is_path x (p ++ y :: q) z.
connected graph
Definition is_connected: Prop :=
forall x y, ~ x == y -> exists p, is_path x p y.
Lemma is_connected_has_neighbor:
is_connected -> forall x y, ~ x == y ->
forall p, exists q, G p q.
forall x y, ~ x == y -> exists p, is_path x p y.
Lemma is_connected_has_neighbor:
is_connected -> forall x y, ~ x == y ->
forall p, exists q, G p q.
distance between nodes (relational)
Definition is_dist x y d: Prop :=
(x == y /\ d = 0) \/ ~ x == y /\
(exists p, is_path x p y /\ S (length p) = d) /\
(forall p, is_path x p y -> S (length p) >= d).
Instance is_dist_compat': Proper pequiv is_dist.
Lemma is_dist_unique:
forall x y d1 d2, is_dist x y d1 -> is_dist x y d2 ->
d1 = d2.
(x == y /\ d = 0) \/ ~ x == y /\
(exists p, is_path x p y /\ S (length p) = d) /\
(forall p, is_path x p y -> S (length p) >= d).
Instance is_dist_compat': Proper pequiv is_dist.
Lemma is_dist_unique:
forall x y d1 d2, is_dist x y d1 -> is_dist x y d2 ->
d1 = d2.
Lemma is_dist_neighbors:
forall r x y nx ny, G x y -> is_dist x r nx ->
is_dist y r ny -> nx <= S ny.
Lemma is_dist_neighbors':
forall r x y nx ny, G x y -> G y x ->
is_dist x r nx -> is_dist y r ny ->
nx = ny \/ nx = S ny \/ S nx = ny.
Lemma is_dist_neighbors_ex:
forall r x n, is_dist x r (S n) ->
exists y, G x y /\ is_dist y r n.
forall r x y nx ny, G x y -> is_dist x r nx ->
is_dist y r ny -> nx <= S ny.
Lemma is_dist_neighbors':
forall r x y nx ny, G x y -> G y x ->
is_dist x r nx -> is_dist y r ny ->
nx = ny \/ nx = S ny \/ S nx = ny.
Lemma is_dist_neighbors_ex:
forall r x n, is_dist x r (S n) ->
exists y, G x y /\ is_dist y r n.
diameter of G (relational)
If G is not connected, defines the greatest diameter among
the diameters of the connected components of G.
Definition is_diameter d: Prop :=
(exists x y, is_dist x y d) /\
(forall x y n, is_dist x y n -> d >= n).
Global Instance is_diameter_compat: Proper pequiv is_diameter.
Lemma is_diameter_unique:
forall d1 d2, is_diameter d1 -> is_diameter d2 -> d1 = d2.
(exists x y, is_dist x y d) /\
(forall x y n, is_dist x y n -> d >= n).
Global Instance is_diameter_compat: Proper pequiv is_diameter.
Lemma is_diameter_unique:
forall d1 d2, is_diameter d1 -> is_diameter d2 -> d1 = d2.
Fixpoint is_simple_b p: bool :=
match p with
| nil => true
| x :: q => if InA_dec DA x q then false else is_simple_b q
end.
Definition is_simple p := is_simple_b p = true.
Global Instance is_simple_b_compat: Proper pequiv is_simple_b.
Global Instance is_simple_compat: Proper pequiv is_simple.
Lemma is_simple_inv:
forall x p, is_simple (x :: p) -> is_simple p.
Lemma is_simple_inv':
forall x p, is_simple (x :: p) -> ~ InA equiv x p.
Lemma simple_le_N:
forall p, is_simple p -> length p <= N.
Open Scope nat_scope.
Global Instance length_compat: Proper (equiv (A := list A) ==> equiv) (length (A := A)).
match p with
| nil => true
| x :: q => if InA_dec DA x q then false else is_simple_b q
end.
Definition is_simple p := is_simple_b p = true.
Global Instance is_simple_b_compat: Proper pequiv is_simple_b.
Global Instance is_simple_compat: Proper pequiv is_simple.
Lemma is_simple_inv:
forall x p, is_simple (x :: p) -> is_simple p.
Lemma is_simple_inv':
forall x p, is_simple (x :: p) -> ~ InA equiv x p.
Lemma simple_le_N:
forall p, is_simple p -> length p <= N.
Open Scope nat_scope.
Global Instance length_compat: Proper (equiv (A := list A) ==> equiv) (length (A := A)).
build a simple path:
code that does the job (but Coq refuses it because of induction guard)
Fixpoint remove_head x q: list A :=
match q with
| nil => nil
| a :: l => if InAb x (a :: l) then l
else remove_head x l
end.
Fixpoint build_simple_path p: list A :=
match p with
| nil => nil
| x :: q => if InA_dec DA x q
then
x :: build_simple_path (remove_head x q)
else x :: build_simple_path q
end.
here a solution that merge the tow above functions:
Definition InAb x l := if InA_dec DA x l then true else false.
Fixpoint bsp (p: list A) (in_remove: bool) (h: A): list A :=
match p with
| nil => nil
| x :: q =>
if in_remove && InAb h (x :: q) then bsp q true h
else if InA_dec DA x q then x :: bsp q true x
else x :: bsp q false x
end.
Definition build_simple_path p :=
match p with nil => nil | x :: q => bsp p false x end.
Lemma build_simple_path_is_simple:
forall p q, q = build_simple_path p -> is_simple q.
Lemma build_simple_path_length:
forall p q, q = build_simple_path p -> length q <= length p.
Lemma InA_hd:
forall p (h:A), p <> nil -> InA equiv (hd h p) p.
Lemma bsp_nil:
forall p ir h, bsp p ir h = nil <->
p = nil \/
ir = true /\
forall x, h == hd x (rev p).
Lemma build_simple_path_not_nil:
forall p, p <> nil-> build_simple_path p <> nil.
Lemma bsp_first:
forall p h, hd h p == hd h (build_simple_path p).
non empty path with no information about first and last
elements
Inductive is_path_: list A -> Prop :=
| is_path_one: forall x, is_path_ (x :: nil)
| is_path_step: forall x hp p, G x hp -> is_path_ (hp :: p)
-> is_path_ (x :: hp :: p).
Lemma is_path__is_path:
forall p x y,
is_path_ (x :: p ++ y :: nil) <-> is_path x p y.
Instance is_path__compat:
Proper (eqlistA (equiv) ==> equiv) is_path_.
Lemma is_path__inv:
forall x p, p <> nil -> G x (hd x p) -> is_path_ p ->
is_path_ (x :: p).
Lemma is_path__inv':
forall x p, is_path_ (x :: p) ->
p = nil \/ G x (hd x p) /\ is_path_ p.
Lemma is_path__cat:
forall p q, is_path_ p -> is_path_ q ->
(forall h1 h2, G (hd h1 (rev p)) (hd h2 q)) ->
is_path_ (p ++ q).
Lemma is_path__cat_conv_l:
forall p q, p <> nil -> is_path_ (p ++ q) -> is_path_ p.
Lemma is_path__cat_conv_m:
forall p q, p <> nil -> q <> nil -> is_path_ (p ++ q) ->
forall h1 h2, G (hd h1 (rev p)) (hd h2 q).
Lemma is_path__cat_conv_r:
forall p q, q <> nil -> is_path_ (p ++ q) -> is_path_ q.
Lemma is_path__cat_conv:
forall p q x y,
is_path_ ((p ++ x :: nil) ++ y :: q) ->
is_path_ (p ++ x :: nil) /\ is_path_ (y :: q) /\
G x y.
Lemma bsp_first_:
forall p,
is_path_ p ->
forall x b l,
(InA equiv x p -> bsp p true x = b :: l -> G x b) /\
(~InA equiv x p -> forall ir, bsp p ir x = b :: l ->
b = hd x p).
Lemma build_simple_path_is_path_:
forall p q,
q = build_simple_path p -> is_path_ p -> is_path_ q.
Lemma bsp_last:
forall p h, hd h (rev p) == hd h (rev (build_simple_path p)).
Lemma path_simple_path:
forall p x y, is_path x p y -> ~ x == y ->
{q | is_simple (x :: q ++ y :: nil)
/\ length q <= length p
/\ is_path x q y}.
Lemma path_simple_path_r:
forall p x y, is_path x p y ->
{ q | is_simple (q ++ y :: nil)
/\ length q <= length p
/\ is_path x q y}.
Lemma path_simple_path_l:
forall p x y, is_path x p y ->
{ q | is_simple (x :: q)
/\ length q <= length p
/\ is_path x q y}.
Lemma dist_le_N:
forall x y d, is_dist x y d -> S d <= N.
Lemma diameter_le_N:
forall d, is_diameter d -> S d <= N.
| is_path_one: forall x, is_path_ (x :: nil)
| is_path_step: forall x hp p, G x hp -> is_path_ (hp :: p)
-> is_path_ (x :: hp :: p).
Lemma is_path__is_path:
forall p x y,
is_path_ (x :: p ++ y :: nil) <-> is_path x p y.
Instance is_path__compat:
Proper (eqlistA (equiv) ==> equiv) is_path_.
Lemma is_path__inv:
forall x p, p <> nil -> G x (hd x p) -> is_path_ p ->
is_path_ (x :: p).
Lemma is_path__inv':
forall x p, is_path_ (x :: p) ->
p = nil \/ G x (hd x p) /\ is_path_ p.
Lemma is_path__cat:
forall p q, is_path_ p -> is_path_ q ->
(forall h1 h2, G (hd h1 (rev p)) (hd h2 q)) ->
is_path_ (p ++ q).
Lemma is_path__cat_conv_l:
forall p q, p <> nil -> is_path_ (p ++ q) -> is_path_ p.
Lemma is_path__cat_conv_m:
forall p q, p <> nil -> q <> nil -> is_path_ (p ++ q) ->
forall h1 h2, G (hd h1 (rev p)) (hd h2 q).
Lemma is_path__cat_conv_r:
forall p q, q <> nil -> is_path_ (p ++ q) -> is_path_ q.
Lemma is_path__cat_conv:
forall p q x y,
is_path_ ((p ++ x :: nil) ++ y :: q) ->
is_path_ (p ++ x :: nil) /\ is_path_ (y :: q) /\
G x y.
Lemma bsp_first_:
forall p,
is_path_ p ->
forall x b l,
(InA equiv x p -> bsp p true x = b :: l -> G x b) /\
(~InA equiv x p -> forall ir, bsp p ir x = b :: l ->
b = hd x p).
Lemma build_simple_path_is_path_:
forall p q,
q = build_simple_path p -> is_path_ p -> is_path_ q.
Lemma bsp_last:
forall p h, hd h (rev p) == hd h (rev (build_simple_path p)).
Lemma path_simple_path:
forall p x y, is_path x p y -> ~ x == y ->
{q | is_simple (x :: q ++ y :: nil)
/\ length q <= length p
/\ is_path x q y}.
Lemma path_simple_path_r:
forall p x y, is_path x p y ->
{ q | is_simple (q ++ y :: nil)
/\ length q <= length p
/\ is_path x q y}.
Lemma path_simple_path_l:
forall p x y, is_path x p y ->
{ q | is_simple (x :: q)
/\ length q <= length p
/\ is_path x q y}.
Lemma dist_le_N:
forall x y d, is_dist x y d -> S d <= N.
Lemma diameter_le_N:
forall d, is_diameter d -> S d <= N.
Lemma is_path_dec:
forall x p y, {is_path x p y}+{~is_path x p y}.
Lemma is_simple_dec: forall p, {is_simple p}+{~is_simple p}.
forall x p y, {is_path x p y}+{~is_path x p y}.
Lemma is_simple_dec: forall p, {is_simple p}+{~is_simple p}.
returns the list of simple paths made from p
+ one predecessor (elements in l)
Fixpoint _enum_list (p: list A) (y: A) (l: list A):
list (list A) :=
match l with
| nil => p :: nil
| a :: ll => if InA_dec DA a p then _enum_list p y ll
else if G_dec a (hd y p) then (a :: p) :: _enum_list p y ll
else _enum_list p y ll
end.
Instance enum_list_compat: Proper pequiv _enum_list.
list (list A) :=
match l with
| nil => p :: nil
| a :: ll => if InA_dec DA a p then _enum_list p y ll
else if G_dec a (hd y p) then (a :: p) :: _enum_list p y ll
else _enum_list p y ll
end.
Instance enum_list_compat: Proper pequiv _enum_list.
increase s by adding one element - when possible - to any
any of its paths
Fixpoint _enum_set (s: list (list A)) (y: A): list (list A) :=
match s with
| nil => nil
| p :: ss => _enum_list p y all ++ _enum_set ss y
end.
Instance enum_set_compat: Proper pequiv _enum_set.
match s with
| nil => nil
| p :: ss => _enum_list p y all ++ _enum_set ss y
end.
Instance enum_set_compat: Proper pequiv _enum_set.
all simple paths to y of length at most n
Fixpoint enum_path0 (y: A) (n: nat): list (list A) :=
match n with
| 0 => nil :: nil
| S nn => _enum_set (enum_path0 y nn) y
end.
Instance enum_path0_compat: Proper pequiv enum_path0.
match n with
| 0 => nil :: nil
| S nn => _enum_set (enum_path0 y nn) y
end.
Instance enum_path0_compat: Proper pequiv enum_path0.
all simple paths from x to y
Definition enum_path (x y: A): list (list A) :=
map_filter
(fun p: list A =>
match p with nil => None
| a :: pp => if DA x a then Some pp else None
end)
(enum_path0 y N).
Instance enum_path_compat: Proper pequiv enum_path.
Lemma enum_list_is_simple: forall y p l q,
is_simple p ->
InA equiv q (_enum_list p y l) -> is_simple q.
Lemma enum_set_is_simple:
forall s, (forall p, InA equiv p s -> is_simple p) ->
forall y p, InA equiv p (_enum_set s y) -> is_simple p.
Lemma enum_path0_is_simple: forall y n p,
InA equiv p (enum_path0 y n) -> is_simple p.
Lemma enum_path_is_simple: forall x y p,
InA equiv p (enum_path x y) -> is_simple (x :: p).
Lemma enum_list_is_path:
forall y p, is_path_ (p ++ y :: nil) ->
forall l q,
InA equiv q (_enum_list p y l) ->
is_path_ (q ++ y :: nil).
Lemma enum_set_is_path:
forall y s, (forall p, InA equiv p s -> is_path_ (p ++ y :: nil)) ->
forall q,
InA equiv q (_enum_set s y) -> is_path_ (q ++ y :: nil).
Lemma enum_path0_is_path:
forall y n p,
InA equiv p (enum_path0 y n) -> is_path_ (p ++ y :: nil).
Lemma enum_path_is_path: forall x y p,
InA equiv p (enum_path x y) -> is_path x p y.
Lemma enum_list_all:
forall l q x y p,
is_path x p y -> is_simple (x :: p) ->
(x :: p == q \/ InA equiv x l /\ p == q) ->
InA equiv (x :: p) (_enum_list q y l).
Lemma enum_set_all:
forall s x y p,
is_path x p y -> is_simple (x :: p) ->
(InA equiv (x :: p) s \/ InA equiv p s) ->
InA equiv (x :: p) (_enum_set s y).
Lemma enum_path0_all:
forall n y x p,
is_path x p y -> is_simple (x :: p) -> length (x :: p) <= n ->
InA equiv (x :: p) (enum_path0 y n).
Lemma enum_path_all: forall x y p,
is_path x p y -> is_simple (x :: p) ->
InA equiv p (enum_path x y).
Lemma exists_path_dec:
forall x y, {p | is_path x p y}+{forall p, ~is_path x p y}.
Lemma exists_path_dec':
forall x y, {p | is_path x p y}+{~exists p, is_path x p y}.
Lemma exists_path_length_dec:
forall x y k, {p | length p <= k /\ is_path x p y}+
{forall p, length p <= k -> ~is_path x p y}.
Lemma is_connected_has_neighbor':
is_connected ->
forall x y, ~ x == y ->
forall p, exists q, ~ p == q /\ G p q.
map_filter
(fun p: list A =>
match p with nil => None
| a :: pp => if DA x a then Some pp else None
end)
(enum_path0 y N).
Instance enum_path_compat: Proper pequiv enum_path.
Lemma enum_list_is_simple: forall y p l q,
is_simple p ->
InA equiv q (_enum_list p y l) -> is_simple q.
Lemma enum_set_is_simple:
forall s, (forall p, InA equiv p s -> is_simple p) ->
forall y p, InA equiv p (_enum_set s y) -> is_simple p.
Lemma enum_path0_is_simple: forall y n p,
InA equiv p (enum_path0 y n) -> is_simple p.
Lemma enum_path_is_simple: forall x y p,
InA equiv p (enum_path x y) -> is_simple (x :: p).
Lemma enum_list_is_path:
forall y p, is_path_ (p ++ y :: nil) ->
forall l q,
InA equiv q (_enum_list p y l) ->
is_path_ (q ++ y :: nil).
Lemma enum_set_is_path:
forall y s, (forall p, InA equiv p s -> is_path_ (p ++ y :: nil)) ->
forall q,
InA equiv q (_enum_set s y) -> is_path_ (q ++ y :: nil).
Lemma enum_path0_is_path:
forall y n p,
InA equiv p (enum_path0 y n) -> is_path_ (p ++ y :: nil).
Lemma enum_path_is_path: forall x y p,
InA equiv p (enum_path x y) -> is_path x p y.
Lemma enum_list_all:
forall l q x y p,
is_path x p y -> is_simple (x :: p) ->
(x :: p == q \/ InA equiv x l /\ p == q) ->
InA equiv (x :: p) (_enum_list q y l).
Lemma enum_set_all:
forall s x y p,
is_path x p y -> is_simple (x :: p) ->
(InA equiv (x :: p) s \/ InA equiv p s) ->
InA equiv (x :: p) (_enum_set s y).
Lemma enum_path0_all:
forall n y x p,
is_path x p y -> is_simple (x :: p) -> length (x :: p) <= n ->
InA equiv (x :: p) (enum_path0 y n).
Lemma enum_path_all: forall x y p,
is_path x p y -> is_simple (x :: p) ->
InA equiv p (enum_path x y).
Lemma exists_path_dec:
forall x y, {p | is_path x p y}+{forall p, ~is_path x p y}.
Lemma exists_path_dec':
forall x y, {p | is_path x p y}+{~exists p, is_path x p y}.
Lemma exists_path_length_dec:
forall x y k, {p | length p <= k /\ is_path x p y}+
{forall p, length p <= k -> ~is_path x p y}.
Lemma is_connected_has_neighbor':
is_connected ->
forall x y, ~ x == y ->
forall p, exists q, ~ p == q /\ G p q.
Minimum of a list
Definition min_list (l: list nat): option nat :=
match l with nil => None
| a :: ll => Some (fold_right min a ll)
end.
Global Instance min_list_compat: Proper pequiv min_list.
Lemma min_list_None:
forall l, min_list l = None <-> l = nil.
Lemma fr_min1:
forall a l, InA equiv (fold_right min a l) (a :: l).
Lemma fr_min2:
forall a l b, InA equiv b (a :: l) -> fold_right min a l <= b.
Lemma fr_min3:
forall m a l, InA equiv m (a :: l) /\
(forall b, InA equiv b (a :: l) -> m <= b)
-> m = fold_right min a l.
Lemma min_list_Some:
forall l m, min_list l = Some m <->
InA equiv m l /\
forall a, InA equiv a l -> m <= a.
match l with nil => None
| a :: ll => Some (fold_right min a ll)
end.
Global Instance min_list_compat: Proper pequiv min_list.
Lemma min_list_None:
forall l, min_list l = None <-> l = nil.
Lemma fr_min1:
forall a l, InA equiv (fold_right min a l) (a :: l).
Lemma fr_min2:
forall a l b, InA equiv b (a :: l) -> fold_right min a l <= b.
Lemma fr_min3:
forall m a l, InA equiv m (a :: l) /\
(forall b, InA equiv b (a :: l) -> m <= b)
-> m = fold_right min a l.
Lemma min_list_Some:
forall l m, min_list l = Some m <->
InA equiv m l /\
forall a, InA equiv a l -> m <= a.
Maximum of a list
Definition max_list (l: list nat): option nat :=
match l with nil => None
| a :: ll => Some (fold_right max a ll)
end.
Global Instance max_list_compat: Proper pequiv max_list.
Lemma max_list_None:
forall l, max_list l = None <-> l = nil.
Lemma fr_max1:
forall a l, InA equiv (fold_right max a l) (a :: l).
Lemma fr_max2:
forall a l b, InA equiv b (a :: l) -> fold_right max a l >= b.
Lemma fr_max3:
forall m a l, InA equiv m (a :: l) /\
(forall b, InA equiv b (a :: l) -> m >= b)
-> m = fold_right max a l.
Lemma max_list_Some:
forall l m, max_list l = Some m <->
InA equiv m l /\
forall a, InA equiv a l -> m >= a.
match l with nil => None
| a :: ll => Some (fold_right max a ll)
end.
Global Instance max_list_compat: Proper pequiv max_list.
Lemma max_list_None:
forall l, max_list l = None <-> l = nil.
Lemma fr_max1:
forall a l, InA equiv (fold_right max a l) (a :: l).
Lemma fr_max2:
forall a l b, InA equiv b (a :: l) -> fold_right max a l >= b.
Lemma fr_max3:
forall m a l, InA equiv m (a :: l) /\
(forall b, InA equiv b (a :: l) -> m >= b)
-> m = fold_right max a l.
Lemma max_list_Some:
forall l m, max_list l = Some m <->
InA equiv m l /\
forall a, InA equiv a l -> m >= a.
Distance between x and y (None if no path exists)
Notation length := (length (A := A)).
Definition compute_dist (x y: A): option nat :=
if DA x y then Some 0 else
match min_list (map length (enum_path x y)) with
| None => None | Some d => Some (S d) end.
Instance compute_dist_compat: Proper pequiv compute_dist.
Lemma compute_dist_is_dist:
forall x y, match compute_dist x y with
| None => forall d, ~is_dist x y d
| Some d => is_dist x y d
end.
Lemma is_dist_dec:
forall x y, {d | is_dist x y d}+{forall d, ~is_dist x y d}.
Lemma is_dist_dec0:
forall x y d, {is_dist x y d}+{~is_dist x y d}.
Lemma dist_exists':
forall x y, {p | ~x == y /\ is_path x p y} + { x == y } ->
{ d | is_dist x y d }.
Lemma dist_exists:
forall x y p, is_path x p y -> { d | is_dist x y d }.
Lemma is_dist_equiv:
forall x y d, is_dist x y d <-> compute_dist x y == Some d.
Definition compute_dist' x y p (hp: is_path x p y): nat :=
proj1_sig (dist_exists x y _ hp).
Lemma compute_dist'_compat:
forall x x' (ex: x == x') y y' (ey: y == y') p p'
(ep: p == p') (hp: is_path x p y)
(hp': is_path x' p' y'),
compute_dist' x y p hp = compute_dist' x' y' p' hp'.
Lemma is_dist_equiv':
forall x y p (hp: is_path x p y),
is_dist x y (compute_dist' x y _ hp).
Lemma is_connected' (ic: is_connected):
forall x y, { p | ~x == y /\ is_path x p y } + { x == y }.
Definition compute_dist'' (ic: is_connected) x y: nat :=
proj1_sig (dist_exists' x y (is_connected' ic x y)).
Instance compute_dist''_compat:
forall ic, Proper (equiv ==> equiv ==> eq) (compute_dist'' ic).
Lemma is_dist_equiv'' (ic: is_connected):
forall x y, is_dist x y (compute_dist'' ic x y).
Definition compute_dist (x y: A): option nat :=
if DA x y then Some 0 else
match min_list (map length (enum_path x y)) with
| None => None | Some d => Some (S d) end.
Instance compute_dist_compat: Proper pequiv compute_dist.
Lemma compute_dist_is_dist:
forall x y, match compute_dist x y with
| None => forall d, ~is_dist x y d
| Some d => is_dist x y d
end.
Lemma is_dist_dec:
forall x y, {d | is_dist x y d}+{forall d, ~is_dist x y d}.
Lemma is_dist_dec0:
forall x y d, {is_dist x y d}+{~is_dist x y d}.
Lemma dist_exists':
forall x y, {p | ~x == y /\ is_path x p y} + { x == y } ->
{ d | is_dist x y d }.
Lemma dist_exists:
forall x y p, is_path x p y -> { d | is_dist x y d }.
Lemma is_dist_equiv:
forall x y d, is_dist x y d <-> compute_dist x y == Some d.
Definition compute_dist' x y p (hp: is_path x p y): nat :=
proj1_sig (dist_exists x y _ hp).
Lemma compute_dist'_compat:
forall x x' (ex: x == x') y y' (ey: y == y') p p'
(ep: p == p') (hp: is_path x p y)
(hp': is_path x' p' y'),
compute_dist' x y p hp = compute_dist' x' y' p' hp'.
Lemma is_dist_equiv':
forall x y p (hp: is_path x p y),
is_dist x y (compute_dist' x y _ hp).
Lemma is_connected' (ic: is_connected):
forall x y, { p | ~x == y /\ is_path x p y } + { x == y }.
Definition compute_dist'' (ic: is_connected) x y: nat :=
proj1_sig (dist_exists' x y (is_connected' ic x y)).
Instance compute_dist''_compat:
forall ic, Proper (equiv ==> equiv ==> eq) (compute_dist'' ic).
Lemma is_dist_equiv'' (ic: is_connected):
forall x y, is_dist x y (compute_dist'' ic x y).
Notation map_filter_dist x :=
(map_filter (fun y => compute_dist x y) all).
Instance map_filter_dist_compat: Proper pequiv (fun x => map_filter_dist x).
Definition compute_diameter: option nat :=
max_list (fold_right
(fun x l => (map_filter_dist x) ++ l) nil
all).
Lemma fr_app:
forall x fl ll (f: A -> list nat) (f_compat: Proper pequiv f),
InA equiv x (fold_right (fun y l => f y ++ l) fl ll) <->
InA equiv x fl \/ exists y, InA equiv y ll /\ InA equiv x (f y).
Lemma fr_app_nil:
forall fl ll (f: A -> list nat) (f_compat: Proper pequiv f),
fold_right (fun y l => f y ++ l) fl ll = nil <->
fl = nil /\ forall x, InA equiv x ll -> f x = nil.
Lemma compute_diameter_is_diameter:
match compute_diameter with
| None => forall d, ~is_diameter d
| Some d => is_diameter d
end.
Lemma is_diameter_dec: {d | is_diameter d}+{forall d, ~is_diameter d}.
Lemma is_diameter_dec0:
forall d, {is_diameter d}+{~is_diameter d}.
Lemma is_diameter_equiv:
forall d, is_diameter d <-> compute_diameter = Some d.
Lemma diameter_exists:
forall (a: A), {d | is_diameter d}.
Definition compute_diameter' (a: A): nat :=
proj1_sig (diameter_exists a).
Lemma is_diameter_equiv':
forall a, is_diameter (compute_diameter' a).
Lemma is_dist_nul:
forall a b, is_dist a b 0 <-> a == b.
Lemma is_dist_nul':
forall a d, is_dist a a d <-> d = 0.
Lemma is_dist_one:
forall a b, ~ a == b -> G a b -> is_dist a b 1.
Lemma is_dist_one':
forall a b d, ~ a == b -> G a b -> is_dist a b d -> d = 1.
Lemma is_diameter_pos:
forall a b d, ~ a == b -> G a b -> is_diameter d -> d > 0.
Lemma compute_diameter'_pos:
forall a b, ~ a == b -> G a b -> compute_diameter' a > 0.
End Graph.
Section Compat_without_G.
Context {A} `{SA: Setoid A}.
Global Instance is_path_compat:
Proper (pequiv ==> equiv ==> eqlistA (equiv) ==> pequiv) (is_path (A := A)).
Global Instance is_dist_compat: Proper pequiv (is_dist (A := A)).
End Compat_without_G.
Section SubGraph.
Context {A} `{SA: Setoid A} {DA: Decider (equiv (A:=A))}.
Definition is_subgraph (G_sub G: relation A): Prop :=
inclusion G_sub G.
Global Instance is_subgraph_compat: Proper pequiv is_subgraph.
Lemma is_path_subgraph:
forall G G_sub, is_subgraph G_sub G ->
forall p x y, is_path G_sub x p y ->
is_path G x p y.
Lemma is_dist_subgraph:
forall G G_sub, is_subgraph G_sub G ->
forall x y n n_sub,
is_dist G x y n -> is_dist G_sub x y n_sub
-> n <= n_sub.
Lemma is_subgraph_dec:
forall l (finite: forall (a:A), InA equiv a l),
forall (G' G: relation A),
Proper pequiv G -> Proper pequiv G' ->
(forall x y, {G x y} + {~G x y}) ->
(forall x y, {G' x y} + {~G' x y}) ->
{is_subgraph G' G} + {~is_subgraph G' G}.
End SubGraph.
Section Path_Chain.
Context {A} `{SA: Setoid A}.
Variable (G: relation A) (G_compat: Proper pequiv G) .
Lemma is_path_chain:
forall a b p, is_path G a p b <-> chain G a (p ++ b :: nil) b.
Lemma chain_is_path:
forall a b p, chain G a p b <->
( a == b /\ p == nil ) \/
exists pp, p == pp ++ b :: nil /\
is_path G a pp b.
End Path_Chain.
Section Tools_for_Distance.
Context {A} `{SA: Setoid A} {DA: Decider (equiv (A:=A))}.
Variable (G: relation A) (G_compat: Proper pequiv G) (G_dec: Decider G).
Hypothesis (Connected: is_connected G).
inclusion G_sub G.
Global Instance is_subgraph_compat: Proper pequiv is_subgraph.
Lemma is_path_subgraph:
forall G G_sub, is_subgraph G_sub G ->
forall p x y, is_path G_sub x p y ->
is_path G x p y.
Lemma is_dist_subgraph:
forall G G_sub, is_subgraph G_sub G ->
forall x y n n_sub,
is_dist G x y n -> is_dist G_sub x y n_sub
-> n <= n_sub.
Lemma is_subgraph_dec:
forall l (finite: forall (a:A), InA equiv a l),
forall (G' G: relation A),
Proper pequiv G -> Proper pequiv G' ->
(forall x y, {G x y} + {~G x y}) ->
(forall x y, {G' x y} + {~G' x y}) ->
{is_subgraph G' G} + {~is_subgraph G' G}.
End SubGraph.
Section Path_Chain.
Context {A} `{SA: Setoid A}.
Variable (G: relation A) (G_compat: Proper pequiv G) .
Lemma is_path_chain:
forall a b p, is_path G a p b <-> chain G a (p ++ b :: nil) b.
Lemma chain_is_path:
forall a b p, chain G a p b <->
( a == b /\ p == nil ) \/
exists pp, p == pp ++ b :: nil /\
is_path G a pp b.
End Path_Chain.
Section Tools_for_Distance.
Context {A} `{SA: Setoid A} {DA: Decider (equiv (A:=A))}.
Variable (G: relation A) (G_compat: Proper pequiv G) (G_dec: Decider G).
Hypothesis (Connected: is_connected G).
finite set of vertices
Definition dist := (compute_dist'' all_here G_compat
G_dec Connected
(DA := DA)).
Global Instance dist_compat: Proper pequiv dist.
Lemma is_dist_dist: forall x y, is_dist G x y (dist x y).
Lemma is_dist_dist': forall (x y: A) n, is_dist G x y n -> dist x y = n.
Lemma dist_nil: forall n, dist n n = 0.
Lemma dist_nil': forall n n', dist n n' = 0 <-> n == n'.
Lemma dist_neighbors:
forall (Bidir: forall x y, G x y -> G y x),
forall r,
forall p q, G p q -> dist q r = dist p r \/
S (dist q r) = dist p r \/
dist q r = S (dist p r).
Lemma dist_neighbor_ex:
forall p r n, dist p r = S n ->
exists q, G p q /\ dist q r = n.
G_dec Connected
(DA := DA)).
Global Instance dist_compat: Proper pequiv dist.
Lemma is_dist_dist: forall x y, is_dist G x y (dist x y).
Lemma is_dist_dist': forall (x y: A) n, is_dist G x y n -> dist x y = n.
Lemma dist_nil: forall n, dist n n = 0.
Lemma dist_nil': forall n n', dist n n' = 0 <-> n == n'.
Lemma dist_neighbors:
forall (Bidir: forall x y, G x y -> G y x),
forall r,
forall p q, G p q -> dist q r = dist p r \/
S (dist q r) = dist p r \/
dist q r = S (dist p r).
Lemma dist_neighbor_ex:
forall p r n, dist p r = S n ->
exists q, G p q /\ dist q r = n.
Tools about diameter
Lemma diam_dist:
forall (one: A),
let Diam := compute_diameter'
all_here G_compat G_dec one (DA := DA) in
forall p q, dist p q <= Diam.
Lemma Diam_pos:
forall one,
let Diam := compute_diameter'
all_here G_compat G_dec one (DA := DA) in
forall (p q: A), ~ p == q -> Diam > 0.
End Tools_for_Distance.
Close Scope signature_scope.
Close Scope nat_scope.
Unset Implicit Arguments.
forall (one: A),
let Diam := compute_diameter'
all_here G_compat G_dec one (DA := DA) in
forall p q, dist p q <= Diam.
Lemma Diam_pos:
forall one,
let Diam := compute_diameter'
all_here G_compat G_dec one (DA := DA) in
forall (p q: A), ~ p == q -> Diam > 0.
End Tools_for_Distance.
Close Scope signature_scope.
Close Scope nat_scope.
Unset Implicit Arguments.