-coqc := coqc -noglob
+coqc := coqc -noglob -opt
coqfiles := $(shell find src -name \*.v | grep -v \\\#)
allfiles := $(coqfiles) $(shell find src -name \*.hs | grep -v \\\#)
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
Require Import ReificationsIsomorphicToGeneralizedArrows.
-(*Require Import HaskStrongCategory.*)
-
Open Scope string_scope.
Extraction Language Haskell.
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'".
end.
- (* core-to-string (-dcoqpass) *)
-
Definition header : string :=
"\documentclass[9pt]{article}"+++eol+++
"\usepackage{amsmath}"+++eol+++
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)) (
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)) (
: 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) :
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).
(*********************************************************************************************************************************)
(* GeneralizedArrowFromReification: *)
(* *)
-(* Turn a generalized arrow into a reification *)
+(* Turn a reification into a generalized arrow *)
(* *)
(*********************************************************************************************************************************)
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;
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;
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
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*)
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 :=
(vec2list (sac_types sac Γ avars))))
|- [weakLT' (branchtype @@ lev)]
}.
-(*Coercion pcb_scb : ProofCaseBranch >-> StrongAltCon.*)
Implicit Arguments ProofCaseBranch [ ].
(* Figure 3, production $\vdash_E$, Uniform rules *)
(* λ^α 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]]
| 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 }),
(* 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)
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.
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)
; 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 :=
+++ /dev/null
-(*********************************************************************************************************************************)
-(* 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.
-*)
-
-
-
rewrite app_comm_cons.
reflexivity.
*)
-admit.
+ admit.
Qed.
Lemma strip_distinct a y : (not (In a (leaves y))) -> stripOutVars (a :: nil) y = y.
| 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}
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 ,
uniqM f => f us >>= fun x => OK (snd x)
end.
-End HaskStrongToWeak.
\ No newline at end of file
+End HaskStrongToWeak.
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.
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] ].
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 Δ) :=
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) ->
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).
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 Γ Δ).
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:
*
* (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.
*)
(*
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 *)
`(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
}.
(*
- * 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 []
| 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).
| 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}.
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
}.
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]
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]
| 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',
@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',
@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.
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
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 :
apply nd_structural_cancelr; auto.
Defined.
-
- (* Structure ExpressionAlgebra (sig:Signature) := *)
-
End Judgments_Category.
Close Scope pf_scope.
+++ /dev/null
-(*********************************************************************************************************************************)
-(* 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.
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 *)
{
}.
+ 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 :=
}.
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 ].
--- /dev/null
+(*********************************************************************************************************************************)
+(* 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.
--- /dev/null
+(*********************************************************************************************************************************)
+(* 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.
--- /dev/null
+(*********************************************************************************************************************************)
+(* 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)) }.
(*********************************************************************************************************************************)
(* 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). *)
(* *)
(*********************************************************************************************************************************)
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
; 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.
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
; 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.
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)
|}.
(*********************************************************************************************************************************)
(* 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 *)
(* *)
(*********************************************************************************************************************************)
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))
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.
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.
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.
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) :
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.
(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.
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.
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.
-Subproject commit 18d94149267db9cf2e8e93977c5506278309173d
+Subproject commit a0b31d2cc2b6cf7184efe4ff01ad682749f779ad
projects / coq-hetmet.git / commitdiff