# Library Graph

Require Import Utf8.
Require Import JMeq.
Require Import FunctionalExtensionality ProofIrrelevance.
Require Import Common.

Set Implicit Arguments.

In a dependently typed programming language like, Coq, it is more natural to define a separate set of edges for each pair of vertices. I define both this type of graph and the one in the book, and define an almost-isomorphism between them. It's actually only an isomorphism up to isomorphism of types; it requires univalence to be a proper isomorphism.

Record Graph :=
{
Vertex :> Type;
Edge : VertexVertexType
}.

Record Graph' :=
{
Vertex' :> Type;
Arrow' : Type;
Graph'Source : Arrow'Vertex';
Graph'Target : Arrow'Vertex'
}.

Section graph_equivalence.
Definition GraphToGraph' (G : Graph) : Graph'
:= {| Vertex' := Vertex G;
Arrow' := { sd : G × G & Edge G (fst sd) (snd sd) };
Graph'Source := (fun sdm fst (projT1 sdm));
Graph'Target := (fun sdm snd (projT1 sdm)) |}.

Definition Graph'ToGraph (G : Graph') : Graph
:= {| Vertex := Vertex' G;
Edge := (fun s d { m : Arrow' G
| Graph'Source _ m = s
Graph'Target _ m = d }) |}.
End graph_equivalence.

## Graph Homomorphisms

Section graph_homomorphisms.
Record GraphHomomorphism (G G' : Graph) :=
{
OnVertices :> Vertex GVertex G';
OnEdges
: src tgt,
Edge G src tgt
→ Edge G' (OnVertices src) (OnVertices tgt)
}.

Definition identity_graph_homomorphism (G : Graph)
: GraphHomomorphism G G.
(fun xx).
exact (fun _ _ xx).
Defined.

Definition compose_graph_homomorphisms
(G G' G'' : Graph)
: GraphHomomorphism G' G''GraphHomomorphism G G'GraphHomomorphism G G''.
intros m1 m2.
(fun xm1 (m2 x)).
exact (fun _ _ eOnEdges m1 _ _ (OnEdges m2 _ _ e)).
Defined.

Lemma GraphHomomorphism_Eq (G G' : Graph)
(m m' : GraphHomomorphism G G')
: ( x, OnVertices m x = OnVertices m' x)
→ ( src tgt e, OnEdges m src tgt e == OnEdges m' src tgt e)
→ m = m'.
intros H1 H2.
assert (H1' : OnVertices m = OnVertices m')
by (apply functional_extensionality_dep; assumption);
destruct m, m';
simpl in *;
subst;
f_equal;
repeat (apply functional_extensionality_dep; intro);
apply JMeq_eq;
intuition.
Qed.
End graph_homomorphisms.

And now the version in the book
Section graph'_homomorphisms.
Record Graph'Homomorphism (G G' : Graph') :=
{
OnVertices' :> Vertex' GVertex' G';
OnArrows' : Arrow' GArrow' G';
SourceCommutes' : x, OnVertices' (Graph'Source G x)
= Graph'Source G' (OnArrows' x);
TargetCommutes' : x, OnVertices' (Graph'Target G x)
= Graph'Target G' (OnArrows' x)
}.

Definition identity_graph'_homomorphism (G : Graph')
: Graph'Homomorphism G G.
(fun xx) (fun xx);
reflexivity.
Defined.

Definition compose_graph'_homomorphisms
(G G' G'' : Graph')
: Graph'Homomorphism G' G''Graph'Homomorphism G G'Graph'Homomorphism G G''.
intros m1 m2.
(fun xm1 (m2 x)) (fun xOnArrows' m1 (OnArrows' m2 x));
abstract (
intros;
simpl;
repeat rewrite SourceCommutes';
repeat rewrite TargetCommutes';
reflexivity
).
Defined.

Lemma Graph'Homomorphism_Eq (G G' : Graph')
(m m' : Graph'Homomorphism G G')
: ( x, OnVertices' m x = OnVertices' m' x)
→ ( x, OnArrows' m x = OnArrows' m' x)
→ m = m'.
intros H1 H2.
assert (H1' : OnVertices' m = OnVertices' m')
by (apply functional_extensionality_dep; assumption).
assert (H2' : OnArrows' m = OnArrows' m')
by (apply functional_extensionality_dep; assumption).
destruct m, m';
simpl in *;
subst;
f_equal;
apply ProofIrrelevance.proof_irrelevance.
Qed.
End graph'_homomorphisms.

Section conversion.
Definition GraphHomomorphismToGraph'Homomorphism (G G' : Graph) (f : GraphHomomorphism G G')
: Graph'Homomorphism (GraphToGraph' G) (GraphToGraph' G')
:= Build_Graph'Homomorphism (GraphToGraph' G) (GraphToGraph' G')
(OnVertices f)
(fun sdeexistT _
(OnVertices f (fst (projT1 sde)),
OnVertices f (snd (projT1 sde)))
(OnEdges f _ _ (projT2 sde))
: { sd : G' × G' & Edge G' (fst sd) (snd sd) } )
(fun _eq_refl)
(fun _eq_refl).

Definition Graph'HomomorphismToGraphHomomorphism (G G' : Graph') (f : Graph'Homomorphism G G')
: GraphHomomorphism (Graph'ToGraph G) (Graph'ToGraph G').
refine (Build_GraphHomomorphism (Graph'ToGraph G) (Graph'ToGraph G')
(OnVertices' f)
(fun src tgt mexist _ (OnArrows' f (proj1_sig m)) _));
abstract (
split;
(rewrite <- (SourceCommutes' f) || rewrite <- (TargetCommutes' f));