Library LangAlg.graph

We define in this module 2-pointed labelled directed graphs, and some operations on them.

Set Implicit Arguments.

Require Export tools.
Require Import finite_functions.

Main definitions

An edge over vertices of type A and labels of type B is a triple, containing its source, its label, and its target.

Definition edge {A B : Set} : Set :=(A × B × A).

A graph is a triple, with an input vertex, a list of edges, and an output vertex.

Definition graph (A B : Set) : Set := A × list (@edge A B) × A.

Section g.

We fix a set of labels.

  Variable L : Set.

  Definition input {A} (g : graph A L) : A := fst (fst g).
  Definition output {A} (g : graph A L) : A := snd g.
  Definition edges {A} (g : graph A L) : list edge := snd (fst g).

  Hint Unfold input output edges.

It is often useful to map a function to a list of edges, applying it to the source and target of every edge (but not on their labels).

Definition map {A B : Set} (f : A → B) l : list (@edge B L) :=
List.map (fun (e : edge) ⇒ match e with (i,α,j) ⇒ (f i,α,f j) end) l.

This map satisfies the usual properties of maps.

  Lemma map_id {A : Set} l : map (@id A) l = l.

  Lemma in_map {A B : Set} (f : A → B) l i α j :
    (i ,α ,j ) ∈ (map f l ) ↔ ∃ x y, (x ,α ,y ) ∈ l ∧ f x = i ∧ f y = j.

  Lemma map_map {A B C : Set} (g : B → C) (f : A → B) l :
    map g (map f l) = map (g ∘ f) l.

  Lemma map_app {A B : Set} (f : A → B) l m :
    map f (l ++m) = map f l ++ map f m.

graph_map applies a function on the vertices of a graph.

  Definition graph_map {X Y: Set} (φ : X → Y) g : graph Y L :=
    (φ (input g),map φ (edges g),φ (output g)).

  Lemma input_graph_map {X Y: Set} (φ : X → Y) g :
    input (graph_map φ g) = φ (input g).

  Lemma output_graph_map {X Y: Set} (φ : X → Y) g :
    output (graph_map φ g) = φ (output g).

  Lemma edges_graph_map {X Y: Set} (φ : X → Y) g :
    edges (graph_map φ g) = map φ (edges g).

  Lemma graph_map_map {X Y Z : Set} (φ : X → Y) (ψ : Y → Z) g :
    graph_map ψ (graph_map φ g) = graph_map (ψ ∘ φ) g.

  Lemma graph_map_id {X: Set} (g : graph X L) :
    graph_map id g = g.

We can extract from a graph its list of vertices, by taking the input vertex, the output vertex and every vertex appear either as the source or the target of some edge.

  Global Instance graph_vertices {A} : Support graph A L :=
    fun g ⇒
      (input g )::(output g )
               ::(flat_map (fun e ⇒ [fst (fst e);snd e ]) (edges g)).

  Lemma in_graph_vertices {A : Set} (i : A) (g : graph A L) :
    i ∈ ⌊ g ⌋ ↔ input g =i ∨ output g =i
                ∨ (∃ α j, (i ,α ,j ) ∈ (edges g ))
                ∨ (∃ α j, (j ,α ,i ) ∈ (edges g )).

  Lemma edges_vertices {A : Set} i a j (g : graph A L) :
    (i ,a ,j ) ∈ edges g → i ∈ ⌊g ⌋ ∧ j ∈ ⌊g ⌋.

Set of labels of a graph.

Global Instance labels {A : Set} : Alphabet (graph A) L :=
fun g ⇒ List.map (snd ∘fst) (edges g).

The set of labels is invariant under morphism.

Lemma variables_graph_map {A B : Set} (f : A → B) (g : graph A L) :
⌈ graph_map f g ⌉ = ⌈ g ⌉.

If two functions φ and ψ coincide on the vertices of a graph g, then the images of g by φ and ψ are equal.

Lemma graph_map_ext_in {X Y : Set} (φ ψ : X → Y) g :
(∀ x, x ∈ ⌊g ⌋ → φ x = ψ x ) → graph_map φ g = graph_map ψ g.

We can obtain the vertices of the image of g by φ by simply applying φ to the vertices of g.

Lemma graph_vertices_map {X Y: Set} g (φ : X → Y) :
⌊graph_map φ g ⌋ = List.map φ ⌊g ⌋.

A map is called internal from g to h whenever every vertex in g is sent to a vertex in h.

Definition internal_map {X Y: Set} (φ : X → Y) g h :=
∀ x, x ∈ ⌊g ⌋ → (φ x ) ∈ ⌊h ⌋.

A map φ is always internal from g to graph_map φ g.

Lemma internal_map_graph_map {X Y: Set} (φ : X → Y) g :
internal_map φ g (graph_map φ g).

φ is an A-premorphism from g to h if for every edge (i,α,j) in g, either

α is in A and φ i is equal to φ j,
there is an edge (φ i,α,φ j) in h.

  Definition is_premorphism {X Y} A φ (g : graph X L) (h : graph Y L):=
    ∀ i α j, (i ,α ,j ) ∈ (edges g ) →
             (α ∈ A ∧ φ i = φ j ) ∨ (φ i ,α ,φ j ) ∈ (edges h ).

  Notation " A ⊨ g -{ φ }⇀ h" := (is_premorphism A φ g h)
                                   (at level 80).

If there is an A-premorphism from g to h, then the labels of g are either labels of h or chosen from A.

Lemma variables_premorphism {X Y : Set} A (φ : X → Y) g h :
A ⊨ g -{φ }⇀ h → ⌈g ⌉ ⊆ ⌈h ⌉ ++ A.

Premorphisms are closed under composition.

  Lemma is_premorphism_compose {X Y Z : Set} (φ1 : X → Y) (φ2 : Y → Z)
        g1 g2 g3 (A B : list L) :
    A ⊨ g1 -{φ1 }⇀ g2 → B ⊨ g2 -{φ2 }⇀ g3 → A ++B ⊨ g1 -{φ2 ∘φ1 }⇀ g3.

If A is contained in B, every A-premorphism is also a B-premorphism.

Lemma is_premorphism_incl {X Y : Set} A B g h (φ : X → Y) :
A ⊆ B → A ⊨ g -{ φ }⇀ h → B ⊨ g -{ φ }⇀ h.

We can compose A-premorphisms and obtain another A-premorphism.

  Lemma is_premorphism_compose_weak {X Y Z : Set} φ1 φ2
        (g1 : graph X L) (g2: graph Y L) (g3: graph Z L) A :
    A ⊨ g1 -{φ1 }⇀ g2 → A ⊨ g2 -{φ2 }⇀ g3 → A ⊨ g1 -{φ2 ∘φ1 }⇀ g3.

We we choose A to be the empty list, then the third condition can be reformulated as the containment of map φ (edges g) inside edges h.

Lemma proper_morphism_diff {X Y : Set} (φ : X → Y) g h :
[] ⊨ g -{φ }⇀ h ↔ (map φ (edges g)) ⊆ (edges h ).

φ is an A-morphism from g to h if

the image of the input of g is the input of h,
the image of the output of g is the output of h,
it is an A-premorphism;
it is internal from g to h.

  Definition is_morphism {X Y} A φ (g : graph X L) (h : graph Y L) :=
    φ (input g) = input h ∧ φ (output g) = output h
    ∧ A ⊨ g -{φ }⇀ h ∧ internal_map φ g h.

  Notation " A ⊨ g -{ φ }→ h " := (is_morphism A φ g h) (at level 80).

Because a morphism is in particular a premorphism, we have the same containment between sets of labels.

Lemma variables_morphism {X Y : Set} A (φ : X → Y) g h :
A ⊨ g -{φ }→ h → ⌈g ⌉ ⊆ ⌈h ⌉ ++ A.

If A is contained in B, every A-morphism is also a B-morphism.

Lemma is_morphism_incl {V1 V2 : Set} A B g h (φ : V1 → V2) :
A ⊆ B → A ⊨ g -{φ }→ h → B ⊨ g -{φ }→ h.

The identity is an ø-morphism from g to itself.

Lemma is_morphism_id {V : Set} (g : graph V L) : [] ⊨ g -{id }→ g.

We can compose morphisms.

  Lemma is_morphism_compose {X Y Z} φ1 φ2
        (g1 : graph X L) (g2: graph Y L) (g3: graph Z L) A B :
    A ⊨ g1 -{φ1 }→ g2 → B ⊨ g2 -{φ2 }→ g3 → A ++B ⊨ g1 -{φ2 ∘φ1 }→ g3.

We can compose A-morphisms. With the lemmas is_morphism_id and is_morphism_incl, this means that graphs and A-morphisms form a category.

  Lemma is_morphism_compose_weak {X Y Z} φ1 φ2
        (g1 : graph X L) (g2: graph Y L) (g3: graph Z L) A :
    A ⊨ g1 -{φ1 }→ g2 → A ⊨ g2 -{φ2 }→ g3 → A ⊨ g1 -{φ2 ∘φ1 }→ g3.

φ is an ø-morphism from g to graph_map φ g.

Lemma graph_map_morphism {X Y: Set} (φ : X → Y) g :
[] ⊨ g -{φ }→(graph_map φ g ).

We can use A-morphisms to define a preorder on graphs.

  Definition hom_order {V} A (g h : graph V L) := ∃ φ, A ⊨ h -{φ }→ g.

  Notation " A ⊨ g ⊲ h " := (hom_order A g h) (at level 80).

  Global Instance hom_order_PreOrder {V:Set} A :
    PreOrder (@hom_order V A).

Containment between sets of labels.

Lemma variables_hom_order {X : Set} A (g h : graph X L) :
A ⊨ g ⊲ h → ⌈h ⌉ ⊆ ⌈g ⌉ ++ A.

The ordering induced by A-morphisms is included in the ordering induced by B-morphisms.

Lemma hom_order_incl {V : Set} A B (g h : graph V L) :
A ⊆ B → A ⊨ g ⊲ h → B ⊨ g ⊲ h.

If two functions coincide on the vertices of a graph g, then one is an A-morphism from g to h if and only if the other is.

Lemma morphism_ext_vertices {X Y: Set} (φ ψ : X → Y) A g h :
(∀ i, i ∈ ⌊ g ⌋ → φ i = ψ i ) → A ⊨ g -{φ }→ h ↔ A ⊨ g -{ψ }→ h.

if ψ is the inverse of φ on the vertices of g, then ψ is an ø-morphism from the image of g by φ to g.

Lemma inverse_graph_map_morphism {X Y : Set} g (φ : X → Y) ψ :
inverse φ ψ ⌊g ⌋ → [] ⊨ (graph_map φ g ) -{ψ }→ g.

If a graph g is greater than the point graph, then its variables are all contained in A.

Lemma contractible_graph A g :
⌈g ⌉ ⊆ A ↔ A ⊨ (0, [], 0) ⊲ g.

We define the path ordering on a graph.

  Inductive path {V}(g : graph V L) : V → V → Prop :=
  | path_re i : path g i i
  | path_trans j i k : path g i j → path g j k → path g i k
  | path_edge i j α : (i ,α ,j ) ∈ (edges g) → path g i j.

  Notation " u -[ G ]→ v " := (path G u v) (at level 80).

This is a preorder.

Global Instance path_PreOrder {V} (g : graph V L) : PreOrder (path g).

If φ is an A-premorphism from g to h, then it preserves the path ordering.

Lemma morphism_is_order_preserving {V1 V2 : Set} A (φ :V1 → V2) g h:
A ⊨ g -{φ }⇀ h → ∀ i j, i -[g ]→j → φ i -[h ]→ φ j.

If y is reachable from x in g, then φ y is reachable from φ x in the image of g by φ.

Lemma graph_map_path {X Y : Set} (φ : X → Y) (g : graph X L) x y :
x -[g ]→ y → φ x -[graph_map φ g ]→ φ y.

The reachability order is non-trivial only between vertices.

Lemma path_non_trivial_only_for_vertices {X:Set} g (i j : X) :
i -[g ]→j → i = j ∨ [i ;j ] ⊆ ⌊g ⌋.

Equivalently, if i and j are different elements such that one is reachable from the other, then i is a vertex (and by symmetry, so is j.

Lemma path_in_vertices {X:Set} g (i j : X) :
i ≠ j → i -[g ]→j ∨ j -[g ]→i → i ∈ ⌊g ⌋.

A third equivalent formulation of the same lemma.

Lemma path_graph_vertices {X : Set} g (i j : X) :
i -[g ]→ j → i ∈ ⌊g ⌋ ↔ j ∈ ⌊g ⌋.

If ψ is the inverse of φ and y is reachable from x in the image of g by φ, then ψ y was reachable from ψ x in g.

Lemma injective_graph_map_path {X Y : Set} (φ : X → Y) ψ g x y :
inverse φ ψ ⌊g ⌋ → x -[graph_map φ g ]→ y → ψ x -[g ]→ ψ y.

The relation hom_eq relates two graphs if there is a pair of ø-morphisms, going both directions between the two graphs. Note that despite the name, it does not mean the two graphs are isomorphic: indeed this pair of morphisms need not be inverses.

  Definition hom_eq {X : Set} (g h : graph X L) :=
    ([] ⊨ g ⊲ h ) ∧ ([] ⊨ h ⊲ g ).

  Infix "⋈" := hom_eq (at level 80).

It is an equivalence relation.

Global Instance hom_eq_Equivalence {X : Set} :
Equivalence (fun g h : graph X L ⇒ g ⋈ h).

Equivalence of sets of labels.

Lemma variables_hom_eq {X : Set} (g h : graph X L) :
g ⋈ h → ⌈g ⌉ ≈ ⌈h ⌉.

If φ is injective, then g and its φ-image are equivalent.

Lemma injective_map_hom_eq {X : Set} g (φ : X → X) :
injective φ ⌊g ⌋ → g ⋈ (graph_map φ g ).

We call a graph connected when any node is reachable from its input and co-reachable from the output.

Definition connected {X} (g : graph X L) :=
∀ i, i ∈ ⌊g ⌋ → input g -[g ]→ i ∧ i -[g ]→output g.

If g and h are isomorphic (i.e. there are ø-morphisms from g to h and h to g that are inverses) then if one of then is connected so is the other.

  Lemma injective_morphism_connected {X Y:Set} g h
        (φ : X → Y) (ψ : Y → X) :
    inverse φ ψ ⌊g ⌋ → inverse ψ φ ⌊h ⌋ →
    [] ⊨ g -{φ }→ h → [] ⊨ h -{ψ }→g → connected g → connected h.

If φ is injective and g is connected then so is the image of g.

Lemma graph_map_injective_connected {X Y: Set} (φ : X → Y) g:
injective φ ⌊g ⌋ → connected g → connected (graph_map φ g).

The union of two graphs is a graph such that:

its input is the input of the first graph;
its output is that of the second graph;
its edges or the union of the edges of both graphs.

The union of g and h is written g⋄h.

  Definition graph_union {X} (g h : graph X L) : graph X L :=
    (input g ,edges g ++edges h ,output h ).

  Infix " ⋄ " := graph_union (at level 40).

  Lemma input_graph_union {X} (g h : graph X L):
    input (g ⋄ h) = input g.

  Lemma output_graph_union {X} (g h : graph X L):
    output (g ⋄ h) = output h.

  Lemma edges_graph_union {X} (g h : graph X L):
    edges (g ⋄ h) = edges g ++ edges h.

The labels of g⋄h are obtained by concatenating the labels of g and those of h.

Lemma variables_graph_union {X} (g h : graph X L):
⌈g ⋄ h ⌉ = ⌈g ⌉ ++ ⌈h ⌉.

The vertices of g⋄h are contained in the union of the vertices of g and those of h. In general this inclusion is strict, as the output of g and the input of h might be missing.

Lemma vertices_graph_union {X} (g h : graph X L) : ⌊g ⋄ h ⌋ ⊆ ⌊g ⌋++⌊h ⌋.

⋄ commutes with graph_map.

Lemma graph_map_union {V Y : Set} (φ : V → Y) (g h : graph V L) :
graph_map φ (g ⋄ h) = (graph_map φ g ) ⋄ (graph_map φ h ).

⋄ is associative.

Lemma graph_union_assoc {V : Set} (f g h : graph V L) :
f ⋄ (g ⋄ h ) = (f ⋄ g ) ⋄ h.

If the output of g is the input of h, and if this node is the only vertex appearing in both graphs, then g ⋄ h is the sequential product of g and h.

Definition good_for_seq {X} (g h : graph X L) :=
output g = input h ∧ (∀ x, x ∈ ⌊g ⌋ → x ∈ ⌊h ⌋ → x = input h ).

The identity is a premorphism from both g and h to their sequential product.

  Lemma seq_graph_union_decomp {X} (g h : graph X L):
    good_for_seq g h →
    id (input g) = input (g ⋄ h)
    ∧ id (input h) = output g
    ∧ [] ⊨ g -{id }⇀ (g ⋄ h )
    ∧ [] ⊨ h -{id }⇀ (g ⋄ h ).

If g is connected, then the set vertices of the sequential product of g and h is the union of the vertices of g and those of h.

Lemma seq_vertices_connected_graph_union {X} (g h : graph X L) :
connected g → good_for_seq g h → ⌊g ⋄ h ⌋ ≈⌊g ⌋++⌊h ⌋.

If g and h are connected, so is their sequential product.

Lemma seq_graph_union_connected {X} (g h : graph X L) :
good_for_seq g h → connected g → connected h → connected (g ⋄ h).

If g and h share the same input, the same output, and otherwise have distinct vertices then g⋄h is their parallel product.

  Definition good_for_par {X} (g h : graph X L) :=
    input g = input h
    ∧ output g = output h
    ∧ (∀ x, x ∈ ⌊g ⌋ → x ∈ ⌊h ⌋ → x = input h ∨ x = output h ).

The vertices of the parallel product is the union of the vertices.

Lemma par_vertices_graph_union {X : Set} (g h : graph X L) :
good_for_par g h → ⌊g ⋄ h ⌋≈⌊g ⌋++⌊h ⌋.

The identity is a morphism from both g and h to their parallel product.

  Lemma par_graph_union_decomp {X : Set} (g h : graph X L) :
    good_for_par g h → [] ⊨ g -{id }→ (g ⋄ h ) ∧ [] ⊨ h -{id }→ (g ⋄ h ).

  Lemma par_graph_union_decomp_left {X : Set} (g h : graph X L) :
    good_for_par g h → [] ⊨ g -{id }→ (g ⋄ h ).

  Lemma par_graph_union_decomp_right {X : Set} (g h : graph X L) :
    good_for_par g h → [] ⊨ h -{id }→ (g ⋄ h ).

The parallel product of two connected graphs is connected.

Lemma par_graph_union_connected {X : Set} (g h : graph X L) :
good_for_par g h → connected g → connected h → connected (g ⋄ h).

A graph is acyclic if its reachability relation is a partial order.

Definition acyclic {V : Set} (g: graph V L):=
PartialOrder eq (path g).

We call a graph good if it is both connected and acyclic.

Definition good {V : Set} (g: graph V L):= connected g ∧ acyclic g.

The image of an acyclic graph by an injective function is acyclic.

Lemma graph_map_injective_acyclic {X Y : Set} (φ : X → Y) g :
injective φ ⌊g ⌋ → acyclic g → acyclic (graph_map φ g).

The image of a good graph by an injective function is good.

Lemma graph_map_injective_good {X Y : Set} (φ : X → Y) g :
injective φ ⌊g ⌋ → good g → good (graph_map φ g).

We may filter a graph according to two boolean predicates.

  Definition filter_graph {A} fs ft (g : graph A L) : graph A L:=
    (input g ,filter (fun e ⇒ match e with
                           | (i,a,j) ⇒ fs i || ft j
                           end) (edges g),
     output g ).

  Lemma input_filter_graph {A : Set} (fs ft : A → bool) (g : graph A L) :
    input (filter_graph fs ft g) = input g.

  Lemma output_filter_graph {A : Set} (fs ft : A → bool) (g : graph A L) :
    output (filter_graph fs ft g) = output g.

  Lemma edges_filter_graph {A : Set} (fs ft : A → bool) (g : graph A L) :
    edges (filter_graph fs ft g) =
    filter (fun e ⇒ match e with
                  | (i,a,j) ⇒ fs i || ft j
                  end) (edges g).

We may lift paths in the filtered graph to the original graph.

Lemma filter_graph_path {A : Set} (fs ft : A → bool) g i j:
i -[ filter_graph fs ft g ]→ j → i -[g ]→ j.

The identity is a morphism from filter_graph fs ft g to g.

Lemma filter_graph_morphism {A : Set} (fs ft : A → bool) g :
[] ⊨ filter_graph fs ft g -{id }→ g.

If every vertex satisfies the predicate, then filtering doesn't change the graph.

Lemma filter_graph_true {A : Set} (fs ft : A → bool) g :
(∀ i, i ∈ ⌊g ⌋ → fs i && ft i = true ) → filter_graph fs ft g = g.

filter_graph commutes with graph_union.

  Lemma filter_graph_union {A : Set} (fs ft : A → bool) g h :
    filter_graph fs ft (g ⋄h) =
    filter_graph fs ft g ⋄ filter_graph fs ft h.

filter_graph commutes with graph_map.

  Lemma filter_graph_map {A B : Set} (fs ft : A → bool) (φ : B → A) g :
    filter_graph fs ft (graph_map φ g)
    = graph_map φ (filter_graph (fs ∘φ) (ft ∘φ) g).

End g.

Graphs with decidable labels and vertices

Section dec_g.
  Variables vert lbl : Set.
  Variable V : decidable_set vert.
  Variable L : decidable_set lbl.

In this case the edges form a decidable set.

Global Instance decidable_edges : decidable_set (@edge vert lbl).

swap a b l replaces every occurrence of the vertex a with the vertex b in the list of edges l.

Definition swap (a b : vert) (l : list (@edge vert lbl)) :=
map {|a \ b |} l.

If φ1 is an internal map from g1 to h1 and φ2 is an internal map from g2 to h2, then φ1⧼⌊g1⌋⧽φ2 is internal between g1⋄g2 and parallel product of h1 and h2.

  Lemma par_internal_graph_union {X} (g1 g2 : graph vert lbl)
        (h1 h2 : graph X lbl) φ1 φ2 :
    good_for_par h1 h2 → internal_map φ1 g1 h1 → internal_map φ2 g2 h2 →
    internal_map (φ1 ⧼⌊g1 ⌋⧽ φ2) (g1 ⋄ g2) (h1 ⋄ h2).

For the sequential product, we additionally need that h1 to be connected.

  Lemma seq_internal_graph_union {X} (g1 g2 : graph vert lbl)
        (h1 h2 : graph X lbl) φ1 φ2 :
    connected h1 →
    good_for_seq h1 h2 →
    internal_map φ1 g1 h1 →
    internal_map φ2 g2 h2 →
    internal_map (φ1 ⧼⌊g1 ⌋⧽φ2) (g1 ⋄ g2) (h1 ⋄ h2).

We can combine a morphism from g1 to h1 and a morphism from g2 to h2 as a morphism from the sequential product of g1 and g2 to the sequential product of h1 and h2.

  Lemma seq_morphism_graph_union {X}
        (g1 g2 : graph vert lbl) (h1 h2 : graph X lbl) φ1 φ2 A :
    connected h1 →
    good_for_seq g1 g2 →
    good_for_seq h1 h2 →
    A ⊨ g1 -{φ1 }→ h1 →
    A ⊨ g2 -{φ2 }→ h2 →
    A ⊨ g1 ⋄ g2 -{φ1 ⧼⌊g1 ⌋⧽φ2 }→ h1 ⋄ h2.

We can combine a morphism from g1 to h and a morphism from g2 to h as a morphism from the parallel product of g1 and g2 to h.

  Lemma par_morphism_graph_union {X}
        (g1 g2 : graph vert lbl) (h : graph X lbl) φ1 φ2 A :
    good_for_par g1 g2 →
    A ⊨ g1 -{φ1 }→ h →
    A ⊨ g2 -{φ2 }→ h →
    A ⊨ g1 ⋄ g2 -{φ1 ⧼⌊g1 ⌋⧽φ2 }→ h.

We can combine a morphism from g1 to h1 and a morphism from g2 to h2 as a morphism from the parallel product of g1 and g2 to the parallel product of h1 and h2.

  Lemma par_par_morphism_graph_union {X}
        (g1 g2 : graph vert lbl) (h1 h2 : graph X lbl) φ1 φ2 A :
    good_for_par g1 g2 →
    good_for_par h1 h2 →
    A ⊨ g1 -{φ1 }→ h1 →
    A ⊨ g2 -{φ2 }→ h2 →
    A ⊨ g1 ⋄ g2 -{φ1 ⧼⌊g1 ⌋⧽φ2 }→ h1 ⋄ h2.

The parallel product is smaller than both its arguments.

  Lemma par_hom_order_weak_left (g1 g2 : graph vert lbl) A :
    good_for_par g1 g2 → A ⊨ g1 ⋄ g2 ⊲ g1.

  Lemma par_hom_order_weak_right (g1 g2 : graph vert lbl) A :
    good_for_par g1 g2 → A ⊨ g1 ⋄ g2 ⊲ g2.

If both g1 and g2 are greater than h so is their parallel product.

Lemma par_smaller_hom_order (g1 g2 h : graph vert lbl) A :
good_for_par g1 g2 → A ⊨ h ⊲ g1 → A ⊨ h ⊲ g2 → A ⊨ h ⊲ g1 ⋄ g2.

If the parallel product of g1 and g2 is greater than a graph h, then both g1 and g2 are greater than h.

Lemma smaller_par_hom_order (g1 g2 h : graph vert lbl) A :
good_for_par g1 g2 → A ⊨ h ⊲ g1 ⋄ g2 → A ⊨ h ⊲ g1 ∧ A ⊨ h ⊲ g2.

The next two lemma state that the homomorphism order on graphs is a congruence for the parallel and sequential products.

  Lemma seq_hom_order (g1 g2 h1 h2 : graph vert lbl) A :
    connected g1 → good_for_seq g1 g2 → good_for_seq h1 h2 →
    A ⊨ g1 ⊲ h1 → A ⊨ g2 ⊲ h2 → A ⊨ g1 ⋄ g2 ⊲ h1 ⋄ h2.

  Lemma par_hom_order (g1 g2 h1 h2 : graph vert lbl) A :
    good_for_par g1 g2 → good_for_par h1 h2 →
    A ⊨ g1 ⊲ h1 → A ⊨ g2 ⊲ h2 → A ⊨ g1 ⋄ g2 ⊲ h1 ⋄ h2.

If φ is a morphism from the sequential product of g1 and g2 to h, then it is a premorphism from both g1 and g2 to h.

  Lemma seq_morphism_graph_union_left {X} (g1 g2 : graph vert lbl)
        (h : graph X lbl) φ A :
    good_for_seq g1 g2 → A ⊨ g1 ⋄ g2 -{φ }→ h →
    A ⊨ g1 -{φ }⇀ h
    ∧ A ⊨ g2 -{φ }⇀ h
    ∧ φ (input g1) = input h
    ∧ φ (output g2) = output h.

If φ is a morphism from the parallel product of g1 and g2 to h, then it is a morphism from both g1 and g2 to h.

  Lemma par_morphism_graph_union_left {X} (g1 g2 : graph vert lbl)
        (h : graph X lbl) φ A :
    good_for_par g1 g2 → A ⊨ g1 ⋄ g2 -{φ }→ h →
    A ⊨ g1 -{φ }→ h ∧ A ⊨ g2 -{φ }→ h.

Conversely, if φ is a morphism from both g1 and g2 to h, then it is a morphism from the parallel product of g1 and g2 to h.

  Lemma par_morphism_graph_union_right {X} (g1 g2 : graph vert lbl)
        (h : graph X lbl) φ A :
    good_for_par g1 g2 → A ⊨ g1 -{φ }→ h → A ⊨ g2 -{φ }→ h →
    A ⊨ g1 ⋄ g2 -{φ }→ h.

If g and h are good and there is a path from i to k in their parallel product, then there this path can be found either in g or in h.

  Lemma path_par_union (g h: graph vert lbl) i k :
    good_for_par g h → good g → good h → i -[g ⋄ h ]→ k →
    i -[g ]→ k ∨ i -[h ]→ k.

If g1 and g2 are good, and there is a path inside their parallel product from i, a node from g1, to k, a node from g2, then either i is the input of the graph, or k is its output.

  Lemma path_par_union_cross
      (g1 g2 : graph vert lbl) i k :
    good_for_par g1 g2 → good g1 → good g2 →
    i ∈ ⌊g1 ⌋ → k ∈ ⌊g2 ⌋ →
    i -[g1 ⋄g2 ]→ k → i = input (g1 ⋄g2) ∨ k = output (g1 ⋄g2).

In the next two lemma, we show that a path in a parallel product whose two ends belong to the same component can be lifted to that component.

  Lemma path_par_union_left (g1 g2 : graph vert lbl) i k :
    good_for_par g1 g2 → good g1 → good g2 →
    i ∈ ⌊g1 ⌋ → k ∈ ⌊g1 ⌋ →
    i -[g1 ⋄g2 ]→ k → i -[g1 ]→ k.

  Lemma path_par_union_right (g1 g2 : graph vert lbl) i k :
    good_for_par g1 g2 → good g1 → good g2 →
    i ∈ ⌊g2 ⌋ → k ∈ ⌊g2 ⌋ → i -[g1 ⋄g2 ]→ k → i -[g2 ]→ k.

For any two graph g1, g2 if there is a path from i to k in either of the graphs, there is one in g1⋄g2.

Lemma path_graph_union (g1 g2 : graph vert lbl) i k :
i -[g1 ]→ k ∨ i -[g2 ]→ k → i -[g1 ⋄g2 ]→ k.

If g1 and g2 are good, then a path in their sequential product exists from i to k exactly if either i and k are equal, or they are different and one of the following conditions hold:

they both come from the same graph, and are linked in that graph
or i is a vertex of g1 and k is a vertex of g2.

  Lemma path_seq (g1 g2 : graph vert lbl) i k :
    good_for_seq g1 g2 → good g1 → good g2 →
    i -[g1 ⋄g2 ]→ k ↔
    i = k
    ∨ (i ≠ k ∧
       (( i ∈ ⌊g1 ⌋ ∧ k ∈ ⌊g1 ⌋ ∧ i -[g1 ]→ k )
        ∨ ( i ∈ ⌊g2 ⌋ ∧ k ∈ ⌊g2 ⌋ ∧ i -[g2 ]→ k )
        ∨ ( i ∈ ⌊g1 ⌋ ∧ k ∈ ⌊g2 ⌋))).

If two graphs are good then their sequential and parallel compositions are also good.

  Lemma good_seq_graph_union (g1 g2 : graph vert lbl) :
    good_for_seq g1 g2 → good g1 → good g2 → good (g1 ⋄g2).

  Lemma good_par_graph_union (g1 g2 : graph vert lbl) :
    good_for_par g1 g2 → good g1 → good g2 → good (g1 ⋄g2).
End dec_g.
Section p.

  Variables vert lbl : Set.
  Variable V : decidable_set vert.
  Variable L : decidable_set lbl.
  Context { g : graph vert lbl }.

Boolean path predicate

Notation " i → j " := (i -[g ]→ j) (at level 80).

ispath g l i j states that l is a valid path from i to j in g.

  Fixpoint ispath l i j :=
    match l with
    | [] ⇒ i = j
    | k::l ⇒ (∃ α, (i ,α ,k) ∈ (edges g ))
             ∧ ispath l k j
    end.

Hence we can prove that whenever there is a path according to ispath from i to j, they are related by the path g relation.

Lemma ispath_path l i j :
ispath l i j → i → j.

We can combine paths by concatenating them.

Lemma ispath_app i j k p1 p2 :
ispath p1 i j → ispath p2 j k → ispath (p1 ++ p2) i k.

Furthermore, if j is reachable from i, then there is a path linking them.

Lemma path_ispath i j :
i → j → ∃ l, ispath l i j.

neighbour g i k tests if there is an edge in g whose source is i and target is k.

  Definition neighbour i k :=
    existsb (fun e ⇒ match e with
                   | ((x,_),y) ⇒ eqX x i && eqX y k end)
            (edges g).

  Lemma neighbour_spec i k :
    neighbour i k = true ↔ ∃ α, (i ,α ,k ) ∈ (edges g ).

is_pathb is the boolean version of is_path.

  Fixpoint ispathb l i j :=
    match l with
    | [] ⇒ eqX i j
    | k::l ⇒ neighbour i k && ispathb l k j
    end.

  Lemma ispathb_ispath l i j :
    ispathb l i j = true ↔ ispath l i j.

We can decompose paths using the intermediary vertices.

Lemma split_path i j k l m :
ispath (l ++(k ::m )) i j → ispath m k j.

If l is a path from i to j, then either i doesn't appear in l, or we can split l into m++i::n such that i doesn't appear in n and n is a path from i to j.

  Lemma path_ispath_short i j l :
    ispath l i j →
    ¬ i ∈ l ∨ ∃ m n, l = m ++(i ::n ) ∧ ¬ i ∈ n ∧ ispath n i j.

Iterating the previous lemma, we can remove every duplicate from a path. Thus is j is reachable from i, there is a path without duplication linking them.

Lemma short_path i j :
i → j → ∃ l, NoDup (i ::l) ∧ ispath l i j.

A path can only use vertices.

Lemma path_is_vertices i j l :
ispath l i j → l ⊆ ⌊g ⌋.

ex_path g i j l n tests whether there is a path of length smaller or equal to n using elements from l linking i and j.

  Fixpoint ex_path i j l n :=
    match n with
    | O ⇒ eqX i j
    | S n ⇒
      eqX i j || existsb (fun k ⇒ neighbour i k && ex_path k j l n) l
    end.

  Lemma ex_path_spec i j l n :
    ex_path i j l n = true ↔
    ∃ p, ispath p i j ∧ p ⊆ l ∧ length p ≤ n.

We may now define exists_path, a boolean function corresponding to the predicate path.

  Definition exists_path i j := ex_path i j ⌊g ⌋ (length ⌊g ⌋).

  Notation " i -?→ j " := (exists_path i j) (at level 50).

  Lemma exists_path_spec i j :
    i -?→ j = true ↔ i → j.

The visible set of vertices of g from k is the set of vertices of g that are either reachable or co-reachable from k.

Definition visible k :=
filter (fun i ⇒ i -?→ k || (k -?→ i )) ⌊g ⌋.

This is also the set of vertices of the filtered graph of g where the source predicate is "is reachable from k" and the target predicate is "can reach k", granted that g is reachable.

  Lemma filter_graph_visible k :
    connected g → k ∈ ⌊g ⌋ →
    ⌊filter_graph (fun i ⇒ k -?→ i) (fun j ⇒ j -?→ k) g ⌋
     ≈ visible k.
End p.
Notation " i -[ g ]?→ j " := (exists_path g i j) (at level 80).

Morphisms between graphs with decidable vertices

Section dec_hom.
  Variables vert1 vert2 lbl : Set.
  Variable V1 : decidable_set vert1.
  Variable V2 : decidable_set vert2.
  Variable L : decidable_set lbl.
  Notation grph A := (graph A lbl).

First, we notice that if φ is a morphism between g and h, then there must be a morphism ψ that has finite support.

  Lemma is_morphism_finite_function A φ
        (g : grph vert1) (h : grph vert2):
    A ⊨ g -{φ }→ h →
    ∃ ψ, finite_support ψ ⌊g ⌋ ⌊h ⌋ (input h) ∧ A ⊨ g -{ψ }→ h.

internal_map_b φ g h is a boolean testing whether φ is internal from g to h.

  Definition internal_map_b φ (g : grph vert1) (h : grph vert2) :=
    inclb (List.map φ ⌊g ⌋) ⌊h ⌋.

  Lemma internal_map_b_spec φ g h :
    internal_map_b φ g h = true ↔ internal_map φ g h.

is_morphismb A φ g h is a boolean testing whether φ is actually an A-morphism between g and h.

  Definition is_morphismb A φ (g : grph vert1) (h : grph vert2) :=
    (eqX (φ (input g)) (input h))
      &&
      ((eqX (φ (output g)) (output h))
         &&
         ((forallb (fun e ⇒
                      match e with
                      | ((i,a),j) ⇒
                        ((inb a A ) && (eqX (φ i) (φ j)))
                        || (inb ((φ i,a),φ j) (edges h))
                      end)
                   (edges g))
            && internal_map_b φ g h )).

  Lemma is_morphismb_correct A φ g h :
    is_morphismb A φ g h = true ↔ A ⊨ g -{ φ }→ h.

ex_is_morphismb A g h is a boolean testing whether there exists an A-morphism from g to h.

  Definition ex_is_morphismb A (g : grph vert1) (h : grph vert2) :=
    existsb (fun φ ⇒ is_morphismb A φ g h)
            (finite_support_functions _ ⌊g ⌋ ⌊h ⌋ (input h)).

  Lemma ex_is_morphismb_correct A g h :
    ex_is_morphismb A g h = true ↔ ∃ φ, A ⊨ g -{φ }→ h.

End dec_hom.