API tools faq
paste
Advertisement
Guest User

Untitled

a guest
Jul 7th, 2017
144
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
OCaml Brief 28.49 KB | None | 0 0
raw download clone embed print report
  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.
  882.   apply 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. *)
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
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.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!