From ec8ee5cde986e5b38bcae38cda9e63eba94f1d9f Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Tue, 29 Mar 2011 09:46:52 -0700 Subject: [PATCH] lots of cleanup --- Makefile | 4 +- src/ExtractionMain.v | 53 +-------- src/GeneralizedArrowCategory.v | 4 +- src/GeneralizedArrowFromReification.v | 14 ++- src/HaskKinds.v | 1 - src/HaskLiteralsAndTyCons.v | 18 +-- src/HaskProof.v | 15 ++- src/HaskProofToLatex.v | 1 - src/HaskStrong.v | 2 - src/HaskStrongCategory.v | 127 --------------------- src/HaskStrongToProof.v | 19 +--- src/HaskStrongToWeak.v | 2 +- src/HaskStrongTypes.v | 56 ++++------ src/HaskWeakToStrong.v | 3 - src/NaturalDeduction.v | 134 ++++++++++++++++++++--- src/NaturalDeductionCategory.v | 5 +- src/NaturalDeductionToLatex.v | 88 --------------- src/ProgrammingLanguage.v | 64 +---------- src/ProgrammingLanguageArrow.v | 68 ++++++++++++ src/ProgrammingLanguageGeneralizedArrow.v | 62 +++++++++++ src/ProgrammingLanguageReification.v | 39 +++++++ src/Reification.v | 10 +- src/ReificationCategory.v | 15 ++- src/ReificationFromGeneralizedArrow.v | 2 +- src/ReificationsAndGeneralizedArrows.v | 11 +- src/ReificationsIsomorphicToGeneralizedArrows.v | 25 ++--- src/WeakFunctorCategory.v | 2 - src/categories | 2 +- 28 files changed, 385 insertions(+), 461 deletions(-) delete mode 100644 src/HaskStrongCategory.v delete mode 100644 src/NaturalDeductionToLatex.v create mode 100644 src/ProgrammingLanguageArrow.v create mode 100644 src/ProgrammingLanguageGeneralizedArrow.v create mode 100644 src/ProgrammingLanguageReification.v diff --git a/Makefile b/Makefile index 9067ab0..74c2601 100644 --- a/Makefile +++ b/Makefile @@ -1,4 +1,4 @@ -coqc := coqc -noglob +coqc := coqc -noglob -opt coqfiles := $(shell find src -name \*.v | grep -v \\\#) allfiles := $(coqfiles) $(shell find src -name \*.hs | grep -v \\\#) @@ -6,7 +6,7 @@ default: build/CoqPass.hs build/CoqPass.hs: $(allfiles) make build/Makefile.coq - cd build; make -f Makefile.coq OPT=-dont-load-proofs ExtractionMain.vo + cd build; make -f Makefile.coq OPT="-opt -dont-load-proofs" ExtractionMain.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/ExtractionMain.v b/src/ExtractionMain.v index 6ae977d..6406f90 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -42,8 +42,6 @@ Require Import HaskProofCategory. Require Import ReificationsIsomorphicToGeneralizedArrows. -(*Require Import HaskStrongCategory.*) - Open Scope string_scope. Extraction Language Haskell. @@ -63,7 +61,6 @@ Extract Inductive unit => "()" [ "()" ]. Extract Inlined Constant string_dec => "(==)". Extract Inlined Constant ascii_dec => "(==)". -(* adapted from ExtrOcamlString.v *) Extract Inductive ascii => "Char" [ "you_forgot_to_patch_coq" ] "you_forgot_to_patch_coq". Extract Constant zero => "'\000'". Extract Constant one => "'\001'". @@ -111,8 +108,6 @@ Section core2proof. end. - (* core-to-string (-dcoqpass) *) - Definition header : string := "\documentclass[9pt]{article}"+++eol+++ "\usepackage{amsmath}"+++eol+++ @@ -131,7 +126,7 @@ Section core2proof. eol+++"\end{document}"+++ eol. - + (* core-to-string (-dcoqpass) *) Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string := addErrorMessage ("input CoreSyn: " +++ toString ce) (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) ( @@ -230,52 +225,6 @@ Section core2proof. apply t. Defined. -(* - Definition env := ★::nil. - Definition freshTV : HaskType env ★ := haskTyVarToType (FreshHaskTyVar _). - Definition idproof0 : ND Rule [] [env > nil > [] |- [freshTV--->freshTV @@ nil]]. - eapply nd_comp. - eapply nd_comp. - eapply nd_rule. - apply RVar. - eapply nd_rule - eapply (RArrange _ _ _ _ (RuCanL _ _)) . - eapply nd_rule. - eapply RLam. - Defined. - - - Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) := - addErrorMessage ("input CoreSyn: " +++ toString ce) - (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) ( - coreExprToWeakExpr ce >>= fun we => - addErrorMessage ("WeakExpr: " +++ toString we) - ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we))) - ((weakTypeOfWeakExpr we) >>= fun t => - (addErrorMessage ("WeakType: " +++ toString t) - ((weakTypeToTypeOfKind φ t ★) >>= fun τ => - addErrorMessage ("HaskType: " +++ toString τ) - ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e => - (let haskProof := @expr2proof _ _ _ _ _ _ e - in (* insert HaskProof-to-HaskProof manipulations here *) - (unFresh (@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof)) - >>= fun e' => Error (@toString _ (ExprToString _ _ _ _) (projT2 e')) -(* - >>= fun e' => - Prelude_error (@toString _ (@ExprToString nat _ _ _ _ _ _) (projT2 e')) - *) -) -)))))))). -(* Error "X").*) -(* - strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply - (projT2 e') - INil - >>= fun q => Error (toString q) - ))))))))). -*)*) - - Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) := addErrorMessage ("input CoreSyn: " +++ toString ce) (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) ( diff --git a/src/GeneralizedArrowCategory.v b/src/GeneralizedArrowCategory.v index 3ec6660..7d8b20b 100644 --- a/src/GeneralizedArrowCategory.v +++ b/src/GeneralizedArrowCategory.v @@ -54,7 +54,7 @@ Definition generalizedArrowOrIdentityFunc s1 s2 (f:GeneralizedArrowOrIdentity s1 : Functor s1 s2 (generalizedArrowOrIdentityFobj _ _ f) := match f with | gaoi_id s => functor_id _ - | gaoi_ga s1 s2 f => ga_functor f >>>> RepresentableFunctor s2 (mon_i s2) + | gaoi_ga s1 s2 f => ga_functor f >>>> HomFunctor s2 (mon_i s2) end. Definition compose_generalizedArrows (s0 s1 s2:SMMEs) : @@ -62,7 +62,7 @@ Definition compose_generalizedArrows (s0 s1 s2:SMMEs) : intro g01. intro g12. refine - {| ga_functor := g01 >>>> RepresentableFunctor s1 (mon_i s1) >>>> g12 |}. + {| ga_functor := g01 >>>> HomFunctor s1 (mon_i s1) >>>> g12 |}. apply MonoidalFunctorsCompose. apply MonoidalFunctorsCompose. apply (ga_functor_monoidal g01). diff --git a/src/GeneralizedArrowFromReification.v b/src/GeneralizedArrowFromReification.v index 8bed743..356ee57 100644 --- a/src/GeneralizedArrowFromReification.v +++ b/src/GeneralizedArrowFromReification.v @@ -1,7 +1,7 @@ (*********************************************************************************************************************************) (* GeneralizedArrowFromReification: *) (* *) -(* Turn a generalized arrow into a reification *) +(* Turn a reification into a generalized arrow *) (* *) (*********************************************************************************************************************************) @@ -70,19 +70,21 @@ Section GArrowFromReification. apply (iso_prod IHx1 IHx2). Defined. - Definition garrow_fobj' (vk:enr_v_mon K) : FullImage (RepresentableFunctor C (me_i C)). + Definition garrow_fobj' (vk:enr_v_mon K) : FullImage (HomFunctor C (me_i C)). exists (ehom(ECategory:=C) (me_i C) (garrow_fobj vk)). abstract (exists (garrow_fobj vk); auto). Defined. - Definition step1_mor {a b}(f:a~~{enr_v_mon K}~~>b) : (garrow_fobj' a)~~{FullImage (RepresentableFunctor C (me_i C))}~~>(garrow_fobj' b). + Definition step1_mor {a b}(f:a~~{enr_v_mon K}~~>b) : (garrow_fobj' a)~~{FullImage (HomFunctor C (me_i C))}~~>(garrow_fobj' b). exists (iso_backward (homset_tensor_iso a) >>> reification_rstar reification \ f >>> iso_forward (homset_tensor_iso b)). abstract (auto). Defined. - Definition step1_functor : Functor (enr_v_mon K) (FullImage (RepresentableFunctor C (me_i C))) garrow_fobj'. + (* The poorly-named "step1_functor" is a functor from the full subcategory in the range of the reification functor + * to the full subcategory in the range of the [host language's] Hom(I,-) functor *) + Definition step1_functor : Functor (enr_v_mon K) (FullImage (HomFunctor C (me_i C))) garrow_fobj'. refine {| fmor := fun a b f => step1_mor f |}. abstract (intros; unfold step1_mor; simpl; apply comp_respects; try reflexivity; @@ -107,7 +109,7 @@ Section GArrowFromReification. apply (fmor_preserves_comp reification)). Defined. - Definition step1_niso : reification ≃ step1_functor >>>> InclusionFunctor _ (FullImage (RepresentableFunctor C (me_i C))). + Definition step1_niso : reification ≃ step1_functor >>>> InclusionFunctor _ (FullImage (HomFunctor C (me_i C))). exists (fun c1 => homset_tensor_iso c1). abstract (intros; simpl; @@ -118,8 +120,10 @@ Section GArrowFromReification. Qed. Opaque homset_tensor_iso. + (* the "step2_functor" is the section of the Hom(I,-) functor *) Definition step2_functor := ff_functor_section_functor _ (ffme_mf_full C) (ffme_mf_faithful C). + (* the generalized arrow is the composition of the two steps *) Definition garrow_functor := step1_functor >>>> step2_functor. Lemma garrow_functor_monoidal_niso diff --git a/src/HaskKinds.v b/src/HaskKinds.v index b61ed07..3539e95 100644 --- a/src/HaskKinds.v +++ b/src/HaskKinds.v @@ -12,7 +12,6 @@ Variable Note : Type. Extract Inlined Con Variable natToString : nat -> string. Extract Inlined Constant natToString => "natToString". Instance NatToStringInstance : ToString nat := { toString := natToString }. -(* Figure 7: production κ, ι *) Inductive Kind : Type := | KindStar : Kind (* ★ - the kind of coercions and the kind of types inhabited by [boxed] values *) | KindArrow : Kind -> Kind -> Kind (* ⇛ - type-function-space; things of kind X⇛Y are NOT inhabited by expressions*) diff --git a/src/HaskLiteralsAndTyCons.v b/src/HaskLiteralsAndTyCons.v index 1b8494f..62d638b 100644 --- a/src/HaskLiteralsAndTyCons.v +++ b/src/HaskLiteralsAndTyCons.v @@ -15,16 +15,16 @@ Variable TyCon : Type. Extract Inlined Constant T Variable TyFun : Type. Extract Inlined Constant TyFun => "TyCon.TyCon". (* Since GHC is written in Haskell, compile-time Haskell constants are represented using Haskell (Prelude) types *) -Variable HaskInt : Type. Extract Inlined Constant HaskInt => "Prelude.Int". -Variable HaskChar : Type. Extract Inlined Constant HaskChar => "Prelude.Char". -Variable HaskFastString : Type. Extract Inlined Constant HaskFastString => "FastString.FastString". -Variable HaskInteger : Type. Extract Inlined Constant HaskInteger => "Prelude.Integer". -Variable HaskRational : Type. Extract Inlined Constant HaskRational => "Prelude.Rational". +Variable HaskInt : Type. Extract Inlined Constant HaskInt => "Prelude.Int". +Variable HaskChar : Type. Extract Inlined Constant HaskChar => "Prelude.Char". +Variable HaskFastString : Type. Extract Inlined Constant HaskFastString => "FastString.FastString". +Variable HaskInteger : Type. Extract Inlined Constant HaskInteger => "Prelude.Integer". +Variable HaskRational : Type. Extract Inlined Constant HaskRational => "Prelude.Rational". -Variable CoreName : Type. Extract Inlined Constant CoreName => "Name.Name". -Variable Class_ : Type. Extract Inlined Constant Class_ => "Class.Class". -Variable CoreIPName : Type -> Type. Extract Constant CoreIPName "’a" => "BasicTypes.IPName". - Extraction Inline CoreIPName. +Variable CoreName : Type. Extract Inlined Constant CoreName => "Name.Name". +Variable Class_ : Type. Extract Inlined Constant Class_ => "Class.Class". +Variable CoreIPName : Type -> Type. Extract Constant CoreIPName "’a" => "BasicTypes.IPName". + Extraction Inline CoreIPName. (* This type extracts exactly onto GHC's Literal.Literal type *) Inductive HaskLiteral := diff --git a/src/HaskProof.v b/src/HaskProof.v index 8802223..72d59cb 100644 --- a/src/HaskProof.v +++ b/src/HaskProof.v @@ -40,7 +40,6 @@ Record ProofCaseBranch {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ ★}{ava (vec2list (sac_types sac Γ avars)))) |- [weakLT' (branchtype @@ lev)] }. -(*Coercion pcb_scb : ProofCaseBranch >-> StrongAltCon.*) Implicit Arguments ProofCaseBranch [ ]. (* Figure 3, production $\vdash_E$, Uniform rules *) @@ -66,11 +65,11 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type := (* λ^α rules *) | RBrak : ∀ Γ Δ t v Σ l, Rule [Γ > Δ > Σ |- [t @@ (v::l) ]] [Γ > Δ > Σ |- [<[v|-t]> @@l]] -| REsc : ∀ Γ Δ t v Σ l, Rule [Γ > Δ > Σ |- [<[v|-t]> @@ l]] [Γ > Δ > Σ |- [t @@ (v::l) ]] +| REsc : ∀ Γ Δ t v Σ l, Rule [Γ > Δ > Σ |- [<[v|-t]> @@ l]] [Γ > Δ > Σ |- [t @@ (v::l)]] (* Part of GHC, but not explicitly in System FC *) -| RNote : ∀ Γ Δ Σ τ l, Note -> Rule [Γ > Δ > Σ |- [τ @@ l]] [Γ > Δ > Σ |- [τ @@ l]] -| RLit : ∀ Γ Δ v l, Rule [ ] [Γ > Δ > []|- [literalType v @@ l]] +| RNote : ∀ Γ Δ Σ τ l, Note -> Rule [Γ > Δ > Σ |- [τ @@ l]] [Γ > Δ > Σ |- [τ @@l]] +| RLit : ∀ Γ Δ v l, Rule [ ] [Γ > Δ > []|- [literalType v @@l]] (* SystemFC rules *) | RVar : ∀ Γ Δ σ l, Rule [ ] [Γ>Δ> [σ@@l] |- [σ @@l]] @@ -78,19 +77,26 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type := | RLam : forall Γ Δ Σ (tx:HaskType Γ ★) te l, Rule [Γ>Δ> Σ,,[tx@@l]|- [te@@l] ] [Γ>Δ> Σ |- [tx--->te @@l]] | RCast : forall Γ Δ Σ (σ₁ σ₂:HaskType Γ ★) l, HaskCoercion Γ Δ (σ₁∼∼∼σ₂) -> Rule [Γ>Δ> Σ |- [σ₁@@l] ] [Γ>Δ> Σ |- [σ₂ @@l]] + | RBindingGroup : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ , Rule ([Γ > Δ > Σ₁ |- τ₁ ],,[Γ > Δ > Σ₂ |- τ₂ ]) [Γ>Δ> Σ₁,,Σ₂ |- τ₁,,τ₂ ] + | RApp : ∀ Γ Δ Σ₁ Σ₂ tx te l, Rule ([Γ>Δ> Σ₁ |- [tx--->te @@l]],,[Γ>Δ> Σ₂ |- [tx@@l]]) [Γ>Δ> Σ₁,,Σ₂ |- [te @@l]] + | RLet : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₂ |- [σ₂@@l]],,[Γ>Δ> Σ₁,,[σ₂@@l] |- [σ₁@@l] ]) [Γ>Δ> Σ₁,,Σ₂ |- [σ₁ @@l]] + | REmptyGroup : ∀ Γ Δ , Rule [] [Γ > Δ > [] |- [] ] + | RAppT : forall Γ Δ Σ κ σ (τ:HaskType Γ κ) l, Rule [Γ>Δ> Σ |- [HaskTAll κ σ @@l]] [Γ>Δ> Σ |- [substT σ τ @@l]] | RAbsT : ∀ Γ Δ Σ κ σ l, Rule [(κ::Γ)> (weakCE Δ) > mapOptionTree weakLT Σ |- [ HaskTApp (weakF σ) (FreshHaskTyVar _) @@ (weakL l)]] [Γ>Δ > Σ |- [HaskTAll κ σ @@ l]] + | RAppCo : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ l, Rule [Γ>Δ> Σ |- [σ₁∼∼σ₂ ⇒ σ@@l]] [Γ>Δ> Σ |- [σ @@l]] | RAbsCo : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) σ l, Rule [Γ > ((σ₁∼∼∼σ₂)::Δ) > Σ |- [σ @@ l]] [Γ > Δ > Σ |- [σ₁∼∼σ₂⇒ σ @@l]] + | RLetRec : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > Σ₁,,(τ₂@@@lev) |- ([τ₁],,τ₂)@@@lev ] [Γ > Δ > Σ₁ |- [τ₁@@lev] ] | RCase : forall Γ Δ lev tc Σ avars tbranches (alts:Tree ??{ sac : @StrongAltCon tc & @ProofCaseBranch tc Γ Δ lev tbranches avars sac }), @@ -102,6 +108,7 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type := (* A rule is considered "flat" if it is neither RBrak nor REsc *) +(* TODO: change this to (if RBrak/REsc -> False) *) Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop := | Flat_RArrange : ∀ Γ Δ h c r a , Rule_Flat (RArrange Γ Δ h c r a) | Flat_RNote : ∀ Γ Δ Σ τ l n , Rule_Flat (RNote Γ Δ Σ τ l n) diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v index fb8c2fa..bdcf1e6 100644 --- a/src/HaskProofToLatex.v +++ b/src/HaskProofToLatex.v @@ -6,7 +6,6 @@ Generalizable All Variables. Require Import Preamble. Require Import General. Require Import NaturalDeduction. -Require Import NaturalDeductionToLatex. Require Import Coq.Strings.String. Require Import Coq.Lists.List. Require Import HaskKinds. diff --git a/src/HaskStrong.v b/src/HaskStrong.v index d688c2f..c5f46dc 100644 --- a/src/HaskStrong.v +++ b/src/HaskStrong.v @@ -20,7 +20,6 @@ Section HaskStrong. Context `{EQD_VV:EqDecidable VV}. (* a StrongCaseBranchWithVVs contains all the data found in a case branch except the expression itself *) - Record StrongCaseBranchWithVVs {tc:TyCon}{Γ}{atypes:IList _ (HaskType Γ) (tyConKind tc)}{sac:@StrongAltCon tc} := { scbwv_exprvars : vec VV (sac_numExprVars sac) ; scbwv_exprvars_distinct : distinct (vec2list scbwv_exprvars) @@ -28,7 +27,6 @@ Section HaskStrong. ; scbwv_ξ := fun ξ lev => update_ξ (weakLT'○ξ) (weakL' lev) (vec2list scbwv_varstypes) }. Implicit Arguments StrongCaseBranchWithVVs [[Γ]]. - (*Coercion scbwv_sac : StrongCaseBranchWithVVs >-> StrongAltCon.*) Inductive Expr : forall Γ (Δ:CoercionEnv Γ), (VV -> LeveledHaskType Γ ★) -> LeveledHaskType Γ ★ -> Type := diff --git a/src/HaskStrongCategory.v b/src/HaskStrongCategory.v deleted file mode 100644 index abbdc72..0000000 --- a/src/HaskStrongCategory.v +++ /dev/null @@ -1,127 +0,0 @@ -(*********************************************************************************************************************************) -(* HaskStrongCategory: *) -(* *) -(* Well-typed Haskell terms in a specific tyvar/covar context form a category: Types(Haskell) *) -(* *) -(*********************************************************************************************************************************) - -Generalizable All Variables. -Require Import Preamble. -Require Import General. -Require Import NaturalDeduction. -Require Import Coq.Strings.String. -Require Import Coq.Lists.List. -Require Import HaskKinds. -Require Import HaskCoreTypes. -Require Import HaskLiteralsAndTyCons. -Require Import HaskStrongTypes. -Require Import HaskStrong. - -(* the category of flat Haskell terms in a specific Γ Δ context *) -(* -Section HaskFlat. - Context (Γ:TypeEnv)(Δ:CoercionEnv Γ). - - Lemma idmor a : [] ~~{SystemFC_Cat_Flat past}~~> [(a,a)]. - (*set (@nd_rule _ Rule (RVar Γ a past)) as q.*) - admit. - Defined. - - Lemma compmor a b c : [(a,b)],,[(b,c)] ~~{SystemFC_Cat_Flat past}~~> [(a,c)]. - admit. - Defined. - - Definition HaskFlat - : ECategory - (SystemFC_Cat_Flat past) - (Tree ??(@CoreType V)) - (fun a s => [(a,s)]). - refine - {| eid := fun a => idmor a - ; ecomp := fun a b c => compmor a b c - |}; intros; simpl in *; auto. - apply (MonoidalCat_all_central (SystemFC_Cat_Flat past)). - apply (MonoidalCat_all_central (SystemFC_Cat_Flat past)). - admit. - admit. - admit. - Defined. - - Definition HaskFlatEnrichment : SurjectiveEnrichment. - refine {| se_enr := {| enr_c := HaskFlat |} |}. - admit. - Defined. - - End HaskFlat. - - (* the category of multi-level Haskell terms (n-ary) with a given past *) - Section Hask. - Context (past:@Past V). - - Lemma idmor' a : [] ~~{SystemFC_Cat past}~~> [(a,a)]. - (*set (@nd_rule _ Rule (RVar Γ a past)) as q.*) - admit. - Defined. - - Lemma compmor' a b c : [(a,b)],,[(b,c)] ~~{SystemFC_Cat past}~~> [(a,c)]. - admit. - Defined. - - Definition Hask - : ECategory - (SystemFC_Cat past) - (Tree ??(@LeveledHaskType V)) - (fun a s => [(a,s)]). - refine - {| eid := fun a => idmor' a - ; ecomp := fun a b c => compmor' a b c - |}; intros; simpl in *; auto. - apply (MonoidalCat_all_central (SystemFC_Cat past)). - apply (MonoidalCat_all_central (SystemFC_Cat past)). - admit. - admit. - admit. - Defined. - - Definition HaskEnrichmentMonoidal : MonoidalEnrichment. - refine {| me_enr := {| enr_c := Hask |} |}. - Admitted. - - Definition HaskEnrichmentMonicMonoidal : MonicMonoidalEnrichment. - refine {| ffme_enr := HaskEnrichmentMonoidal |}. - admit. - admit. - admit. - Defined. - End Hask. - - Section ReificationAndGeneralizedArrow. - Context - (past:list ((Tree ??(@LeveledHaskType V)) * V)) - (Σ:(Tree ??(@LeveledHaskType V))) - (n:V). - - Definition SystemFC_Reification - : Reification - (HaskFlatEnrichment (((Σ,n)::past))) - (HaskEnrichmentMonicMonoidal (*past*)) - (me_i (HaskEnrichmentMonicMonoidal (*past*))). - (* refine {| reification_rstar_f := EscBrak_Functor Γ past n Σ |}.*) - admit. - Defined. -(* - Definition SystemFC_GArrow := - garrow_from_reification - (HaskFlatEnrichment (((Σ,n)::past))) - (HaskEnrichmentMonicMonoidal (*past*)) - SystemFC_Reification. - *) - (* I think we have to add a proof that the derived GArrow's range is in the "monoidal closure" of the reification functor; - * from there we can show that -- in the case of Hask and System FC -- that range is a retract of some other subcategory - * of Hask which consists of the (GArrow g => g a b) morphisms *) - - End ReificationAndGeneralizedArrow. -*) - - - diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index c29963e..d5e57f8 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -142,7 +142,7 @@ Lemma strip_twice_lemma x y t : stripOutVars x (stripOutVars y t) = stripOutVars rewrite app_comm_cons. reflexivity. *) -admit. + admit. Qed. Lemma strip_distinct a y : (not (In a (leaves y))) -> stripOutVars (a :: nil) y = y. @@ -363,21 +363,6 @@ Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ | ELR_leaf Γ Δ ξ lev v t e => [t] | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypes b1),,(eLetRecTypes b2) end. -(* -Fixpoint eLetRecVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??VV := - match elrb with - | ELR_nil Γ Δ ξ lev => [] - | ELR_leaf Γ Δ ξ lev v _ _ e => [v] - | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecVars b1),,(eLetRecVars b2) - end. - -Fixpoint eLetRecTypesVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(VV * HaskType Γ ★):= - match elrb with - | ELR_nil Γ Δ ξ lev => [] - | ELR_leaf Γ Δ ξ lev v t _ e => [(v, t)] - | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypesVars b1),,(eLetRecTypesVars b2) - end. -*) Lemma stripping_nothing_is_inert {Γ:TypeEnv} @@ -579,7 +564,7 @@ Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v t reflexivity. Qed. -(* IDEA: use multi-conclusion proofs instead *) +(* TODO: use multi-conclusion proofs instead *) Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type := | lrsp_nil : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _) | lrsp_leaf : forall v t e , diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v index 1761b83..e956dd6 100644 --- a/src/HaskStrongToWeak.v +++ b/src/HaskStrongToWeak.v @@ -213,4 +213,4 @@ Section HaskStrongToWeak. uniqM f => f us >>= fun x => OK (snd x) end. -End HaskStrongToWeak. \ No newline at end of file +End HaskStrongToWeak. diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v index 2ee78b2..224d70b 100644 --- a/src/HaskStrongTypes.v +++ b/src/HaskStrongTypes.v @@ -21,7 +21,6 @@ Variable dataConExVars_ : CoreDataCon -> list CoreVar. Extract Inlined Const Variable dataConEqTheta_ : CoreDataCon -> list PredType. Extract Inlined Constant dataConEqTheta_ => "DataCon.dataConEqTheta". Variable dataConOrigArgTys_: CoreDataCon -> list CoreType. Extract Inlined Constant dataConOrigArgTys_=>"DataCon.dataConOrigArgTys". -(* TODO: might be a better idea to panic here than simply drop things that look wrong *) Definition dataConExTyVars cdc := filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (dataConExVars_ cdc)). Opaque dataConExTyVars. @@ -79,27 +78,25 @@ Section Raw. Inductive RawCoercionKind : Type := mkRawCoercionKind : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawCoercionKind. - Section CV. - - (* the PHOAS type which stands for coercion variables of System FC *) - - - (* Figure 7: γ, δ *) - Inductive RawHaskCoer {CV:Type} : RawCoercionKind -> Prop := (* FIXME *). -(* - | CoVar : CV -> RawHaskCoer (* g *) - | CoType : RawHaskType -> RawHaskCoer (* τ *) - | CoApp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* γ γ *) - | CoAppT : RawHaskCoer -> RawHaskType -> RawHaskCoer (* γ@v *) - | CoCFApp : ∀ n, CoFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* C γⁿ *) - | CoTFApp : ∀ n, TyFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* S_n γⁿ *) - | CoAll : Kind -> (TV -> RawHaskCoer) -> RawHaskCoer (* ∀a:κ.γ *) - | CoSym : RawHaskCoer -> RawHaskCoer (* sym *) - | CoComp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* ◯ *) - | CoLeft : RawHaskCoer -> RawHaskCoer (* left *) - | CoRight : RawHaskCoer -> RawHaskCoer (* right *). -*) - End CV. + (* Figure 7: γ, δ; CV is the PHOAS type which stands for coercion variables of System FC *) + Inductive RawHaskCoer {CV:Type} : RawCoercionKind -> Prop := . + (* + * This has been disabled until we manage to reconcile SystemFC's + * coercions with what GHC actually implements (they are not the + * same!) + * + | CoVar : CV -> RawHaskCoer (* g *) + | CoType : RawHaskType -> RawHaskCoer (* τ *) + | CoApp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* γ γ *) + | CoAppT : RawHaskCoer -> RawHaskType -> RawHaskCoer (* γ@v *) + | CoCFApp : ∀ n, CoFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* C γⁿ *) + | CoTFApp : ∀ n, TyFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* S_n γⁿ *) + | CoAll : Kind -> (TV -> RawHaskCoer) -> RawHaskCoer (* ∀a:κ.γ *) + | CoSym : RawHaskCoer -> RawHaskCoer (* sym *) + | CoComp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* ◯ *) + | CoLeft : RawHaskCoer -> RawHaskCoer (* left *) + | CoRight : RawHaskCoer -> RawHaskCoer (* right *). + *) End Raw. Implicit Arguments TCon [ [TV] ]. @@ -294,13 +291,6 @@ Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ apply weakCK. apply IHκ. Defined. -(* -Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) := - match κ as K return list (HaskCoercionKind (app K Γ)) with - | nil => hck - | _ => map weakCK' hck - end. -*) Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) := map weakCK' hck. Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) := @@ -309,10 +299,6 @@ Definition weakF {Γ:TypeEnv}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv T forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV κ -> RawHaskType TV κ₂ := fun TV ite tv => (f TV (weakITE ite) tv). -(* I keep mixing up left/right folds *) -(* Eval compute in (fold_right (fun x y => "("+++x+++y+++")") "x" ("a"::"b"::"c"::nil)). *) -(*Eval compute in (fold_left (fun x y => "("+++x+++y+++")") ("a"::"b"::"c"::nil) "x").*) - Fixpoint caseType0 {Γ}(lk:list Kind) : IList _ (HaskType Γ) lk -> HaskType Γ (fold_right KindArrow ★ lk) -> @@ -492,7 +478,9 @@ end. Definition compareHT Γ κ (ht1 ht2:HaskType Γ κ) := compareT (length Γ) (ht1 (fun _ => nat) (count' Γ O)) (ht2 (fun _ => nat) (count' Γ O)). -(* This is not provable in Coq's logic because the Coq function space +(* The PHOAS axioms + * + * This is not provable in Coq's logic because the Coq function space * is "too big" - although its only definable inhabitants are Coq * functions, it is not provable in Coq that all function space * inhabitants are definable (i.e. there are no "exotic" inhabitants). diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v index b2521e3..1b34865 100644 --- a/src/HaskWeakToStrong.v +++ b/src/HaskWeakToStrong.v @@ -19,9 +19,6 @@ Require Import HaskStrongTypes. Require Import HaskStrong. Require Import HaskCoreVars. -(* can remove *) -Require Import HaskStrongToWeak. - Open Scope string_scope. Definition TyVarResolver Γ := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt). Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, ???(HaskCoVar Γ Δ). diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v index acb21d0..dde0a0c 100644 --- a/src/NaturalDeduction.v +++ b/src/NaturalDeduction.v @@ -12,9 +12,7 @@ Require Import Coq.Strings.Ascii. Require Import Coq.Strings.String. (* - * IMPORTANT!!! - * - * Unlike most formalizations, this library offers TWO different ways + * Unlike most formalizations, this library offers two different ways * to represent a natural deduction proof. To demonstrate this, * consider the signature of the propositional calculus: * @@ -82,6 +80,22 @@ Require Import Coq.Strings.String. * (NaturalDeduction.v) and are designed specifically in order to * circumvent the problem in the previous paragraph. * + * These proofs are actually structurally explicit on (potentially) + * two different levels. The beginning of this file formalizes + * natural deduction proofs with explicit structural operations for + * manipulating lists of judgments – for example, the open + * hypotheses of an incomplete proof. The class + * TreeStructuralRules further down in the file instantiates ND + * such that Judgments is actually a pair of trees of propositions, + * and there will be a whole *other* set of rules for manipulating + * the structure of a tree of propositions *within* a single + * judgment. + * + * The flattening functor ends up mapping the first kind of + * structural operation (moving around judgments) onto the second + * kind (moving around propositions/types). That's why everything + * is so laboriously explicit - there's important information in + * those structural operations. *) (* @@ -116,8 +130,10 @@ Section Natural_Deduction. forall conclusions:Tree ??Judgment, Type := - (* natural deduction: you may infer anything from itself -- "identity proof" *) + (* natural deduction: you may infer nothing from nothing *) | nd_id0 : [ ] /⋯⋯/ [ ] + + (* natural deduction: you may infer anything from itself -- "identity proof" *) | nd_id1 : forall h, [ h ] /⋯⋯/ [ h ] (* natural deduction: you may discard conclusions *) @@ -139,7 +155,9 @@ Section Natural_Deduction. `(pf2: x /⋯⋯/ c), ( h /⋯⋯/ c) - (* structural rules on lists of judgments *) + (* Structural rules on lists of judgments - note that this is completely separate from the structural + * rules for *contexts* within a sequent. The rules below manipulate lists of *judgments* rather than + * lists of *propositions*. *) | nd_cancell : forall {a}, [] ,, a /⋯⋯/ a | nd_cancelr : forall {a}, a ,, [] /⋯⋯/ a | nd_llecnac : forall {a}, a /⋯⋯/ [] ,, a @@ -238,10 +256,10 @@ Section Natural_Deduction. }. (* - * Single-conclusion proofs; this is an alternate representation - * where each inference has only a single conclusion. These have - * worse compositionality properties than ND's (they don't form a - * category), but are easier to emit as LaTeX code. + * Natural Deduction proofs which are Structurally Implicit on the + * level of judgments. These proofs have poor compositionality + * properties (vertically, they look more like lists than trees) but + * are easier to do induction over. *) Inductive SCND : Tree ??Judgment -> Tree ??Judgment -> Type := | scnd_weak : forall c , SCND c [] @@ -292,8 +310,8 @@ Section Natural_Deduction. | scnd_weak c => let case_weak := tt in _ | scnd_comp ht ct c pn' rule => let case_comp := tt in let qq := closedFromPnodes _ _ pn' in _ | scnd_branch ht c1 c2 pn' pn'' => let case_branch := tt in - let q1 := closedFromPnodes _ _ pn' in - let q2 := closedFromPnodes _ _ pn'' in _ + let q1 := closedFromPnodes _ _ pn' in + let q2 := closedFromPnodes _ _ pn'' in _ end (refl_equal _) (refl_equal _))) h c pn2 cnd). @@ -325,6 +343,7 @@ Section Natural_Deduction. | cnd_branch c1 c2 cnd1 cnd2 => nd_llecnac ;; nd_prod (closedNDtoNormalND cnd1) (closedNDtoNormalND cnd2) end. + (* Natural Deduction systems whose judgments happen to be pairs of the same type *) Section Sequents. Context {S:Type}. (* type of sequent components *) Context {sequent:S->S->Judgment}. @@ -332,10 +351,12 @@ Section Natural_Deduction. Notation "a |= b" := (sequent a b). Notation "a === b" := (@ndr_eqv ndr _ _ a b) : nd_scope. + (* Sequent systems with initial sequents *) Class SequentCalculus := { nd_seq_reflexive : forall a, ND [ ] [ a |= a ] }. - + + (* Sequent systems with a cut rule *) Class CutRule (nd_cutrule_seq:SequentCalculus) := { nd_cut : forall a b c, [ a |= b ] ,, [ b |= c ] /⋯⋯/ [ a |= c ] ; nd_cut_left_identity : forall a b, (( (nd_seq_reflexive a)**(nd_id _));; nd_cut _ _ b) === nd_cancell @@ -345,14 +366,16 @@ Section Natural_Deduction. }. End Sequents. -(*Implicit Arguments SequentCalculus [ S ]*) -(*Implicit Arguments CutRule [ S ]*) + + (* Sequent systems in which each side of the sequent is a tree of something *) Section SequentsOfTrees. Context {T:Type}{sequent:Tree ??T -> Tree ??T -> Judgment}. Context (ndr:ND_Relation). Notation "a |= b" := (sequent a b). Notation "a === b" := (@ndr_eqv ndr _ _ a b) : nd_scope. + (* Sequent systems in which we can re-arrange the tree to the left of the turnstile - note that these rules + * mirror nd_{cancell,cancelr,rlecnac,llecnac,assoc,cossa} but are completely separate from them *) Class TreeStructuralRules := { tsr_ant_assoc : forall {x a b c}, ND [((a,,b),,c) |= x] [(a,,(b,,c)) |= x] ; tsr_ant_cossa : forall {x a b c}, ND [(a,,(b,,c)) |= x] [((a,,b),,c) |= x] @@ -364,6 +387,7 @@ Section Natural_Deduction. Notation "[# a #]" := (nd_rule a) : nd_scope. + (* Sequent systems in which we can add any proposition to both sides of the sequent (sort of a "horizontal weakening") *) Context `{se_cut : @CutRule _ sequent ndr sc}. Class SequentExpansion := { se_expand_left : forall tau {Gamma Sigma}, ND [ Gamma |= Sigma ] [tau,,Gamma|=tau,,Sigma] @@ -539,7 +563,7 @@ Inductive nd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall | nd_property_rule : forall h c r, P h c r -> @nd_property _ _ P h c (nd_rule r). Hint Constructors nd_property. -(* witnesses the fact that every Rule in a particular proof satisfies the given predicate *) +(* witnesses the fact that every Rule in a particular proof satisfies the given predicate (for ClosedND) *) Inductive cnd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall {c}, @ClosedND Judgment Rule c -> Prop := | cnd_property_weak : @cnd_property _ _ P _ cnd_weak | cnd_property_rule : forall h c r cnd', @@ -552,6 +576,7 @@ Inductive cnd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : foral @cnd_property _ _ P c2 cnd2 -> @cnd_property _ _ P _ (cnd_branch _ _ cnd1 cnd2). +(* witnesses the fact that every Rule in a particular proof satisfies the given predicate (for SCND) *) Inductive scnd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : forall {h c}, @SCND Judgment Rule h c -> Prop := | scnd_property_weak : forall c, @scnd_property _ _ P _ _ (scnd_weak c) | scnd_property_comp : forall h x c r cnd', @@ -564,5 +589,84 @@ Inductive scnd_property {Judgment}{Rule}(P:forall h c, @Rule h c -> Prop) : fora @scnd_property _ _ P x c2 cnd2 -> @scnd_property _ _ P x _ (scnd_branch _ _ _ cnd1 cnd2). +(* renders a proof as LaTeX code *) +Section ToLatex. + + Context {Judgment : Type}. + Context {Rule : forall (hypotheses:Tree ??Judgment)(conclusion:Tree ??Judgment), Type}. + Context {JudgmentToLatexMath : ToLatexMath Judgment}. + Context {RuleToLatexMath : forall h c, ToLatexMath (Rule h c)}. + + Open Scope string_scope. + + Definition judgments2latex (j:Tree ??Judgment) := treeToLatexMath (mapOptionTree toLatexMath j). + + Definition eolL : LatexMath := rawLatexMath eol. + + (* invariant: each proof shall emit its hypotheses visibly, except nd_id0 *) + Section SCND_toLatex. + + (* indicates which rules should be hidden (omitted) from the rendered proof; useful for structural operations *) + Context (hideRule : forall h c (r:Rule h c), bool). + + Fixpoint SCND_toLatexMath {h}{c}(pns:SCND(Rule:=Rule) h c) : LatexMath := + match pns with + | scnd_branch ht c1 c2 pns1 pns2 => SCND_toLatexMath pns1 +++ rawLatexMath " \hspace{1cm} " +++ SCND_toLatexMath pns2 + | scnd_weak c => rawLatexMath "" + | scnd_comp ht ct c pns rule => if hideRule _ _ rule + then SCND_toLatexMath pns + else rawLatexMath "\trfrac["+++ toLatexMath rule +++ rawLatexMath "]{" +++ eolL +++ + SCND_toLatexMath pns +++ rawLatexMath "}{" +++ eolL +++ + toLatexMath c +++ rawLatexMath "}" +++ eolL + end. + End SCND_toLatex. + + (* this is a work-in-progress; please use SCND_toLatexMath for now *) + Fixpoint nd_toLatexMath {h}{c}(nd:@ND _ Rule h c)(indent:string) := + match nd with + | nd_id0 => rawLatexMath indent +++ + rawLatexMath "% nd_id0 " +++ eolL + | nd_id1 h' => rawLatexMath indent +++ + rawLatexMath "% nd_id1 "+++ judgments2latex h +++ eolL + | nd_weak h' => rawLatexMath indent +++ + rawLatexMath "\inferrule*[Left=ndWeak]{" +++ toLatexMath h' +++ rawLatexMath "}{ }" +++ eolL + | nd_copy h' => rawLatexMath indent +++ + rawLatexMath "\inferrule*[Left=ndCopy]{"+++judgments2latex h+++ + rawLatexMath "}{"+++judgments2latex c+++rawLatexMath "}" +++ eolL + | nd_prod h1 h2 c1 c2 pf1 pf2 => rawLatexMath indent +++ + rawLatexMath "% prod " +++ eolL +++ + rawLatexMath indent +++ + rawLatexMath "\begin{array}{c c}" +++ eolL +++ + (nd_toLatexMath pf1 (" "+++indent)) +++ + rawLatexMath indent +++ + rawLatexMath " & " +++ eolL +++ + (nd_toLatexMath pf2 (" "+++indent)) +++ + rawLatexMath indent +++ + rawLatexMath "\end{array}" + | nd_comp h m c pf1 pf2 => rawLatexMath indent +++ + rawLatexMath "% comp " +++ eolL +++ + rawLatexMath indent +++ + rawLatexMath "\begin{array}{c}" +++ eolL +++ + (nd_toLatexMath pf1 (" "+++indent)) +++ + rawLatexMath indent +++ + rawLatexMath " \\ " +++ eolL +++ + (nd_toLatexMath pf2 (" "+++indent)) +++ + rawLatexMath indent +++ + rawLatexMath "\end{array}" + | nd_cancell a => rawLatexMath indent +++ + rawLatexMath "% nd-cancell " +++ (judgments2latex a) +++ eolL + | nd_cancelr a => rawLatexMath indent +++ + rawLatexMath "% nd-cancelr " +++ (judgments2latex a) +++ eolL + | nd_llecnac a => rawLatexMath indent +++ + rawLatexMath "% nd-llecnac " +++ (judgments2latex a) +++ eolL + | nd_rlecnac a => rawLatexMath indent +++ + rawLatexMath "% nd-rlecnac " +++ (judgments2latex a) +++ eolL + | nd_assoc a b c => rawLatexMath "" + | nd_cossa a b c => rawLatexMath "" + | nd_rule h c r => toLatexMath r + end. + +End ToLatex. + Close Scope pf_scope. Close Scope nd_scope. diff --git a/src/NaturalDeductionCategory.v b/src/NaturalDeductionCategory.v index b64ac4b..0a413e7 100644 --- a/src/NaturalDeductionCategory.v +++ b/src/NaturalDeductionCategory.v @@ -36,6 +36,7 @@ Section Judgments_Category. Notation "pf1 === pf2" := (@ndr_eqv _ _ nd_eqv _ _ pf1 pf2). + (* 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 @@ -51,6 +52,7 @@ Section Judgments_Category. intros; apply ndr_comp_associativity. Defined. + (* it is monoidal, with the judgment-tree-formation operator as its tensor *) Definition Judgments_Category_monoidal_endofunctor_fobj : Judgments_Category ×× Judgments_Category -> Judgments_Category := fun xy => (fst_obj _ _ xy),,(snd_obj _ _ xy). Definition Judgments_Category_monoidal_endofunctor_fmor : @@ -201,9 +203,6 @@ Section Judgments_Category. apply nd_structural_cancelr; auto. Defined. - - (* Structure ExpressionAlgebra (sig:Signature) := *) - End Judgments_Category. Close Scope pf_scope. diff --git a/src/NaturalDeductionToLatex.v b/src/NaturalDeductionToLatex.v deleted file mode 100644 index 1f6f32a..0000000 --- a/src/NaturalDeductionToLatex.v +++ /dev/null @@ -1,88 +0,0 @@ -(*********************************************************************************************************************************) -(* NaturalDeductionToLatex: rendering natural deduction proofs as LaTeX code *) -(*********************************************************************************************************************************) - -Generalizable All Variables. -Require Import Preamble. -Require Import General. -Require Import Coq.Strings.Ascii. -Require Import Coq.Strings.String. -Require Import NaturalDeduction. - -Section ToLatex. - - Context {Judgment : Type}. - Context {Rule : forall (hypotheses:Tree ??Judgment)(conclusion:Tree ??Judgment), Type}. - Context {JudgmentToLatexMath : ToLatexMath Judgment}. - Context {RuleToLatexMath : forall h c, ToLatexMath (Rule h c)}. - - Open Scope string_scope. - - Definition judgments2latex (j:Tree ??Judgment) := treeToLatexMath (mapOptionTree toLatexMath j). - - Definition eolL : LatexMath := rawLatexMath eol. - - (* invariant: each proof shall emit its hypotheses visibly, except nd_id0 *) - Section SCND_toLatex. - - (* indicates which rules should be hidden (omitted) from the rendered proof; useful for structural operations *) - Context (hideRule : forall h c (r:Rule h c), bool). - - Fixpoint SCND_toLatexMath {h}{c}(pns:SCND(Rule:=Rule) h c) : LatexMath := - match pns with - | scnd_branch ht c1 c2 pns1 pns2 => SCND_toLatexMath pns1 +++ rawLatexMath " \hspace{1cm} " +++ SCND_toLatexMath pns2 - | scnd_weak c => rawLatexMath "" - | scnd_comp ht ct c pns rule => if hideRule _ _ rule - then SCND_toLatexMath pns - else rawLatexMath "\trfrac["+++ toLatexMath rule +++ rawLatexMath "]{" +++ eolL +++ - SCND_toLatexMath pns +++ rawLatexMath "}{" +++ eolL +++ - toLatexMath c +++ rawLatexMath "}" +++ eolL - end. - End SCND_toLatex. - - (* this is a work-in-progress; please use SCND_toLatexMath for now *) - Fixpoint nd_toLatexMath {h}{c}(nd:@ND _ Rule h c)(indent:string) := - match nd with - | nd_id0 => rawLatexMath indent +++ - rawLatexMath "% nd_id0 " +++ eolL - | nd_id1 h' => rawLatexMath indent +++ - rawLatexMath "% nd_id1 "+++ judgments2latex h +++ eolL - | nd_weak h' => rawLatexMath indent +++ - rawLatexMath "\inferrule*[Left=ndWeak]{" +++ toLatexMath h' +++ rawLatexMath "}{ }" +++ eolL - | nd_copy h' => rawLatexMath indent +++ - rawLatexMath "\inferrule*[Left=ndCopy]{"+++judgments2latex h+++ - rawLatexMath "}{"+++judgments2latex c+++rawLatexMath "}" +++ eolL - | nd_prod h1 h2 c1 c2 pf1 pf2 => rawLatexMath indent +++ - rawLatexMath "% prod " +++ eolL +++ - rawLatexMath indent +++ - rawLatexMath "\begin{array}{c c}" +++ eolL +++ - (nd_toLatexMath pf1 (" "+++indent)) +++ - rawLatexMath indent +++ - rawLatexMath " & " +++ eolL +++ - (nd_toLatexMath pf2 (" "+++indent)) +++ - rawLatexMath indent +++ - rawLatexMath "\end{array}" - | nd_comp h m c pf1 pf2 => rawLatexMath indent +++ - rawLatexMath "% comp " +++ eolL +++ - rawLatexMath indent +++ - rawLatexMath "\begin{array}{c}" +++ eolL +++ - (nd_toLatexMath pf1 (" "+++indent)) +++ - rawLatexMath indent +++ - rawLatexMath " \\ " +++ eolL +++ - (nd_toLatexMath pf2 (" "+++indent)) +++ - rawLatexMath indent +++ - rawLatexMath "\end{array}" - | nd_cancell a => rawLatexMath indent +++ - rawLatexMath "% nd-cancell " +++ (judgments2latex a) +++ eolL - | nd_cancelr a => rawLatexMath indent +++ - rawLatexMath "% nd-cancelr " +++ (judgments2latex a) +++ eolL - | nd_llecnac a => rawLatexMath indent +++ - rawLatexMath "% nd-llecnac " +++ (judgments2latex a) +++ eolL - | nd_rlecnac a => rawLatexMath indent +++ - rawLatexMath "% nd-rlecnac " +++ (judgments2latex a) +++ eolL - | nd_assoc a b c => rawLatexMath "" - | nd_cossa a b c => rawLatexMath "" - | nd_rule h c r => toLatexMath r - end. - -End ToLatex. diff --git a/src/ProgrammingLanguage.v b/src/ProgrammingLanguage.v index de7c7f0..5ce624f 100644 --- a/src/ProgrammingLanguage.v +++ b/src/ProgrammingLanguage.v @@ -27,12 +27,6 @@ Require Import FunctorCategories_ch7_7. Require Import NaturalDeduction. Require Import NaturalDeductionCategory. -Require Import FreydCategories. - -Require Import Reification. -Require Import GeneralizedArrow. -Require Import GeneralizedArrowFromReification. - Section Programming_Language. Context {T : Type}. (* types of the language *) @@ -168,12 +162,17 @@ Section Programming_Language. { }. + Lemma CartesianEnrMonoidal (e:Enrichment) `(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 := @@ -186,56 +185,5 @@ Structure ProgrammingLanguageSMME := }. Coercion plsmme_pl : ProgrammingLanguageSMME >-> ProgrammingLanguage. Coercion plsmme_smme : ProgrammingLanguageSMME >-> SurjectiveMonicMonoidalEnrichment. - -Section ArrowInLanguage. - Context (Host:ProgrammingLanguageSMME). - Context `(CC:CartesianCat (me_mon Host)). - Context `(K:@ECategory _ _ _ _ _ _ (@car_mn _ _ _ _ _ _ _ CC) C Kehom). - Context `(pmc:PreMonoidalCat K bobj mobj (@one _ _ _ (cartesian_terminal C))). - (* FIXME *) - (* - Definition ArrowInProgrammingLanguage := - @FreydCategory _ _ _ _ _ _ (@car_mn _ _ _ _ _ _ _ CC) _ _ _ _ pmc. - *) -End ArrowInLanguage. - -Section GArrowInLanguage. - Context (Guest:ProgrammingLanguageSMME). - Context (Host :ProgrammingLanguageSMME). - Definition GeneralizedArrowInLanguage := GeneralizedArrow Guest Host. - - (* FIXME - Definition ArrowsAreGeneralizedArrows : ArrowInProgrammingLanguage -> GeneralizedArrowInLanguage. - *) - Definition TwoLevelLanguage := Reification Guest Host (me_i Host). - - Context (GuestHost:TwoLevelLanguage). - - Definition FlatObject (x:TypesL _ _ Host) := - forall y1 y2, not ((reification_r_obj GuestHost y1 y2)=x). - - Definition FlatSubCategory := FullSubcategory (TypesL _ _ Host) FlatObject. - - Section Flattening. - - Context (F:Retraction (TypesL _ _ Host) FlatSubCategory). - Definition FlatteningOfReification := garrow_from_reification Guest Host GuestHost >>>> F. - Lemma FlatteningIsNotDestructive : - FlatteningOfReification >>>> retraction_retraction F >>>> RepresentableFunctor _ (me_i Host) ~~~~ GuestHost. - admit. - Qed. - - End Flattening. - -End GArrowInLanguage. - -Inductive NLevelLanguage : nat -> ProgrammingLanguageSMME -> Type := -| NLevelLanguage_zero : forall lang, NLevelLanguage O lang -| NLevelLanguage_succ : forall (L1 L2:ProgrammingLanguageSMME) n, - TwoLevelLanguage L1 L2 -> NLevelLanguage n L1 -> NLevelLanguage (S n) L2. - -Definition OmegaLevelLanguage : Type := - { f : nat -> ProgrammingLanguageSMME - & forall n, TwoLevelLanguage (f n) (f (S n)) }. - + Implicit Arguments ND [ Judgment ]. diff --git a/src/ProgrammingLanguageArrow.v b/src/ProgrammingLanguageArrow.v new file mode 100644 index 0000000..6bf0f24 --- /dev/null +++ b/src/ProgrammingLanguageArrow.v @@ -0,0 +1,68 @@ +(*********************************************************************************************************************************) +(* ProgrammingLanguageArrow *) +(* *) +(* Arrows in ProgrammingLanguages. *) +(* *) +(*********************************************************************************************************************************) + +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. +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 Enrichment_ch2_8. +Require Import RepresentableStructure_ch7_2. +Require Import FunctorCategories_ch7_7. + +Require Import NaturalDeduction. +Require Import NaturalDeductionCategory. + +Require Import ProgrammingLanguage. +Require Import ProgrammingLanguageGeneralizedArrow. +Require Import FreydCategories. + +Section ArrowInLanguage. + + Section ArrowInLanguage. + Context {MF}{mn:MonoidalCat TypesL (fun x => (fst_obj _ _ x),,(snd_obj _ _ x)) MF []} (CC:CartesianCat mn). + Context {Kehom}(K:@ECategory _ _ TypesL _ mn [] mn TypesL Kehom). + Context {bc:BinoidalCat (Underlying K) (@T_Branch _)}. + Context (pmc:@PreMonoidalCat _ _ _ _ bc (@one _ _ _ (car_terminal(CartesianCat:=CC)))). + Definition ArrowInProgrammingLanguage := @FreydCategory _ _ _ _ _ _ mn _ _ _ _ pmc. + End ArrowInLanguage. + + Definition ArrowsAreGeneralizedArrows (Host:ProgrammingLanguageSMME) + {mf}{mn}{cc}{kehom}{CC} + (arrow:ArrowInProgrammingLanguage Host _ _ CC mf mn cc kehom) : GeneralizedArrowInLanguage. + + Definition TwoLevelLanguage := Reification Guest Host (me_i Host). + + Context (GuestHost:TwoLevelLanguage). + + Definition FlatObject (x:TypesL _ _ Host) := + forall y1 y2, not ((reification_r_obj GuestHost y1 y2)=x). + + Definition FlatSubCategory := FullSubcategory (TypesL _ _ Host) FlatObject. + + Section Flattening. + + Context (F:Retraction (TypesL _ _ Host) FlatSubCategory). + Definition FlatteningOfReification := garrow_from_reification Guest Host GuestHost >>>> F. + Lemma FlatteningIsNotDestructive : + FlatteningOfReification >>>> retraction_retraction F >>>> HomFunctor _ (me_i Host) ~~~~ GuestHost. + admit. + Qed. + + End Flattening. + +End GArrowInLanguage. diff --git a/src/ProgrammingLanguageGeneralizedArrow.v b/src/ProgrammingLanguageGeneralizedArrow.v new file mode 100644 index 0000000..620ca9f --- /dev/null +++ b/src/ProgrammingLanguageGeneralizedArrow.v @@ -0,0 +1,62 @@ +(*********************************************************************************************************************************) +(* ProgrammingLanguageArrow *) +(* *) +(* Arrows in ProgrammingLanguages. *) +(* *) +(*********************************************************************************************************************************) + +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. +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 Enrichment_ch2_8. +Require Import RepresentableStructure_ch7_2. +Require Import FunctorCategories_ch7_7. + +Require Import NaturalDeduction. +Require Import NaturalDeductionCategory. + +Require Import FreydCategories. + +Require Import GeneralizedArrowFromReification. +Section GArrowInLanguage. + + Definition GeneralizedArrowInLanguage (Guest:ProgrammingLanguageSMME) (Host :ProgrammingLanguageSMME) + := GeneralizedArrow Guest Host. + + Definition ArrowsAreGeneralizedArrows (Host:ProgrammingLanguageSMME) + {mf}{mn}{cc}{kehom}{CC} + (arrow:ArrowInProgrammingLanguage Host _ _ CC mf mn cc kehom) : GeneralizedArrowInLanguage. + + Definition TwoLevelLanguage := Reification Guest Host (me_i Host). + + Context (GuestHost:TwoLevelLanguage). + + Definition FlatObject (x:TypesL _ _ Host) := + forall y1 y2, not ((reification_r_obj GuestHost y1 y2)=x). + + Definition FlatSubCategory := FullSubcategory (TypesL _ _ Host) FlatObject. + + Section Flattening. + + Context (F:Retraction (TypesL _ _ Host) FlatSubCategory). + Definition FlatteningOfReification := garrow_from_reification Guest Host GuestHost >>>> F. + Lemma FlatteningIsNotDestructive : + FlatteningOfReification >>>> retraction_retraction F >>>> HomFunctor _ (me_i Host) ~~~~ GuestHost. + admit. + Qed. + + End Flattening. + +End GArrowInLanguage. diff --git a/src/ProgrammingLanguageReification.v b/src/ProgrammingLanguageReification.v new file mode 100644 index 0000000..589f748 --- /dev/null +++ b/src/ProgrammingLanguageReification.v @@ -0,0 +1,39 @@ +(*********************************************************************************************************************************) +(* ProgrammingLanguageReification *) +(* *) +(* Reifications in ProgrammingLanguages. *) +(* *) +(*********************************************************************************************************************************) + +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. +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 Enrichment_ch2_8. +Require Import RepresentableStructure_ch7_2. +Require Import FunctorCategories_ch7_7. + +Require Import Reification. +Require Import NaturalDeduction. +Require Import NaturalDeductionCategory. +Require Import ProgrammingLanguage. + +Inductive NLevelLanguage : nat -> ProgrammingLanguageSMME -> Type := +| NLevelLanguage_zero : forall lang, NLevelLanguage O lang +| NLevelLanguage_succ : forall (L1 L2:ProgrammingLanguageSMME) n, + TwoLevelLanguage L1 L2 -> NLevelLanguage n L1 -> NLevelLanguage (S n) L2. + +Definition OmegaLevelLanguage : Type := + { f : nat -> ProgrammingLanguageSMME + & forall n, TwoLevelLanguage (f n) (f (S n)) }. diff --git a/src/Reification.v b/src/Reification.v index 2f2ba67..f60c43e 100644 --- a/src/Reification.v +++ b/src/Reification.v @@ -1,8 +1,8 @@ (*********************************************************************************************************************************) (* Reification: *) (* *) -(* A reification is a functor R from one enrichING category A to another enrichING category B which forms a commuting square *) -(* with every pair of hom-functors Hom(X,-):a->A and Hom(Y,-):b->B up to natural isomorphism. *) +(* A reification is a functor R from one enrichING category A to another enrichING category B which, for every X, forms *) +(* a commuting square with Hom(X,-):a->A and Hom(I,-):b->B (up to natural isomorphism). *) (* *) (*********************************************************************************************************************************) @@ -23,7 +23,7 @@ Require Import Coherence_ch7_8. Require Import Enrichment_ch2_8. Require Import RepresentableStructure_ch7_2. -Opaque RepresentableFunctor. +Opaque HomFunctor. Opaque functor_comp. Structure Reification (K:Enrichment) (C:Enrichment) (CI:C) := { reification_r_obj : K -> K -> C @@ -31,9 +31,9 @@ Structure Reification (K:Enrichment) (C:Enrichment) (CI:C) := ; reification_r : forall k:K, Functor K C (reification_r_obj k) ; reification_rstar_f : Functor (enr_v K) (enr_v C) reification_rstar_obj ; reification_rstar : MonoidalFunctor (enr_v_mon K) (enr_v_mon C) reification_rstar_f -; reification_commutes : ∀ k, reification_r k >>>> RepresentableFunctor C CI <~~~> RepresentableFunctor K k >>>> reification_rstar_f +; reification_commutes : ∀ k, reification_r k >>>> HomFunctor C CI <~~~> HomFunctor K k >>>> reification_rstar_f }. -Transparent RepresentableFunctor. +Transparent HomFunctor. Transparent functor_comp. Coercion reification_rstar : Reification >-> MonoidalFunctor. diff --git a/src/ReificationCategory.v b/src/ReificationCategory.v index 0227f60..e57df4d 100644 --- a/src/ReificationCategory.v +++ b/src/ReificationCategory.v @@ -26,10 +26,13 @@ Require Import Reification. Require Import WeakFunctorCategory. Require Import SmallSMMEs. -(* Technically reifications form merely a *semicategory* (no identity +(* + * Technically reifications form merely a *semicategory* (no identity * maps), but one can always freely adjoin identity maps (and nothing * else) to a semicategory to get a category whose non-identity-map - * portion is identical to the original semicategory + * portion is identical to the original semicategory (closing under + * composition after putting in the identity maps never produces any + * additional maps) * * Also, technically this category has ALL enrichments (not just the * surjective monic monoidal ones), though there maps OUT OF only the @@ -67,19 +70,19 @@ Definition compose_reifications (s0 s1 s2:SMMEs) : ; reification_r := fun K => (reification_r X K) >>>> (reification_r X0 (mon_i s1)) |}. intro K. - set (ni_associativity (reification_r X K) (reification_r X0 (mon_i s1)) (RepresentableFunctor s2 (mon_i s2))) as q. + set (ni_associativity (reification_r X K) (reification_r X0 (mon_i s1)) (HomFunctor s2 (mon_i s2))) as q. eapply ni_comp. apply q. clear q. set (reification_commutes X K) as comm1. set (reification_commutes X0 (mon_i s1)) as comm2. - set (RepresentableFunctor s0 K) as a in *. + set (HomFunctor s0 K) as a in *. set (reification_rstar_f X) as a' in *. set (reification_rstar_f X0) as x in *. set (reification_r X K) as b in *. set (reification_r X0 (mon_i s1)) as c in *. - set (RepresentableFunctor s2 (mon_i s2)) as c' in *. - set (RepresentableFunctor s1 (mon_i s1)) as b' in *. + set (HomFunctor s2 (mon_i s2)) as c' in *. + set (HomFunctor s1 (mon_i s1)) as b' in *. apply (ni_comp(F2:=b >>>> (b' >>>> x))). apply (@ni_respects _ _ _ _ _ _ _ _ _ _ b _ b _ (c >>>> c') _ (b' >>>> x)). apply ni_id. diff --git a/src/ReificationFromGeneralizedArrow.v b/src/ReificationFromGeneralizedArrow.v index e6f8ad6..a53b2e2 100644 --- a/src/ReificationFromGeneralizedArrow.v +++ b/src/ReificationFromGeneralizedArrow.v @@ -27,7 +27,7 @@ Require Import GeneralizedArrow. Definition reification_from_garrow (K:Enrichment) {ce} (C:MonoidalEnrichment ce) (garrow : GeneralizedArrow K C) : Reification K C (mon_i C). refine - {| reification_r := fun k:K => RepresentableFunctor K k >>>> garrow + {| reification_r := fun k:K => HomFunctor K k >>>> garrow ; reification_rstar_f := garrow >>>> me_mf C ; reification_rstar := MonoidalFunctorsCompose _ _ _ _ _ garrow (me_mf C) |}. diff --git a/src/ReificationsAndGeneralizedArrows.v b/src/ReificationsAndGeneralizedArrows.v index d59b030..6a615ac 100644 --- a/src/ReificationsAndGeneralizedArrows.v +++ b/src/ReificationsAndGeneralizedArrows.v @@ -1,7 +1,8 @@ (*********************************************************************************************************************************) (* ReificationsAndGeneralizedArrows: *) (* *) -(* The category of generalized arrows and the category of reifications are equivalent categories. *) +(* For each pair of enrichments E1 and E2, there is a bijection between the generalized arrows E1->E2 and the reifications *) +(* E1->E2 *) (* *) (*********************************************************************************************************************************) @@ -53,7 +54,7 @@ Section ReificationsEquivalentToGeneralizedArrows. Definition roundtrip_lemma `(K:SurjectiveEnrichment se) `(C:MonicMonoidalEnrichment e ce) (reification : Reification K C (me_i C)) - := roundtrip_lemma' (RepresentableFunctor C (me_i C)) (ffme_mf_full C) (ffme_mf_faithful C) (step1_functor K C reification). + := roundtrip_lemma' (HomFunctor C (me_i C)) (ffme_mf_full C) (ffme_mf_faithful C) (step1_functor K C reification). Lemma roundtrip_reification_to_reification `(K:SurjectiveEnrichment se) `(C:MonicMonoidalEnrichment e ce) (reification : Reification K C (me_i C)) @@ -61,7 +62,7 @@ Section ReificationsEquivalentToGeneralizedArrows. simpl. unfold mon_f. unfold garrow_functor. - apply (if_comp(F2:=(step1_functor K C reification >>>> InclusionFunctor _ (FullImage (RepresentableFunctor C (me_i C)))))). + apply (if_comp(F2:=(step1_functor K C reification >>>> InclusionFunctor _ (FullImage (HomFunctor C (me_i C)))))). apply (@step1_niso _ K _ _ C reification). apply (if_inv (roundtrip_lemma K C reification)). Qed. @@ -69,10 +70,10 @@ Section ReificationsEquivalentToGeneralizedArrows. Lemma roundtrip_garrow_to_garrow `(K:SurjectiveEnrichment se) `(C:MonicMonoidalEnrichment e ce) (garrow : GeneralizedArrow K C) : garrow ≃ garrow_from_reification K C (reification_from_garrow K C garrow). - apply (ffc_functor_weakly_monic _ (ffme_mf_conservative C)). + apply (ffc_functor_weakly_monic _ (ffme_mf_full C) (ffme_mf_faithful C) (ffme_mf_conservative C) (ffme_mf_conservative C)). apply if_inv. apply (if_comp(F2:=(step1_functor K C (reification_from_garrow K C garrow) - >>>> InclusionFunctor _ (FullImage (RepresentableFunctor C (me_i C)))))). + >>>> InclusionFunctor _ (FullImage (HomFunctor C (me_i C)))))). unfold mf_f. unfold garrow_from_reification. unfold garrow_functor. diff --git a/src/ReificationsIsomorphicToGeneralizedArrows.v b/src/ReificationsIsomorphicToGeneralizedArrows.v index 25febe0..1542b46 100644 --- a/src/ReificationsIsomorphicToGeneralizedArrows.v +++ b/src/ReificationsIsomorphicToGeneralizedArrows.v @@ -33,16 +33,9 @@ Require Import WeakFunctorCategory. Section ReificationsIsomorphicToGeneralizedArrows. - (* - Lemma step1_lemma (s0 s1 s2:SmallSMMEs.SMMEs)(r01:Reification s0 s1 (me_i s1))(r12:Reification s1 s2 (me_i s2)) : - ∀A : enr_v_mon s0, - garrow_fobj' s1 s2 r12 (ehom(ECategory:=s1) (me_i s1) (garrow_fobj s0 s1 r01 A)) - ≅ garrow_fobj' s0 s2 (compose_reifications s0 s1 s2 r01 r12) A. - *) - Lemma step1_lemma (s0 s1 s2:SmallSMMEs.SMMEs)(r01:Reification s0 s1 (me_i s1))(r12:Reification s1 s2 (me_i s2)) : (step1_functor s0 s1 r01 >>>> - InclusionFunctor (enr_v s1) (FullImage (RepresentableFunctor s1 (me_i s1)))) >>>> step1_functor s1 s2 r12 + InclusionFunctor (enr_v s1) (FullImage (HomFunctor s1 (me_i s1)))) >>>> step1_functor s1 s2 r12 ≃ step1_functor s0 s2 (compose_reifications s0 s1 s2 r01 r12). admit. Defined. @@ -152,7 +145,7 @@ Section ReificationsIsomorphicToGeneralizedArrows. apply if_id. unfold mf_f; simpl. apply (if_associativity - ((ga_functor g0 >>>> RepresentableFunctor s0 (mon_i s0))) (ga_functor g) (RepresentableFunctor s2 (me_i s2))). + ((ga_functor g0 >>>> HomFunctor s0 (mon_i s0))) (ga_functor g) (HomFunctor s2 (me_i s2))). Defined. Definition M2 (c1 c2 : SmallSMMEs.SMMEs) : @@ -221,20 +214,19 @@ Section ReificationsIsomorphicToGeneralizedArrows. apply if_id. unfold mf_f; simpl. apply (if_respects - (F0:=((garrow_functor s1 s0 r >>>> RepresentableFunctor s0 (mon_i s0)) >>>> garrow_functor s0 s2 r0)) + (F0:=((garrow_functor s1 s0 r >>>> HomFunctor s0 (mon_i s0)) >>>> garrow_functor s0 s2 r0)) (F1:=(garrow_functor s1 s2 (compose_reifications s1 s0 s2 r r0))) - (G0:=(RepresentableFunctor s2 (mon_i s2))) - (G1:=(RepresentableFunctor s2 (mon_i s2)))); + (G0:=(HomFunctor s2 (mon_i s2))) + (G1:=(HomFunctor s2 (mon_i s2)))); [ idtac | apply if_id ]. eapply if_comp. idtac. - apply (if_associativity (garrow_functor s1 s0 r) (RepresentableFunctor s0 (mon_i s0)) (garrow_functor s0 s2 r0)). - Set Printing Coercions. + apply (if_associativity (garrow_functor s1 s0 r) (HomFunctor s0 (mon_i s0)) (garrow_functor s0 s2 r0)). idtac. unfold garrow_functor at 1. unfold step2_functor at 1. set (roundtrip_lemma' - (RepresentableFunctor (enr_c (smme_e s0)) (me_i (smme_mon s0))) + (HomFunctor (enr_c (smme_e s0)) (me_i (smme_mon s0))) (ffme_mf_full (smme_mee s0)) (ffme_mf_faithful (smme_mee s0)) (step1_functor (smme_see s1) (smme_mee s0) r) ) as q. @@ -243,7 +235,6 @@ Section ReificationsIsomorphicToGeneralizedArrows. (G1:=garrow_functor (smme_see s0) (smme_mee s2) r0) q (if_id _)) as q'. apply (if_comp q'). - Unset Printing Coercions. clear q' q. unfold garrow_functor at 2. unfold garrow_functor at 1. @@ -268,7 +259,7 @@ Section ReificationsIsomorphicToGeneralizedArrows. clear H. unfold mf_f in q. apply (if_respects(F0:=ga_functor g)(F1:=garrow_functor s1 s2 (reification_from_garrow s1 s2 g)) - (G0:=RepresentableFunctor s2 (mon_i s2))(G1:=RepresentableFunctor s2 (mon_i s2))). + (G0:=HomFunctor s2 (mon_i s2))(G1:=HomFunctor s2 (mon_i s2))). apply q. apply if_id. diff --git a/src/WeakFunctorCategory.v b/src/WeakFunctorCategory.v index 5e52faa..b6adae6 100644 --- a/src/WeakFunctorCategory.v +++ b/src/WeakFunctorCategory.v @@ -21,8 +21,6 @@ Require Import NaturalTransformations_ch7_4. Require Import NaturalIsomorphisms_ch7_5. Require Import MonoidalCategories_ch7_8. Require Import Coherence_ch7_8. -(*Require Import Enrichment_ch2_8.*) -(*Require Import RepresentableStructure_ch7_2.*) Section WeakFunctorCategory. diff --git a/src/categories b/src/categories index 18d9414..a0b31d2 160000 --- a/src/categories +++ b/src/categories @@ -1 +1 @@ -Subproject commit 18d94149267db9cf2e8e93977c5506278309173d +Subproject commit a0b31d2cc2b6cf7184efe4ff01ad682749f779ad -- 1.7.10.4