X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FProgrammingLanguage.v;h=933785af591887f446bc8a85fd9d556ae7ca4045;hp=d1a0875a6d5b2a8108544d999e0dacf25b635572;hb=64d416692bda1d36c33b5efa245d46dcf546ad4a;hpb=2e2cdd77d4c1ed9ecb1793f9499079cfd6d999f2 diff --git a/src/ProgrammingLanguage.v b/src/ProgrammingLanguage.v index d1a0875..933785a 100644 --- a/src/ProgrammingLanguage.v +++ b/src/ProgrammingLanguage.v @@ -1,7 +1,7 @@ (*********************************************************************************************************************************) (* ProgrammingLanguage *) (* *) -(* Basic assumptions about programming languages . *) +(* Basic assumptions about programming languages. *) (* *) (*********************************************************************************************************************************) @@ -9,6 +9,7 @@ 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. @@ -17,478 +18,277 @@ 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 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. +Require Import Enrichments. +Require Import NaturalDeduction. +Require Import NaturalDeductionCategory. -(* - * Everything in the rest of this section is just groundwork meant to - * 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 Programming_Language. - (* Formalized Definition 4.1.1, production $\tau$ *) Context {T : Type}. (* types of the language *) 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 - * corresponding to productions $e$ and $x$ of 4.1.1, and TreeOT can - * be used for productions $\Gamma$ and $\Sigma$ *) - - (* to do: sequent calculus equals natural deduction over sequents, theorem equals sequent with null antecedent, *) + Notation "cs |= ss" := (sequent cs ss) : pl_scope. Context {Rule : Tree ??Judg -> Tree ??Judg -> Type}. - Notation "H /⋯⋯/ C" := (ND Rule H C) : al_scope. + Notation "H /⋯⋯/ C" := (ND Rule H C) : pl_scope. Open Scope pf_scope. Open Scope nd_scope. - Open Scope al_scope. - - (* Formalized Definition 4.1 - * - * Note that from this abstract interface, the terms (expressions) - * in the proof are not accessible at all; they don't need to be -- - * so long as we have access to the equivalence relation upon - * proof-conclusions. Moreover, hiding the expressions actually - * makes the encoding in CiC work out easier for two reasons: - * - * 1. Because the denotation function is provided a proof rather - * than a term, it is a total function (the denotation function is - * often undefined for ill-typed terms). - * - * 2. We can define arr_composition of proofs without having to know how - * to compose expressions. The latter task is left up to the client - * function which extracts an expression from a completed proof. - * - * This also means that we don't need an explicit proof obligation for 4.1.2. - *) - Class ProgrammingLanguage := - - (* Formalized Definition 4.1: denotational semantics equivalence relation on the conclusions of proofs *) - { 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; - * we rely on "completeness of atomic initial segments" (http://en.wikipedia.org/wiki/Completeness_of_atomic_initial_sequents) - * to generate the rest *) - ; al_reflexive_seq : forall t, Rule [] [t|=t] - - (* these can all be absorbed into a separate "sequent calculus" presentation *) - ; al_ant_assoc : forall {a b c d}, Rule [(a,,b),,c|=d] [(a,,(b,,c))|=d] - ; al_ant_cossa : forall {a b c d}, Rule [a,,(b,,c)|=d] [((a,,b),,c)|=d] - ; al_ant_cancell : forall {a b }, Rule [ [],,a |=b] [ a |=b] - ; al_ant_cancelr : forall {a b }, Rule [a,,[] |=b] [ a |=b] - ; al_ant_llecnac : forall {a b }, Rule [ a |=b] [ [],,a |=b] - ; al_ant_rlecnac : forall {a b }, Rule [ a |=b] [ a,,[] |=b] - ; al_suc_assoc : forall {a b c d}, Rule [d|=(a,,b),,c] [d|=(a,,(b,,c))] - ; al_suc_cossa : forall {a b c d}, Rule [d|=a,,(b,,c)] [d|=((a,,b),,c)] - ; al_suc_cancell : forall {a b }, Rule [a|=[],,b ] [a|= b ] - ; al_suc_cancelr : forall {a b }, Rule [a|=b,,[] ] [a|= b ] - ; al_suc_llecnac : forall {a b }, Rule [a|= b ] [a|=[],,b ] - ; al_suc_rlecnac : forall {a b }, Rule [a|= b ] [a|=b,,[] ] - - ; al_horiz_expand_left : forall tau {Gamma Sigma}, Rule [ Gamma |= Sigma ] [tau,,Gamma|=tau,,Sigma] - ; al_horiz_expand_right : forall tau {Gamma Sigma}, Rule [ Gamma |= Sigma ] [Gamma,,tau|=Sigma,,tau] - - (* these are essentially one way of formalizing - * "completeness of atomic initial segments" (http://en.wikipedia.org/wiki/Completeness_of_atomic_initial_sequents) *) - ; al_horiz_expand_left_reflexive : forall a b, [#al_reflexive_seq b#];;[#al_horiz_expand_left a#]===[#al_reflexive_seq (a,,b)#] - ; al_horiz_expand_right_reflexive : forall a b, [#al_reflexive_seq a#];;[#al_horiz_expand_right b#]===[#al_reflexive_seq (a,,b)#] - ; al_horiz_expand_right_then_cancel : forall a, - ((([#al_reflexive_seq (a,, [])#] ;; [#al_ant_cancelr#]);; [#al_suc_cancelr#]) === [#al_reflexive_seq a#]) - - ; al_vert_expand_ant_left : forall x `(pf:[a|=b]/⋯⋯/[c|=d]), [x,,a |= b ]/⋯⋯/[x,,c |= d ] - ; al_vert_expand_ant_right : forall x `(pf:[a|=b]/⋯⋯/[c|=d]), [ a,,x|= b ]/⋯⋯/[ c,,x|= d ] - ; al_vert_expand_suc_left : forall x `(pf:[a|=b]/⋯⋯/[c|=d]), [ a |=x,,b ]/⋯⋯/[ c |=x,,d ] - ; al_vert_expand_suc_right : forall x `(pf:[a|=b]/⋯⋯/[c|=d]), [ a |= b,,x]/⋯⋯/[ c |= d,,x] - ; al_vert_expand_ant_l_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]), - f===g -> al_vert_expand_ant_left x f === al_vert_expand_ant_left x g - ; al_vert_expand_ant_r_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]), - f===g -> al_vert_expand_ant_right x f === al_vert_expand_ant_right x g - ; al_vert_expand_suc_l_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]), - f===g -> al_vert_expand_suc_left x f === al_vert_expand_suc_left x g - ; al_vert_expand_suc_r_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]), - f===g -> al_vert_expand_suc_right x f === al_vert_expand_suc_right x g - ; al_vert_expand_ant_l_preserves_id : forall x a b, al_vert_expand_ant_left x (nd_id [a|=b]) === nd_id [x,,a|=b] - ; al_vert_expand_ant_r_preserves_id : forall x a b, al_vert_expand_ant_right x (nd_id [a|=b]) === nd_id [a,,x|=b] - ; al_vert_expand_suc_l_preserves_id : forall x a b, al_vert_expand_suc_left x (nd_id [a|=b]) === nd_id [a|=x,,b] - ; al_vert_expand_suc_r_preserves_id : forall x a b, al_vert_expand_suc_right x (nd_id [a|=b]) === nd_id [a|=b,,x] - ; al_vert_expand_ant_l_preserves_comp : forall x a b c d e f (h:[a|=b]/⋯⋯/[c|=d])(g:[c|=d]/⋯⋯/[e|=f]), - (al_vert_expand_ant_left x (h;;g)) === (al_vert_expand_ant_left x h);;(al_vert_expand_ant_left x g) - ; al_vert_expand_ant_r_preserves_comp : forall x a b c d e f (h:[a|=b]/⋯⋯/[c|=d])(g:[c|=d]/⋯⋯/[e|=f]), - (al_vert_expand_ant_right x (h;;g)) === (al_vert_expand_ant_right x h);;(al_vert_expand_ant_right x g) - ; al_vert_expand_suc_l_preserves_comp : forall x a b c d e f (h:[a|=b]/⋯⋯/[c|=d])(g:[c|=d]/⋯⋯/[e|=f]), - (al_vert_expand_suc_left x (h;;g)) === (al_vert_expand_suc_left x h);;(al_vert_expand_suc_left x g) - ; al_vert_expand_suc_r_preserves_comp : forall x a b c d e f (h:[a|=b]/⋯⋯/[c|=d])(g:[c|=d]/⋯⋯/[e|=f]), - (al_vert_expand_suc_right x (h;;g)) === (al_vert_expand_suc_right x h);;(al_vert_expand_suc_right x g) - - ; al_subst : forall a b c, [ a |= b ] ,, [ b |= c ] /⋯⋯/ [ a |= c ] - ; al_subst_associativity : forall {a b c d}, - ((al_subst a b c) ** (nd_id1 (c|=d))) ;; - (al_subst a c d) - === - nd_assoc ;; - ((nd_id1 (a|=b)) ** (al_subst b c d) ;; - (al_subst a b d)) - ; al_subst_associativity' : forall {a b c d}, - nd_cossa ;; - ((al_subst a b c) ** (nd_id1 (c|=d))) ;; - (al_subst a c d) - === - ((nd_id1 (a|=b)) ** (al_subst b c d) ;; - (al_subst a b d)) - - ; 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#] - ; al_subst_commutes_with_horiz_expand_right : forall a b c d, - [#al_horiz_expand_right d#] ** [#al_horiz_expand_right d#] ;; al_subst (a,, d) (b,, d) (c,, d) - === al_subst a b c;; [#al_horiz_expand_right d#] - ; al_subst_commutes_with_vertical_expansion : forall t0 t1 t2, forall (f:[[]|=t1]/⋯⋯/[[]|=t0])(g:[[]|=t0]/⋯⋯/[[]|=t2]), - (((nd_rlecnac;; - ((([#al_reflexive_seq (t1,, [])#];; al_vert_expand_ant_left t1 (al_vert_expand_suc_right [] f));; - (nd_rule al_ant_cancelr));; (nd_rule al_suc_cancelr)) ** nd_id0);; - (nd_id [t1 |= t0]) ** - ((([#al_reflexive_seq (t0,, [])#];; al_vert_expand_ant_left t0 (al_vert_expand_suc_right [] g));; - (nd_rule al_ant_cancelr));; (nd_rule al_suc_cancelr)));; - al_subst t1 t0 t2) - === - ((([#al_reflexive_seq (t1,, [])#];; - (al_vert_expand_ant_left t1 (al_vert_expand_suc_right [] f);; - al_vert_expand_ant_left t1 (al_vert_expand_suc_right [] g)));; - (nd_rule al_ant_cancelr));; (nd_rule al_suc_cancelr)) - }. + Open Scope pl_scope. - Notation "pf1 === pf2" := (@ndr_eqv _ _ al_eqv _ _ pf1 pf2) : temporary_scope3. - Open Scope temporary_scope3. - - Lemma al_subst_respects {PL:ProgrammingLanguage} : - forall {a b c}, - forall - (f : [] /⋯⋯/ [a |= b]) - (f' : [] /⋯⋯/ [a |= b]) - (g : [] /⋯⋯/ [b |= c]) - (g' : [] /⋯⋯/ [b |= c]), - (f === f') -> - (g === g') -> - (f ** g;; al_subst _ _ _) === (f' ** g';; al_subst _ _ _). - intros. - setoid_rewrite H. - setoid_rewrite H0. - reflexivity. - Defined. - - (* languages with unrestricted substructural rules (like that of Section 5) additionally implement this class *) - 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 : ProgrammingLanguageWithUnrestrictedSubstructuralRules >-> ProgrammingLanguage. - - (* languages with a fixpoint operator *) - Class ProgrammingLanguageWithFixpointOperator `(al:ProgrammingLanguage) := - { alwfpo_al := al - ; al_fix : forall a b x, Rule [a,,x |= b,,x] [a |= b] + Class ProgrammingLanguage := + { pl_eqv0 : @ND_Relation Judg Rule + ; pl_snd :> @SequentND Judg Rule _ sequent + ; pl_cnd :> @ContextND Judg Rule T sequent pl_snd + ; pl_eqv1 :> @SequentND_Relation Judg Rule _ sequent pl_snd pl_eqv0 + ; pl_eqv :> @ContextND_Relation Judg Rule _ sequent pl_snd pl_cnd pl_eqv0 pl_eqv1 }. - Coercion alwfpo_al : ProgrammingLanguageWithFixpointOperator >-> ProgrammingLanguage. + 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 JudgmentsL :=@Judgments_Category_monoidal _ Rule al_eqv. + Definition Judgments_cartesian := @Judgments_Category_CartesianCat _ Rule pl_eqv. + + Definition JudgmentsL := Judgments_cartesian. Definition identityProof t : [] ~~{JudgmentsL}~~> [t |= t]. unfold hom; simpl. - apply nd_rule. - apply al_reflexive_seq. + apply snd_initial. Defined. Definition cutProof a b c : [a |= b],,[b |= c] ~~{JudgmentsL}~~> [a |= c]. unfold hom; simpl. - apply al_subst. + apply snd_cut. Defined. - Definition TypesLFC : ECategory JudgmentsL (Tree ??T) (fun x y => [x|=y]). + Existing Instance pl_eqv. + + Definition TypesL : 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'. + 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. - Definition TypesLEnrichedInJudgments0 : Enrichment. - refine {| enr_c := TypesLFC |}. + 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. - 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. + 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 TypesL_binoidal : BinoidalCat TypesLFC (@T_Branch _). + Definition Types_binoidal : EBinoidalCat TypesL. refine - {| bin_first := TypesL_first - ; bin_second := TypesL_second + {| ebc_first := Types_first + ; ebc_second := Types_second |}. Defined. - Definition Pairing : prod_obj TypesL_binoidal TypesL_binoidal -> TypesL_binoidal. - admit. + 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. - Definition Pairing_Functor : Functor (TypesL_binoidal ×× TypesL_binoidal) TypesL_binoidal Pairing. - admit. + + 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. - Definition TypesL : MonoidalCat TypesL_binoidal Pairing Pairing_Functor []. + + 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; unfold eqv; simpl. admit. Defined. - Definition TypesLEnrichedInJudgments1 : SurjectiveEnrichment. - refine {| se_enr := TypesLEnrichedInJudgments0 |}. - simpl. + Instance Types_cancelr : Types_first [] <~~~> functor_id _ := + { ni_iso := Types_cancelr_iso }. + intros; simpl. admit. Defined. - Definition TypesLEnrichedInJudgments2 : MonoidalEnrichment. - refine {| me_enr := TypesLEnrichedInJudgments0 ; me_mon := TypesL |}. - simpl. + Instance Types_cancell : Types_second [] <~~~> functor_id _ := + { ni_iso := Types_cancell_iso }. admit. Defined. - Definition TypesLEnrichedInJudgments3 : MonicMonoidalEnrichment. - refine {| ffme_enr := TypesLEnrichedInJudgments2 |}; simpl. - admit. - admit. + 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 }. 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). + 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) }. + admit. + Defined. - Definition FlatSubCategory := FullSubcategory (TypesL L2) FlatObject. + Instance Types_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. +*) +admit. +admit. + intros; simpl; reflexivity. + intros; simpl; reflexivity. + admit. (* assoc central *) + admit. (* cancelr central *) + admit. (* cancell central *) + Defined. - 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 TypesEnrichedInJudgments : Enrichment. + refine + {| enr_v_mon := Judgments_Category_monoidal _ + ; enr_c_pm := Types_PreMonoidal + ; enr_c_bin := Types_binoidal + |}. + Defined. - Definition FlatteningOfReification := - (garrow_from_reification (TypesLEnrichedInJudgments1 L1) (TypesLEnrichedInJudgments3 L2) L12) >>>> retraction. + Structure HasProductTypes := + { + }. - Lemma FlatteningIsNotDestructive : - FlatteningOfReification >>>> retraction_inv >>>> RepresentableFunctor _ (me_i (TypesLEnrichedInJudgments3 L2)) ~~~~ L12. + (* + Lemma CartesianEnrMonoidal (e:PreMonoidalEnrichment) + `(C:CartesianCat(Ob:= _)(Hom:= _)(C:=Underlying (enr_c e))) : MonoidalEnrichment e. admit. - Qed. + Defined. + *) - End TwoLevelLanguage. - - Close Scope temporary_scope3. - Close Scope al_scope. - Close Scope nd_scope. - Close Scope pf_scope. + (* need to prove that if we have cartesian tuples we have cartesian contexts *) + (* + Definition LanguagesWithProductsAreSMME : HasProductTypes -> SurjectiveMonicMonoidalEnrichment TypesEnrichedInJudgments. + admit. + Defined. + *) + End LanguageCategory. 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))) - as parametric_morphism_al_vert_expand_suc_right. - intros; apply al_vert_expand_suc_r_respects; auto. - Defined. - Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_suc_left T Rule AL a b c d e) - with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv))) - as parametric_morphism_al_vert_expand_suc_left. - intros; apply al_vert_expand_suc_l_respects; auto. - Defined. - Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_ant_right T Rule AL a b c d e) - with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv))) - as parametric_morphism_al_vert_expand_ant_right. - intros; apply al_vert_expand_ant_r_respects; auto. - Defined. - Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_ant_left T Rule AL a b c d e) - with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv))) - as parametric_morphism_al_vert_expand_ant_left. - intros; apply al_vert_expand_ant_l_respects; auto. - Defined. -Close Scope nd_scope. - -Notation "cs |= ss" := (@sequent _ cs ss) : al_scope. (* -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 Judg [ ]. -*) - - -(* proofs which are generic and apply to any acceptable langauge (most of section 4) *) -Section Programming_Language_Facts. - - (* the ambient language about which we are proving facts *) - 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 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(ProgrammingLanguage:=Lang). - Existing Instance lang_al_eqv. - - Ltac distribute := - match goal with - [ |- ?G ] => - match G with - context ct [(?A ** ?B) ;; (?C ** ?D)] => - setoid_rewrite <- (ndr_prod_preserves_comp A B C D) - end - end. - - Ltac sequentialize_product A B := - match goal with - [ |- ?G ] => - match G with - | context ct [(A ** B)] => - setoid_replace (A ** B) - with ((A ** (nd_id _)) ;; ((nd_id _) ** B)) - (*with ((A ** (nd_id _)) ;; ((nd_id _) ** B))*) - end end. - Ltac sequentialize_product' A B := - match goal with - [ |- ?G ] => - match G with - | context ct [(A ** B)] => - setoid_replace (A ** B) - with (((nd_id _) ** B) ;; (A ** (nd_id _))) - (*with ((A ** (nd_id _)) ;; ((nd_id _) ** B))*) - end end. - Ltac distribute' := - match goal with - [ |- ?G ] => - match G with - context ct [(?A ;; ?B) ** (?C ;; ?D)] => - setoid_rewrite (ndr_prod_preserves_comp A B C D) - end - end. - Ltac distribute_left_product_with_id := - match goal with - [ |- ?G ] => - match G with - context ct [(nd_id ?A) ** (?C ;; ?D)] => - setoid_replace ((nd_id A) ** (C ;; D)) with ((nd_id A ;; nd_id A) ** (C ;; D)); - [ setoid_rewrite (ndr_prod_preserves_comp (nd_id A) C (nd_id A) D) | idtac ] - end - end. - Ltac distribute_right_product_with_id := - match goal with - [ |- ?G ] => - match G with - context ct [(?C ;; ?D) ** (nd_id ?A)] => - setoid_replace ((C ;; D) ** (nd_id A)) with ((C ;; D) ** (nd_id A ;; nd_id A)); - [ setoid_rewrite (ndr_prod_preserves_comp C (nd_id A) D (nd_id A)) | idtac ] - end - end. - - (* another phrasing of al_subst_associativity; obligations tend to show up in this form *) - Lemma al_subst_associativity'' : - forall (a b : T) (f : [] /⋯⋯/ [[a] |= [b]]) (c : T) (g : [] /⋯⋯/ [[b] |= [c]]) - (d : T) (h : [] /⋯⋯/ [[c] |= [d]]), - nd_llecnac;; ((nd_llecnac;; (f ** g;; al_subst [a] [b] [c])) ** h;; al_subst [a] [c] [d]) === - nd_llecnac;; (f ** (nd_llecnac;; (g ** h;; al_subst [b] [c] [d]));; al_subst [a] [b] [d]). - intros. - sequentialize_product' (nd_llecnac;; (f ** g;; al_subst [a] [b] [c])) h. - repeat setoid_rewrite <- ndr_comp_associativity. - distribute_right_product_with_id. - repeat setoid_rewrite ndr_comp_associativity. - set (@al_subst_associativity) as q. setoid_rewrite q. clear q. - apply ndr_comp_respects; try reflexivity. - repeat setoid_rewrite <- ndr_comp_associativity. - apply ndr_comp_respects; try reflexivity. - sequentialize_product f ((nd_llecnac;; g ** h);; al_subst [b] [c] [d]). - distribute_left_product_with_id. - repeat setoid_rewrite <- ndr_comp_associativity. - apply ndr_comp_respects; try reflexivity. - setoid_rewrite <- ndr_prod_preserves_comp. - repeat setoid_rewrite ndr_comp_left_identity. - repeat setoid_rewrite ndr_comp_right_identity. - admit. - admit. - admit. - admit. - admit. - Qed. - - Close Scope temporary_scope4. - Close Scope al_scope. - Close Scope nd_scope. - Close Scope pf_scope. - Close Scope isomorphism_scope. -End Programming_Language_Facts. - -(*Coercion AL_SurjectiveEnrichment : ProgrammingLanguage >-> SurjectiveEnrichment.*) -(*Coercion AL_MonicMonoidalEnrichment : ProgrammingLanguage >-> MonicMonoidalEnrichment.*) -*) \ No newline at end of file +Structure ProgrammingLanguageSMME := +{ plsmme_t : Type +; plsmme_judg : Type +; plsmme_sequent : Tree ??plsmme_t -> Tree ??plsmme_t -> plsmme_judg +; plsmme_rule : Tree ??plsmme_judg -> Tree ??plsmme_judg -> Type +; plsmme_pl : @ProgrammingLanguage plsmme_t plsmme_judg plsmme_sequent plsmme_rule +; plsmme_smme : SurjectiveMonicMonoidalEnrichment (TypesEnrichedInJudgments _ _ plsmme_pl) +}. +Coercion plsmme_pl : ProgrammingLanguageSMME >-> ProgrammingLanguage. +Coercion plsmme_smme : ProgrammingLanguageSMME >-> SurjectiveMonicMonoidalEnrichment. +*) +Implicit Arguments ND [ Judgment ].