From: Adam Megacz Date: Sat, 30 Apr 2011 04:47:25 +0000 (-0700) Subject: clean up hints for NaturalDeduction, split ProgrammingLanguage into multiple files X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=034f7e7856bebbbcb3c83946aa603c640b17f3bb clean up hints for NaturalDeduction, split ProgrammingLanguage into multiple files --- diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v index 719e714..3aeb7db 100644 --- a/src/NaturalDeduction.v +++ b/src/NaturalDeduction.v @@ -229,18 +229,7 @@ Section Natural_Deduction. Hint Constructors Structural. Hint Constructors BuiltFrom. Hint Constructors NDPredicateClosure. - - Hint Extern 1 => apply nd_structural_id0. - Hint Extern 1 => apply nd_structural_id1. - Hint Extern 1 => apply nd_structural_cancell. - Hint Extern 1 => apply nd_structural_cancelr. - Hint Extern 1 => apply nd_structural_llecnac. - Hint Extern 1 => apply nd_structural_rlecnac. - Hint Extern 1 => apply nd_structural_assoc. - Hint Extern 1 => apply nd_structural_cossa. - Hint Extern 1 => apply ndpc_p. - Hint Extern 1 => apply ndpc_prod. - Hint Extern 1 => apply ndpc_comp. + Hint Unfold StructuralND. Lemma nd_id_structural : forall sl, StructuralND (nd_id sl). intros. @@ -464,42 +453,6 @@ Coercion sndr_ndr : SequentND_Relation >-> ND_Relation. Coercion cndr_sndr : ContextND_Relation >-> SequentND_Relation. Implicit Arguments ND [ Judgment ]. -Hint Constructors Structural. -Hint Extern 1 => apply nd_id_structural. -Hint Extern 1 => apply ndr_builtfrom_structural. -Hint Extern 1 => apply nd_structural_id0. -Hint Extern 1 => apply nd_structural_id1. -Hint Extern 1 => apply nd_structural_cancell. -Hint Extern 1 => apply nd_structural_cancelr. -Hint Extern 1 => apply nd_structural_llecnac. -Hint Extern 1 => apply nd_structural_rlecnac. -Hint Extern 1 => apply nd_structural_assoc. -Hint Extern 1 => apply nd_structural_cossa. -Hint Extern 1 => apply ndpc_p. -Hint Extern 1 => apply ndpc_prod. -Hint Extern 1 => apply ndpc_comp. -Hint Extern 1 => apply builtfrom_refl. -Hint Extern 1 => apply builtfrom_prod1. -Hint Extern 1 => apply builtfrom_prod2. -Hint Extern 1 => apply builtfrom_comp1. -Hint Extern 1 => apply builtfrom_comp2. -Hint Extern 1 => apply builtfrom_P. - -Hint Extern 1 => apply snd_inert_initial. -Hint Extern 1 => apply snd_inert_cut. -Hint Extern 1 => apply snd_inert_structural. - -Hint Extern 1 => apply cnd_inert_initial. -Hint Extern 1 => apply cnd_inert_cut. -Hint Extern 1 => apply cnd_inert_structural. -Hint Extern 1 => apply cnd_inert_cnd_ant_assoc. -Hint Extern 1 => apply cnd_inert_cnd_ant_cossa. -Hint Extern 1 => apply cnd_inert_cnd_ant_cancell. -Hint Extern 1 => apply cnd_inert_cnd_ant_cancelr. -Hint Extern 1 => apply cnd_inert_cnd_ant_llecnac. -Hint Extern 1 => apply cnd_inert_cnd_ant_rlecnac. -Hint Extern 1 => apply cnd_inert_se_expand_left. -Hint Extern 1 => apply cnd_inert_se_expand_right. (* This first notation gets its own scope because it can be confusing when we're working with multiple different kinds * of proofs. When only one kind of proof is in use, it's quite helpful though. *) @@ -509,10 +462,39 @@ Notation "a ** b" := (nd_prod a b) : nd_scope. Notation "[# a #]" := (nd_rule a) : nd_scope. Notation "a === b" := (@ndr_eqv _ _ _ _ _ a b) : nd_scope. +Hint Constructors Structural. +Hint Constructors ND_Relation. +Hint Constructors BuiltFrom. +Hint Constructors NDPredicateClosure. +Hint Constructors ContextND_Inert. +Hint Constructors SequentND_Inert. +Hint Unfold StructuralND. + (* enable setoid rewriting *) Open Scope nd_scope. Open Scope pf_scope. +Hint Extern 2 (StructuralND (nd_id _)) => apply nd_id_structural. +Hint Extern 2 (NDPredicateClosure _ ( _ ;; _ ) ) => apply ndpc_comp. +Hint Extern 2 (NDPredicateClosure _ ( _ ** _ ) ) => apply ndpc_prod. +Hint Extern 2 (NDPredicateClosure (@Structural _ _) (nd_id _)) => apply nd_id_structural. +Hint Extern 2 (BuiltFrom _ _ ( _ ;; _ ) ) => apply builtfrom_comp1. +Hint Extern 2 (BuiltFrom _ _ ( _ ;; _ ) ) => apply builtfrom_comp2. +Hint Extern 2 (BuiltFrom _ _ ( _ ** _ ) ) => apply builtfrom_prod1. +Hint Extern 2 (BuiltFrom _ _ ( _ ** _ ) ) => apply builtfrom_prod2. + +(* Hint Constructors has failed me! *) +Hint Extern 2 (@Structural _ _ _ _ (@nd_id0 _ _)) => apply nd_structural_id0. +Hint Extern 2 (@Structural _ _ _ _ (@nd_id1 _ _ _)) => apply nd_structural_id1. +Hint Extern 2 (@Structural _ _ _ _ (@nd_cancell _ _ _)) => apply nd_structural_cancell. +Hint Extern 2 (@Structural _ _ _ _ (@nd_cancelr _ _ _)) => apply nd_structural_cancelr. +Hint Extern 2 (@Structural _ _ _ _ (@nd_llecnac _ _ _)) => apply nd_structural_llecnac. +Hint Extern 2 (@Structural _ _ _ _ (@nd_rlecnac _ _ _)) => apply nd_structural_rlecnac. +Hint Extern 2 (@Structural _ _ _ _ (@nd_assoc _ _ _ _ _)) => apply nd_structural_assoc. +Hint Extern 2 (@Structural _ _ _ _ (@nd_cossa _ _ _ _ _)) => apply nd_structural_cossa. + +Hint Extern 4 (NDPredicateClosure _ _) => apply ndpc_p. + Add Parametric Relation {jt rt ndr h c} : (h/⋯⋯/c) (@ndr_eqv jt rt ndr h c) reflexivity proved by (@Equivalence_Reflexive _ _ (ndr_eqv_equivalence h c)) symmetry proved by (@Equivalence_Symmetric _ _ (ndr_eqv_equivalence h c)) @@ -534,7 +516,8 @@ Section ND_Relation_Facts. (* useful *) Lemma ndr_comp_right_identity : forall h c (f:h/⋯⋯/c), ndr_eqv (f ;; nd_id c) f. - intros; apply (ndr_builtfrom_structural f); auto. + intros; apply (ndr_builtfrom_structural f). auto. + auto. Defined. (* useful *) diff --git a/src/NaturalDeductionCategory.v b/src/NaturalDeductionCategory.v index d721a97..9360bfa 100644 --- a/src/NaturalDeductionCategory.v +++ b/src/NaturalDeductionCategory.v @@ -136,9 +136,9 @@ Section Judgments_Category. ; pmon_assoc_ll := jud_mon_assoc_ll }. unfold functor_fobj; unfold fmor; simpl; - apply Build_Pentagon; simpl; intros; apply (ndr_builtfrom_structural nd_id0); auto. + apply Build_Pentagon; simpl; intros; apply (ndr_builtfrom_structural nd_id0); auto 10. unfold functor_fobj; unfold fmor; simpl; - apply Build_Triangle; simpl; intros; apply (ndr_builtfrom_structural nd_id0); auto. + apply Build_Triangle; simpl; intros; apply (ndr_builtfrom_structural nd_id0); auto 10. intros; unfold eqv; simpl; auto; reflexivity. intros; unfold eqv; simpl; auto; reflexivity. intros; unfold eqv; simpl; apply Judgments_Category_Commutative. diff --git a/src/ProgrammingLanguage.v b/src/ProgrammingLanguage.v index dc2256c..83b435a 100644 --- a/src/ProgrammingLanguage.v +++ b/src/ProgrammingLanguage.v @@ -26,9 +26,7 @@ Require Import Enrichment_ch2_8. Require Import RepresentableStructure_ch7_2. Require Import FunctorCategories_ch7_7. -Require Import Enrichments. Require Import NaturalDeduction. -Require Import NaturalDeductionCategory. Section Programming_Language. @@ -47,687 +45,15 @@ Section Programming_Language. Open Scope pl_scope. Class ProgrammingLanguage := - { pl_eqv0 : @ND_Relation PLJudg Rule + { pl_eqv0 :> @ND_Relation PLJudg Rule ; pl_snd :> @SequentND PLJudg Rule _ sequent ; pl_cnd :> @ContextND PLJudg Rule T sequent pl_snd ; pl_eqv1 :> @SequentND_Relation PLJudg Rule _ sequent pl_snd pl_eqv0 ; pl_eqv :> @ContextND_Relation PLJudg Rule _ sequent pl_snd pl_cnd pl_eqv0 pl_eqv1 }. Notation "pf1 === pf2" := (@ndr_eqv _ _ pl_eqv _ _ pf1 pf2) : temporary_scope3. - - Section LanguageCategory. - - Context (PL:ProgrammingLanguage). - - (* category of judgments in a fixed type/coercion context *) - Definition Judgments_cartesian := @Judgments_Category_CartesianCat _ Rule pl_eqv. - - Definition JudgmentsL := Judgments_cartesian. - - Definition identityProof t : [] ~~{JudgmentsL}~~> [t |= t]. - unfold hom; simpl. - apply snd_initial. - Defined. - - Definition cutProof a b c : [a |= b],,[b |= c] ~~{JudgmentsL}~~> [a |= c]. - unfold hom; simpl. - apply snd_cut. - Defined. - - Existing Instance pl_eqv. - - Definition TypesL : ECategory JudgmentsL (Tree ??T) (fun x y => [x|=y]). - refine - {| eid := identityProof - ; ecomp := cutProof - |}; intros. - apply (mon_commutative(MonoidalCat:=JudgmentsL)). - apply (mon_commutative(MonoidalCat:=JudgmentsL)). - unfold identityProof; unfold cutProof; simpl; eapply cndr_inert. apply pl_eqv. auto. auto. - unfold identityProof; unfold cutProof; simpl; eapply cndr_inert. apply pl_eqv. auto. auto. - unfold identityProof; unfold cutProof; simpl; eapply cndr_inert. apply pl_eqv. auto. auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - Defined. - - Instance Types_first c : EFunctor TypesL TypesL (fun x => x,,c ) := - { efunc := fun x y => cnd_expand_right(ContextND:=pl_cnd) x y c }. - intros; apply (mon_commutative(MonoidalCat:=JudgmentsL)). - intros. unfold ehom. unfold hom. unfold identityProof. unfold eid. simpl. unfold identityProof. - apply (cndr_inert pl_cnd); auto. - intros. unfold ehom. unfold comp. simpl. unfold cutProof. - rewrite <- (@ndr_prod_preserves_comp _ _ pl_eqv _ _ (cnd_expand_right _ _ c) _ _ (nd_id1 (b|=c0)) - _ (nd_id1 (a,,c |= b,,c)) _ (cnd_expand_right _ _ c)). - setoid_rewrite (@ndr_comp_right_identity _ _ pl_eqv _ [a,, c |= b,, c]). - setoid_rewrite (@ndr_comp_left_identity _ _ pl_eqv [b |= c0]). - simpl; eapply cndr_inert. apply pl_eqv. auto. auto. - Defined. - - Instance Types_second c : EFunctor TypesL TypesL (fun x => c,,x) := - { efunc := fun x y => ((@cnd_expand_left _ _ _ _ _ _ x y c)) }. - intros; apply (mon_commutative(MonoidalCat:=JudgmentsL)). - intros. unfold ehom. unfold hom. unfold identityProof. unfold eid. simpl. unfold identityProof. - eapply cndr_inert; auto. apply pl_eqv. - intros. unfold ehom. unfold comp. simpl. unfold cutProof. - rewrite <- (@ndr_prod_preserves_comp _ _ pl_eqv _ _ (cnd_expand_left _ _ c) _ _ (nd_id1 (b|=c0)) - _ (nd_id1 (c,,a |= c,,b)) _ (cnd_expand_left _ _ c)). - setoid_rewrite (@ndr_comp_right_identity _ _ pl_eqv _ [c,,a |= c,,b]). - setoid_rewrite (@ndr_comp_left_identity _ _ pl_eqv [b |= c0]). - simpl; eapply cndr_inert. apply pl_eqv. auto. auto. - Defined. - - Definition Types_binoidal : EBinoidalCat TypesL (@T_Branch _). - refine - {| ebc_first := Types_first - ; ebc_second := Types_second - |}. - Defined. - - Instance Types_assoc_iso a b c : Isomorphic(C:=TypesL) ((a,,b),,c) (a,,(b,,c)) := - { iso_forward := snd_initial _ ;; cnd_ant_cossa _ a b c - ; iso_backward := snd_initial _ ;; cnd_ant_assoc _ a b c - }. - simpl; eapply cndr_inert. unfold identityProof; apply pl_eqv. auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - auto. - simpl; eapply cndr_inert. unfold identityProof; apply pl_eqv. auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - auto. - Defined. - - Instance Types_cancelr_iso a : Isomorphic(C:=TypesL) (a,,[]) a := - { iso_forward := snd_initial _ ;; cnd_ant_rlecnac _ a - ; iso_backward := snd_initial _ ;; cnd_ant_cancelr _ a - }. - unfold eqv; unfold comp; simpl. - eapply cndr_inert. apply pl_eqv. auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - auto. - unfold eqv; unfold comp; simpl. - eapply cndr_inert. apply pl_eqv. auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - auto. - Defined. - - Instance Types_cancell_iso a : Isomorphic(C:=TypesL) ([],,a) a := - { iso_forward := snd_initial _ ;; cnd_ant_llecnac _ a - ; iso_backward := snd_initial _ ;; cnd_ant_cancell _ a - }. - unfold eqv; unfold comp; simpl. - eapply cndr_inert. apply pl_eqv. auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - auto. - unfold eqv; unfold comp; simpl. - eapply cndr_inert. apply pl_eqv. auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - auto. - Defined. - - (* this tactical searches the environment; setoid_rewrite doesn't seem to be able to do that properly sometimes *) - Ltac nd_swap_ltac P EQV := - match goal with - [ |- context [ (?F ** nd_id _) ;; (nd_id _ ** ?G) ] ] => - set (@nd_swap _ _ EQV _ _ _ _ F G) as P - end. - - Instance Types_assoc a b : Types_second a >>>> Types_first b <~~~> Types_first b >>>> Types_second a := - { ni_iso := fun c => Types_assoc_iso a c b }. - intros. - Opaque nd_id. - simpl. - Transparent nd_id. - - rename A into X. - rename B into Y. - unfold ehom. - nd_swap_ltac p pl_eqv. - setoid_rewrite p. - clear p. - - setoid_rewrite (@nd_prod_split_left _ Rule pl_eqv _ _ _ []). - setoid_rewrite (@nd_prod_split_left _ Rule pl_eqv _ _ _ []). - setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []). - setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []). - - repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). - setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv). - - set (ni_commutes' (jud_mon_cancelr pl_eqv) f) as q. - Opaque nd_id. - simpl in q. - setoid_rewrite <- q. - - clear q. - set (ni_commutes' (jud_mon_cancell pl_eqv) f) as q. - simpl in q. - set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'. - set (isos_forward_equal_then_backward_equal _ _ q') as qq. - simpl in qq. - setoid_rewrite qq in q. - clear q' qq. - setoid_rewrite <- q. - - setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). - apply ndr_comp_respects; try reflexivity. - - Transparent nd_id. - apply (cndr_inert pl_cnd); auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - Defined. - - Instance Types_assoc_ll a b : Types_second (a,,b) <~~~> Types_second b >>>> Types_second a := - { ni_iso := fun c => Types_assoc_iso a b c }. - intros. - Opaque nd_id. - simpl. - Transparent nd_id. - - rename A into X. - rename B into Y. - unfold ehom. - nd_swap_ltac p pl_eqv. - setoid_rewrite p. - clear p. - - setoid_rewrite (@nd_prod_split_left _ Rule pl_eqv _ _ _ []). - setoid_rewrite (@nd_prod_split_left _ Rule pl_eqv _ _ _ []). - setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []). - - repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). - setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv). - - set (ni_commutes' (jud_mon_cancelr pl_eqv) f) as q. - Opaque nd_id. - simpl in q. - setoid_rewrite <- q. - - clear q. - set (ni_commutes' (jud_mon_cancell pl_eqv) f) as q. - simpl in q. - set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'. - set (isos_forward_equal_then_backward_equal _ _ q') as qq. - simpl in qq. - setoid_rewrite qq in q. - clear q' qq. - setoid_rewrite <- q. - - setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). - apply ndr_comp_respects; try reflexivity. - - Transparent nd_id. - apply (cndr_inert pl_cnd); auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - Defined. - - Instance Types_assoc_rr a b : Types_first (a,,b) <~~~> Types_first a >>>> Types_first b := - { ni_iso := fun c => iso_inv _ _ (Types_assoc_iso c a b) }. - intros. - Opaque nd_id. - simpl. - Transparent nd_id. - - rename A into X. - rename B into Y. - unfold ehom. - nd_swap_ltac p pl_eqv. - setoid_rewrite p. - clear p. - - setoid_rewrite (@nd_prod_split_left _ Rule pl_eqv _ _ _ []). - setoid_rewrite (@nd_prod_split_left _ Rule pl_eqv _ _ _ []). - setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []). - - repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). - setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv). - - set (ni_commutes' (jud_mon_cancelr pl_eqv) f) as q. - Opaque nd_id. - simpl in q. - setoid_rewrite <- q. - - clear q. - set (ni_commutes' (jud_mon_cancell pl_eqv) f) as q. - simpl in q. - set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'. - set (isos_forward_equal_then_backward_equal _ _ q') as qq. - simpl in qq. - setoid_rewrite qq in q. - clear q' qq. - setoid_rewrite <- q. - - setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). - apply ndr_comp_respects; try reflexivity. - - Transparent nd_id. - apply (cndr_inert pl_cnd); auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - Defined. - - Instance Types_cancelr : Types_first [] <~~~> functor_id _ := - { ni_iso := Types_cancelr_iso }. - intros. - Opaque nd_id. - simpl. - unfold ehom. - nd_swap_ltac p pl_eqv. - setoid_rewrite p. - setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []). - repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). - setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv). - - set (ni_commutes' (jud_mon_cancelr pl_eqv) f) as q. - Opaque nd_id. - simpl in q. - setoid_rewrite <- q. - clear q. - - set (ni_commutes' (jud_mon_cancell pl_eqv) f) as q. - simpl in q. - set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'. - set (isos_forward_equal_then_backward_equal _ _ q') as qq. - simpl in qq. - setoid_rewrite qq in q. - clear q' qq. - setoid_rewrite <- q. - - setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). - apply ndr_comp_respects; try reflexivity. - Transparent nd_id. - simpl. - apply (cndr_inert pl_cnd); auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - Defined. - - Instance Types_cancell : Types_second [] <~~~> functor_id _ := - { ni_iso := Types_cancell_iso }. - intros. - Opaque nd_id. - simpl. - unfold ehom. - nd_swap_ltac p pl_eqv. - setoid_rewrite p. - setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []). - repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). - setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv). - - set (ni_commutes' (jud_mon_cancelr pl_eqv) f) as q. - Opaque nd_id. - simpl in q. - setoid_rewrite <- q. - clear q. - - set (ni_commutes' (jud_mon_cancell pl_eqv) f) as q. - simpl in q. - set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'. - set (isos_forward_equal_then_backward_equal _ _ q') as qq. - simpl in qq. - setoid_rewrite qq in q. - clear q' qq. - setoid_rewrite <- q. - setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). - - apply ndr_comp_respects; try reflexivity. - Transparent nd_id. - simpl. - apply (cndr_inert pl_cnd); auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - Defined. - - Lemma TypesL_assoc_central a b c : CentralMorphism(H:=Types_binoidal) #((Types_assoc a b) c). - intros. - apply Build_CentralMorphism. - Opaque nd_id. - intros. - unfold bin_obj. - unfold ebc_bobj. - simpl. - unfold ehom. - nd_swap_ltac p pl_eqv. - setoid_rewrite p. - clear p. - setoid_rewrite (@nd_prod_split_left _ Rule pl_eqv _ _ _ []). - setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []). - repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). - setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv). - - set (ni_commutes' (jud_mon_cancelr pl_eqv) g) as q. - Opaque nd_id. - simpl in q. - setoid_rewrite <- q. - clear q. - - set (ni_commutes' (jud_mon_cancell pl_eqv) g) as q. - simpl in q. - set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'. - set (isos_forward_equal_then_backward_equal _ _ q') as qq. - simpl in qq. - setoid_rewrite qq in q. - clear q' qq. - setoid_rewrite <- q. - - setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). - apply ndr_comp_respects. - reflexivity. - - Transparent nd_id. - apply (cndr_inert pl_cnd); auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - - Opaque nd_id. - intros. - unfold bin_obj. - unfold ebc_bobj. - simpl. - unfold ehom. - symmetry. - nd_swap_ltac p pl_eqv. - setoid_rewrite p. - clear p. - setoid_rewrite (@nd_prod_split_left _ Rule pl_eqv _ _ _ []). - setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []). - repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). - setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv). - - set (ni_commutes' (jud_mon_cancelr pl_eqv) g) as q. - Opaque nd_id. - simpl in q. - setoid_rewrite <- q. - clear q. - - set (ni_commutes' (jud_mon_cancell pl_eqv) g) as q. - simpl in q. - set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'. - set (isos_forward_equal_then_backward_equal _ _ q') as qq. - simpl in qq. - setoid_rewrite qq in q. - clear q' qq. - setoid_rewrite <- q. - - setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). - apply ndr_comp_respects. - reflexivity. - - Transparent nd_id. - apply (cndr_inert pl_cnd); auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - Qed. - - Lemma TypesL_cancell_central a : CentralMorphism(H:=Types_binoidal) #(Types_cancell a). - intros. - apply Build_CentralMorphism. - Opaque nd_id. - intros. - unfold bin_obj. - unfold ebc_bobj. - simpl. - unfold ehom. - nd_swap_ltac p pl_eqv. - setoid_rewrite p. - clear p. - setoid_rewrite (@nd_prod_split_left _ Rule pl_eqv _ _ _ []). - setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []). - repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). - setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv). - - set (ni_commutes' (jud_mon_cancelr pl_eqv) g) as q. - Opaque nd_id. - simpl in q. - setoid_rewrite <- q. - clear q. - - set (ni_commutes' (jud_mon_cancell pl_eqv) g) as q. - simpl in q. - set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'. - set (isos_forward_equal_then_backward_equal _ _ q') as qq. - simpl in qq. - setoid_rewrite qq in q. - clear q' qq. - setoid_rewrite <- q. - - setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). - apply ndr_comp_respects. - reflexivity. - - Transparent nd_id. - apply (cndr_inert pl_cnd); auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - - Opaque nd_id. - intros. - unfold bin_obj. - unfold ebc_bobj. - simpl. - unfold ehom. - symmetry. - nd_swap_ltac p pl_eqv. - setoid_rewrite p. - clear p. - setoid_rewrite (@nd_prod_split_left _ Rule pl_eqv _ _ _ []). - setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []). - repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). - setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv). - - set (ni_commutes' (jud_mon_cancelr pl_eqv) g) as q. - Opaque nd_id. - simpl in q. - setoid_rewrite <- q. - clear q. - - set (ni_commutes' (jud_mon_cancell pl_eqv) g) as q. - simpl in q. - set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'. - set (isos_forward_equal_then_backward_equal _ _ q') as qq. - simpl in qq. - setoid_rewrite qq in q. - clear q' qq. - setoid_rewrite <- q. - - setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). - apply ndr_comp_respects. - reflexivity. - - Transparent nd_id. - apply (cndr_inert pl_cnd); auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - Qed. - - Lemma TypesL_cancelr_central a : CentralMorphism(H:=Types_binoidal) #(Types_cancelr a). - intros. - apply Build_CentralMorphism. - Opaque nd_id. - intros. - unfold bin_obj. - unfold ebc_bobj. - simpl. - unfold ehom. - nd_swap_ltac p pl_eqv. - setoid_rewrite p. - clear p. - setoid_rewrite (@nd_prod_split_left _ Rule pl_eqv _ _ _ []). - setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []). - repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). - setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv). - - set (ni_commutes' (jud_mon_cancelr pl_eqv) g) as q. - Opaque nd_id. - simpl in q. - setoid_rewrite <- q. - clear q. - - set (ni_commutes' (jud_mon_cancell pl_eqv) g) as q. - simpl in q. - set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'. - set (isos_forward_equal_then_backward_equal _ _ q') as qq. - simpl in qq. - setoid_rewrite qq in q. - clear q' qq. - setoid_rewrite <- q. - - setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). - apply ndr_comp_respects. - reflexivity. - - Transparent nd_id. - apply (cndr_inert pl_cnd); auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - - Opaque nd_id. - intros. - unfold bin_obj. - unfold ebc_bobj. - simpl. - unfold ehom. - symmetry. - nd_swap_ltac p pl_eqv. - setoid_rewrite p. - clear p. - setoid_rewrite (@nd_prod_split_left _ Rule pl_eqv _ _ _ []). - setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []). - repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). - setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv). - - set (ni_commutes' (jud_mon_cancelr pl_eqv) g) as q. - Opaque nd_id. - simpl in q. - setoid_rewrite <- q. - clear q. - - set (ni_commutes' (jud_mon_cancell pl_eqv) g) as q. - simpl in q. - set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'. - set (isos_forward_equal_then_backward_equal _ _ q') as qq. - simpl in qq. - setoid_rewrite qq in q. - clear q' qq. - setoid_rewrite <- q. - - setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv). - apply ndr_comp_respects. - reflexivity. - - Transparent nd_id. - apply (cndr_inert pl_cnd); auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - apply ndpc_comp; auto. - Qed. - - Instance TypesL_PreMonoidal : PreMonoidalCat Types_binoidal [] := - { pmon_assoc := Types_assoc - ; pmon_cancell := Types_cancell - ; pmon_cancelr := Types_cancelr - ; pmon_assoc_rr := Types_assoc_rr - ; pmon_assoc_ll := Types_assoc_ll - }. - apply Build_Pentagon. - intros; simpl. - eapply cndr_inert. apply pl_eqv. - apply ndpc_comp. - apply ndpc_comp. - auto. - apply ndpc_comp. - apply ndpc_prod. - apply ndpc_comp. - apply ndpc_comp. - auto. - apply ndpc_comp. - auto. - auto. - auto. - auto. - auto. - auto. - apply ndpc_comp. - apply ndpc_comp. - auto. - apply ndpc_comp. - auto. - auto. - auto. - - apply Build_Triangle; intros; simpl. - eapply cndr_inert. apply pl_eqv. - auto. - apply ndpc_comp. - apply ndpc_comp. - auto. - apply ndpc_comp. - auto. - auto. - auto. - eapply cndr_inert. apply pl_eqv. auto. - auto. - intros; simpl; reflexivity. - intros; simpl; reflexivity. - apply TypesL_assoc_central. - apply TypesL_cancelr_central. - apply TypesL_cancell_central. - Defined. - - Definition TypesEnrichedInJudgments : SurjectiveEnrichment. - refine - {| senr_c_pm := TypesL_PreMonoidal - ; senr_v := JudgmentsL - ; senr_v_bin := Judgments_Category_binoidal _ - ; senr_v_pmon := Judgments_Category_premonoidal _ - ; senr_v_mon := Judgments_Category_monoidal _ - ; senr_c_bin := Types_binoidal - ; senr_c := TypesL - |}. - Defined. - - End LanguageCategory. + Coercion pl_eqv : ProgrammingLanguage >-> ContextND_Relation. + Coercion pl_cnd : ProgrammingLanguage >-> ContextND. End Programming_Language. -Implicit Arguments ND [ Judgment ]. + diff --git a/src/ProgrammingLanguageArrow.v b/src/ProgrammingLanguageArrow.v index 5dbce6d..5386d3e 100644 --- a/src/ProgrammingLanguageArrow.v +++ b/src/ProgrammingLanguageArrow.v @@ -30,7 +30,7 @@ Require Import FunctorCategories_ch7_7. Require Import NaturalDeduction. Require Import NaturalDeductionCategory. -Require Import ProgrammingLanguage. +Require Import ProgrammingLanguageCategory. Require Import FreydCategories. Require Import Enrichments. Require Import GeneralizedArrow. diff --git a/src/ProgrammingLanguageCategory.v b/src/ProgrammingLanguageCategory.v new file mode 100644 index 0000000..d415a35 --- /dev/null +++ b/src/ProgrammingLanguageCategory.v @@ -0,0 +1,650 @@ +(*********************************************************************************************************************************) +(* ProgrammingLanguageCategory *) +(* *) +(* The category Types(L) *) +(* *) +(*********************************************************************************************************************************) + +Generalizable All Variables. +Require Import Preamble. +Require Import General. +Require Import Categories_ch1_3. +Require Import InitialTerminal_ch2_2. +Require Import Functors_ch1_4. +Require Import Isomorphisms_ch1_5. +Require Import ProductCategories_ch1_6_1. +Require Import OppositeCategories_ch1_6_2. +Require Import Enrichment_ch2_8. +Require Import Subcategories_ch7_1. +Require Import NaturalTransformations_ch7_4. +Require Import NaturalIsomorphisms_ch7_5. +Require Import BinoidalCategories. +Require Import PreMonoidalCategories. +Require Import MonoidalCategories_ch7_8. +Require Import Coherence_ch7_8. +Require Import Enrichment_ch2_8. +Require Import RepresentableStructure_ch7_2. +Require Import FunctorCategories_ch7_7. + +Require Import NaturalDeduction. +Require Import ProgrammingLanguage. + Export ProgrammingLanguage. + +Require Import NaturalDeductionCategory. + +Open Scope nd_scope. +(* I am at a loss to explain why "auto" can't handle this *) +Ltac ndpc_tac := + match goal with + | [ |- NDPredicateClosure ?P (?A ;; ?B) ] => apply ndpc_comp; ndpc_tac + | [ |- NDPredicateClosure ?P (?A ** ?B) ] => apply ndpc_prod; ndpc_tac + | _ => auto + end. + +(* this tactical searches the environment; setoid_rewrite doesn't seem to be able to do that properly sometimes *) +Ltac nd_swap_ltac P EQV := + match goal with + [ |- context [ (?F ** nd_id _) ;; (nd_id _ ** ?G) ] ] => + set (@nd_swap _ _ EQV _ _ _ _ F G) as P + end. + +(* I still wish I knew why "Hint Constructors" doesn't work *) +Hint Extern 5 => apply snd_inert_initial. +Hint Extern 5 => apply snd_inert_cut. +Hint Extern 5 => apply snd_inert_structural. +Hint Extern 5 => apply cnd_inert_initial. +Hint Extern 5 => apply cnd_inert_cut. +Hint Extern 5 => apply cnd_inert_structural. +Hint Extern 5 => apply cnd_inert_cnd_ant_assoc. +Hint Extern 5 => apply cnd_inert_cnd_ant_cossa. +Hint Extern 5 => apply cnd_inert_cnd_ant_cancell. +Hint Extern 5 => apply cnd_inert_cnd_ant_cancelr. +Hint Extern 5 => apply cnd_inert_cnd_ant_llecnac. +Hint Extern 5 => apply cnd_inert_cnd_ant_rlecnac. +Hint Extern 5 => apply cnd_inert_se_expand_left. +Hint Extern 5 => apply cnd_inert_se_expand_right. + +Hint Extern 2 (@Structural _ _ _ _ (@nd_id _ _ [] )) => simpl; auto. +Hint Extern 2 (@Structural _ _ _ _ (@nd_id _ _ [ _ ])) => simpl; auto. + +Section ProgrammingLanguageCategory. + + Context {T : Type}. (* types of the language *) + + Context {Rule : Tree ??(@PLJudg T) -> Tree ??(@PLJudg T) -> Type}. + Notation "cs |= ss" := (@sequent T cs ss) : pl_scope. + + Notation "H /⋯⋯/ C" := (ND Rule H C) : pl_scope. + + Open Scope pf_scope. + Open Scope nd_scope. + Open Scope pl_scope. + + Context (PL:@ProgrammingLanguage T Rule). + + (* category of judgments in a fixed type/coercion context *) + Definition Judgments_cartesian := @Judgments_Category_CartesianCat _ Rule pl_eqv. + + Definition JudgmentsL := Judgments_cartesian. + + Definition identityProof t : [] ~~{JudgmentsL}~~> [t |= t]. + unfold hom; simpl. + apply snd_initial. + Defined. + + Definition cutProof a b c : [a |= b],,[b |= c] ~~{JudgmentsL}~~> [a |= c]. + unfold hom; simpl. + apply snd_cut. + Defined. + + Instance TypesL : ECategory JudgmentsL (Tree ??T) (fun x y => [x|=y]) := + { eid := identityProof + ; ecomp := cutProof + }. + intros; apply (mon_commutative(MonoidalCat:=JudgmentsL)). + intros; apply (mon_commutative(MonoidalCat:=JudgmentsL)). + abstract (intros; unfold identityProof; unfold cutProof; simpl; eapply cndr_inert; auto; apply PL). + abstract (intros; unfold identityProof; unfold cutProof; simpl; eapply cndr_inert; auto; apply PL). + abstract (intros; unfold identityProof; unfold cutProof; simpl; eapply cndr_inert; + [ apply PL | idtac | idtac ]; apply ndpc_comp; auto). + Defined. + + Instance Types_first c : EFunctor TypesL TypesL (fun x => x,,c ) := + { efunc := fun x y => cnd_expand_right(ContextND:=pl_cnd) x y c }. + intros; apply (mon_commutative(MonoidalCat:=JudgmentsL)). + abstract (intros; simpl; apply (cndr_inert pl_cnd); auto). + abstract (intros; unfold ehom; unfold comp; simpl; unfold cutProof; + rewrite <- (@ndr_prod_preserves_comp _ _ PL _ _ (cnd_expand_right _ _ c) _ _ (nd_id1 (b|=c0)) + _ (nd_id1 (a,,c |= b,,c)) _ (cnd_expand_right _ _ c)); + setoid_rewrite (@ndr_comp_right_identity _ _ PL _ [a,, c |= b,, c]); + setoid_rewrite (@ndr_comp_left_identity _ _ PL [b |= c0]); + simpl; eapply cndr_inert; [ apply PL | auto | auto ]). + Defined. + + Instance Types_second c : EFunctor TypesL TypesL (fun x => c,,x) := + { efunc := fun x y => ((@cnd_expand_left _ _ _ _ _ _ x y c)) }. + intros; apply (mon_commutative(MonoidalCat:=JudgmentsL)). + abstract (intros; simpl; apply (cndr_inert pl_cnd); auto). + intros; unfold ehom; unfold comp; simpl; unfold cutProof; + abstract (rewrite <- (@ndr_prod_preserves_comp _ _ PL _ _ (cnd_expand_left _ _ c) _ _ (nd_id1 (b|=c0)) + _ (nd_id1 (c,,a |= c,,b)) _ (cnd_expand_left _ _ c)); + setoid_rewrite (@ndr_comp_right_identity _ _ PL _ [c,,a |= c,,b]); + setoid_rewrite (@ndr_comp_left_identity _ _ PL [b |= c0]); + simpl; eapply cndr_inert; [ apply PL | auto | auto ]). + Defined. + + Instance Types_binoidal : EBinoidalCat TypesL (@T_Branch _) := + { ebc_first := Types_first + ; ebc_second := Types_second + }. + + Instance Types_assoc_iso a b c : Isomorphic(C:=TypesL) ((a,,b),,c) (a,,(b,,c)) := + { iso_forward := snd_initial _ ;; cnd_ant_cossa _ a b c + ; iso_backward := snd_initial _ ;; cnd_ant_assoc _ a b c + }. + abstract (simpl; eapply cndr_inert; unfold identityProof; [ apply PL | idtac | idtac ]; ndpc_tac). + abstract (simpl; eapply cndr_inert; unfold identityProof; [ apply PL | idtac | idtac ]; ndpc_tac). + Defined. + + Instance Types_cancelr_iso a : Isomorphic(C:=TypesL) (a,,[]) a := + { iso_forward := snd_initial _ ;; cnd_ant_rlecnac _ a + ; iso_backward := snd_initial _ ;; cnd_ant_cancelr _ a + }. + abstract (simpl; eapply cndr_inert; unfold identityProof; [ apply PL | idtac | idtac ]; ndpc_tac). + abstract (simpl; eapply cndr_inert; unfold identityProof; [ apply PL | idtac | idtac ]; ndpc_tac). + Defined. + + Instance Types_cancell_iso a : Isomorphic(C:=TypesL) ([],,a) a := + { iso_forward := snd_initial _ ;; cnd_ant_llecnac _ a + ; iso_backward := snd_initial _ ;; cnd_ant_cancell _ a + }. + abstract (simpl; eapply cndr_inert; unfold identityProof; [ apply PL | idtac | idtac ]; ndpc_tac). + abstract (simpl; eapply cndr_inert; unfold identityProof; [ apply PL | idtac | idtac ]; ndpc_tac). + Defined. + + Lemma coincide' : nd_llecnac === nd_rlecnac. + set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'. + set (isos_forward_equal_then_backward_equal _ _ q') as qq. + apply qq. + Qed. + + Lemma Types_assoc_lemma : ∀a b X Y : TypesL, + ∀f : X ~~{ TypesL }~~> Y, + #(Types_assoc_iso a X b) >>> (Types_first b >>>> Types_second a) \ f ~~ + (Types_second a >>>> Types_first b) \ f >>> #(Types_assoc_iso a Y b). + intros. + Opaque nd_id. + simpl. + Transparent nd_id. + unfold ehom. + + nd_swap_ltac p PL. + setoid_rewrite p. + clear p. + + repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL). + + setoid_rewrite (@nd_prod_split_left _ Rule PL _ _ _ []). + setoid_rewrite (@nd_prod_split_left _ Rule PL _ _ _ []). + setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []). + setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []). + + setoid_rewrite (@ndr_comp_associativity _ Rule PL). + setoid_rewrite (@ndr_comp_associativity _ Rule PL). + setoid_rewrite <- (@ndr_comp_associativity _ Rule PL). + + set (ni_commutes' (jud_mon_cancelr PL) f) as q. + simpl in q. + setoid_rewrite <- q. + clear q. + + set (ni_commutes' (jud_mon_cancell PL) f) as q. + simpl in q. + setoid_rewrite coincide' in q. + setoid_rewrite <- q. + clear q. + + setoid_rewrite (@ndr_comp_associativity _ Rule PL). + apply ndr_comp_respects; try reflexivity. + + apply (cndr_inert pl_cnd); auto; ndpc_tac; auto. + Qed. + + Instance Types_assoc a b : Types_second a >>>> Types_first b <~~~> Types_first b >>>> Types_second a := + { ni_iso := fun c => Types_assoc_iso a c b }. + apply Types_assoc_lemma. + Defined. + + Lemma Types_assoc_ll_lemma : + ∀a b X Y : TypesL, + ∀f : X ~~{ TypesL }~~> Y, + #(Types_assoc_iso a b X) >>> (Types_second b >>>> Types_second a) \ f ~~ + Types_second (a,, b) \ f >>> #(Types_assoc_iso a b Y). + + intros. + Opaque nd_id. + simpl. + Transparent nd_id. + unfold ehom. + nd_swap_ltac p PL. + setoid_rewrite p. + clear p. + + setoid_rewrite (@nd_prod_split_left _ Rule PL _ _ _ []). + setoid_rewrite (@nd_prod_split_left _ Rule PL _ _ _ []). + setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []). + + repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL). + setoid_rewrite <- (@ndr_comp_associativity _ Rule PL). + + set (ni_commutes' (jud_mon_cancelr PL) f) as q. + Opaque nd_id. + simpl in q. + setoid_rewrite <- q. + + clear q. + set (ni_commutes' (jud_mon_cancell PL) f) as q. + simpl in q. + set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'. + set (isos_forward_equal_then_backward_equal _ _ q') as qq. + simpl in qq. + setoid_rewrite qq in q. + clear q' qq. + setoid_rewrite <- q. + + setoid_rewrite (@ndr_comp_associativity _ Rule PL). + apply ndr_comp_respects; try reflexivity. + + Transparent nd_id. + apply (cndr_inert pl_cnd); auto; ndpc_tac. + Qed. + + Instance Types_assoc_ll a b : Types_second (a,,b) <~~~> Types_second b >>>> Types_second a := + { ni_iso := fun c => Types_assoc_iso a b c }. + apply Types_assoc_ll_lemma. + Defined. + + Lemma Types_assoc_rr_lemma : + ∀a b A B : TypesL, + ∀f : A ~~{ TypesL }~~> B, + #(Types_assoc_iso A a b) ⁻¹ >>> (Types_first a >>>> Types_first b) \ f ~~ + Types_first (a,, b) \ f >>> #(Types_assoc_iso B a b) ⁻¹. + intros. + Opaque nd_id. + simpl. + Transparent nd_id. + + rename A into X. + rename B into Y. + unfold ehom. + nd_swap_ltac p PL. + setoid_rewrite p. + clear p. + + setoid_rewrite (@nd_prod_split_left _ Rule PL _ _ _ []). + setoid_rewrite (@nd_prod_split_left _ Rule PL _ _ _ []). + setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []). + + repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL). + setoid_rewrite <- (@ndr_comp_associativity _ Rule PL). + + set (ni_commutes' (jud_mon_cancelr PL) f) as q. + Opaque nd_id. + simpl in q. + setoid_rewrite <- q. + + clear q. + set (ni_commutes' (jud_mon_cancell PL) f) as q. + simpl in q. + set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'. + set (isos_forward_equal_then_backward_equal _ _ q') as qq. + simpl in qq. + setoid_rewrite qq in q. + clear q' qq. + setoid_rewrite <- q. + + setoid_rewrite (@ndr_comp_associativity _ Rule PL). + apply ndr_comp_respects; try reflexivity. + + Transparent nd_id. + apply (cndr_inert pl_cnd); auto; ndpc_tac. + Qed. + + Instance Types_assoc_rr a b : Types_first (a,,b) <~~~> Types_first a >>>> Types_first b := + { ni_iso := fun c => iso_inv _ _ (Types_assoc_iso c a b) }. + apply Types_assoc_rr_lemma. + Defined. + + Lemma Types_cancelr_lemma : + ∀A B : TypesL, + ∀f : A ~~{ TypesL }~~> B, + #(Types_cancelr_iso A) >>> functor_id TypesL \ f ~~ + Types_first [] \ f >>> #(Types_cancelr_iso B). + intros. + Opaque nd_id. + simpl. + unfold ehom. + nd_swap_ltac p PL. + setoid_rewrite p. + setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []). + repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL). + setoid_rewrite <- (@ndr_comp_associativity _ Rule PL). + + set (ni_commutes' (jud_mon_cancelr PL) f) as q. + Opaque nd_id. + simpl in q. + setoid_rewrite <- q. + clear q. + + set (ni_commutes' (jud_mon_cancell PL) f) as q. + simpl in q. + set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'. + set (isos_forward_equal_then_backward_equal _ _ q') as qq. + simpl in qq. + setoid_rewrite qq in q. + clear q' qq. + setoid_rewrite <- q. + + setoid_rewrite (@ndr_comp_associativity _ Rule PL). + apply ndr_comp_respects; try reflexivity. + Transparent nd_id. + simpl. + apply (cndr_inert pl_cnd); auto; ndpc_tac. + Qed. + + Instance Types_cancelr : Types_first [] <~~~> functor_id _ := + { ni_iso := Types_cancelr_iso }. + apply Types_cancelr_lemma. + Defined. + + Lemma Types_cancell_lemma : + ∀A B : TypesL, + ∀f : A ~~{ TypesL }~~> B, + #(Types_cancell_iso A) >>> functor_id TypesL \ f ~~ + Types_second [] \ f >>> #(Types_cancell_iso B). + intros. + Opaque nd_id. + simpl. + unfold ehom. + nd_swap_ltac p PL. + setoid_rewrite p. + setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []). + repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL). + setoid_rewrite <- (@ndr_comp_associativity _ Rule PL). + + set (ni_commutes' (jud_mon_cancelr PL) f) as q. + Opaque nd_id. + simpl in q. + setoid_rewrite <- q. + clear q. + + set (ni_commutes' (jud_mon_cancell PL) f) as q. + simpl in q. + set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'. + set (isos_forward_equal_then_backward_equal _ _ q') as qq. + simpl in qq. + setoid_rewrite qq in q. + clear q' qq. + setoid_rewrite <- q. + setoid_rewrite (@ndr_comp_associativity _ Rule PL). + + apply ndr_comp_respects; try reflexivity. + Transparent nd_id. + simpl. + apply (cndr_inert pl_cnd); auto; ndpc_tac. + Qed. + + Instance Types_cancell : Types_second [] <~~~> functor_id _ := + { ni_iso := Types_cancell_iso }. + apply Types_cancell_lemma. + Defined. + + Lemma TypesL_assoc_central a b c : CentralMorphism(H:=Types_binoidal) #((Types_assoc a b) c). + intros. + apply Build_CentralMorphism. + intros. + unfold bin_obj. + unfold ebc_bobj. + Opaque nd_id. + simpl. + unfold ehom. + nd_swap_ltac p PL. + setoid_rewrite p. + clear p. + setoid_rewrite (@nd_prod_split_left _ Rule PL _ _ _ []). + setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []). + repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL). + setoid_rewrite <- (@ndr_comp_associativity _ Rule PL). + + set (ni_commutes' (jud_mon_cancelr PL) g) as q. + Opaque nd_id. + simpl in q. + setoid_rewrite <- q. + clear q. + + set (ni_commutes' (jud_mon_cancell PL) g) as q. + simpl in q. + set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'. + set (isos_forward_equal_then_backward_equal _ _ q') as qq. + simpl in qq. + setoid_rewrite qq in q. + clear q' qq. + setoid_rewrite <- q. + + setoid_rewrite (@ndr_comp_associativity _ Rule PL). + apply ndr_comp_respects. + reflexivity. + + Transparent nd_id. + apply (cndr_inert pl_cnd); auto; ndpc_tac. + + Opaque nd_id. + intros. + unfold bin_obj. + unfold ebc_bobj. + simpl. + unfold ehom. + symmetry. + nd_swap_ltac p PL. + setoid_rewrite p. + clear p. + setoid_rewrite (@nd_prod_split_left _ Rule PL _ _ _ []). + setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []). + repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL). + setoid_rewrite <- (@ndr_comp_associativity _ Rule PL). + + set (ni_commutes' (jud_mon_cancelr PL) g) as q. + Opaque nd_id. + simpl in q. + setoid_rewrite <- q. + clear q. + + set (ni_commutes' (jud_mon_cancell PL) g) as q. + simpl in q. + set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'. + set (isos_forward_equal_then_backward_equal _ _ q') as qq. + simpl in qq. + setoid_rewrite qq in q. + clear q' qq. + setoid_rewrite <- q. + + setoid_rewrite (@ndr_comp_associativity _ Rule PL). + apply ndr_comp_respects. + reflexivity. + + Transparent nd_id. + apply (cndr_inert pl_cnd); auto; ndpc_tac. + Qed. + + Lemma TypesL_cancell_central a : CentralMorphism(H:=Types_binoidal) #(Types_cancell a). + intros. + apply Build_CentralMorphism. + Opaque nd_id. + intros. + unfold bin_obj. + unfold ebc_bobj. + simpl. + unfold ehom. + nd_swap_ltac p PL. + setoid_rewrite p. + clear p. + setoid_rewrite (@nd_prod_split_left _ Rule PL _ _ _ []). + setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []). + repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL). + setoid_rewrite <- (@ndr_comp_associativity _ Rule PL). + + set (ni_commutes' (jud_mon_cancelr PL) g) as q. + Opaque nd_id. + simpl in q. + setoid_rewrite <- q. + clear q. + + set (ni_commutes' (jud_mon_cancell PL) g) as q. + simpl in q. + set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'. + set (isos_forward_equal_then_backward_equal _ _ q') as qq. + simpl in qq. + setoid_rewrite qq in q. + clear q' qq. + setoid_rewrite <- q. + + setoid_rewrite (@ndr_comp_associativity _ Rule PL). + apply ndr_comp_respects. + reflexivity. + + Transparent nd_id. + apply (cndr_inert pl_cnd); auto; ndpc_tac. + + Opaque nd_id. + intros. + unfold bin_obj. + unfold ebc_bobj. + simpl. + unfold ehom. + symmetry. + nd_swap_ltac p PL. + setoid_rewrite p. + clear p. + setoid_rewrite (@nd_prod_split_left _ Rule PL _ _ _ []). + setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []). + repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL). + setoid_rewrite <- (@ndr_comp_associativity _ Rule PL). + + set (ni_commutes' (jud_mon_cancelr PL) g) as q. + Opaque nd_id. + simpl in q. + setoid_rewrite <- q. + clear q. + + set (ni_commutes' (jud_mon_cancell PL) g) as q. + simpl in q. + set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'. + set (isos_forward_equal_then_backward_equal _ _ q') as qq. + simpl in qq. + setoid_rewrite qq in q. + clear q' qq. + setoid_rewrite <- q. + + setoid_rewrite (@ndr_comp_associativity _ Rule PL). + apply ndr_comp_respects. + reflexivity. + + Transparent nd_id. + apply (cndr_inert pl_cnd); auto; ndpc_tac. + Qed. + + Lemma TypesL_cancelr_central a : CentralMorphism(H:=Types_binoidal) #(Types_cancelr a). + intros. + apply Build_CentralMorphism. + Opaque nd_id. + intros. + unfold bin_obj. + unfold ebc_bobj. + simpl. + unfold ehom. + nd_swap_ltac p PL. + setoid_rewrite p. + clear p. + setoid_rewrite (@nd_prod_split_left _ Rule PL _ _ _ []). + setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []). + repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL). + setoid_rewrite <- (@ndr_comp_associativity _ Rule PL). + + set (ni_commutes' (jud_mon_cancelr PL) g) as q. + Opaque nd_id. + simpl in q. + setoid_rewrite <- q. + clear q. + + set (ni_commutes' (jud_mon_cancell PL) g) as q. + simpl in q. + set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'. + set (isos_forward_equal_then_backward_equal _ _ q') as qq. + simpl in qq. + setoid_rewrite qq in q. + clear q' qq. + setoid_rewrite <- q. + + setoid_rewrite (@ndr_comp_associativity _ Rule PL). + apply ndr_comp_respects. + reflexivity. + + Transparent nd_id. + apply (cndr_inert pl_cnd); auto; ndpc_tac. + + Opaque nd_id. + intros. + unfold bin_obj. + unfold ebc_bobj. + simpl. + unfold ehom. + symmetry. + nd_swap_ltac p PL. + setoid_rewrite p. + clear p. + setoid_rewrite (@nd_prod_split_left _ Rule PL _ _ _ []). + setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []). + repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL). + setoid_rewrite <- (@ndr_comp_associativity _ Rule PL). + + set (ni_commutes' (jud_mon_cancelr PL) g) as q. + Opaque nd_id. + simpl in q. + setoid_rewrite <- q. + clear q. + + set (ni_commutes' (jud_mon_cancell PL) g) as q. + simpl in q. + set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'. + set (isos_forward_equal_then_backward_equal _ _ q') as qq. + simpl in qq. + setoid_rewrite qq in q. + clear q' qq. + setoid_rewrite <- q. + + setoid_rewrite (@ndr_comp_associativity _ Rule PL). + apply ndr_comp_respects. + reflexivity. + + Transparent nd_id. + apply (cndr_inert pl_cnd); auto; ndpc_tac. + Qed. + + Instance TypesL_PreMonoidal : PreMonoidalCat Types_binoidal [] := + { pmon_assoc := Types_assoc + ; pmon_cancell := Types_cancell + ; pmon_cancelr := Types_cancelr + ; pmon_assoc_rr := Types_assoc_rr + ; pmon_assoc_ll := Types_assoc_ll + }. + abstract (apply Build_Pentagon; intros; simpl; eapply cndr_inert; try apply PL; ndpc_tac). + abstract (apply Build_Triangle; intros; simpl; eapply cndr_inert; try apply PL; ndpc_tac). + intros; simpl; reflexivity. + intros; simpl; reflexivity. + apply TypesL_assoc_central. + apply TypesL_cancelr_central. + apply TypesL_cancell_central. + Defined. + +End ProgrammingLanguageCategory. + diff --git a/src/ProgrammingLanguageEnrichment.v b/src/ProgrammingLanguageEnrichment.v new file mode 100644 index 0000000..332a8ba --- /dev/null +++ b/src/ProgrammingLanguageEnrichment.v @@ -0,0 +1,52 @@ +(*********************************************************************************************************************************) +(* ProgrammingLanguageEnrichment *) +(* *) +(* Types are enriched in Judgments. *) +(* *) +(*********************************************************************************************************************************) + +Generalizable All Variables. +Require Import Preamble. +Require Import General. +Require Import Categories_ch1_3. +Require Import InitialTerminal_ch2_2. +Require Import Functors_ch1_4. +Require Import Isomorphisms_ch1_5. +Require Import ProductCategories_ch1_6_1. +Require Import OppositeCategories_ch1_6_2. +Require Import Enrichment_ch2_8. +Require Import Subcategories_ch7_1. +Require Import NaturalTransformations_ch7_4. +Require Import NaturalIsomorphisms_ch7_5. +Require Import BinoidalCategories. +Require Import PreMonoidalCategories. +Require Import MonoidalCategories_ch7_8. +Require Import Coherence_ch7_8. +Require Import Enrichment_ch2_8. +Require Import RepresentableStructure_ch7_2. +Require Import FunctorCategories_ch7_7. + +Require Import Enrichments. +Require Import NaturalDeduction. +Require Import NaturalDeductionCategory. +Require Import ProgrammingLanguageCategory. + Export ProgrammingLanguageCategory. + +Section ProgrammingLanguageEnrichment. + + Context `(PL:ProgrammingLanguage). + + Definition TypesEnrichedInJudgments : SurjectiveEnrichment. + refine + {| senr_c_pm := TypesL_PreMonoidal PL + ; senr_v := JudgmentsL PL + ; senr_v_bin := Judgments_Category_binoidal _ + ; senr_v_pmon := Judgments_Category_premonoidal _ + ; senr_v_mon := Judgments_Category_monoidal _ + ; senr_c_bin := Types_binoidal PL + ; senr_c := TypesL PL + |}. + Defined. + +End ProgrammingLanguageEnrichment. + diff --git a/src/ProgrammingLanguageFlattening.v b/src/ProgrammingLanguageFlattening.v index 4438dd2..4c2a66b 100644 --- a/src/ProgrammingLanguageFlattening.v +++ b/src/ProgrammingLanguageFlattening.v @@ -27,7 +27,7 @@ Require Import Reification. Require Import NaturalDeduction. Require Import NaturalDeductionCategory. Require Import GeneralizedArrow. -Require Import ProgrammingLanguage. +Require Import ProgrammingLanguageEnrichment. Require Import ProgrammingLanguageReification. Require Import SectionRetract_ch2_4. Require Import GeneralizedArrowFromReification. diff --git a/src/ProgrammingLanguageGeneralizedArrow.v b/src/ProgrammingLanguageGeneralizedArrow.v index bed54b6..8fe0391 100644 --- a/src/ProgrammingLanguageGeneralizedArrow.v +++ b/src/ProgrammingLanguageGeneralizedArrow.v @@ -30,7 +30,7 @@ Require Import NaturalDeductionCategory. Require Import Enrichments. Require Import Reification. Require Import GeneralizedArrow. -Require Import ProgrammingLanguage. +Require Import ProgrammingLanguageEnrichment. Section ProgrammingLanguageGeneralizedArrow. diff --git a/src/ProgrammingLanguageReification.v b/src/ProgrammingLanguageReification.v index 932c517..c1a06d8 100644 --- a/src/ProgrammingLanguageReification.v +++ b/src/ProgrammingLanguageReification.v @@ -28,6 +28,7 @@ Require Import Reification. Require Import NaturalDeduction. Require Import NaturalDeductionCategory. Require Import ProgrammingLanguage. +Require Import ProgrammingLanguageCategory. Require Import Enrichments. Section ProgrammingLanguageReification.