API tools faq
paste
Advertisement
Guest User

Untitled

a guest
Jul 7th, 2017
92
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
OCaml Brief 12.26 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 And (P Q : Type) : Type :=
  6. | both : P -> Q -> And P Q.
  7.  
  8. Definition And_idem (P : Type) : P -> And P P.
  9. intro p; apply (both p p).
  10. Defined.
  11.  
  12. Inductive Sigma (T : Type) (P : T -> Type) : Type :=
  13. | witness : forall t : T, P t -> Sigma P.
  14.  
  15. Definition Relation (T : Type) := T -> T -> Type.
  16.  
  17. Record Equivalence {T : Type} (R : Relation T)
  18.   := { equivalence_reflexivity : forall x, R x x
  19.      ; equivalence_symmetry : forall x y, R x y -> R y x
  20.      ; equivalence_transitivity : forall x y z, R x y -> R y z -> R x z
  21.      }.
  22.  
  23. Record Category (Ob : Type) (Hom : Ob -> Ob -> Type)
  24.                 (Hom_eq : forall X Y, Relation (Hom X Y))
  25.   := { identity : forall X, Hom X X
  26.      ; compose : forall X Y Z, Hom X Y -> Hom Y Z -> Hom X Z
  27.      ; compose_respectful_left : forall X Y Z (f f' : Hom X Y) (g : Hom Y Z),
  28.        Hom_eq _ _ f f' -> Hom_eq _ _ (compose f g) (compose f' g)
  29.      ; compose_respectful_right : forall X Y Z (f : Hom X Y) (g g' : Hom Y Z),
  30.        Hom_eq _ _ g g' -> Hom_eq _ _ (compose f g) (compose f g')
  31.      ; hom_equivalence : forall X Y, Equivalence (Hom_eq X Y)
  32.      ; category_left_identity : forall X Y (f : Hom X Y),
  33.        Hom_eq _ _ (compose (identity _) f) f
  34.      ; category_right_identity : forall X Y (f : Hom X Y),
  35.        Hom_eq _ _ (compose f (identity _)) f
  36.      ; category_associativity : forall X Y Z W (f : Hom X Y) (g : Hom Y Z) (h : Hom Z W),
  37.        Hom_eq _ _ (compose f (compose g h))
  38.                   (compose (compose f g) h)
  39.      }.
  40.  
  41. Notation "f '[' C ']'  g" := (compose C _ _ _ f g) (at level 20).
  42. Notation "'1_' C" := (identity C _) (at level 20).
  43.  
  44. Ltac refl :=
  45.   eapply equivalence_reflexivity;
  46.     [apply hom_equivalence;assumption].
  47. Ltac symm :=
  48.   eapply equivalence_symmetry;
  49.     [apply hom_equivalence;assumption|idtac].
  50. Ltac trans :=
  51.   eapply equivalence_transitivity;
  52.     [apply hom_equivalence;assumption|idtac|idtac].
  53.  
  54. Section Isomorphism.
  55.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  56.  
  57.   Definition Isomorphism (X Y : C_Ob) :=
  58.     @Sigma (And (C_Hom X Y) (C_Hom Y X))
  59.            (fun fg =>
  60.              match fg with
  61.                | both f g =>
  62.                  And (C_Hom_eq (compose C _ _ _ g f) (identity C _))
  63.                      (C_Hom_eq (compose C _ _ _ f g) (identity C _))
  64.              end).
  65.  
  66.   Definition isomorphism_to (X Y : C_Ob) (i : Isomorphism X Y) : C_Hom X Y.
  67.   destruct i as [[to from] _]; apply to.
  68.   Defined.
  69.  
  70.   Definition isomorphism_from (X Y : C_Ob) (i : Isomorphism X Y) : C_Hom Y X.
  71.   destruct i as [[to from] _]; apply from.
  72.   Defined.
  73.  
  74.   Theorem Isomorphism_Equivalence : Equivalence Isomorphism.
  75.   apply Build_Equivalence.
  76.  
  77.   Lemma Isomorphism_Identity : forall x : C_Ob, Isomorphism x x.
  78.     intro x; apply (witness _ (both (identity C x) (identity C x))).
  79.     apply And_idem.
  80.     apply category_left_identity.
  81.   Defined.
  82.   apply Isomorphism_Identity.
  83.  
  84.   intros x y [[I J] [i j]].
  85.   apply (witness _ (both J I)).
  86.   apply (both j i).
  87.  
  88.   Lemma Isomorphism_Compose : forall x y z : C_Ob, Isomorphism x y -> Isomorphism y z -> Isomorphism x z.
  89.     intros x y z [[I J] [i j]] [[I' J'] [i' j']].
  90.     apply (witness _ (both (compose C _ _ _ I I') (compose C _ _ _ J' J))).
  91.     apply both.
  92.    
  93.     trans.
  94.     apply (category_associativity C).
  95.     trans.
  96.     apply (compose_respectful_left C).
  97.     trans.
  98.     symm.
  99.     apply (category_associativity C).
  100.     apply (compose_respectful_right C).
  101.     apply i.
  102.     assert (C_Hom_eq (compose C z y y J' (identity C y))
  103.                      J').
  104.     apply category_right_identity.
  105.     trans.
  106.     apply (compose_respectful_left C).
  107.     apply X.
  108.     assumption.
  109.    
  110.     trans.
  111.     apply (category_associativity C).
  112.     trans.
  113.     apply (compose_respectful_left C).
  114.     trans.
  115.     symm.
  116.     apply (category_associativity C).
  117.     apply (compose_respectful_right C).
  118.     apply j'.
  119.     assert (C_Hom_eq (compose C x y y I (identity C y))
  120.                      I).
  121.     apply category_right_identity.
  122.     trans.
  123.     apply (compose_respectful_left C).
  124.     apply X.
  125.     assumption.
  126.     Defined.
  127.   apply Isomorphism_Compose.
  128.   Defined.
  129. End Isomorphism.
  130.  
  131. Section Functor.
  132.   Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  133.   Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).
  134.  
  135.   Record Functor
  136.     := { Map_Ob : C_Ob -> D_Ob
  137.        ; Map_Hom : forall X Y, C_Hom X Y -> D_Hom (Map_Ob X) (Map_Ob Y)
  138.        ; functor_identity : forall X, D_Hom_eq (Map_Hom (identity C X)) (identity D (Map_Ob X))
  139.        ; functor_compose : forall X Y Z (f : C_Hom X Y) (g : C_Hom Y Z),
  140.          D_Hom_eq (Map_Hom (compose C _ _ _ f g)) (compose D _ _ _ (Map_Hom f) (Map_Hom g))
  141.     }.
  142.  
  143.   Notation "F '@' x" := (Map_Ob F x) (at level 20).
  144.   Notation "F '$' f" := (Map_Hom F f) (at level 20).
  145.  
  146.   Definition Functor_equality (F G : Functor) :=
  147.     @Sigma (forall X : C_Ob,
  148.              Isomorphism D (Map_Ob F X) (Map_Ob G X))
  149.           (fun Ob_iso =>
  150.             forall X Y (f : C_Hom X Y),
  151.               D_Hom_eq (Map_Hom F f)
  152.                        (compose D _ _ _
  153.                          (isomorphism_to (Ob_iso _))
  154.                          (compose D _ _ _
  155.                            (Map_Hom G f)
  156.                             (isomorphism_from (Ob_iso _))))).
  157.  
  158.   Theorem Functor_equivalence : Equivalence Functor_equality.
  159.     apply Build_Equivalence.
  160.    
  161.     intro x.
  162.     unfold Functor_equality.
  163.     apply witness with (t := (fun X => @Isomorphism_Identity _ _ _ D (Map_Ob x X))).
  164.     intros X Y f.
  165.     simpl.
  166.     trans.
  167.     symm.
  168.     apply category_left_identity.
  169.     apply compose_respectful_right.
  170.     trans.
  171.     symm.
  172.     apply category_right_identity.
  173.     apply compose_respectful_right.
  174.     refl.
  175.    
  176.     intros F G.
  177.     intros [F' F''].
  178.    
  179.     pose (Isomorphism_Equivalence D).
  180.     pose (match e with
  181.             | Build_Equivalence _ Isymm _ => Isymm
  182.           end) as Isymm.
  183.     unfold Functor_equality.
  184.     apply (witness _ (fun X => Isymm _ _ (F' X))).
  185.     intros X Y f.
  186.     unfold Isymm in *; unfold e in *; simpl.
  187.     generalize (F'' _ _ f).
  188.    
  189.     destruct (F' X); simpl.
  190.     destruct t; simpl.
  191.     destruct y; simpl.
  192.     destruct (F' Y); simpl.
  193.     destruct t; simpl.
  194.     destruct y; simpl.
  195.    
  196.     intro.
  197.     assert (
  198.       D_Hom_eq (compose D _ _ _ d0 (compose D _ _ _ (Map_Hom F f) d3))
  199.       (compose D _ _ _ d0 (compose D _ _ _
  200.         (compose D (Map_Ob F X) (Map_Ob G X) (Map_Ob F Y) d
  201.             (compose D (Map_Ob G X) (Map_Ob G Y) (Map_Ob F Y)
  202.                (Map_Hom G f) d4)) d3))
  203.       ).
  204.     apply compose_respectful_right.
  205.     apply compose_respectful_left.
  206.     assumption.
  207.    
  208.     trans.
  209.     Focus 2.
  210.     symm.
  211.     apply X1.
  212.     (* Gf = (d0 ((d (Gf d4)) d3)) *)
  213.     Lemma YUK
  214.       (F : Functor)
  215.       (G : Functor)
  216.       (X : C_Ob)
  217.       (Y : C_Ob)
  218.       (f : C_Hom X Y)
  219.       (d : D_Hom (F @ X) (G @ X))
  220.       (d0 : D_Hom (G @ X) (F @ X))
  221.       (d1 : D_Hom_eq (d0 [D] d) (identity D _))
  222.       (d2 : D_Hom_eq (d [D] d0) (identity D _))
  223.       (d3 : D_Hom (F @ Y) (G @ Y))
  224.       (d4 : D_Hom (G @ Y) (F @ Y))
  225.       (d5 : D_Hom_eq (d4 [D] d3) (identity D _))
  226.       (d6 : D_Hom_eq (d3 [D] d4) (identity D _))
  227.       (X0 : D_Hom_eq (F $ f) (d [D] ((G $ f) [D] d4)))
  228.       (X1 : D_Hom_eq (d0 [D] ((F $ f) [D] d3))
  229.              (d0 [D] ((d [D] ((G $ f) [D] d4)) [D] d3))) :
  230.       D_Hom_eq (G $ f) (d0 [D] ((d [D] ((G $ f) [D] d4)) [D] d3)).
  231.      
  232.       cut (D_Hom_eq (G $ f) ((G $ f) [D] (identity D _))).
  233.       cut (D_Hom_eq ((G $ f) [D] (identity D _)) ((G $ f) [D] (d4 [D] d3))).
  234.       cut (D_Hom_eq ((G $ f) [D] (d4 [D] d3)) ((identity D _) [D] ((G $ f) [D] (d4 [D] d3)))).
  235.       cut (D_Hom_eq ((identity D _) [D] ((G $ f) [D] (d4 [D] d3))) ((d0 [D] d) [D] ((G $ f) [D] (d4 [D] d3)))).
  236.       cut (D_Hom_eq ((d0 [D] d) [D] ((G $ f) [D] (d4 [D] d3))) (d0 [D] (d [D] ((G $ f) [D] (d4 [D] d3))))).
  237.       cut (D_Hom_eq (d0 [D] (d [D] ((G $ f) [D] (d4 [D] d3)))) (d0 [D] (d [D] (((G $ f) [D] d4) [D] d3)))).
  238.       cut (D_Hom_eq (d0 [D] (d [D] (((G $ f) [D] d4) [D] d3))) (d0 [D] ((d [D] ((G $ f) [D] d4)) [D] d3))).
  239.       intros.
  240.      
  241.       do 7 (trans;[hypothesis|]); refl.
  242.      
  243.       apply compose_respectful_right.
  244.       apply (category_associativity D _ _ _ _ d ((G $ f) [D] d4) d3).
  245.      
  246.       do 2 apply compose_respectful_right.
  247.       apply category_associativity.
  248.      
  249.       symm; apply category_associativity.
  250.      
  251.       apply compose_respectful_left.
  252.       symm; assumption.
  253.      
  254.       symm; apply category_left_identity.
  255.      
  256.       apply compose_respectful_right.
  257.       symm; assumption.
  258.    
  259.       symm; apply category_right_identity.
  260.     Defined.
  261.     apply YUK; assumption.
  262.    
  263.     intros x y z F G; unfold Functor_equality.
  264.     destruct F.
  265.     destruct G.
  266.     pose (Isomorphism_Equivalence D).
  267.     pose (match e with
  268.             | Build_Equivalence _ _ Itrans => Itrans
  269.           end) as Itrans.
  270.     unfold Functor_equality.
  271.     apply (witness _ (fun X => Itrans _ _ _ (t X) (t0 X))).
  272.     intros; simpl.
  273.    
  274.     generalize (d X Y f).
  275.     generalize (d0 X Y f).
  276.    
  277.     destruct (t X); simpl.
  278.     destruct t1; destruct y0; simpl.
  279.     destruct (t0 X); simpl.
  280.     destruct t1; destruct y0; simpl.
  281.     simpl.
  282.     destruct (t Y); simpl.
  283.     destruct t1; destruct y0; simpl.
  284.     destruct (t0 Y); simpl.
  285.     destruct t1; destruct y0; simpl.
  286.     simpl.
  287.     (* Xf = ((d1 d5)(Zf (d14 d10))) *)
  288.    
  289.     Lemma BLECH
  290.       (F : Functor)
  291.       (G : Functor)
  292.       (H : Functor)
  293.       (X : C_Ob)
  294.       (Y : C_Ob)
  295.       (f : C_Hom X Y)
  296.       (d1 : D_Hom (F @ X) (G @ X))
  297.       (d2 : D_Hom (G @ X) (F @ X))
  298.       (d3 : D_Hom_eq (d2 [D] d1) (identity D _))
  299.       (d4 : D_Hom_eq (d1 [D] d2) (identity D _))
  300.       (d5 : D_Hom (G @ X) (H @ X))
  301.       (d6 : D_Hom (H @ X) (G @ X))
  302.       (d7 : D_Hom_eq (d6 [D] d5) (identity D _))
  303.       (d8 : D_Hom_eq (d5 [D] d6) (identity D _))
  304.       (d9 : D_Hom (F @ Y) (G @ Y))
  305.       (d10 : D_Hom (G @ Y) (F @ Y))
  306.       (d11 : D_Hom_eq (d10 [D] d9) (identity D _))
  307.       (d12 : D_Hom_eq (d9 [D] d10) (identity D _))
  308.       (d13 : D_Hom (G @ Y) (H @ Y))
  309.       (d14 : D_Hom (H @ Y) (G @ Y))
  310.       (d15 : D_Hom_eq (d14 [D] d13) (identity D _))
  311.       (d16 : D_Hom_eq (d13 [D] d14) (identity D _))
  312.     (WW : D_Hom_eq (F $ f) (d1 [D] ((G $ f) [D] d10)))
  313.     (MM : D_Hom_eq (G $ f) (d5 [D] ((H $ f) [D] d14))) :
  314.    D_Hom_eq (F $ f) ((d1 [D] d5) [D] ((H $ f) [D] (d14 [D] d10))).
  315.       symm.
  316.       cut (D_Hom_eq
  317.         (G $ f)
  318.         (d5 [D] ((H $ f) [D] d14))).
  319.       cut (D_Hom_eq
  320.         (F $ f)
  321.         (d1 [D] ((G $ f) [D] d10))).
  322.       intros.
  323.      
  324.       Ltac step K :=
  325.         match goal with |- D_Hom_eq ?X ?Y =>
  326.           cut (D_Hom_eq X K);[intro;trans;hypothesis|]
  327.         end.
  328.      
  329.       step (((d1 [D] d5) [D] (((H $ f) [D] d14) [D] d10))).
  330.       step ((d1 [D] (d5 [D] (((H $ f) [D] d14) [D] d10)))).
  331.       match goal with |- D_Hom_eq ?X ?y =>
  332.         cut (D_Hom_eq X ((d1 [D] ((d5 [D] ((H $ f) [D] d14)) [D] d10))))
  333.       end.
  334.       intro.
  335.       trans.
  336.       apply X4.
  337.      
  338.       match goal with |- D_Hom_eq ?X ?y =>
  339.         cut (D_Hom_eq X (d1 [D] ((G $ f) [D] d10)))
  340.       end.
  341.       intro; trans.
  342.       apply X5.
  343.      
  344.       apply compose_respectful_right.
  345.       trans.
  346.       apply compose_respectful_left.
  347.       apply X1.
  348.       symm.
  349.       apply (category_associativity D _ _ _ _ d5 ((H $ f) [D] d14) d10).
  350.      
  351.       apply compose_respectful_right.
  352.       apply compose_respectful_left.
  353.       symm; hypothesis.
  354.      
  355.       step ((d1 [D] (d5 [D] (((H $ f) [D] d14) [D] d10)))).
  356.      
  357.       apply (category_associativity D _ _ _ _).
  358.       symm; apply (category_associativity D _ _ _ _).
  359.       trans; [apply X0|].
  360.       apply compose_respectful_right.
  361.       symm.
  362.       step (((d5 [D] ((H $ f) [D] d14)) [D] d10)).
  363.       symm; assumption.
  364.       apply (category_associativity D _ _ _ _ d5).
  365.       apply compose_respectful_right.
  366.       apply (category_associativity D _ _ _ _).
  367.      
  368.       assumption.
  369.    
  370.       assumption.
  371.    
  372.     Defined.
  373.     intros.
  374.     eapply BLECH; hypothesis.
  375.   Defined.
  376. End Functor.
  377.  
  378.  
  379.  
  380. (*
  381. *** Local Variables: ***
  382. *** coq-prog-args: ("-emacs-U" "-nois") ***
  383. *** End: ***
  384. *)
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!