• API
• FAQ
• Tools
• Archive
SHARE
TWEET

Untitled

a guest Jul 7th, 2017 76 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
1. Set Implicit Arguments.
2.
3. Ltac hypothesis := match goal with [ H : _ |- _ ] => apply H end.
4.
5. Inductive False : Type :=.
6.
7. Definition Not (P : Type) := P -> False.
8.
9. Inductive True : Type :=
10. | I : True.
11.
12. Inductive Identity (T : Type) (t : T) : T -> Type :=
13. | identical : Identity t t.
14.
15. Inductive And (P Q : Type) : Type :=
16. | both : P -> Q -> And P Q.
17.
18. Inductive Or (P Q : Type) : Type :=
19. | inleft : P -> Or P Q
20. | inright : Q -> Or P Q.
21.
22. Definition Decidable (P : Type) := Or P (Not P).
23.
24. Definition And_idem (P : Type) : P -> And P P.
25. intro p; apply (both p p).
26. Defined.
27.
28. Inductive Sigma (T : Type) (P : T -> Type) : Type :=
29. | witness : forall t : T, P t -> Sigma P.
30.
31. Definition Relation (T : Type) := T -> T -> Type.
32.
33. Record Equivalence {T : Type} (R : Relation T)
34.   := { equivalence_reflexivity : forall x, R x x
35.      ; equivalence_symmetry : forall x y, R x y -> R y x
36.      ; equivalence_transitivity : forall x y z, R x y -> R y z -> R x z
37.      }.
38.
39. Theorem Equivalence_Identity {T : Type} : Equivalence (@Identity T).
40. apply Build_Equivalence.
41. intros; constructor.
42. intros; elim H; constructor.
43. intros; elim H0; elim H; constructor.
44. Defined.
45.
46. Theorem Equivalence_Identity_map {X T : Type} (f : X -> T) : Equivalence (fun x y => @Identity T (f x) (f y)).
47. apply Build_Equivalence.
48. intros; constructor.
49. intros; elim H; constructor.
50. intros; elim H0; elim H; constructor.
51. Defined.
52.
53. Record Category (Ob : Type) (Hom : Ob -> Ob -> Type)
54.                 (Hom_eq : forall X Y, Relation (Hom X Y))
55.   := { identity : forall X, Hom X X
56.      ; compose : forall X Y Z, Hom X Y -> Hom Y Z -> Hom X Z
57.      ; compose_respectful_left : forall X Y Z (f f' : Hom X Y) (g : Hom Y Z),
58.        Hom_eq _ _ f f' -> Hom_eq _ _ (compose f g) (compose f' g)
59.      ; compose_respectful_right : forall X Y Z (f : Hom X Y) (g g' : Hom Y Z),
60.        Hom_eq _ _ g g' -> Hom_eq _ _ (compose f g) (compose f g')
61.      ; hom_equivalence : forall X Y, Equivalence (Hom_eq X Y)
62.      ; category_left_identity : forall X Y (f : Hom X Y),
63.        Hom_eq _ _ (compose (identity _) f) f
64.      ; category_right_identity : forall X Y (f : Hom X Y),
65.        Hom_eq _ _ (compose f (identity _)) f
66.      ; category_associativity : forall X Y Z W (f : Hom X Y) (g : Hom Y Z) (h : Hom Z W),
67.        Hom_eq _ _ (compose f (compose g h))
68.                   (compose (compose f g) h)
69.      }.
70.
71. Notation "f '[' C ']'  g" := (compose C _ _ _ f g) (at level 20).
72. Notation "'1_' C" := (identity C _) (at level 20).
73.
74. Ltac refl :=
75.   eapply equivalence_reflexivity;
76.     [apply hom_equivalence;assumption].
77. Ltac symm :=
78.   eapply equivalence_symmetry;
79.     [apply hom_equivalence;assumption|idtac].
80. Ltac trans :=
81.   eapply equivalence_transitivity;
82.     [apply hom_equivalence;assumption|idtac|idtac].
83.
84. Section Isomorphism.
85.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
86.
87.   Definition Isomorphism (X Y : C_Ob) :=
88.     @Sigma (And (C_Hom X Y) (C_Hom Y X))
89.            (fun fg =>
90.              match fg with
91.                | both f g =>
92.                  And (C_Hom_eq (compose C _ _ _ g f) (identity C _))
93.                      (C_Hom_eq (compose C _ _ _ f g) (identity C _))
94.              end).
95.
96.   Definition isomorphism_to (X Y : C_Ob) (i : Isomorphism X Y) : C_Hom X Y.
97.   destruct i as [[to from] _]; apply to.
98.   Defined.
99.
100.   Definition isomorphism_from (X Y : C_Ob) (i : Isomorphism X Y) : C_Hom Y X.
101.   destruct i as [[to from] _]; apply from.
102.   Defined.
103.
104.   Theorem Isomorphism_Equivalence : Equivalence Isomorphism.
105.   apply Build_Equivalence.
106.
107.   Lemma Isomorphism_Identity : forall x : C_Ob, Isomorphism x x.
108.     intro x; apply (witness _ (both (identity C x) (identity C x))).
109.     apply And_idem.
110.     apply category_left_identity.
111.   Defined.
112.   apply Isomorphism_Identity.
113.
114.   intros x y [[I J] [i j]].
115.   apply (witness _ (both J I)).
116.   apply (both j i).
117.
118.   Lemma Isomorphism_Compose : forall x y z : C_Ob, Isomorphism x y -> Isomorphism y z -> Isomorphism x z.
119.     intros x y z [[I J] [i j]] [[I' J'] [i' j']].
120.     apply (witness _ (both (compose C _ _ _ I I') (compose C _ _ _ J' J))).
121.     apply both.
122.
123.     trans.
124.     apply (category_associativity C).
125.     trans.
126.     apply (compose_respectful_left C).
127.     trans.
128.     symm.
129.     apply (category_associativity C).
130.     apply (compose_respectful_right C).
131.     apply i.
132.     assert (C_Hom_eq (compose C z y y J' (identity C y))
133.                      J').
134.     apply category_right_identity.
135.     trans.
136.     apply (compose_respectful_left C).
137.     apply X.
138.     assumption.
139.
140.     trans.
141.     apply (category_associativity C).
142.     trans.
143.     apply (compose_respectful_left C).
144.     trans.
145.     symm.
146.     apply (category_associativity C).
147.     apply (compose_respectful_right C).
148.     apply j'.
149.     assert (C_Hom_eq (compose C x y y I (identity C y))
150.                      I).
151.     apply category_right_identity.
152.     trans.
153.     apply (compose_respectful_left C).
154.     apply X.
155.     assumption.
156.     Defined.
157.   apply Isomorphism_Compose.
158.   Defined.
159. End Isomorphism.
160.
161. Section Functor.
162.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
163.   Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).
164.
165.   Record Functor
166.     := { Map_Ob : C_Ob -> D_Ob
167.        ; Map_Hom : forall X Y, C_Hom X Y -> D_Hom (Map_Ob X) (Map_Ob Y)
168.        ; functor_identity : forall X, D_Hom_eq (Map_Hom (identity C X)) (identity D (Map_Ob X))
169.        ; functor_compose : forall X Y Z (f : C_Hom X Y) (g : C_Hom Y Z),
170.          D_Hom_eq (Map_Hom (compose C _ _ _ f g)) (compose D _ _ _ (Map_Hom f) (Map_Hom g))
171.        ; Map_Hom_respectful : forall X Y (f f' : C_Hom X Y),
172.          C_Hom_eq f f' -> D_Hom_eq (Map_Hom f) (Map_Hom f')
173.     }.
174.
175.   Notation "F '@' x" := (Map_Ob F x) (at level 20).
176.   Notation "F '\$' f" := (Map_Hom F f) (at level 20).
177.
178.   Definition Functor_equality (F G : Functor) :=
179.     @Sigma (forall X : C_Ob,
180.              Isomorphism D (Map_Ob F X) (Map_Ob G X))
181.           (fun Ob_iso =>
182.             forall X Y (f : C_Hom X Y),
183.               D_Hom_eq (Map_Hom F f)
184.                        (compose D _ _ _
185.                          (isomorphism_to (Ob_iso _))
186.                          (compose D _ _ _
187.                            (Map_Hom G f)
188.                             (isomorphism_from (Ob_iso _))))).
189.
190.   Theorem Functor_equivalence : Equivalence Functor_equality.
191.     apply Build_Equivalence.
192.
193.     intro x.
194.     unfold Functor_equality.
195.     apply witness with (t := (fun X => @Isomorphism_Identity _ _ _ D (Map_Ob x X))).
196.     intros X Y f.
197.     simpl.
198.     trans.
199.     symm.
200.     apply category_left_identity.
201.     apply compose_respectful_right.
202.     trans.
203.     symm.
204.     apply category_right_identity.
205.     apply compose_respectful_right.
206.     refl.
207.
208.     intros F G.
209.     intros [F' F''].
210.
211.     pose (Isomorphism_Equivalence D).
212.     pose (match e with
213.             | Build_Equivalence _ Isymm _ => Isymm
214.           end) as Isymm.
215.     unfold Functor_equality.
216.     apply (witness _ (fun X => Isymm _ _ (F' X))).
217.     intros X Y f.
218.     unfold Isymm in *; unfold e in *; simpl.
219.     generalize (F'' _ _ f).
220.
221.     destruct (F' X); simpl.
222.     destruct t; simpl.
223.     destruct y; simpl.
224.     destruct (F' Y); simpl.
225.     destruct t; simpl.
226.     destruct y; simpl.
227.
228.     intro.
229.     assert (
230.       D_Hom_eq (compose D _ _ _ d0 (compose D _ _ _ (Map_Hom F f) d3))
231.       (compose D _ _ _ d0 (compose D _ _ _
232.         (compose D (Map_Ob F X) (Map_Ob G X) (Map_Ob F Y) d
233.             (compose D (Map_Ob G X) (Map_Ob G Y) (Map_Ob F Y)
234.                (Map_Hom G f) d4)) d3))
235.       ).
236.     apply compose_respectful_right.
237.     apply compose_respectful_left.
238.     assumption.
239.
240.     trans.
241.     Focus 2.
242.     symm.
243.     apply X1.
244.     (* Gf = (d0 ((d (Gf d4)) d3)) *)
245.     Lemma YUK
246.       (F : Functor)
247.       (G : Functor)
248.       (X : C_Ob)
249.       (Y : C_Ob)
250.       (f : C_Hom X Y)
251.       (d : D_Hom (F @ X) (G @ X))
252.       (d0 : D_Hom (G @ X) (F @ X))
253.       (d1 : D_Hom_eq (d0 [D] d) (identity D _))
254.       (d2 : D_Hom_eq (d [D] d0) (identity D _))
255.       (d3 : D_Hom (F @ Y) (G @ Y))
256.       (d4 : D_Hom (G @ Y) (F @ Y))
257.       (d5 : D_Hom_eq (d4 [D] d3) (identity D _))
258.       (d6 : D_Hom_eq (d3 [D] d4) (identity D _))
259.       (X0 : D_Hom_eq (F \$ f) (d [D] ((G \$ f) [D] d4)))
260.       (X1 : D_Hom_eq (d0 [D] ((F \$ f) [D] d3))
261.              (d0 [D] ((d [D] ((G \$ f) [D] d4)) [D] d3))) :
262.       D_Hom_eq (G \$ f) (d0 [D] ((d [D] ((G \$ f) [D] d4)) [D] d3)).
263.
264.       cut (D_Hom_eq (G \$ f) ((G \$ f) [D] (identity D _))).
265.       cut (D_Hom_eq ((G \$ f) [D] (identity D _)) ((G \$ f) [D] (d4 [D] d3))).
266.       cut (D_Hom_eq ((G \$ f) [D] (d4 [D] d3)) ((identity D _) [D] ((G \$ f) [D] (d4 [D] d3)))).
267.       cut (D_Hom_eq ((identity D _) [D] ((G \$ f) [D] (d4 [D] d3))) ((d0 [D] d) [D] ((G \$ f) [D] (d4 [D] d3)))).
268.       cut (D_Hom_eq ((d0 [D] d) [D] ((G \$ f) [D] (d4 [D] d3))) (d0 [D] (d [D] ((G \$ f) [D] (d4 [D] d3))))).
269.       cut (D_Hom_eq (d0 [D] (d [D] ((G \$ f) [D] (d4 [D] d3)))) (d0 [D] (d [D] (((G \$ f) [D] d4) [D] d3)))).
270.       cut (D_Hom_eq (d0 [D] (d [D] (((G \$ f) [D] d4) [D] d3))) (d0 [D] ((d [D] ((G \$ f) [D] d4)) [D] d3))).
271.       intros.
272.
273.       do 7 (trans;[hypothesis|]); refl.
274.
275.       apply compose_respectful_right.
276.       apply (category_associativity D _ _ _ _ d ((G \$ f) [D] d4) d3).
277.
278.       do 2 apply compose_respectful_right.
279.       apply category_associativity.
280.
281.       symm; apply category_associativity.
282.
283.       apply compose_respectful_left.
284.       symm; assumption.
285.
286.       symm; apply category_left_identity.
287.
288.       apply compose_respectful_right.
289.       symm; assumption.
290.
291.       symm; apply category_right_identity.
292.     Defined.
293.     apply YUK; assumption.
294.
295.     intros x y z F G; unfold Functor_equality.
296.     destruct F.
297.     destruct G.
298.     pose (Isomorphism_Equivalence D).
299.     pose (match e with
300.             | Build_Equivalence _ _ Itrans => Itrans
301.           end) as Itrans.
302.     unfold Functor_equality.
303.     apply (witness _ (fun X => Itrans _ _ _ (t X) (t0 X))).
304.     intros; simpl.
305.
306.     generalize (d X Y f).
307.     generalize (d0 X Y f).
308.
309.     destruct (t X); simpl.
310.     destruct t1; destruct y0; simpl.
311.     destruct (t0 X); simpl.
312.     destruct t1; destruct y0; simpl.
313.     simpl.
314.     destruct (t Y); simpl.
315.     destruct t1; destruct y0; simpl.
316.     destruct (t0 Y); simpl.
317.     destruct t1; destruct y0; simpl.
318.     simpl.
319.     (* Xf = ((d1 d5)(Zf (d14 d10))) *)
320.
321.     Lemma BLECH
322.       (F : Functor)
323.       (G : Functor)
324.       (H : Functor)
325.       (X : C_Ob)
326.       (Y : C_Ob)
327.       (f : C_Hom X Y)
328.       (d1 : D_Hom (F @ X) (G @ X))
329.       (d2 : D_Hom (G @ X) (F @ X))
330.       (d3 : D_Hom_eq (d2 [D] d1) (identity D _))
331.       (d4 : D_Hom_eq (d1 [D] d2) (identity D _))
332.       (d5 : D_Hom (G @ X) (H @ X))
333.       (d6 : D_Hom (H @ X) (G @ X))
334.       (d7 : D_Hom_eq (d6 [D] d5) (identity D _))
335.       (d8 : D_Hom_eq (d5 [D] d6) (identity D _))
336.       (d9 : D_Hom (F @ Y) (G @ Y))
337.       (d10 : D_Hom (G @ Y) (F @ Y))
338.       (d11 : D_Hom_eq (d10 [D] d9) (identity D _))
339.       (d12 : D_Hom_eq (d9 [D] d10) (identity D _))
340.       (d13 : D_Hom (G @ Y) (H @ Y))
341.       (d14 : D_Hom (H @ Y) (G @ Y))
342.       (d15 : D_Hom_eq (d14 [D] d13) (identity D _))
343.       (d16 : D_Hom_eq (d13 [D] d14) (identity D _))
344.     (WW : D_Hom_eq (F \$ f) (d1 [D] ((G \$ f) [D] d10)))
345.     (MM : D_Hom_eq (G \$ f) (d5 [D] ((H \$ f) [D] d14))) :
346.    D_Hom_eq (F \$ f) ((d1 [D] d5) [D] ((H \$ f) [D] (d14 [D] d10))).
347.       symm.
348.       cut (D_Hom_eq
349.         (G \$ f)
350.         (d5 [D] ((H \$ f) [D] d14))).
351.       cut (D_Hom_eq
352.         (F \$ f)
353.         (d1 [D] ((G \$ f) [D] d10))).
354.       intros.
355.
356.       Ltac step K :=
357.         match goal with |- D_Hom_eq ?X ?Y =>
358.           cut (D_Hom_eq X K);[intro;trans;hypothesis|]
359.         end.
360.
361.       step (((d1 [D] d5) [D] (((H \$ f) [D] d14) [D] d10))).
362.       step ((d1 [D] (d5 [D] (((H \$ f) [D] d14) [D] d10)))).
363.       match goal with |- D_Hom_eq ?X ?y =>
364.         cut (D_Hom_eq X ((d1 [D] ((d5 [D] ((H \$ f) [D] d14)) [D] d10))))
365.       end.
366.       intro.
367.       trans.
368.       apply X4.
369.
370.       match goal with |- D_Hom_eq ?X ?y =>
371.         cut (D_Hom_eq X (d1 [D] ((G \$ f) [D] d10)))
372.       end.
373.       intro; trans.
374.       apply X5.
375.
376.       apply compose_respectful_right.
377.       trans.
378.       apply compose_respectful_left.
379.       apply X1.
380.       symm.
381.       apply (category_associativity D _ _ _ _ d5 ((H \$ f) [D] d14) d10).
382.
383.       apply compose_respectful_right.
384.       apply compose_respectful_left.
385.       symm; hypothesis.
386.
387.       step ((d1 [D] (d5 [D] (((H \$ f) [D] d14) [D] d10)))).
388.
389.       apply (category_associativity D _ _ _ _).
390.       symm; apply (category_associativity D _ _ _ _).
391.       trans; [apply X0|].
392.       apply compose_respectful_right.
393.       symm.
394.       step (((d5 [D] ((H \$ f) [D] d14)) [D] d10)).
395.       symm; assumption.
396.       apply (category_associativity D _ _ _ _ d5).
397.       apply compose_respectful_right.
398.       apply (category_associativity D _ _ _ _).
399.
400.       assumption.
401.
402.       assumption.
403.
404.     Defined.
405.     intros.
406.     eapply BLECH; hypothesis.
407.   Defined.
408. End Functor.
409.
410. Section Functors.
411.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
412.   Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).
413.   Context {E_Ob E_Hom E_Hom_eq} (E : @Category E_Ob E_Hom E_Hom_eq).
414.
415.   Theorem Functor_Equal (F : Functor C D) {X Y} (f f' : C_Hom X Y) : C_Hom_eq f f' -> D_Hom_eq (Map_Hom F _ _ f) (Map_Hom F _ _ f').
416.   intros; apply Map_Hom_respectful.
417.   assumption.
418.   Defined.
419.
420.   Definition Identity_Functor : Functor C C.
421.   Print Build_Functor.
422.   apply (Build_Functor C C
423.     (fun X => X)
424.     (fun X Y f => f)).
425.   intros; refl.
426.   intros; refl.
427.   intros; assumption.
428.   Defined.
429.
430.   Definition Compose_Functor (F : Functor C D) (G : Functor D E) : Functor C E.
431.   Print Build_Functor.
432.   apply (Build_Functor C E
433.     (fun X => Map_Ob G (Map_Ob F X))
434.     (fun X Y f => Map_Hom G _ _ (Map_Hom F _ _ f))).
435.
436.   intros.
437.   trans.
438.   apply Map_Hom_respectful.
439.   apply (functor_identity F X).
440.   apply (functor_identity G _).
441.
442.   intros.
443.   trans.
444.   apply Map_Hom_respectful.
445.   apply (functor_compose F).
446.   apply (functor_compose G).
447.
448.   intros.
449.   apply Map_Hom_respectful.
450.   apply Map_Hom_respectful.
451.   assumption.
452.   Defined.
453. End Functors.
454.
455. Section NaturalTransformation.
456.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
457.   Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).
458.
459.   Context (F G : Functor C D).
460.
461.   Record NaturalTransformation
462.     := { Component : forall X : C_Ob, D_Hom (Map_Ob F X) (Map_Ob G X)
463.        ; naturality : forall X Y (f : C_Hom X Y),
464.          D_Hom_eq (compose D _ _ _ (Map_Hom F _ _ f) (Component Y))
465.                   (compose D _ _ _ (Component X) (Map_Hom G _ _ f))
466.        }.
467. End NaturalTransformation.
468.
469. Section NaturalTransformations.
470.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
471.   Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).
472.
473.   Context (F G H : Functor C D).
474.
475.   Print Component.
476.   Definition NaturalTransformation_Equivalence : Equivalence (fun (eta nu : NaturalTransformation F G) => forall X : C_Ob, D_Hom_eq (Component eta X) (Component nu X)).
477.   apply Build_Equivalence.
478.
479.   intros; refl.
480.
481.   intros; symm; hypothesis.
482.
483.   intros; trans; hypothesis.
484.   Defined.
485.
486.   Definition Identity_NaturalTransformation : NaturalTransformation F F.
487.   apply (Build_NaturalTransformation F F
488.     (fun X => identity D (Map_Ob F X))).
489.   intros; trans.
490.   apply category_right_identity.
491.   symm; apply category_left_identity.
492.   Defined.
493.
494.   Definition Compose_NaturalTransformation (eta : NaturalTransformation F G) (nu : NaturalTransformation G H) : NaturalTransformation F H.
495.   apply (Build_NaturalTransformation F H
496.     (fun X => compose D _ _ _ (Component eta X) (Component nu X))).
497.   intros.
498.   trans.
499.   apply (category_associativity D).
500.   trans.
501.   apply (compose_respectful_left D).
502.   apply (naturality eta).
503.   trans.
504.   symm; apply (category_associativity D).
505.   symm.
506.   trans.
507.   symm.
508.   apply (category_associativity D).
509.   apply (compose_respectful_right D).
510.   symm.
511.   apply (naturality nu).
512.   Defined.
513. End NaturalTransformations.
514.
515.
516. Section FunctorCategory.
517.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
518.   Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).
519.   Definition FunctorCategory : @Category
520.     (Functor C D) (fun F G => NaturalTransformation F G)
521.     (fun F G =>
522.       fun (eta nu : NaturalTransformation F G) =>
523.         forall X : C_Ob,
524.           D_Hom_eq (Component eta X) (Component nu X)).
525.   Print Build_Category.
526.   Print Identity_NaturalTransformation.
527.   apply (@Build_Category
528.
529.     (Functor C D)
530.     (fun F G => NaturalTransformation F G)
531.     (fun F G =>
532.       fun (eta nu : NaturalTransformation F G) =>
533.         forall X : C_Ob,
534.           D_Hom_eq (Component eta X) (Component nu X))
535.
536.     (fun F => Identity_NaturalTransformation F)
537.     (fun _ _ _ eta nu => Compose_NaturalTransformation eta nu));
538.   simpl; intros.
539.
540.   apply compose_respectful_left.
541.   hypothesis.
542.
543.   apply compose_respectful_right.
544.   hypothesis.
545.
546.   apply NaturalTransformation_Equivalence.
547.
548.   apply category_left_identity.
549.
550.   apply category_right_identity.
551.
552.   apply category_associativity.
553.   Defined.
554. End FunctorCategory.
555.
556. Section OppositeCategory.
557.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
558.
559.   Definition OppositeCategory : @Category C_Ob (fun Y X => C_Hom X Y) (fun Y X f => C_Hom_eq f).
560.   apply (Build_Category
561.     (fun Y X => C_Hom X Y) (fun Y X f => C_Hom_eq f)
562.     (fun X => identity C X)
563.     (fun X Y Z f g => compose C Z Y X g f)).
564.   intros; apply compose_respectful_right; hypothesis.
565.   intros; apply compose_respectful_left; hypothesis.
566.   intros;
567.     apply Build_Equivalence; destruct (hom_equivalence C X Y);
568.       hypothesis.
569.   intros; apply category_right_identity.
570.   intros; apply category_left_identity.
571.   intros; symm; apply category_associativity.
572.   Defined.
573. End OppositeCategory.
574.
575. Section UniqueExistence.
576.   Context {C_Ob : Type}
577.           {C_Hom : C_Ob -> C_Ob -> Type}
578.           {C_Hom_eq : forall X Y, Relation (C_Hom X Y)}.
579.
580.   Definition ExistsUnique {X Y} (C : @Category C_Ob C_Hom C_Hom_eq) (P : C_Hom X Y -> Type) :=
581.     Sigma (fun f =>
582.       And (P f) (forall f' : C_Hom X Y, P f' -> C_Hom_eq f f')).
583. End UniqueExistence.
584.
585. Section TerminalObject.
586.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
587.
588.   Definition Terminal (T : C_Ob) :=
589.     forall X, ExistsUnique C (fun (f : C_Hom X T) => True).
590.
591.   (** TODO: unique up to unique isomorphism,
592.      needs predicative definition of isomorphism **)
593.   Theorem Terminal_unique (T T' : C_Ob) :
594.     Terminal T -> Terminal T' -> Isomorphism C T T'.
595.   unfold Terminal; unfold Isomorphism; intros.
596.   pose (X T); pose (X T').
597.   pose (X0 T); pose (X0 T').
598.   destruct e; destruct e0; destruct e1; destruct e2.
599.   apply (witness _ (both t1 t0)).
600.   destruct a; destruct a2.
601.   pose (c (t1 [C] t0) I).
602.   pose (c0 (t0 [C] t1) I).
603.   pose (c (identity C _) I).
604.   pose (c0 (identity C _) I).
605.   constructor.
606.   trans; [symm|]; hypothesis.
607.   trans; [symm|]; hypothesis.
608.   Defined.
609.
610. End TerminalObject.
611.
612. Section ConstantFunctor.
613.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
614.   Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).
615.
616.   Definition Delta (U : D_Ob) : Functor C D.
617.   apply (Build_Functor C D
618.     (fun _ => U)
619.     (fun _ _ _ => identity D U)).
620.   intro; refl.
621.   intros; symm; apply category_left_identity.
622.   intros; refl.
623.   Defined.
624. End ConstantFunctor.
625.
626. Section Cone.
627.   Context {II_Ob II_Hom II_Hom_eq} (II : @Category II_Ob II_Hom II_Hom_eq).
628.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
629.
630.   Definition Cone (U : C_Ob) (D : Functor II C) := NaturalTransformation (Delta II C U) D.
631. End Cone.
632.
633.
634.
635.
636. Section SYMBOLIC.
637.
638.   Inductive Symbolic_Objects := aSYM | bSYM | cSYM | dSYM | eSYM.
639.   Inductive Symbolic_Maps : Symbolic_Objects -> Symbolic_Objects -> Type :=
640.   | fSYM : Symbolic_Maps aSYM bSYM
641.   | gSYM : Symbolic_Maps bSYM cSYM
642.   | hSYM : Symbolic_Maps cSYM dSYM
643.   | kSYM : Symbolic_Maps dSYM eSYM.
644.   Inductive Symbolic_Syntax : Symbolic_Objects -> Symbolic_Objects -> Type :=
645.   | idSYM : forall S, Symbolic_Syntax S S
646.   | compSYM : forall X Y Z, Symbolic_Syntax X Y -> Symbolic_Syntax Y Z -> Symbolic_Syntax X Z
647.   | symbolSYM : forall X Y, Symbolic_Maps X Y -> Symbolic_Syntax X Y.
648.   Inductive Symbolic_Closure : Symbolic_Objects -> Symbolic_Objects -> Type :=
649.   | nilClosure : forall X, Symbolic_Closure X X
650.   | consClosure : forall X Y Z, Symbolic_Maps X Y -> Symbolic_Closure Y Z -> Symbolic_Closure X Z.
651.
652.   Fixpoint Symbolic_append x y z (f : Symbolic_Closure x y) : Symbolic_Closure y z -> Symbolic_Closure x z :=
653.   match f in Symbolic_Closure A' B' return Symbolic_Closure B' z -> Symbolic_Closure A' z with
654.     | nilClosure _ => fun y => y
655.     | consClosure _ _ _ k x => fun y => consClosure k (Symbolic_append x y)
656.   end.
657.
658.   Theorem Symbolic_append_nil :
659.     forall (X Y : Symbolic_Objects) (f : Symbolic_Closure X Y),
660.       Identity (Symbolic_append f (nilClosure Y)) f.
661.   induction f.
662.   constructor.
663.   simpl.
664.   cut (Identity f (Symbolic_append f (nilClosure Z))).
665.   intro H; elim H.
666.   constructor.
667.   apply (equivalence_symmetry (Equivalence_Identity)).
668.   assumption.
669.   Defined.
670.
671.   Theorem Symbolic_append_associative :
672.   forall (X Y Z W : Symbolic_Objects) (f : Symbolic_Closure X Y)
673.     (g : Symbolic_Closure Y Z) (h : Symbolic_Closure Z W),
674.     Identity (Symbolic_append f (Symbolic_append g h))
675.   (Symbolic_append (Symbolic_append f g) h).
676.   induction f.
677.   constructor.
678.   intros.
679.   simpl.
680.   cut (
681.     Identity (Symbolic_append f (Symbolic_append g h))
682.              (Symbolic_append (Symbolic_append f g) h)
683.   ).
684.   intro H; elim H.
685.   constructor.
686.   apply IHf.
687.   Defined.
688.
689.   Definition Symbolic_Semantics {X Y} (S : Symbolic_Syntax X Y) : Symbolic_Closure X Y.
690.   induction S.
691.   constructor.
692.   apply (Symbolic_append IHS1 IHS2).
693.   apply (consClosure s (nilClosure _)).
694.   Defined.
695.
696.   Definition Symbolic_eq := (fun X Y (f g : Symbolic_Syntax X Y) => Identity (Symbolic_Semantics f) (Symbolic_Semantics g)).
697.
698.   Definition Symbolic_Cat : Category Symbolic_Syntax Symbolic_eq.
699.   apply (@Build_Category _ Symbolic_Syntax Symbolic_eq
700.     (fun x => idSYM x)
701.     (fun x y z F G => compSYM F G));
702.   unfold Symbolic_eq in *; simpl.
703.
704.   intros; elim H; constructor.
705.
706.   intros; elim H; constructor.
707.
708.   intros; apply Equivalence_Identity_map.
709.
710.   intros; constructor.
711.
712.   intros.
713.   apply Symbolic_append_nil.
714.
715.   intros.
716.   apply Symbolic_append_associative.
717.   Defined.
718.
719.   Fixpoint Quote_Semantics (X Y : Symbolic_Objects) (f : Symbolic_Closure X Y) : Symbolic_Syntax X Y :=
720.     match f with
721.       | nilClosure _ => identity Symbolic_Cat _
722.       | consClosure _ _ _ s f =>
723.         compose Symbolic_Cat _ _ _ (symbolSYM s) (Quote_Semantics f)
724.     end.
725.
726.   Lemma quote_eval_harmony {X Y} (f : Symbolic_Syntax X Y) :
727.     Symbolic_eq (Quote_Semantics (Symbolic_Semantics f))
728.                 f.
729.   unfold Symbolic_eq.
730.   Lemma quote_eval_harmony' {X Y} (f : Symbolic_Closure X Y) :
731.     Identity (Symbolic_Semantics (Quote_Semantics f))
732.              f.
733.     induction f; simpl.
734.     constructor.
735.     pose (equivalence_symmetry (Equivalence_Identity) _ _ IHf).
736.     elim i.
737.     constructor.
738.   Defined.
739.   apply quote_eval_harmony'.
740.   Defined.
741.
742.   Definition X := Symbolic_Cat.
743.   Notation "'<' e '>'" := (symbolSYM e).
744.
745.   Theorem NASTY_THEOREM :
746.     Symbolic_eq ((< fSYM > [X] < gSYM >) [X] (< hSYM > [X] < kSYM >))
747.                 ((< fSYM > [X] (< gSYM > [X] < hSYM >)) [X] < kSYM >).
748.   constructor.
749.   Defined.
750.
751.   Axiom Ob : Type.
752.   Axiom a b c d e : Ob.
753.   Axiom ARR : Ob -> Ob -> Type.
754.   Axiom f : ARR a b.
755.   Axiom g : ARR b c.
756.   Axiom h : ARR c d.
757.   Axiom k : ARR d e.
758.   Axiom REL : forall X Y, Relation (ARR X Y).
759.
760.   Axiom ARR_category : @Category Ob ARR REL.
761.
762.   Definition interpret_symbolic_object := (fun X =>
763.       match X with
764.         | aSYM => a
765.         | bSYM => b
766.         | cSYM => c
767.         | dSYM => d
768.         | eSYM => e
769.       end).
770.
771.   Definition interpret_symbolic_syntax (X Y : Symbolic_Objects) (f : Symbolic_Syntax X Y) : ARR (interpret_symbolic_object X) (interpret_symbolic_object Y).
772.
773.   induction f; simpl in *.
774.
775.   apply (identity ARR_category).
776.
777.   apply (compose ARR_category _ _ _ IHf1 IHf2).
778.
779.   destruct s; simpl.
780.   apply f.
781.   apply g.
782.   apply h.
783.   apply k.
784.   Defined.
785.
786.   Definition interp_symbolic_syntax (X Y : Symbolic_Objects) (f : Symbolic_Closure X Y) : ARR (interpret_symbolic_object X) (interpret_symbolic_object Y).
787.   induction f.
788.   apply (identity ARR_category).
789.   apply (compose ARR_category _ _ _ (interpret_symbolic_syntax (symbolSYM s)) IHf).
790.   Defined.
791.
792.   Theorem interp_factors (X Y : Symbolic_Objects) : forall f : Symbolic_Syntax X Y,
793.     REL (interpret_symbolic_syntax f)
794.         (interp_symbolic_syntax (Symbolic_Semantics f)).
795.     induction f0;
796.       simpl.
797.     apply (equivalence_reflexivity (hom_equivalence ARR_category _ _)).
798.     Lemma factor_through_append X Y Z (f : Symbolic_Closure X Y) (g : Symbolic_Closure Y Z) :
799.     REL (interp_symbolic_syntax f [ARR_category] interp_symbolic_syntax g)
800.         (interp_symbolic_syntax (Symbolic_append f g)).
801.       induction f.
802.       simpl.
803.       apply category_left_identity.
804.       pose (IHf g).
805.       assert (
806.         REL (interp_symbolic_syntax (Symbolic_append (consClosure s f0) g))
807.             ((interpret_symbolic_syntax (symbolSYM s)) [ARR_category] (interp_symbolic_syntax (Symbolic_append f0 g)))
808.       ).
809.       apply (equivalence_reflexivity (hom_equivalence ARR_category _ _)).
810.       eapply (equivalence_transitivity (hom_equivalence ARR_category _ _)).
811.       Focus 2.
812.       apply (equivalence_symmetry (hom_equivalence ARR_category _ _)).
813.       apply X1.
814.       assert (
815.         REL
816.         (interp_symbolic_syntax (consClosure s f0) [ARR_category]
817.           interp_symbolic_syntax g)
818.         ((interpret_symbolic_syntax < s > [ARR_category] interp_symbolic_syntax f0) [ARR_category]
819.           interp_symbolic_syntax g)
820.       ).
821.       apply (equivalence_reflexivity (hom_equivalence ARR_category _ _)).
822.       eapply (equivalence_transitivity (hom_equivalence ARR_category _ _)).
823.       apply X2.
824.       eapply (equivalence_transitivity (hom_equivalence ARR_category _ _)).
825.       apply (equivalence_symmetry (hom_equivalence ARR_category _ _)).
826.       apply (category_associativity ARR_category).
827.       apply compose_respectful_right.
828.       hypothesis.
829.     Defined.
830.
831.     Focus 2.
832.     destruct s; simpl;
833.       apply (equivalence_symmetry (hom_equivalence ARR_category _ _));
834.         apply category_right_identity.
835.
836.     eapply (equivalence_transitivity (hom_equivalence ARR_category _ _)).
837.     Focus 2.
838.     apply (@factor_through_append _ _ _ (Symbolic_Semantics f0_1) (Symbolic_Semantics f0_2)).
839.     eapply (equivalence_transitivity (hom_equivalence ARR_category _ _)).
840.     apply compose_respectful_left.
841.     apply IHf0_1.
842.     eapply (equivalence_transitivity (hom_equivalence ARR_category _ _)).
843.     apply compose_respectful_right.
844.     apply IHf0_2.
845.     apply (equivalence_reflexivity (hom_equivalence ARR_category _ _)).
846.   Defined.
847.
848.   Definition Symbolic_ARR_Functor : Functor Symbolic_Cat ARR_category.
849.   Print Functor.
850.   apply (Build_Functor Symbolic_Cat ARR_category
851.     interpret_symbolic_object
852.     interpret_symbolic_syntax);
853.   simpl; intros.
854.
855.   apply (hom_equivalence ARR_category).
856.   apply (hom_equivalence ARR_category).
857.
858.   pose (quote_eval_harmony f0).
859.   pose (quote_eval_harmony f').
860.
861.   pose (interp_factors f0).
862.   pose (interp_factors f').
863.
864.   eapply (equivalence_transitivity (hom_equivalence ARR_category _ _)).
865.   apply r.
866.
867.   eapply (equivalence_transitivity (hom_equivalence ARR_category _ _)).
868.   Focus 2.
869.   eapply (equivalence_symmetry (hom_equivalence ARR_category _ _)).
870.   apply r0.
871.   elim H.
872.   apply (equivalence_reflexivity (hom_equivalence ARR_category _ _)).
873.
874.   Defined.
875.
876.   Definition Y := ARR_category.
877.   Theorem NASTY_THEOREM_easy_proof :
878.     REL ((f [Y] g) [Y] (h [Y] k))
879.         ((f [Y] (g [Y] h)) [Y] k).
880.   pose NASTY_THEOREM.
881.   pose (Functor_Equal Symbolic_ARR_Functor s) as GIFT.
883.   Defined.
884.
885. (* FAIL *)
886.
887. End SYMBOLIC.
888.
889. Print Assumptions NASTY_THEOREM_easy_proof.
890.
891.
892.
893.
894.
895. (*
896. *** Local Variables: ***
897. *** coq-prog-args: ("-emacs-U" "-nois") ***
898. *** End: ***
899. *)
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.
Not a member of Pastebin yet?