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.