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));
        destruct_head_hnf @sig;
        split_and;
        subst;
        reflexivity
      ).
  Defined.
End conversion.