# 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 gList.map (sndfst) (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 φ 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 Lg 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.
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 gh.
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 gh 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 gh 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.
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.
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.
If g and h are connected, so is their sequential product.
If g and h share the same input, the same output, and otherwise have distinct vertices then gh 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.
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 ematch 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 ematch 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 (gh) =
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 g1g2 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 (φ1g1φ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.
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 -{φ1g1φ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.
The parallel product is smaller than both its arguments.
If both g1 and g2 are greater than h so is their parallel product.
If the parallel product of g1 and g2 is greater than a graph h, then both g1 and g2 are greater than h.
The next two lemma state that the homomorphism order on graphs is a congruence for the parallel and sequential products.
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.
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.
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.
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.
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.
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.
For any two graph g1, g2 if there is a path from i to k in either of the graphs, there is one in g1g2.
Lemma path_graph_union (g1 g2 : graph vert lbl) i k :
i -[g1]→ k i -[g2]→ k i -[g1g2]→ 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.
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 (g1g2).

Lemma good_par_graph_union (g1 g2 : graph vert lbl) :
good_for_par g1 g2 good g1 good g2 good (g1g2).
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 ematch 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::lneighbour 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.
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
| OeqX i j
| S n
eqX i j || existsb (fun kneighbour 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 ii -?→ 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 ik -?→ i) (fun jj -?→ 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.
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.