X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FNaturalDeductionCategory.v;h=9360bfa6eb8eaa9403ae095f6ae4ff6c4884a43c;hp=23ddb566cf26bcbe39602898d03c1155691c21ec;hb=034f7e7856bebbbcb3c83946aa603c640b17f3bb;hpb=76f4613eaa5989e29bfd59d716c216ee5386c5f7 diff --git a/src/NaturalDeductionCategory.v b/src/NaturalDeductionCategory.v index 23ddb56..9360bfa 100644 --- a/src/NaturalDeductionCategory.v +++ b/src/NaturalDeductionCategory.v @@ -1,7 +1,7 @@ (*********************************************************************************************************************************) (* NaturalDeductionCategory: *) (* *) -(* Natural Deduction proofs form a category (under mild assumptions, see below) *) +(* Natural Deduction proofs form a category *) (* *) (*********************************************************************************************************************************) @@ -14,14 +14,16 @@ Require Import Algebras_ch4. Require Import Categories_ch1_3. 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 MonoidalCategories_ch7_8. Require Import Coherence_ch7_8. +Require Import InitialTerminal_ch2_2. +Require Import BinoidalCategories. +Require Import PreMonoidalCategories. +Require Import MonoidalCategories_ch7_8. Open Scope nd_scope. Open Scope pf_scope. @@ -33,15 +35,10 @@ 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)) := + (* there is a category whose objects are judgments and whose morphisms are proofs *) + 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 @@ -51,126 +48,144 @@ Section Judgments_Category. | unfold Symmetric; intros; symmetry; auto | unfold Transitive; intros; transitivity y; auto ]. unfold Proper; unfold respectful; intros; simpl; apply ndr_comp_respects; auto. - intros; apply ndr_comp_left_identity. - intros; apply ndr_comp_right_identity. + intros; apply (ndr_builtfrom_structural f); auto. + intros; apply (ndr_builtfrom_structural f); auto. intros; apply ndr_comp_associativity. 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). - Definition Judgments_Category_monoidal_endofunctor_fmor : - forall a b, (a~~{Judgments_Category ×× Judgments_Category}~~>b) -> - ((Judgments_Category_monoidal_endofunctor_fobj a) - ~~{Judgments_Category}~~> - (Judgments_Category_monoidal_endofunctor_fobj b)). - intros. - destruct a. - destruct b. - destruct X. - exact (h**h0). - Defined. - Definition Judgments_Category_monoidal_endofunctor - : Functor (Judgments_Category ×× Judgments_Category) Judgments_Category Judgments_Category_monoidal_endofunctor_fobj. - refine {| fmor := Judgments_Category_monoidal_endofunctor_fmor |}; intros; simpl. - abstract (destruct a; destruct b; destruct f; destruct f'; auto; destruct H; simpl in *; apply ndr_prod_respects; auto). - abstract (destruct a; simpl in *; reflexivity). - abstract (destruct a; destruct b; destruct c; destruct f; destruct g; symmetry; simpl in *; apply ndr_prod_preserves_comp). + (* Judgments form a binoidal category *) + Instance jud_first (a:Judgments_Category) : Functor Judgments_Category Judgments_Category (fun x => x,,a) := + { fmor := fun b c (f:b /⋯⋯/ c) => f ** (nd_id a) }. + intros; unfold eqv; simpl; apply ndr_prod_respects; auto. + intros; unfold eqv in *; simpl in *; reflexivity. + intros; unfold eqv in *; simpl in *; apply (ndr_builtfrom_structural (nd_id a)); auto. + intros; unfold eqv in *; simpl in *. + setoid_rewrite <- ndr_prod_preserves_comp. + apply (ndr_builtfrom_structural (f;;g)); auto. Defined. - + Instance jud_second (a:Judgments_Category) : Functor Judgments_Category Judgments_Category (fun x => a,,x) := + { fmor := fun b c (f:b /⋯⋯/ c) => (nd_id a) ** f }. + intros; unfold eqv; simpl; apply ndr_prod_respects; auto. + intros; unfold eqv in *; simpl in *; reflexivity. + intros; unfold eqv in *; simpl in *; apply (ndr_builtfrom_structural (nd_id a)); auto. + intros; unfold eqv in *; simpl in *. + setoid_rewrite <- ndr_prod_preserves_comp. + apply (ndr_builtfrom_structural (f;;g)); auto. + Defined. + Instance Judgments_Category_binoidal : BinoidalCat Judgments_Category (@T_Branch (??Judgment)) := + { bin_first := jud_first + ; bin_second := jud_second }. + + (* and that category is commutative (all morphisms central) *) + Instance Judgments_Category_Commutative : CommutativeCat Judgments_Category_binoidal. + apply Build_CommutativeCat. + intros; apply Build_CentralMorphism; intros; unfold eqv; simpl in *. + setoid_rewrite <- (ndr_prod_preserves_comp (nd_id a) g f (nd_id d)). + setoid_rewrite <- (ndr_prod_preserves_comp f (nd_id _) (nd_id _) g). + setoid_rewrite ndr_comp_left_identity. + setoid_rewrite ndr_comp_right_identity. + reflexivity. + setoid_rewrite <- (ndr_prod_preserves_comp (nd_id _) f g (nd_id _)). + setoid_rewrite <- (ndr_prod_preserves_comp g (nd_id _) (nd_id _) f). + setoid_rewrite ndr_comp_left_identity. + setoid_rewrite ndr_comp_right_identity. + reflexivity. + Defined. + + (* Judgments form a premonoidal category *) 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 |}. + unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural nd_id0); auto. + unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural nd_id0); 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 |}; + unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural nd_id0); 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 |}; + unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural nd_id0); 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. + Instance jud_mon_cancelr : jud_first [] <~~~> functor_id Judgments_Category := + { ni_iso := jud_cancelr_iso }. + intros; unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural f); 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. + Instance jud_mon_cancell : jud_second [] <~~~> functor_id Judgments_Category := + { ni_iso := jud_cancell_iso }. + intros; unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural f); 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. - intros. - destruct X as [a c]. - destruct a as [a b]. - apply (jud_assoc_iso a b c). + Instance jud_mon_assoc : forall a b, a ⋊- >>>> - ⋉b <~~~> - ⋉b >>>> a ⋊- := + { ni_iso := fun c => jud_assoc_iso a c b }. + intros; unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural f); auto. Defined. - Definition jud_mon_assoc : - ((Judgments_Category_monoidal_endofunctor **** (functor_id _)) >>>> Judgments_Category_monoidal_endofunctor) - <~~~> - func_cossa >>>> ((((functor_id _) **** Judgments_Category_monoidal_endofunctor) >>>> Judgments_Category_monoidal_endofunctor)). - refine {| ni_iso := jud_mon_assoc_iso |}. + Instance jud_mon_assoc_rr : forall a b, - ⋉(a ⊗ b) <~~~> - ⋉a >>>> - ⋉b. 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. - setoid_rewrite ndr_prod_associativity. - setoid_rewrite ndr_comp_associativity. - 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. + apply ni_inv. + refine {| ni_iso := fun c => (jud_assoc_iso _ _ _) |}. + intros; unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural f); 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. + Instance jud_mon_assoc_ll : forall a b, (a ⊗ b) ⋊- <~~~> b ⋊- >>>> a ⋊- := + { ni_iso := fun c => jud_assoc_iso _ _ _ }. + intros; unfold eqv; unfold comp; simpl; apply (ndr_builtfrom_structural f); 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_premonoidal : PreMonoidalCat Judgments_Category_binoidal [] := + { pmon_cancelr := jud_mon_cancelr + ; pmon_cancell := jud_mon_cancell + ; pmon_assoc := jud_mon_assoc + ; pmon_assoc_rr := jud_mon_assoc_rr + ; 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 10. + unfold functor_fobj; unfold fmor; simpl; + 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. + intros; unfold eqv; simpl; apply Judgments_Category_Commutative. + intros; unfold eqv; simpl; apply Judgments_Category_Commutative. + Defined. + + (* commutative premonoidal categories are monoidal *) + Instance Judgments_Category_monoidal : MonoidalCat Judgments_Category_premonoidal := + { mon_commutative := Judgments_Category_Commutative }. + + (* Judgments also happens to have a terminal object - the empty list of judgments *) + Instance Judgments_Category_Terminal : TerminalObject Judgments_Category []. + refine {| drop := nd_weak ; drop_unique := _ |}. + abstract (intros; unfold eqv; simpl; apply ndr_void_proofs_irrelevant). + Defined. - - (* Structure ExpressionAlgebra (sig:Signature) := *) + (* Judgments is also a diagonal category via nd_copy *) + Instance Judgments_Category_Diagonal : DiagonalCat Judgments_Category_monoidal. + intros. + refine {| copy := nd_copy |}; intros; simpl. + setoid_rewrite ndr_comp_associativity. + setoid_rewrite <- (ndr_prod_preserves_copy f). + apply ndr_comp_respects; try reflexivity. + etransitivity. + symmetry. + apply ndr_prod_preserves_comp. + setoid_rewrite ndr_comp_left_identity. + setoid_rewrite ndr_comp_right_identity. + reflexivity. + setoid_rewrite ndr_comp_associativity. + setoid_rewrite <- (ndr_prod_preserves_copy f). + apply ndr_comp_respects; try reflexivity. + etransitivity. + symmetry. + apply ndr_prod_preserves_comp. + setoid_rewrite ndr_comp_left_identity. + setoid_rewrite ndr_comp_right_identity. + reflexivity. + Defined. + + (* Judgments is a cartesian category: it has a terminal object, diagonal morphisms, and the right naturalities *) + Instance Judgments_Category_CartesianCat : CartesianCat Judgments_Category_monoidal := + { car_terminal := Judgments_Category_Terminal ; car_diagonal := Judgments_Category_Diagonal }. + intros; unfold eqv; simpl; symmetry; apply ndr_copy_then_weak_left. + intros; unfold eqv; simpl; symmetry; apply ndr_copy_then_weak_right. + Defined. End Judgments_Category.