From 2e2cdd77d4c1ed9ecb1793f9499079cfd6d999f2 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Fri, 25 Mar 2011 11:16:24 -0700 Subject: [PATCH] ProgrammingLanguage: significant cleanups --- src/ProgrammingLanguage.v | 598 ++++++++++++--------------------------------- 1 file changed, 163 insertions(+), 435 deletions(-) diff --git a/src/ProgrammingLanguage.v b/src/ProgrammingLanguage.v index 073dfef..d1a0875 100644 --- a/src/ProgrammingLanguage.v +++ b/src/ProgrammingLanguage.v @@ -1,7 +1,7 @@ (*********************************************************************************************************************************) -(* NaturalDeduction: *) +(* ProgrammingLanguage *) (* *) -(* Structurally explicit natural deduction proofs. *) +(* Basic assumptions about programming languages . *) (* *) (*********************************************************************************************************************************) @@ -22,23 +22,31 @@ Require Import Coherence_ch7_8. Require Import Enrichment_ch2_8. Require Import RepresentableStructure_ch7_2. Require Import NaturalDeduction. +Require Import NaturalDeductionCategory. +Require Import Reification. +Require Import FreydCategories. +Require Import InitialTerminal_ch2_2. +Require Import FunctorCategories_ch7_7. +Require Import GeneralizedArrowFromReification. +Require Import GeneralizedArrow. (* * Everything in the rest of this section is just groundwork meant to - * build up to the definition of the AcceptableLanguage class, which + * build up to the definition of the ProgrammingLanguage class, which * appears at the end of the section. References to "the instance" * mean instances of that class. Think of this section as being one * big Class { ... } definition, except that we declare most of the * stuff outside the curly brackets in order to take advantage of * Coq's section mechanism. *) -Section Acceptable_Language. +Section Programming_Language. (* Formalized Definition 4.1.1, production $\tau$ *) Context {T : Type}. (* types of the language *) - Inductive Sequent := sequent : Tree ??T -> Tree ??T -> Sequent. + Context (Judg : Type). + Context (sequent : Tree ??T -> Tree ??T -> Judg). Notation "cs |= ss" := (sequent cs ss) : al_scope. (* Because of term irrelevance we need only store the *erased* (def * 4.4) trees; for this reason there is no Coq type directly @@ -47,7 +55,7 @@ Section Acceptable_Language. (* to do: sequent calculus equals natural deduction over sequents, theorem equals sequent with null antecedent, *) - Context {Rule : Tree ??Sequent -> Tree ??Sequent -> Type}. + Context {Rule : Tree ??Judg -> Tree ??Judg -> Type}. Notation "H /⋯⋯/ C" := (ND Rule H C) : al_scope. @@ -73,10 +81,10 @@ Section Acceptable_Language. * * This also means that we don't need an explicit proof obligation for 4.1.2. *) - Class AcceptableLanguage := + Class ProgrammingLanguage := (* Formalized Definition 4.1: denotational semantics equivalence relation on the conclusions of proofs *) - { al_eqv : @ND_Relation Sequent Rule + { al_eqv : @ND_Relation Judg Rule where "pf1 === pf2" := (@ndr_eqv _ _ al_eqv _ _ pf1 pf2) (* Formalized Definition 4.1.3; note that t here is either $\top$ or a single type, not a Tree of types; @@ -149,8 +157,8 @@ Section Acceptable_Language. ((nd_id1 (a|=b)) ** (al_subst b c d) ;; (al_subst a b d)) - ; al_subst_left_identity : forall `(pf:h/⋯⋯/[t1|=t2]), nd_llecnac;;(( [#al_reflexive_seq t1#]**pf);; al_subst _ _ _) === pf - ; al_subst_right_identity : forall `(pf:h/⋯⋯/[t1|=t2]), nd_rlecnac;;((pf**[#al_reflexive_seq t2#] );; al_subst _ _ _) === pf + ; al_subst_left_identity : forall a b, (( [#al_reflexive_seq a#]**(nd_id _));; al_subst _ _ b) === nd_cancell + ; al_subst_right_identity : forall a b, (((nd_id _)**[#al_reflexive_seq a#] );; al_subst b _ _) === nd_cancelr ; al_subst_commutes_with_horiz_expand_left : forall a b c d, [#al_horiz_expand_left d#] ** [#al_horiz_expand_left d#];; al_subst (d,, a) (d,, b) (d,, c) === al_subst a b c;; [#al_horiz_expand_left d#] @@ -175,8 +183,8 @@ Section Acceptable_Language. Notation "pf1 === pf2" := (@ndr_eqv _ _ al_eqv _ _ pf1 pf2) : temporary_scope3. Open Scope temporary_scope3. - Lemma al_subst_respects : - forall {AL:AcceptableLanguage}{a b c}, + Lemma al_subst_respects {PL:ProgrammingLanguage} : + forall {a b c}, forall (f : [] /⋯⋯/ [a |= b]) (f' : [] /⋯⋯/ [a |= b]) @@ -191,47 +199,158 @@ Section Acceptable_Language. reflexivity. Defined. - (* a contextually closed language *) - (* - Class ContextuallyClosedAcceptableLanguage := - { ccal_al : AcceptableLanguage - ; ccal_contextual_closure_operator : Tree ??T -> Tree ??T -> Tree ??T - where "a -~- b" := (ccal_contextual_closure_operator a b) - ; ccal_contextual_closure : forall {a b c d}(f:[a|=b]/⋯⋯/[c|=d]), [[]|=a-~-b]/⋯⋯/[[]|=c-~-d] - ; ccal_contextual_closure_respects : forall {a b c d}(f f':[a|=b]/⋯⋯/[c|=d]), - f===f' -> (ccal_contextual_closure f)===(ccal_contextual_closure f') - ; ccal_contextual_closure_preserves_comp : forall {a b c d e f}(f':[a|=b]/⋯⋯/[c|=d])(g':[c|=d]/⋯⋯/[e|=f]), - (ccal_contextual_closure f');;(ccal_contextual_closure g') === (ccal_contextual_closure (f';;g')) - ; ccal_contextual_closure_preserves_id : forall {a b}, ccal_contextual_closure (nd_id [a|=b]) === nd_id [[]|=a-~-b] - }. - Coercion ccal_al : ContextuallyClosedAcceptableLanguage >-> AcceptableLanguage. - *) - (* languages with unrestricted substructural rules (like that of Section 5) additionally implement this class *) - Class AcceptableLanguageWithUnrestrictedSubstructuralRules := - { alwusr_al :> AcceptableLanguage + Class ProgrammingLanguageWithUnrestrictedSubstructuralRules := + { alwusr_al :> ProgrammingLanguage ; al_contr : forall a b, Rule [a,,a |= b ] [ a |= b] ; al_exch : forall a b c, Rule [a,,b |= c ] [(b,,a)|= c] ; al_weak : forall a b, Rule [[] |= b ] [ a |= b] }. - Coercion alwusr_al : AcceptableLanguageWithUnrestrictedSubstructuralRules >-> AcceptableLanguage. + Coercion alwusr_al : ProgrammingLanguageWithUnrestrictedSubstructuralRules >-> ProgrammingLanguage. (* languages with a fixpoint operator *) - Class AcceptableLanguageWithFixpointOperator `(al:AcceptableLanguage) := + Class ProgrammingLanguageWithFixpointOperator `(al:ProgrammingLanguage) := { alwfpo_al := al ; al_fix : forall a b x, Rule [a,,x |= b,,x] [a |= b] }. - Coercion alwfpo_al : AcceptableLanguageWithFixpointOperator >-> AcceptableLanguage. + Coercion alwfpo_al : ProgrammingLanguageWithFixpointOperator >-> ProgrammingLanguage. + + Section LanguageCategory. + + Context (PL:ProgrammingLanguage). + + (* category of judgments in a fixed type/coercion context *) + Definition JudgmentsL :=@Judgments_Category_monoidal _ Rule al_eqv. + + Definition identityProof t : [] ~~{JudgmentsL}~~> [t |= t]. + unfold hom; simpl. + apply nd_rule. + apply al_reflexive_seq. + Defined. + + Definition cutProof a b c : [a |= b],,[b |= c] ~~{JudgmentsL}~~> [a |= c]. + unfold hom; simpl. + apply al_subst. + Defined. + + Definition TypesLFC : ECategory JudgmentsL (Tree ??T) (fun x y => [x|=y]). + refine + {| eid := identityProof + ; ecomp := cutProof + |}; intros. + apply MonoidalCat_all_central. + apply MonoidalCat_all_central. + unfold identityProof; unfold cutProof; simpl. + apply al_subst_left_identity. + unfold identityProof; unfold cutProof; simpl. + apply al_subst_right_identity. + unfold identityProof; unfold cutProof; simpl. + apply al_subst_associativity'. + Defined. + + Definition TypesLEnrichedInJudgments0 : Enrichment. + refine {| enr_c := TypesLFC |}. + Defined. + + Definition TypesL_first c : EFunctor TypesLFC TypesLFC (fun x => x,,c ). +(* + eapply Build_EFunctor; intros. + eapply MonoidalCat_all_central. + unfold eqv. + simpl. +*) + admit. + Defined. + + Definition TypesL_second c : EFunctor TypesLFC TypesLFC (fun x => c,,x ). + admit. + Defined. + + Definition TypesL_binoidal : BinoidalCat TypesLFC (@T_Branch _). + refine + {| bin_first := TypesL_first + ; bin_second := TypesL_second + |}. + Defined. + + Definition Pairing : prod_obj TypesL_binoidal TypesL_binoidal -> TypesL_binoidal. + admit. + Defined. + Definition Pairing_Functor : Functor (TypesL_binoidal ×× TypesL_binoidal) TypesL_binoidal Pairing. + admit. + Defined. + Definition TypesL : MonoidalCat TypesL_binoidal Pairing Pairing_Functor []. + admit. + Defined. + + Definition TypesLEnrichedInJudgments1 : SurjectiveEnrichment. + refine {| se_enr := TypesLEnrichedInJudgments0 |}. + simpl. + admit. + Defined. + + Definition TypesLEnrichedInJudgments2 : MonoidalEnrichment. + refine {| me_enr := TypesLEnrichedInJudgments0 ; me_mon := TypesL |}. + simpl. + admit. + Defined. + + Definition TypesLEnrichedInJudgments3 : MonicMonoidalEnrichment. + refine {| ffme_enr := TypesLEnrichedInJudgments2 |}; simpl. + admit. + admit. + admit. + Defined. + + End LanguageCategory. + + (* + Definition ArrowInProgrammingLanguage (L:ProgrammingLanguage)(tc:Terminal (TypesL L)) := + FreydCategory (TypesL L) (TypesL L). + *) + + Definition TwoLevelLanguage (L1 L2:ProgrammingLanguage) := + Reification (TypesLEnrichedInJudgments1 L1) (TypesLEnrichedInJudgments3 L2) (me_i (TypesLEnrichedInJudgments3 L2)). + + Inductive NLevelLanguage : nat -> ProgrammingLanguage -> Type := + | NLevelLanguage_zero : forall lang, NLevelLanguage O lang + | NLevelLanguage_succ : forall L1 L2 n, TwoLevelLanguage L1 L2 -> NLevelLanguage n L1 -> NLevelLanguage (S n) L2. + + Definition OmegaLevelLanguage (PL:ProgrammingLanguage) : Type := + forall n:nat, NLevelLanguage n PL. + Section TwoLevelLanguage. + Context `(L12:TwoLevelLanguage L1 L2). + + Definition FlatObject (x:TypesL L2) := + forall y1 y2, not ((reification_r_obj L12 y1 y2)=x). + + Definition FlatSubCategory := FullSubcategory (TypesL L2) FlatObject. + + Context `(retraction :@Functor _ _ (TypesL L2) _ _ FlatSubCategory retract_obj). + Context `(retraction_inv :@Functor _ _ FlatSubCategory _ _ (TypesL L2) retract_inv_obj). + Context (retraction_works:retraction >>>> retraction_inv ~~~~ functor_id _). + + Definition FlatteningOfReification := + (garrow_from_reification (TypesLEnrichedInJudgments1 L1) (TypesLEnrichedInJudgments3 L2) L12) >>>> retraction. + + Lemma FlatteningIsNotDestructive : + FlatteningOfReification >>>> retraction_inv >>>> RepresentableFunctor _ (me_i (TypesLEnrichedInJudgments3 L2)) ~~~~ L12. + admit. + Qed. + + End TwoLevelLanguage. + Close Scope temporary_scope3. Close Scope al_scope. Close Scope nd_scope. Close Scope pf_scope. -End Acceptable_Language. +End Programming_Language. Implicit Arguments ND [ Judgment ]. +(* Open Scope nd_scope. Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_suc_right T Rule AL a b c d e) with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv))) @@ -257,27 +376,27 @@ Close Scope nd_scope. Notation "cs |= ss" := (@sequent _ cs ss) : al_scope. (* -Definition mapSequent {T R:Type}(f:Tree ??T -> Tree ??R)(seq:@Sequent T) : @Sequent R := +Definition mapJudg {T R:Type}(f:Tree ??T -> Tree ??R)(seq:@Judg T) : @Judg R := match seq with sequentpair a b => pair (f a) (f b) end. -Implicit Arguments Sequent [ ]. +Implicit Arguments Judg [ ]. *) (* proofs which are generic and apply to any acceptable langauge (most of section 4) *) -Section Acceptable_Language_Facts. +Section Programming_Language_Facts. (* the ambient language about which we are proving facts *) - Context `(Lang : @AcceptableLanguage T Rule). + Context `(Lang : @ProgrammingLanguage T Rule). (* just for this section *) Open Scope nd_scope. Open Scope al_scope. Open Scope pf_scope. - Notation "H /⋯⋯/ C" := (@ND Sequent Rule H C) : temporary_scope4. + Notation "H /⋯⋯/ C" := (@ND Judg Rule H C) : temporary_scope4. Notation "a === b" := (@ndr_eqv _ _ al_eqv _ _ a b) : temporary_scope4. Open Scope temporary_scope4. - Definition lang_al_eqv := al_eqv(AcceptableLanguage:=Lang). + Definition lang_al_eqv := al_eqv(ProgrammingLanguage:=Lang). Existing Instance lang_al_eqv. Ltac distribute := @@ -363,404 +482,13 @@ Section Acceptable_Language_Facts. admit. Qed. - (* Formalized Definition 4.6 *) - Section Types1. - Instance Types1 : Category T (fun t1 t2 => [ ] /⋯⋯/ [ [t1] |= [t2] ]) := - { eqv := fun ta tb pf1 pf2 => pf1 === pf2 - ; id := fun t => [#al_reflexive_seq [t]#] - ; comp := fun {ta tb tc:T}(pf1:[]/⋯⋯/[[ta]|=[tb]])(pf2:[]/⋯⋯/[[tb]|=[tc]]) => nd_llecnac ;; ((pf1 ** pf2) ;; (al_subst _ _ _)) - }. - intros; apply Build_Equivalence; - [ unfold Reflexive; intros; reflexivity - | unfold Symmetric; intros; symmetry; auto - | unfold Transitive; intros; transitivity y; auto ]. - unfold Proper; unfold respectful; intros; simpl. - apply ndr_comp_respects. reflexivity. - apply al_subst_respects; auto. - intros; simpl. apply al_subst_left_identity. - intros; simpl. - assert (@nd_llecnac _ Rule [] === @nd_rlecnac _ _ []). - apply ndr_structural_indistinguishable; auto. - setoid_rewrite H. - apply al_subst_right_identity. - intros; apply al_subst_associativity''. - Defined. - End Types1. - - (* Formalized Definition 4.10 *) - Instance Judgments : Category (Tree ??Sequent) (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 - }. - intros; apply Build_Equivalence; - [ unfold Reflexive; intros; reflexivity - | 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_comp_associativity. - Defined. - - (* a "primitive" proof has exactly one hypothesis and one conclusion *) - Inductive IsPrimitive : forall (h_:Tree ??(@Sequent T)), Type := - isPrimitive : forall h, IsPrimitive [h]. - Hint Constructors IsPrimitive. - Instance IsPrimitiveSubCategory : SubCategory Judgments IsPrimitive (fun _ _ _ _ _ => True). - apply Build_SubCategory; intros; auto. - Defined. - - (* The primitive judgments form a subcategory; nearly all of the - * functors we build that go into Judgments will factor through the - * inclusion functor for this subcategory. Explicitly constructing - * it makes the formalization easier, but distracts from what's - * actually going on (from an expository perspective) *) - Definition PrimitiveJudgments := SubCategoriesAreCategories Judgments IsPrimitiveSubCategory. - Definition PrimitiveInclusion := InclusionFunctor Judgments IsPrimitiveSubCategory. - - Section Types0. - Inductive IsNil : Tree ??(@Sequent T) -> Prop := isnil : IsNil []. - Inductive IsClosed : Tree ??(@Sequent T) -> Prop := isclosed:forall t, IsClosed [[]|=[t]]. - Inductive IsIdentity : forall h c, (h /⋯⋯/ c) -> Prop := - | isidentity0 : forall t, IsIdentity t t (nd_id t) - | isidentity1 : forall t pf1 pf2, IsIdentity t t pf1 -> IsIdentity t t pf2 -> IsIdentity t t (pf1 ;; pf2). - Inductive IsInTypes0 (h c:Tree ??Sequent)(pf:h /⋯⋯/ c) : Prop := - | iit0_id0 : IsNil h -> IsNil c -> IsIdentity _ _ pf -> IsInTypes0 _ _ pf - | iit0_id1 : @IsClosed h -> @IsClosed c -> IsIdentity _ _ pf -> IsInTypes0 _ _ pf - | iit0_term : IsNil h -> @IsClosed c -> IsInTypes0 _ _ pf. - Instance Types0P : SubCategory Judgments - (fun x:Judgments => IsInTypes0 _ _ (id(Category:=Judgments) x)) - (fun h c _ _ f => IsInTypes0 h c f). - intros. - apply Build_SubCategory; intros; simpl. - auto. - inversion H0. - inversion H1; subst. - inversion H2; subst. - inversion H; subst. inversion H4; subst. - apply iit0_id0; auto. apply isidentity1; auto. - inversion H5. - inversion H5. - inversion H1; subst. - inversion H2; subst. - inversion H3; subst. clear H8. clear H7. - inversion H; subst. inversion H5. - inversion H4; subst. - inversion H6; subst. - apply iit0_id1; auto. apply isidentity1; auto. - clear H10. clear H8. - apply iit0_id1; auto. apply isidentity1; auto. - inversion H4; subst. inversion H; subst. - inversion H8. - inversion H6. - apply iit0_term; auto. - clear H7; subst. - inversion H; subst. - inversion H4; subst. - apply iit0_term; auto. - inversion H4; subst. - inversion H7; subst. clear H14. - apply iit0_id1; auto. apply isidentity1; auto. - clear H13. - apply iit0_id1; auto. apply isidentity1; auto. - inversion H4; subst. - inversion H; subst. - inversion H10. - inversion H7. - apply iit0_term; auto. - inversion H1; subst. - inversion H; subst. - inversion H3; subst. apply iit0_term; auto. - inversion H4. - inversion H4. - Qed. - - (* Formalized Definition 4.8 *) - Definition Types0 := SubCategoriesAreCategories Judgments Types0P. - End Types0. - - (* Formalized Definition 4.11 *) - Instance Judgments_binoidal : BinoidalCat Judgments (fun a b:Tree ??Sequent => a,,b) := - { bin_first := fun x => @Build_Functor _ _ Judgments _ _ Judgments (fun a => a,,x) (fun a b (f:a/⋯⋯/b) => f**(nd_id x)) _ _ _ - ; bin_second := fun x => @Build_Functor _ _ Judgments _ _ Judgments (fun a => x,,a) (fun a b (f:a/⋯⋯/b) => (nd_id x)**f) _ _ _ - }. - intros. simpl. simpl in H. setoid_rewrite H. reflexivity. - intros. simpl. reflexivity. - intros. simpl. setoid_rewrite <- ndr_prod_preserves_comp. setoid_rewrite ndr_comp_left_identity. reflexivity. - intros. simpl. simpl in H. setoid_rewrite H. reflexivity. - intros. simpl. reflexivity. - intros. simpl. setoid_rewrite <- ndr_prod_preserves_comp. setoid_rewrite ndr_comp_left_identity. reflexivity. - Defined. - - Definition jud_assoc_iso (a b c:Judgments) : @Isomorphic _ _ Judgments ((a,,b),,c) (a,,(b,,c)). - apply (@Build_Isomorphic _ _ Judgments _ _ nd_assoc nd_cossa); simpl; auto. - Defined. - Definition jud_cancelr_iso (a:Judgments) : @Isomorphic _ _ Judgments (a,,[]) a. - apply (@Build_Isomorphic _ _ Judgments _ _ nd_cancelr nd_rlecnac); simpl; auto. - Defined. - Definition jud_cancell_iso (a:Judgments) : @Isomorphic _ _ Judgments ([],,a) a. - apply (@Build_Isomorphic _ _ Judgments _ _ nd_cancell nd_llecnac); simpl; auto. - Defined. - - (* just for this section *) - Notation "a ⊗ b" := (@bin_obj _ _ Judgments _ Judgments_binoidal a b). - Notation "c ⋊ -" := (@bin_second _ _ Judgments _ Judgments_binoidal c). - Notation "- ⋉ c" := (@bin_first _ _ Judgments _ Judgments_binoidal c). - Notation "c ⋊ f" := ((c ⋊ -) \ f). - Notation "g ⋉ c" := ((- ⋉ c) \ g). - - Hint Extern 1 => apply (@nd_structural_id0 _ Rule). - Hint Extern 1 => apply (@nd_structural_id1 _ Rule). - Hint Extern 1 => apply (@nd_structural_weak _ Rule). - Hint Extern 1 => apply (@nd_structural_copy _ Rule). - Hint Extern 1 => apply (@nd_structural_prod _ Rule). - Hint Extern 1 => apply (@nd_structural_comp _ Rule). - Hint Extern 1 => apply (@nd_structural_cancell _ Rule). - Hint Extern 1 => apply (@nd_structural_cancelr _ Rule). - Hint Extern 1 => apply (@nd_structural_llecnac _ Rule). - Hint Extern 1 => apply (@nd_structural_rlecnac _ Rule). - Hint Extern 1 => apply (@nd_structural_assoc _ Rule). - Hint Extern 1 => apply (@nd_structural_cossa _ Rule). - Hint Extern 2 => apply (@ndr_structural_indistinguishable _ Rule). - - Program Instance Judgments_premonoidal : PreMonoidalCat Judgments_binoidal [ ] := - { pmon_assoc := fun a b => @Build_NaturalIsomorphism _ _ _ _ _ _ _ _ _ _ (fun x => (jud_assoc_iso a x b)) _ - ; pmon_cancell := @Build_NaturalIsomorphism _ _ _ _ _ _ _ _ _ _ (fun x => (jud_cancell_iso x)) _ - ; pmon_cancelr := @Build_NaturalIsomorphism _ _ _ _ _ _ _ _ _ _ (fun x => (jud_cancelr_iso x)) _ - ; pmon_assoc_rr := fun a b => @Build_NaturalIsomorphism _ _ _ _ _ _ _ _ _ _ (fun x => (jud_assoc_iso x a b)⁻¹) _ - ; pmon_assoc_ll := fun a b => @Build_NaturalIsomorphism _ _ _ _ _ _ _ _ _ _ (fun x => jud_assoc_iso a b x) _ - }. - Next Obligation. - setoid_rewrite (ndr_prod_associativity (nd_id a) f (nd_id b)). - 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. - Next Obligation. - 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. - Next Obligation. - 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. - Next Obligation. - apply Build_Pentagon; intros. - simpl; apply ndr_structural_indistinguishable; auto. - Defined. - Next Obligation. - apply Build_Triangle; intros; - simpl; apply ndr_structural_indistinguishable; auto. - Defined. - Next Obligation. - setoid_rewrite (ndr_prod_associativity f (nd_id a) (nd_id b)). - repeat setoid_rewrite <- ndr_comp_associativity. - apply ndr_comp_respects; try reflexivity. - eapply transitivity; [ idtac | apply ndr_comp_left_identity ]. - apply ndr_comp_respects; try reflexivity; simpl; auto. - Defined. - Next Obligation. - setoid_rewrite (ndr_prod_associativity (nd_id a) (nd_id b) 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. - Check (@Judgments_premonoidal). (* to force Coq to verify that we've finished all the obligations *) - - Definition Judgments_monoidal_endofunctor_fobj : Judgments ×× Judgments -> Judgments := - (fun xy => - match xy with - | pair_obj x y => T_Branch x y - end). - Definition Judgments_monoidal_endofunctor_fmor : - forall a b, (a~~{Judgments ×× Judgments}~~>b) -> - ((Judgments_monoidal_endofunctor_fobj a)~~{Judgments}~~>(Judgments_monoidal_endofunctor_fobj b)). - intros. - destruct a. - destruct b. - destruct X. - exact (h**h0). - Defined. - Definition Judgments_monoidal_endofunctor : Functor (Judgments ×× Judgments) Judgments Judgments_monoidal_endofunctor_fobj. - refine {| fmor := Judgments_monoidal_endofunctor_fmor |}; intros; simpl. - abstract (destruct a; destruct b; destruct f; destruct f'; auto; destruct H; apply ndr_prod_respects; auto). - abstract (destruct a; simpl; reflexivity). - abstract (destruct a; destruct b; destruct c; destruct f; destruct g; symmetry; apply ndr_prod_preserves_comp). - Defined. - - Instance Judgments_monoidal : MonoidalCat _ _ Judgments_monoidal_endofunctor [ ]. - admit. - Defined. - - (* all morphisms in the category of Judgments are central; there's probably a very short route from here to CartesianCat *) - Lemma all_central : forall a b:Judgments, forall (f:a~>b), CentralMorphism f. - intros; apply Build_CentralMorphism; intros. - simpl. - setoid_rewrite <- (ndr_prod_preserves_comp f (nd_id _) (nd_id _) g). - setoid_rewrite <- (ndr_prod_preserves_comp (nd_id _) g f (nd_id _)). - setoid_rewrite ndr_comp_left_identity. - setoid_rewrite ndr_comp_right_identity. - reflexivity. - simpl. - setoid_rewrite <- (ndr_prod_preserves_comp g (nd_id _) (nd_id _) f). - setoid_rewrite <- (ndr_prod_preserves_comp (nd_id _) f g (nd_id _)). - setoid_rewrite ndr_comp_left_identity. - setoid_rewrite ndr_comp_right_identity. - reflexivity. - Defined. - - (* - Instance NoHigherOrderFunctionTypes : SubCategory Judgments - Instance NoFunctionTypes : SubCategory Judgments - Lemma first_order_functions_eliminable : IsomorphicCategories NoHigherOrderFunctionTypes NoFunctionTypes - *) - - (* Formalized Theorem 4.19 *) - Instance Types_omega_e : ECategory Judgments_monoidal (Tree ??T) (fun tt1 tt2 => [ tt1 |= tt2 ]) := - { eid := fun tt => [#al_reflexive_seq tt#] - ; ecomp := fun a b c => al_subst a b c - }. - admit. - admit. - admit. - admit. - admit. - Defined. - - Definition Types_omega_monoidal_functor - : Functor (Types_omega_e ×× Types_omega_e) Types_omega_e (fun a => match a with pair_obj a1 a2 => a1,,a2 end). - admit. - Defined. - - Instance Types_omega_monoidal : MonoidalCat Types_omega_e _ Types_omega_monoidal_functor []. - admit. - Defined. - - Definition AL_Enrichment : Enrichment. - refine {| enr_c := Types_omega_e |}. - Defined. - - Definition AL_SurjectiveEnrichment : SurjectiveEnrichment. - refine {| se_enr := AL_Enrichment |}. - unfold treeDecomposition. - intros; induction d; simpl. - destruct a. - destruct s. - exists [pair t t0]; auto. - exists []; auto. - destruct IHd1. - destruct IHd2. - exists (x,,x0); subst; auto. - Defined. - - Definition AL_MonoidalEnrichment : MonoidalEnrichment. - refine {| me_enr := AL_SurjectiveEnrichment ; me_mon := Types_omega_monoidal |}. - admit. - Defined. - - Definition AL_MonicMonoidalEnrichment : MonicMonoidalEnrichment. - refine {| ffme_enr := AL_MonoidalEnrichment |}. - admit. - admit. - admit. - Defined. - - (* - Instance Types_omega_be : BinoidalECategory Types_omega_e := - { bec_obj := fun tt1 tt2 => tt1,,tt2 - ; bec_efirst := fun a b c => nd_rule (@al_horiz_expand_right _ _ Lang _ _ _) - ; bec_esecond := fun a b c => nd_rule (@al_horiz_expand_left _ _ Lang _ _ _) - }. - intros; apply all_central. - intros; apply all_central. - intros. unfold eid. simpl. - setoid_rewrite <- al_horiz_expand_right_reflexive. - reflexivity. - intros. unfold eid. simpl. - setoid_rewrite <- al_horiz_expand_left_reflexive. - reflexivity. - intros. simpl. - set (@al_subst_commutes_with_horiz_expand_right _ _ _ a b c d) as q. - setoid_rewrite <- q. clear q. - apply ndr_comp_respects; try reflexivity. - distribute. - apply ndr_prod_respects. - eapply transitivity; [ idtac | apply ndr_comp_right_identity ]. - apply ndr_comp_respects; reflexivity. - eapply transitivity; [ idtac | apply ndr_comp_left_identity ]. - apply ndr_comp_respects; reflexivity. - intros. simpl. - set (@al_subst_commutes_with_horiz_expand_left _ _ _ a b c d) as q. - setoid_rewrite <- q. clear q. - apply ndr_comp_respects; try reflexivity. - distribute. - apply ndr_prod_respects. - eapply transitivity; [ idtac | apply ndr_comp_right_identity ]. - apply ndr_comp_respects; reflexivity. - eapply transitivity; [ idtac | apply ndr_comp_left_identity ]. - apply ndr_comp_respects; reflexivity. - Defined. - *) - - Definition Types_omega : Category _ (fun tt1 tt2 => [ ]/⋯⋯/[ tt1 |= tt2 ]) := Underlying Types_omega_e. - Existing Instance Types_omega. - - (* - Definition Types_omega_binoidal : BinoidalCat Types_omega (fun tt1 tt2 => tt1,,tt2) := Underlying_binoidal Types_omega_be. - Existing Instance Types_omega_binoidal. - *) - - (* takes an "operation in the context" (proof from [b|=Top]/⋯⋯/[a|=Top]) and turns it into a function a-->b; note the variance *) - Definition context_operation_as_function - : forall {a}{b} (f:[b|=[]]~~{Judgments}~~>[a|=[]]), []~~{Judgments}~~>[a|=b]. - intros. - apply (@al_vert_expand_suc_right _ _ _ b _ _) in f. - simpl in f. - apply (@al_vert_expand_ant_left _ _ _ [] _ _) in f. - simpl in f. - set ([#al_reflexive_seq _#] ;; f ;; [#al_ant_cancell#] ;; [#al_suc_cancell#]) as f'. - exact f'. - Defined. - - (* takes an "operation in the context" (proof from [Top|=a]/⋯⋯/[Top|=b]) and turns it into a function a-->b; note the variance *) - Definition cocontext_operation_as_function - : forall {a}{b} (f:[[]|=a]~~{Judgments}~~>[[]|=b]), []~~{Judgments}~~>[a|=b]. - intros. unfold hom. unfold hom in f. - apply al_vert_expand_ant_right with (x:=a) in f. - simpl in f. - apply al_vert_expand_suc_left with (x:=[]) in f. - simpl in f. - set ([#al_reflexive_seq _#] ;; f ;; [#al_ant_cancell#] ;; [#al_suc_cancell#]) as f'. - exact f'. - Defined. - - - Definition function_as_context_operation - : forall {a}{b}{c} (f:[]~~{Judgments}~~>[a|=b]), [b|=c]~~{Judgments}~~>[a|=c] - := fun a b c f => RepresentableFunctorºᑭ Types_omega_e c \ f. - Definition function_as_cocontext_operation - : forall {a}{b}{c} (f:[]/⋯⋯/[a|=b]), [c|=a]~~{Judgments}~~>[c|=b] - := fun a b c f => RepresentableFunctor Types_omega_e c \ f. - Close Scope temporary_scope4. Close Scope al_scope. Close Scope nd_scope. Close Scope pf_scope. Close Scope isomorphism_scope. -End Acceptable_Language_Facts. +End Programming_Language_Facts. -Coercion AL_SurjectiveEnrichment : AcceptableLanguage >-> SurjectiveEnrichment. -Coercion AL_MonicMonoidalEnrichment : AcceptableLanguage >-> MonicMonoidalEnrichment. +(*Coercion AL_SurjectiveEnrichment : ProgrammingLanguage >-> SurjectiveEnrichment.*) +(*Coercion AL_MonicMonoidalEnrichment : ProgrammingLanguage >-> MonicMonoidalEnrichment.*) +*) \ No newline at end of file -- 1.7.10.4