X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FNaturalDeductionCategory.v;h=b64ac4ba9f91e3cb10b37aa7025ae55f339d8208;hp=23ddb566cf26bcbe39602898d03c1155691c21ec;hb=e3e2ce9cb83acdd8191049b4e9bd3d4fcf6a4db4;hpb=76f4613eaa5989e29bfd59d716c216ee5386c5f7 diff --git a/src/NaturalDeductionCategory.v b/src/NaturalDeductionCategory.v index 23ddb56..b64ac4b 100644 --- a/src/NaturalDeductionCategory.v +++ b/src/NaturalDeductionCategory.v @@ -22,6 +22,7 @@ Require Import NaturalTransformations_ch7_4. Require Import NaturalIsomorphisms_ch7_5. Require Import MonoidalCategories_ch7_8. Require Import Coherence_ch7_8. +Require Import InitialTerminal_ch2_2. Open Scope nd_scope. Open Scope pf_scope. @@ -33,15 +34,9 @@ Section Judgments_Category. Context {Rule : forall (hypotheses:Tree ??Judgment)(conclusion:Tree ??Judgment), Type}. Context (nd_eqv : @ND_Relation Judgment Rule). - (* actually you can use any type as the objects, so long as you give a mapping from that type to judgments *) - Context {Ob : Type}. - Context (ob2judgment : Ob -> Judgment). - Coercion ob2judgment : Ob >-> Judgment. - Notation "pf1 === pf2" := (@ndr_eqv _ _ nd_eqv _ _ pf1 pf2). - Instance Judgments_Category - : Category (Tree ??Ob) (fun h c => (mapOptionTree ob2judgment h) /⋯⋯/ (mapOptionTree ob2judgment c)) := + Instance Judgments_Category : Category (Tree ??Judgment) (fun h c => h /⋯⋯/ c) := { id := fun h => nd_id _ ; comp := fun a b c f g => f ;; g ; eqv := fun a b f g => f === g @@ -57,10 +52,7 @@ Section Judgments_Category. Defined. Definition Judgments_Category_monoidal_endofunctor_fobj : Judgments_Category ×× Judgments_Category -> Judgments_Category := - (fun xy => - match xy with - | pair_obj x y => T_Branch x y - end). + fun xy => (fst_obj _ _ xy),,(snd_obj _ _ xy). Definition Judgments_Category_monoidal_endofunctor_fmor : forall a b, (a~~{Judgments_Category ×× Judgments_Category}~~>b) -> ((Judgments_Category_monoidal_endofunctor_fobj a) @@ -70,6 +62,7 @@ Section Judgments_Category. destruct a. destruct b. destruct X. + simpl in *. exact (h**h0). Defined. Definition Judgments_Category_monoidal_endofunctor @@ -81,51 +74,53 @@ Section Judgments_Category. Defined. Definition jud_assoc_iso (a b c:Judgments_Category) : @Isomorphic _ _ Judgments_Category ((a,,b),,c) (a,,(b,,c)). - apply (@Build_Isomorphic _ _ Judgments_Category _ _ - (@nd_assoc _ Rule (mapOptionTree ob2judgment a) (mapOptionTree ob2judgment b) (mapOptionTree ob2judgment c) - : (a,, b),, c ~~{Judgments_Category}~~> a,, (b,, c)) - (@nd_cossa _ Rule (mapOptionTree ob2judgment a) (mapOptionTree ob2judgment b) (mapOptionTree ob2judgment c) - : a,, (b,, c) ~~{Judgments_Category}~~> (a,, b),, c)); simpl; auto. + refine + {| iso_forward := nd_assoc + ; iso_backward := nd_cossa |}; + abstract (simpl; auto). Defined. Definition jud_cancelr_iso (a:Judgments_Category) : @Isomorphic _ _ Judgments_Category (a,,[]) a. - apply (@Build_Isomorphic _ _ Judgments_Category _ _ - (@nd_cancelr _ Rule (mapOptionTree ob2judgment a) : a,,[] ~~{Judgments_Category}~~> a) - (@nd_rlecnac _ Rule (mapOptionTree ob2judgment a) : a ~~{Judgments_Category}~~> a,,[])); simpl; auto. + refine + {| iso_forward := nd_cancelr + ; iso_backward := nd_rlecnac |}; + abstract (simpl; auto). Defined. Definition jud_cancell_iso (a:Judgments_Category) : @Isomorphic _ _ Judgments_Category ([],,a) a. - apply (@Build_Isomorphic _ _ Judgments_Category _ _ - (@nd_cancell _ Rule (mapOptionTree ob2judgment a) : [],,a ~~{Judgments_Category}~~> a) - (@nd_llecnac _ Rule (mapOptionTree ob2judgment a) : a ~~{Judgments_Category}~~> [],,a)); simpl; auto. + refine + {| iso_forward := nd_cancell + ; iso_backward := nd_llecnac |}; + abstract (simpl; auto). Defined. Definition jud_mon_cancelr : (func_rlecnac [] >>>> Judgments_Category_monoidal_endofunctor) <~~~> functor_id Judgments_Category. refine {| ni_iso := fun x => jud_cancelr_iso x |}; intros; simpl. - setoid_rewrite (ndr_prod_right_identity f). - repeat setoid_rewrite ndr_comp_associativity. - apply ndr_comp_respects; try reflexivity. - symmetry. - eapply transitivity; [ idtac | apply ndr_comp_right_identity ]. - apply ndr_comp_respects; try reflexivity; simpl; auto. + abstract (setoid_rewrite (ndr_prod_right_identity f); + repeat setoid_rewrite ndr_comp_associativity; + apply ndr_comp_respects; try reflexivity; + symmetry; + eapply transitivity; [ idtac | apply ndr_comp_right_identity ]; + apply ndr_comp_respects; try reflexivity; simpl; auto). Defined. Definition jud_mon_cancell : (func_llecnac [] >>>> Judgments_Category_monoidal_endofunctor) <~~~> functor_id Judgments_Category. eapply Build_NaturalIsomorphism. instantiate (1:=fun x => jud_cancell_iso x). - intros; simpl. - setoid_rewrite (ndr_prod_left_identity f). - repeat setoid_rewrite ndr_comp_associativity. - apply ndr_comp_respects; try reflexivity. - symmetry. - eapply transitivity; [ idtac | apply ndr_comp_right_identity ]. - apply ndr_comp_respects; try reflexivity; simpl; auto. + abstract (intros; simpl; + setoid_rewrite (ndr_prod_left_identity f); + repeat setoid_rewrite ndr_comp_associativity; + apply ndr_comp_respects; try reflexivity; + symmetry; + eapply transitivity; [ idtac | apply ndr_comp_right_identity ]; + apply ndr_comp_respects; try reflexivity; simpl; auto). Defined. - Definition jud_mon_assoc_iso : - forall X, - (((Judgments_Category_monoidal_endofunctor **** (functor_id _)) >>>> Judgments_Category_monoidal_endofunctor) X) ≅ - (func_cossa >>>> ((((functor_id _) **** Judgments_Category_monoidal_endofunctor) >>>> Judgments_Category_monoidal_endofunctor))) X. + Definition jud_mon_assoc_iso : forall X, + (((Judgments_Category_monoidal_endofunctor **** (functor_id _)) >>>> + Judgments_Category_monoidal_endofunctor) X) ≅ + (func_cossa >>>> ((((functor_id _) **** Judgments_Category_monoidal_endofunctor) >>>> + Judgments_Category_monoidal_endofunctor))) X. intros. destruct X as [a c]. destruct a as [a b]. - apply (jud_assoc_iso a b c). + exact (jud_assoc_iso a b c). Defined. Definition jud_mon_assoc : ((Judgments_Category_monoidal_endofunctor **** (functor_id _)) >>>> Judgments_Category_monoidal_endofunctor) @@ -133,41 +128,78 @@ Section Judgments_Category. func_cossa >>>> ((((functor_id _) **** Judgments_Category_monoidal_endofunctor) >>>> Judgments_Category_monoidal_endofunctor)). refine {| ni_iso := jud_mon_assoc_iso |}. intros. - destruct A as [a1 a3]. destruct a1 as [a1 a2]. - destruct B as [b1 b3]. destruct b1 as [b1 b2]. - destruct f as [f1 f3]. destruct f1 as [f1 f2]. - simpl. + unfold hom in *. + destruct A as [a1 a3]. destruct a1 as [a1 a2]. simpl in *. + destruct B as [b1 b3]. destruct b1 as [b1 b2]. simpl in *. + destruct f as [f1 f3]. destruct f1 as [f1 f2]. simpl in *. + unfold hom in *. + unfold ob in *. + unfold functor_fobj; unfold fmor; unfold functor_product_fobj; unfold Judgments_Category_monoidal_endofunctor_fobj; simpl. setoid_rewrite ndr_prod_associativity. setoid_rewrite ndr_comp_associativity. setoid_rewrite ndr_comp_associativity. apply ndr_comp_respects; try reflexivity. + etransitivity. symmetry. - eapply transitivity; [ idtac | apply ndr_comp_right_identity ]. - apply ndr_comp_respects; try reflexivity; simpl; auto. + apply ndr_comp_right_identity. + apply ndr_comp_respects; try reflexivity. + apply ndr_structural_indistinguishable; auto. Defined. Instance Judgments_Category_monoidal : MonoidalCat _ _ Judgments_Category_monoidal_endofunctor [ ] := { mon_cancelr := jud_mon_cancelr ; mon_cancell := jud_mon_cancell ; mon_assoc := jud_mon_assoc }. - apply Build_Pentagon; simpl; intros; apply ndr_structural_indistinguishable; auto. - apply Build_Triangle; simpl; intros; apply ndr_structural_indistinguishable; auto. + abstract + (unfold functor_fobj; unfold fmor; unfold functor_product_fobj; unfold Judgments_Category_monoidal_endofunctor_fobj; simpl; + apply Build_Pentagon; simpl; intros; apply ndr_structural_indistinguishable; auto). + abstract + (unfold functor_fobj; unfold fmor; unfold functor_product_fobj; unfold Judgments_Category_monoidal_endofunctor_fobj; simpl; + apply Build_Triangle; simpl; intros; apply ndr_structural_indistinguishable; auto). Defined. - (* Given some mapping "rep" that turns a (Tree ??T) intoto Judgment, - * this asserts that we have sensible structural rules with respect - * to that mapping. Doing all of this "with respect to a mapping" - * lets us avoid duplicating code for both the antecedent and - * succedent of sequent deductions. *) - Class TreeStructuralRules {T:Type}(rep:Tree ??T -> Judgment) := - { tsr_eqv : @ND_Relation Judgment Rule where "pf1 === pf2" := (@ndr_eqv _ _ tsr_eqv _ _ pf1 pf2) - ; tsr_ant_assoc : forall {a b c}, Rule [rep ((a,,b),,c)] [rep ((a,,(b,,c)))] - ; tsr_ant_cossa : forall {a b c}, Rule [rep (a,,(b,,c))] [rep (((a,,b),,c))] - ; tsr_ant_cancell : forall {a }, Rule [rep ( [],,a )] [rep ( a )] - ; tsr_ant_cancelr : forall {a }, Rule [rep (a,,[] )] [rep ( a )] - ; tsr_ant_llecnac : forall {a }, Rule [rep ( a )] [rep ( [],,a )] - ; tsr_ant_rlecnac : forall {a }, Rule [rep ( a )] [rep ( a,,[] )] - }. + Instance Judgments_Category_Terminal : Terminal Judgments_Category. + refine {| one := [] ; drop := nd_weak' ; drop_unique := _ |}. + abstract (intros; unfold eqv; simpl; apply ndr_void_proofs_irrelevant). + Defined. + + Instance Judgments_Category_Diagonal : DiagonalCat Judgments_Category_monoidal. + refine {| copy_nt := _ |}. + intros. + refine {| nt_component := nd_copy |}. + intros. + unfold hom in *; unfold ob in *; unfold eqv. + simpl. + rewrite ndr_prod_preserves_copy; auto. + reflexivity. + Defined. + + Instance Judgments_Category_CartesianCat : CartesianCat Judgments_Category_monoidal. + refine {| car_terminal := Judgments_Category_Terminal ; car_diagonal := Judgments_Category_Diagonal + ; car_one := iso_id [] |} + ; intros; unfold hom; simpl + ; unfold functor_fobj; unfold fmor; unfold functor_product_fobj; unfold Judgments_Category_monoidal_endofunctor_fobj; simpl. + + apply ndr_structural_indistinguishable; auto. + apply nd_structural_comp; auto. + apply nd_structural_comp; auto. + unfold copy; simpl; apply nd_structural_copy; auto. + apply nd_structural_prod; auto. + apply nd_structural_comp; auto. + apply weak'_structural. + apply nd_structural_id0; auto. + apply nd_structural_cancell; auto. + + apply ndr_structural_indistinguishable; auto. + apply nd_structural_comp; auto. + apply nd_structural_comp; auto. + unfold copy; simpl; apply nd_structural_copy; auto. + apply nd_structural_prod; auto. + apply nd_structural_comp; auto. + apply weak'_structural. + apply nd_structural_id0; auto. + apply nd_structural_cancelr; auto. + Defined. (* Structure ExpressionAlgebra (sig:Signature) := *)