Library Exercise_4_1_2_31


Require Import Utf8.
Require Import Omega JMeq.
Require Import Common Isomorphism PathsCategory Graph.

Set Implicit Arguments.

Generalizable All Variables.


Exercise 4.1.2.31

Problem

Recall the graph G from Example 3.3.1.2. Let C = F(G) be the free category on G. What is Hom_C(v, x)? What is Hom_C(x, v)?
Here is a picture of the graph G = (V, A, src, tgt): << g ________ v f w / -------> x \________ h G := j __ ________ / / i | y z \__/ ________/ k >> We have [V = {v, w, x, y, z}] and [A = {f, g, h, i, j, k}]. The source and target functions [src, tgt : A V] can be captured in the table to the left below: << A || src | tgt V -------------- --- f || v | w v g || w | x w h || w | x x i || y | y y j || y | z z k || z | y >>

  Inductive V := v | w | x | y | z.
  Inductive A : VVSet :=
  | f : A v w
  | g : A w x
  | h : A w x
  | i : A y y
  | j : A y z
  | k : A z y.

  Definition G : Graph := @Build_Graph V A.
  Definition C : Category := @PathsCategory (Vertex G) (Edge G).

  Inductive Hom_C_v_x := gf | hf.
  Definition Hom_C_x_v := .

  Local Ltac t' tac :=
    repeat match goal with
             | _progress (simpl in *; repeat intro; hnf in *; tac; trivial)
             | [ H : _ |- _ ] ⇒ solve [ inversion H; trivial ]
             | [ H : _ |- _ ] ⇒ solve [ destruct H; trivial ]
             | [ H : _ |- _ ] ⇒ solve [ apply JMeq_eq; destruct H;
                                         try reflexivity; trivial ]
             | _progress subst_eq_refl
             | [ |- context[match ?x return with __ end] ]
               ⇒ solve [ destruct x ]
           end.

  Local Ltac t'' tac :=
    repeat match goal with
             | [ e : A ?a ?b |- _ ] ⇒ let a' := fresh in
                                        let b' := fresh in
                                        set (a' := a) in *;
                                          set (b' := b) in *;
                                          cut (a = a'); [ | reflexivity ];
                                          cut (b = b'); [ | reflexivity ];
                                          destruct e;
                                          t' tac
             | _progress (repeat f_equal)
             | _progress clear
             | _progress (t' tac)
           end.

  Local Ltac t''' tac :=
    t'' tac; try (apply JMeq_eq; solve [ t'' tac ]).

  Local Ltac t'''' tac :=
    repeat match goal with
             | _progress (t'' tac; try solve [ left; t''' idtac
                                                 | right; t''' idtac ])
             | [ H : _ = _ |- _ ] ⇒ destruct H
           end.
  Lemma Hom_C_x_v_empty_helper : Morphism C x vFalse.
    intro m; hnf in m.
    match goal with
      | [ m : path _ ?a ?b |- _ ] ⇒ let a' := fresh in
                                     let b' := fresh in
                                     set (a' := a) in *;
                                       set (b' := b) in *;
                                       cut (a = a'); [ | reflexivity ];
                                       cut (b = b'); [ | reflexivity ];
                                       clearbody a' b';
                                       induction m;
                                       t' subst
    end.
  Qed.
  Lemma Hom_C_v_x_only_helper S D (m : Morphism C S D)
        (Hs : v = S)
        (Hd : x = D)
        (g' : Morphism C _ _ := AddEdge NoEdges g)
        (f' : Morphism C _ _ := AddEdge NoEdges f)
        (h' : Morphism C _ _ := AddEdge NoEdges h)
  : (m = match Hs with
           | eq_refl ⇒ (match Hd with
                           | eq_reflg'
                         end f')%morphism
         end)
    + (m = match Hs with
             | eq_refl ⇒ (match Hd with
                             | eq_reflh'
                           end f')%morphism
           end).
    hnf in m;
    subst g' f' h'; simpl.
    induction m; [ subst | ]; t' idtac.
    induction m; [ subst | ]; t' idtac.
    induction m; [ | ]; t' idtac;
    t'''' idtac.
  Qed.

  Let Hom {obj} C := @Morphism obj C.
  Lemma Hom_C_x_v_empty : (Hom C x v ).
  Proof.
     (fun x : Hom C x vmatch Hom_C_x_v_empty_helper x return with end).
     (fun x : match x return _ with end);
      simpl;
      intro; t' idtac.
  Qed.

  Lemma Hom_C_v_x_two_elements : (Hom C v x Hom_C_v_x).
  Proof.
     (fun x : Hom C v xmatch Hom_C_v_x_only_helper x eq_refl eq_refl with
                                   | inl _gf
                                   | inr _hf
                                 end).
     (let g' := AddEdge NoEdges g : Morphism C _ _ in
            let f' := AddEdge NoEdges f : Morphism C _ _ in
            let h' := AddEdge NoEdges h : Morphism C _ _ in
            (fun x : Hom_C_v_xmatch x return _ with
                                    | gf ⇒ (g' f')%morphism
                                    | hf ⇒ (h' f')%morphism
                                  end));
      simpl;
      try intros [ | ];
      intros;
      try match goal with
            | [ |- context[match ?x with __ end] ] ⇒ solve [ destruct x; t' idtac ]
          end.
  Qed.
End Exercise_4_1_2_31.