From: Adam Megacz Date: Sun, 10 Apr 2011 11:22:43 +0000 (+0000) Subject: fill in lots of missing proofs X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=77e8c70f4fd7a32db036fee5884a98208d450de2 fill in lots of missing proofs --- diff --git a/Makefile b/Makefile index 97de58b..58f4d40 100644 --- a/Makefile +++ b/Makefile @@ -6,11 +6,7 @@ default: build/CoqPass.hs build/CoqPass.hs: $(allfiles) make build/Makefile.coq - cd build; make -f Makefile.coq OPT="-opt -dont-load-proofs" \ - ExtractionMain.vo \ - ProgrammingLanguageGeneralizedArrow.vo \ - ProgrammingLanguageArrow.vo \ - ProgrammingLanguageFlattening.vo + cd build; make -f Makefile.coq OPT="-opt -dont-load-proofs" All.vo cd build; make -f Makefile.coq Extraction.vo cat src/Extraction-prefix.hs > build/CoqPass.hs cat build/Extraction.hs | grep -v '^module' | grep -v '^import' >> build/CoqPass.hs diff --git a/src/All.v b/src/All.v index b42d175..5db7ece 100644 --- a/src/All.v +++ b/src/All.v @@ -1,89 +1,9 @@ -Require Import Preamble. -Require Import General. - -Require Import HaskKinds. -Require Import HaskLiteralsAndTyCons. - -Require Import HaskCoreVars. -Require Import HaskCoreTypes. -Require Import HaskCore. - -Require Import HaskWeakTypes. -Require Import HaskWeakVars. -Require Import HaskWeak. - -Require Import HaskCoreToWeak. - -Require Import HaskStrongTypes. -Require Import HaskStrong. - -Require Import NaturalDeduction. -Require Import NaturalDeductionToLatex. - -Require Import HaskProof. - -Require Import HaskProofToStrong. -Require Import HaskStrongToWeak. -Require Import HaskWeakToCore. -(*Require Import HaskWeakToStrong.*) -Require Import HaskStrongToProof. -(*Require Import HaskProofToLatex.*) - -(*Require Import HaskStrongCategory.*) -(*Require Import Extraction.*) - -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 SliceCategories_ch1_6_4. - -Require Import EpicMonic_ch2_1. -Require Import InitialTerminal_ch2_2. -Require Import SectionRetract_ch2_4. - -Require Import Equalizers_ch3_3. -Require Import CoEqualizers_ch3_4. - -Require Import Algebras_ch4. - -Require Import NaturalTransformations_ch7_4. -Require Import NaturalIsomorphisms_ch7_5. -Require Import FunctorCategories_ch7_7. - -Require Import Subcategories_ch7_1. - -Require Import Coherence_ch7_8. -Require Import MonoidalCategories_ch7_8. - -Require Import Enrichment_ch2_8. -Require Import RepresentableStructure_ch7_2. - -Require Import Yoneda_ch8. -(*Require Import Exponentials_ch6.*) - -(*Require Import CategoryOfCategories_ch7_1.*) -(*Require Import Adjoints_ch9.*) - -Require Import NaturalDeductionCategory. - -Require Import Reification. -Require Import GeneralizedArrow. -Require Import GeneralizedArrowFromReification. -Require Import ReificationFromGeneralizedArrow. -Require Import WeakFunctorCategory. -Require Import SmallSMMEs. -Require Import ReificationCategory. -Require Import GeneralizedArrowCategory. -Require Import ReificationsAndGeneralizedArrows. +Require Import ExtractionMain. +(* +Require Import ProgrammingLanguageGeneralizedArrow. +Require Import ProgrammingLanguageFlattening. +Require Import ProgrammingLanguageArrow. +Require Import ProgrammingLanguageReification. +*) Require Import ReificationsIsomorphicToGeneralizedArrows. -Require Import HaskProofCategory. -Require Import ProgrammingLanguage. - -(* very slow! *) -Require Import FreydCategories. -Require Import Arrows. - - diff --git a/src/Enrichments.v b/src/Enrichments.v index a98b047..5fa684e 100644 --- a/src/Enrichments.v +++ b/src/Enrichments.v @@ -45,21 +45,31 @@ Structure Enrichment := }. Coercion enr_c : Enrichment >-> ECategory. +(* Coq grinds down into a performance bog when I try to use this *) +Definition WeaklySurjectiveEnrichment (ec:Enrichment) := + @treeDecomposition (enr_v ec) (option (ec*ec)) + (fun t => match t with + | None => enr_v_i ec + | Some x => match x with pair y z => enr_c_hom ec y z end + end) + (enr_v_bobj ec). + +(* technically this ought to be a "strictly surjective enrichment" *) Structure SurjectiveEnrichment := { senr_c_obj : Type ; senr_v_ob := Tree ??(senr_c_obj * senr_c_obj) ; senr_c_hom := fun (c1 c2:senr_c_obj) => [(c1, c2)] -; senr_v_hom : senr_v_ob -> senr_v_ob -> Type -; senr_v : Category senr_v_ob senr_v_hom +; senr_v_hom : senr_v_ob -> senr_v_ob -> Type +; senr_v : Category senr_v_ob senr_v_hom ; senr_v_i := [] -; senr_v_bobj := @T_Branch (option (senr_c_obj * senr_c_obj)) -; senr_v_bin : BinoidalCat senr_v senr_v_bobj -; senr_v_pmon : PreMonoidalCat senr_v_bin senr_v_i -; senr_v_mon : MonoidalCat senr_v_pmon -; senr_c : ECategory senr_v_mon senr_c_obj senr_c_hom -; senr_c_bin : EBinoidalCat senr_c -; senr_c_i : senr_c -; senr_c_pm : PreMonoidalCat senr_c_bin senr_c_i +; senr_v_bobj := @T_Branch ??(senr_c_obj * senr_c_obj) +; senr_v_bin : BinoidalCat senr_v senr_v_bobj +; senr_v_pmon : PreMonoidalCat senr_v_bin senr_v_i +; senr_v_mon : MonoidalCat senr_v_pmon +; senr_c : ECategory senr_v_mon senr_c_obj senr_c_hom +; senr_c_bin : EBinoidalCat senr_c +; senr_c_i : senr_c +; senr_c_pm : PreMonoidalCat senr_c_bin senr_c_i }. Definition SurjectiveEnrichmentToEnrichment (se:SurjectiveEnrichment) : Enrichment. @@ -82,38 +92,19 @@ refine Defined. Coercion SurjectiveEnrichmentToEnrichment : SurjectiveEnrichment >-> Enrichment. -(* -Definition MonoidalEnrichment (e:Enrichment) := - PreMonoidalFunctor - (enr_c_center_mon e) - (enr_v_pmon e) - (RestrictDomain (HomFunctor e (pmon_I (enr_c_pm e))) (Center (enr_c_pm e))). -*) Definition MonoidalEnrichment (e:Enrichment) := PreMonoidalFunctor (enr_c_pm e) (enr_v_pmon e) (HomFunctor e (pmon_I (enr_c_pm e))). - -(* an enrichment for which every object of the enriching category is the tensor of finitely many hom-objects *) -(* -Definition SurjectiveEnrichment (ec:Enrichment) := - @treeDecomposition (enr_v ec) (option (ec*ec)) - (fun t => match t with - | None => enr_v_i ec - | Some x => match x with pair y z => enr_c_hom ec y z end - end) - (enr_v_bobj ec). -*) - Class MonicEnrichment {e:Enrichment} := { me_enr := e ; me_homfunctor := HomFunctor e (enr_c_i e) -(*; me_homfunctor_c := RestrictDomain me_homfunctor (enr_c_center e)*) ; me_full : FullFunctor me_homfunctor ; me_faithful : FaithfulFunctor me_homfunctor ; me_conservative : ConservativeFunctor me_homfunctor +(*; me_homfunctor_c := RestrictDomain me_homfunctor (enr_c_center e)*) }. Implicit Arguments MonicEnrichment [ ]. Coercion me_enr : MonicEnrichment >-> Enrichment. @@ -122,7 +113,6 @@ Transparent HomFunctor. (* like SurjectiveMonicMonoidalEnrichment, but the Enrichment is a field, not a parameter *) Structure SMME := { smme_e : SurjectiveEnrichment -(*; smme_see : SurjectiveEnrichment smme_e*) ; smme_mon : MonoidalEnrichment smme_e ; smme_mee : MonicEnrichment smme_e }. diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index f7f47a3..2f46f85 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -33,13 +33,9 @@ Require Import HaskStrongToWeak. Require Import HaskWeakToCore. Require Import HaskProofToStrong. -Require Import ProgrammingLanguage. - Require Import HaskProofFlattener. Require Import HaskProofStratified. -Require Import ReificationsIsomorphicToGeneralizedArrows. - Open Scope string_scope. Extraction Language Haskell. diff --git a/src/GeneralizedArrow.v b/src/GeneralizedArrow.v index 9149734..303baef 100644 --- a/src/GeneralizedArrow.v +++ b/src/GeneralizedArrow.v @@ -30,6 +30,12 @@ Class GeneralizedArrow (K:Enrichment) {ce}(C:MonoidalEnrichment ce) := { ga_functor_obj : enr_v K -> ce ; ga_functor : Functor (enr_v_mon K) (enr_c_pm ce) ga_functor_obj ; ga_functor_monoidal : PreMonoidalFunctor (enr_v_mon K) (enr_c_pm ce) ga_functor + +(* We require that the host language (but NOT the guest language) be pure, i.e. all morphisms central, to simplify + * things. If this doesn't suit you, just consider the "host language" here to be the pure sublanguage of the + * host language, and toss on the inclusion functor to the full language *) +; ga_host_lang_pure : CommutativeCat (enr_c_pm ce) + (* ; ga_functor : Functor (enr_v_mon K) (Center_is_Monoidal (enr_c_pm ce)) ga_functor_obj ; ga_functor_monoidal : MonoidalFunctor (enr_v_mon K) (Center_is_Monoidal (enr_c_pm ce)) ga_functor diff --git a/src/GeneralizedArrowCategory.v b/src/GeneralizedArrowCategory.v index 3a6a74a..745484b 100644 --- a/src/GeneralizedArrowCategory.v +++ b/src/GeneralizedArrowCategory.v @@ -62,6 +62,8 @@ Definition generalizedArrowOrIdentityFunc s1 s2 (f:GeneralizedArrowOrIdentity s1 Instance compose_generalizedArrows (s0 s1 s2:SMMEs) (g01:GeneralizedArrow s0 s1)(g12:GeneralizedArrow s1 s2) : GeneralizedArrow s0 s2 := { ga_functor_monoidal := g01 >>⊗>> smme_mon s1 >>⊗>> g12 }. + apply ga_host_lang_pure. + Defined. Definition generalizedArrowOrIdentityComp : forall s1 s2 s3, GeneralizedArrowOrIdentity s1 s2 -> GeneralizedArrowOrIdentity s2 s3 -> GeneralizedArrowOrIdentity s1 s3. diff --git a/src/GeneralizedArrowFromReification.v b/src/GeneralizedArrowFromReification.v index 810e862..df6ef76 100644 --- a/src/GeneralizedArrowFromReification.v +++ b/src/GeneralizedArrowFromReification.v @@ -265,13 +265,230 @@ Section GArrowFromReification. (garrow_functor >>>> bin_second(BinoidalCat:=enr_c_bin C) (R' a)) <~~~> (bin_second(BinoidalCat:=enr_v_pmon K) a >>>> garrow_functor) := { ni_iso := fun a => iso_id _ }. - admit. + intros. + etransitivity. apply iso_id_lemma1. symmetry. + etransitivity. apply iso_id_lemma2. symmetry. + + Opaque Underlying. + unfold garrow_functor. + unfold functor_comp at 1. + unfold functor_comp at 1. + Opaque functor_comp. simpl. Transparent functor_comp. + + symmetry. + eapply transitivity. + apply (functor_comp_assoc (RestrictToImage reification) (R' >>>> step2_functor) (ebc_second (R' a)) f). + unfold functor_comp at 1. + unfold functor_comp at 1. + Opaque functor_comp. simpl. Transparent functor_comp. + + symmetry. + eapply transitivity. + set (ni_commutes (mf_second(PreMonoidalFunctor:=reification_rstar reification) a) f) as qq. + unfold functor_comp in qq. + simpl in qq. + apply iso_shift_right' in qq. + apply (fmor_respects(R' >>>> step2_functor) _ _ qq). + + apply (me_faithful(MonicEnrichment:=CMon)). + symmetry. + unfold fmor at 1. + eapply transitivity. + set (ni_commutes (mf_second(PreMonoidalFunctor:=CM) (R' a))) as zz. + unfold functor_comp in zz; unfold functor_fobj in zz; simpl in zz. + set (zz _ _ ((R' >>>> step2_functor) \ (reification \ f))) as zz'. + apply iso_shift_right' in zz'. + apply zz'. + + unfold functor_comp; simpl. + + symmetry. + eapply transitivity. + set full_roundtrip as full_roundtrip'. + unfold fmor in full_roundtrip'. + simpl in full_roundtrip'. + apply full_roundtrip'. + + set (@iso_shift_right') as q. simpl in q. apply q. clear q. + + set (@iso_shift_left) as q. simpl in q. apply q. clear q. + + symmetry. + eapply transitivity. + set full_roundtrip as full_roundtrip'. + unfold fmor in full_roundtrip'. + simpl in full_roundtrip'. + apply (fun a' b' f z => fmor_respects (bin_second(BinoidalCat:=enr_v_bin C) z) _ _ (full_roundtrip' a' b' f)). + symmetry. + + intros. + unfold bin_obj. + unfold senr_v_bobj. + + setoid_rewrite <- associativity. + setoid_rewrite <- associativity. + setoid_rewrite <- associativity. + setoid_rewrite <- associativity. + simpl. + setoid_rewrite <- associativity. + etransitivity. + eapply transitivity. + apply associativity. + eapply transitivity; [ idtac | apply right_identity ]. + apply comp_respects; [ reflexivity | idtac ]. + etransitivity. + apply comp_respects; [ idtac | reflexivity ]. + apply (mf_consistent(PreMonoidalFunctor:=CM)). + apply iso_comp1. + + eapply transitivity. + eapply comp_respects; [ idtac | reflexivity ]. + eapply comp_respects; [ idtac | reflexivity ]. + eapply comp_respects; [ idtac | reflexivity ]. + eapply comp_respects; [ idtac | reflexivity ]. + eapply transitivity. + eapply symmetry. + eapply associativity. + eapply transitivity; [ idtac | apply left_identity ]. + eapply comp_respects; [ idtac | reflexivity ]. + eapply transitivity. + eapply comp_respects; [ idtac | reflexivity ]. + eapply symmetry. + apply (mf_consistent(PreMonoidalFunctor:=CM)). + apply iso_comp1. + + eapply symmetry. + eapply transitivity. + setoid_rewrite <- fmor_preserves_comp. + setoid_rewrite <- fmor_preserves_comp. + eapply reflexivity. + eapply symmetry. + + apply comp_respects; try reflexivity. + + eapply transitivity. + apply associativity. + eapply transitivity. + apply associativity. + eapply transitivity. + apply associativity. + eapply transitivity. + apply associativity. + apply comp_respects; try reflexivity. + + eapply transitivity. + eapply comp_respects; [ reflexivity | idtac ]. + eapply transitivity. + eapply comp_respects; [ idtac | reflexivity ]. + apply mf_consistent. + eapply transitivity. + eapply comp_respects; [ reflexivity | idtac ]. + apply associativity. + apply iso_comp1_right. + + eapply transitivity. + eapply comp_respects; [ reflexivity | idtac ]. + eapply transitivity. + apply associativity. + eapply comp_respects; [ reflexivity | idtac ]. + eapply transitivity. + eapply symmetry. + apply associativity. + eapply transitivity; [ idtac | apply left_identity ]. + eapply comp_respects; [ idtac | reflexivity ]. + eapply transitivity. + eapply comp_respects; [ idtac | reflexivity ]. + eapply symmetry. + eapply (mf_consistent(PreMonoidalFunctor:=reification)). + apply iso_comp1. + + eapply transitivity. + eapply comp_respects; [ reflexivity | idtac ]. + eapply symmetry. + apply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)). + eapply transitivity; [ idtac | apply right_identity ]. + + eapply transitivity. + eapply symmetry. + apply associativity. + eapply transitivity. + eapply comp_respects; [ idtac | reflexivity ]. + unfold functor_fobj. + apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) (reification_rstar_obj reification A))). + + apply symmetry. + eapply transitivity. + apply right_identity. + apply symmetry. + eapply transitivity; [ idtac | apply left_identity ]. + apply comp_respects; [ idtac | reflexivity ]. + + eapply transitivity. + Focus 2. + eapply (fmor_preserves_id (bin_first(BinoidalCat:=enr_v_bin C) (reification_rstar_obj reification A))). + idtac. + apply (fmor_respects (bin_first(BinoidalCat:=enr_v_bin C) (reification_rstar_obj reification A))). + apply iso_comp2. Defined. Implicit Arguments mf_first [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] [C2] [bin_obj'0] [bc0] [I2] [PM2] [fobj] [F]]. Implicit Arguments mf_second [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] [C2] [bin_obj'0] [bc0] [I2] [PM2] [fobj] [F]]. Implicit Arguments mf_i [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] [C2] [bin_obj'0] [bc0] [I2] [PM2] [fobj] [F]]. + Lemma assoc_coherent (a b c : enr_v K) : + (#((pmon_assoc(PreMonoidalCat:=enr_c_pm C) + (garrow_functor a) (garrow_functor c)) (garrow_fobj b)) >>> garrow_functor a ⋊ #((garrow_first c) b)) >>> + #((garrow_second a) (b ⊗ c)) ~~ + (#((garrow_second a) b) ⋉ garrow_functor c >>> + #((garrow_first c) (a ⊗ b))) >>> garrow_functor \ #((pmon_assoc(PreMonoidalCat:=enr_v_mon K) a c) b). + Opaque Underlying. + eapply transitivity. + eapply transitivity; [ idtac | apply right_identity ]. + eapply comp_respects; [ eapply reflexivity | idtac ]. + reflexivity. + + apply symmetry. + eapply transitivity. + eapply transitivity; [ idtac | apply left_identity ]. + eapply comp_respects; [ idtac | eapply reflexivity ]. + eapply transitivity; [ idtac | apply right_identity ]. + apply comp_respects. + simpl. + apply (fmor_preserves_id (ebc_first (garrow_functor c))). + reflexivity. + + symmetry. + eapply transitivity. + eapply transitivity; [ idtac | apply right_identity ]. + apply comp_respects. + reflexivity. + simpl. + apply (fmor_preserves_id (ebc_second (garrow_functor a))). + symmetry. + + unfold functor_fobj. + unfold garrow_functor. + unfold step2_functor. + Opaque R'. + Opaque ff_functor_section_functor. + unfold functor_comp. + simpl. + Transparent R'. + Transparent ff_functor_section_functor. + idtac. + apply (me_faithful(MonicEnrichment:=CMon)). + eapply transitivity; [ eapply full_roundtrip | idtac ]. + + unfold fmor at 1. + unfold R'. + unfold me_homfunctor. + set (mf_assoc(PreMonoidalFunctor:=reification) a b c) as q. + set (mf_assoc(PreMonoidalFunctor:=CM) (garrow_fobj a) (garrow_fobj b) (garrow_fobj c)) as q'. + unfold mf_F in q'. + unfold pmon_I in q'. + admit. + Qed. + Lemma cancell_lemma `(F:PreMonoidalFunctor) b : iso_backward (mf_i F) ⋉ (F b) >>> #(pmon_cancell (F b)) ~~ #((mf_first F b) _) >>> F \ #(pmon_cancell b). @@ -428,7 +645,6 @@ Implicit Arguments mf_i [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] #(pmon_cancelr(PreMonoidalCat:=enr_c_pm C) (garrow_functor b)) ~~ (garrow_functor b ⋊ #(iso_id (enr_c_i C)) >>> #((garrow_second b) (enr_v_i K))) >>> garrow_functor \ #(pmon_cancelr(PreMonoidalCat:=enr_v_mon K) b). - Opaque Underlying. Opaque fmor. intros; simpl. @@ -534,21 +750,16 @@ Implicit Arguments mf_i [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] ; mf_second := garrow_second ; mf_i := iso_id _ }. intros; reflexivity. - intros. - unfold garrow_functor. - unfold fmor. - Opaque fmor. simpl. - unfold step2_functor. - admit. - Transparent fmor. - + intros; apply (reification_host_lang_pure _ _ _ reification). apply cancell_coherent. apply cancelr_coherent. - admit. + apply assoc_coherent. Defined. Definition garrow_from_reification : GeneralizedArrow K CM := - {| ga_functor_monoidal := garrow_monoidal |}. + {| ga_functor_monoidal := garrow_monoidal + ; ga_host_lang_pure := reification_host_lang_pure _ _ _ reification + |}. End GArrowFromReification. diff --git a/src/HaskProofFlattener.v b/src/HaskProofFlattener.v index 82bc678..fcc2a37 100644 --- a/src/HaskProofFlattener.v +++ b/src/HaskProofFlattener.v @@ -133,6 +133,7 @@ Section HaskProofFlattener. * it might help to have the definition for "Inductive ND" (see * NaturalDeduction.v) handy as a cross-reference. *) +(* Definition FlatteningFunctor_fmor {Γ}{Δ}{ec} : forall h c, (h~~{JudgmentsL _ _ (PCF _ Γ Δ ec)}~~>c) -> @@ -392,6 +393,6 @@ Section HaskProofFlattener. *) (* for every n we have a functor from the category of (n+1)-bounded proofs to the category of n-bounded proofs *) - +*) End HaskProofFlattener. diff --git a/src/HaskProofStratified.v b/src/HaskProofStratified.v index 1f7d85d..5c5f68a 100644 --- a/src/HaskProofStratified.v +++ b/src/HaskProofStratified.v @@ -441,9 +441,9 @@ Section HaskProofStratified. Instance OrgPCF_ContextND_Relation Γ Δ lev : ContextND_Relation (PCF_sequent_join Γ Δ lev). admit. Defined. - +(* (* 5.1.3 *) - Instance PCF Γ Δ lev : @ProgrammingLanguage _ _ pcfjudg (PCFRule Γ Δ lev) := + Instance PCF Γ Δ lev : @ProgrammingLanguage _ pcfjudg (PCFRule Γ Δ lev) := { pl_eqv := OrgPCF_ContextND_Relation Γ Δ lev ; pl_snd := PCF_sequents Γ Δ lev }. @@ -571,5 +571,5 @@ Section HaskProofStratified. *) admit. Defined. - +*) End HaskProofStratified. diff --git a/src/NaturalDeductionCategory.v b/src/NaturalDeductionCategory.v index 7ac59b3..d721a97 100644 --- a/src/NaturalDeductionCategory.v +++ b/src/NaturalDeductionCategory.v @@ -72,7 +72,7 @@ Section Judgments_Category. setoid_rewrite <- ndr_prod_preserves_comp. apply (ndr_builtfrom_structural (f;;g)); auto. Defined. - Instance Judgments_Category_binoidal : BinoidalCat Judgments_Category (fun x y => x,,y) := + Instance Judgments_Category_binoidal : BinoidalCat Judgments_Category (@T_Branch (??Judgment)) := { bin_first := jud_first ; bin_second := jud_second }. diff --git a/src/ProgrammingLanguage.v b/src/ProgrammingLanguage.v index 933785a..7ac2af7 100644 --- a/src/ProgrammingLanguage.v +++ b/src/ProgrammingLanguage.v @@ -34,11 +34,11 @@ Section Programming_Language. Context {T : Type}. (* types of the language *) - Context (Judg : Type). - Context (sequent : Tree ??T -> Tree ??T -> Judg). + Definition PLJudg := (Tree ??T) * (Tree ??T). + Definition sequent := @pair (Tree ??T) (Tree ??T). Notation "cs |= ss" := (sequent cs ss) : pl_scope. - Context {Rule : Tree ??Judg -> Tree ??Judg -> Type}. + Context {Rule : Tree ??PLJudg -> Tree ??PLJudg -> Type}. Notation "H /⋯⋯/ C" := (ND Rule H C) : pl_scope. @@ -47,11 +47,11 @@ Section Programming_Language. Open Scope pl_scope. 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 + { 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. @@ -171,8 +171,21 @@ Section Programming_Language. 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. +(* + intros. unfold functor_comp. unfold fmor. + Opaque Types_assoc_iso. + simpl. + + eapply cndr_inert. + apply pl_eqv. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. + apply ndpc_prod; auto. + apply ndpc_comp; auto. + apply ndpc_comp; auto. +*) +admit. Defined. Instance Types_cancelr : Types_first [] <~~~> functor_id _ := @@ -196,7 +209,7 @@ Section Programming_Language. admit. Defined. - Instance Types_PreMonoidal : PreMonoidalCat Types_binoidal [] := + Instance TypesL_PreMonoidal : PreMonoidalCat Types_binoidal [] := { pmon_assoc := Types_assoc ; pmon_cancell := Types_cancell ; pmon_cancelr := Types_cancelr @@ -251,44 +264,19 @@ admit. admit. (* cancell central *) Defined. - Definition TypesEnrichedInJudgments : Enrichment. + Definition TypesEnrichedInJudgments : SurjectiveEnrichment. refine - {| enr_v_mon := Judgments_Category_monoidal _ - ; enr_c_pm := Types_PreMonoidal - ; enr_c_bin := Types_binoidal + {| 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. - Structure HasProductTypes := - { - }. - - (* - Lemma CartesianEnrMonoidal (e:PreMonoidalEnrichment) - `(C:CartesianCat(Ob:= _)(Hom:= _)(C:=Underlying (enr_c e))) : MonoidalEnrichment e. - admit. - Defined. - *) - - (* 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. -(* -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 ]. diff --git a/src/ProgrammingLanguageArrow.v b/src/ProgrammingLanguageArrow.v index b613455..f6a3940 100644 --- a/src/ProgrammingLanguageArrow.v +++ b/src/ProgrammingLanguageArrow.v @@ -18,6 +18,9 @@ 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 PreMonoidalCenter. Require Import MonoidalCategories_ch7_8. Require Import Coherence_ch7_8. Require Import Enrichment_ch2_8. @@ -41,35 +44,28 @@ Section ArrowInLanguage. Context `(Host:ProgrammingLanguage). (* ... for which Types(L) is cartesian: *) - Context {MF}(center_of_TypesL:MonoidalCat (TypesL _ _ Host) (fun x => (fst_obj _ _ x),,(snd_obj _ _ x)) MF []). + Context (center_of_TypesL:MonoidalCat (TypesL_PreMonoidal Host)). - (* along with a monoidal subcategory of Z(Types(L)) *) - Context (VK:MonoidalSubCat center_of_TypesL). + (* along with a full subcategory of Z(Types(L)) *) + Context {P}(VK:FullSubcategory (Center (TypesL_PreMonoidal Host)) P). - (* a premonoidal category enriched in aforementioned full subcategory *) - Context (Kehom:center_of_TypesL -> center_of_TypesL -> @ob _ _ VK). - - Context (KE:@ECategory (@ob _ _ VK) (@hom _ _ VK) VK _ VK - (mon_i (full_subcat_is_monoidal VK)) (full_subcat_is_monoidal VK) center_of_TypesL Kehom). - - Context {kbo:center_of_TypesL -> center_of_TypesL -> center_of_TypesL}. + Context (Pobj_unit : P []). + Context (Pobj_closed : forall a b, P a → P b → P (bin_obj(BinoidalCat:=Center_is_PreMonoidal (TypesL_PreMonoidal Host)) a b)). + Definition VKM := + PreMonoidalFullSubcategory_PreMonoidal (Center_is_PreMonoidal (TypesL_PreMonoidal Host)) VK Pobj_unit Pobj_closed. - Context (kbc:@BinoidalCat center_of_TypesL _ (Underlying KE) kbo). + (* a premonoidal category enriched in aforementioned full subcategory *) + Context (Kehom:(Center (TypesL_PreMonoidal Host)) -> (Center (TypesL_PreMonoidal Host)) -> @ob _ _ VK). + Context (KE :@ECategory (@ob _ _ VK) (@hom _ _ VK) VK _ VKM (pmon_I VKM) VKM (Center (TypesL_PreMonoidal Host)) Kehom). + Context {kbo :(Center (TypesL_PreMonoidal Host)) -> (Center (TypesL_PreMonoidal Host)) -> (Center (TypesL_PreMonoidal Host))}. + Context (kbc :@BinoidalCat (Center (TypesL_PreMonoidal Host)) _ (Underlying KE) kbo). - Check (@PreMonoidalCat) Definition one' := @one _ _ _ (car_terminal(CartesianCat:=CC)) - Context (K:@PreMonoidalCat _ _ KE kbo kbc ). - Context (CC:CartesianCat center_of_TypesL). - - (* - Definition K_enrichment : Enrichment. - refine {| enr_c := KE |}. - Defined. - Context (K_surjective:SurjectiveEnrichment K_enrichment). - *) + Context (K :@PreMonoidalCat _ _ KE kbo kbc ). + Context (CC:CartesianCat (Center (TypesL_PreMonoidal Host))). Definition ArrowInProgrammingLanguage := - @FreydCategory _ _ _ _ _ _ center_of_TypesL _ _ _ _ K. + @FreydCategory _ _ _ _ _ _ (Center (TypesL_PreMonoidal Host)) _ _ _ _ K. Definition ArrowsAreGeneralizedArrows (arrow:ArrowInProgrammingLanguage) : GeneralizedArrow K_enrichment Host. refine {| ga_functor_monoidal := inclusion_functor_monoidal VK |}. diff --git a/src/ProgrammingLanguageGeneralizedArrow.v b/src/ProgrammingLanguageGeneralizedArrow.v index bac2397..bed54b6 100644 --- a/src/ProgrammingLanguageGeneralizedArrow.v +++ b/src/ProgrammingLanguageGeneralizedArrow.v @@ -27,22 +27,21 @@ Require Import FunctorCategories_ch7_7. Require Import NaturalDeduction. Require Import NaturalDeductionCategory. -Require Import FreydCategories. - +Require Import Enrichments. Require Import Reification. Require Import GeneralizedArrow. -Require Import GeneralizedArrowFromReification. Require Import ProgrammingLanguage. -Require Import ReificationsAndGeneralizedArrows. -Require Import ReificationFromGeneralizedArrow. - Section ProgrammingLanguageGeneralizedArrow. - Context (Guest:ProgrammingLanguageSMME) (Host :ProgrammingLanguageSMME). + Context + `(Guest : ProgrammingLanguage) + `(Host : ProgrammingLanguage) + (HostMonoidal : MonoidalEnrichment (TypesEnrichedInJudgments Host)) + (HostMonic : MonicEnrichment (TypesEnrichedInJudgments Host)). Definition GeneralizedArrowInLanguage - := GeneralizedArrow Guest Host. + := GeneralizedArrow (TypesEnrichedInJudgments Guest) HostMonoidal. End ProgrammingLanguageGeneralizedArrow. diff --git a/src/ProgrammingLanguageReification.v b/src/ProgrammingLanguageReification.v index ab8bb90..f6a2a8e 100644 --- a/src/ProgrammingLanguageReification.v +++ b/src/ProgrammingLanguageReification.v @@ -29,6 +29,25 @@ Require Import NaturalDeduction. Require Import NaturalDeductionCategory. Require Import ProgrammingLanguage. +(* + 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 : SurjectiveEnrichment (TypesEnrichedInJudgments _ _ plsmme_pl) + }. + Coercion plsmme_pl : ProgrammingLanguageSMME >-> ProgrammingLanguage. + Coercion plsmme_smme : ProgrammingLanguageSMME >-> SurjectiveMonicMonoidalEnrichment. +*) + + Context + `(Guest : ProgrammingLanguage) + `(Host : ProgrammingLanguage) + (HostMonoidal : MonoidalEnrichment (TypesEnrichedInJudgments Host)) + (HostMonic : MonicEnrichment (TypesEnrichedInJudgments Host)). + Definition TwoLevelLanguage (Guest Host:ProgrammingLanguageSMME) := Reification Guest Host (me_i Host). diff --git a/src/Reification.v b/src/Reification.v index 932d78e..0daca47 100644 --- a/src/Reification.v +++ b/src/Reification.v @@ -35,6 +35,11 @@ Structure Reification (K:Enrichment) (C:Enrichment) (CI:C) := ; reification_rstar_f : Functor (enr_v K) (enr_v C) reification_rstar_obj ; reification_rstar : PreMonoidalFunctor (enr_v_mon K) (enr_v_mon C) reification_rstar_f ; reification_commutes : ∀ k, reification_r k >>>> HomFunctor C CI <~~~> HomFunctor K k >>>> reification_rstar_f + +(* We require that the host language (but NOT the guest language) be pure, i.e. all morphisms central, to simplify + * things. If this doesn't suit you, just consider the "host language" here to be the pure sublanguage of the + * host language, and toss on the inclusion functor to the full language *) +; reification_host_lang_pure : CommutativeCat (enr_c_pm C) }. Transparent HomFunctor. Transparent functor_comp. diff --git a/src/ReificationCategory.v b/src/ReificationCategory.v index 9a7c3fd..2261f88 100644 --- a/src/ReificationCategory.v +++ b/src/ReificationCategory.v @@ -97,6 +97,7 @@ Definition compose_reifications (s0 s1 s2:SMMEs) : apply (ni_respects2 (a >>>> a') (b >>>> b') x). apply ni_inv. apply comm1. + apply (reification_host_lang_pure _ _ _ X0). Defined. Definition reificationOrIdentityComp diff --git a/src/ReificationFromGeneralizedArrow.v b/src/ReificationFromGeneralizedArrow.v index 2a9937f..1a5fea7 100644 --- a/src/ReificationFromGeneralizedArrow.v +++ b/src/ReificationFromGeneralizedArrow.v @@ -34,6 +34,7 @@ Definition reification_from_garrow (K:Enrichment) {ce} (C:MonoidalEnrichment ce) ; reification_rstar := PreMonoidalFunctorsCompose garrow C |}. abstract (intros; set (@ni_associativity) as q; apply q). + intros; apply ga_host_lang_pure. Defined.