From e539b49ae3148ab1967b5ea0709734171180b86d Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 11 Apr 2011 07:24:23 +0000 Subject: [PATCH] unbreak lots more stuff --- src/All.v | 3 +- src/Enrichments.v | 6 +- src/GeneralizedArrow.v | 23 +-- src/GeneralizedArrowFromReification.v | 4 +- src/HaskProofFlattener.v | 117 +++++------ src/HaskProofStratified.v | 333 +++++++++++++++++--------------- src/ProgrammingLanguage.v | 18 +- src/ProgrammingLanguageArrow.v | 49 ++--- src/ProgrammingLanguageFlattening.v | 69 ++++--- src/ProgrammingLanguageReification.v | 45 ++--- src/ReificationFromGeneralizedArrow.v | 2 +- src/ReificationsAndGeneralizedArrows.v | 3 +- src/categories | 2 +- 13 files changed, 355 insertions(+), 319 deletions(-) diff --git a/src/All.v b/src/All.v index 25fa85d..d4956dd 100644 --- a/src/All.v +++ b/src/All.v @@ -1,7 +1,6 @@ Require Import ExtractionMain. -Require Import ProgrammingLanguageGeneralizedArrow. -Require Import ProgrammingLanguageFlattening. Require Import ProgrammingLanguageArrow. Require Import ProgrammingLanguageReification. +Require Import ProgrammingLanguageFlattening. Require Import ReificationsIsomorphicToGeneralizedArrows. diff --git a/src/Enrichments.v b/src/Enrichments.v index 5fa684e..7c24bfa 100644 --- a/src/Enrichments.v +++ b/src/Enrichments.v @@ -37,7 +37,8 @@ Structure Enrichment := ; enr_c_obj : Type ; enr_c_hom : enr_c_obj -> enr_c_obj -> enr_v ; enr_c : ECategory enr_v_mon enr_c_obj enr_c_hom -; enr_c_bin : EBinoidalCat enr_c +; enr_c_bobj : enr_c_obj -> enr_c_obj -> enr_c_obj +; enr_c_bin : EBinoidalCat enr_c enr_c_bobj ; enr_c_i : enr_c ; enr_c_pm : PreMonoidalCat enr_c_bin enr_c_i ; enr_c_center := Center enr_c_bin @@ -67,7 +68,8 @@ Structure SurjectiveEnrichment := ; senr_v_pmon : PreMonoidalCat senr_v_bin senr_v_i ; senr_v_mon : MonoidalCat senr_v_pmon ; senr_c : ECategory senr_v_mon senr_c_obj senr_c_hom -; senr_c_bin : EBinoidalCat senr_c +; senr_c_bobj : senr_c_obj -> senr_c_obj -> senr_c_obj +; senr_c_bin : EBinoidalCat senr_c senr_c_bobj ; senr_c_i : senr_c ; senr_c_pm : PreMonoidalCat senr_c_bin senr_c_i }. diff --git a/src/GeneralizedArrow.v b/src/GeneralizedArrow.v index 303baef..f246cbe 100644 --- a/src/GeneralizedArrow.v +++ b/src/GeneralizedArrow.v @@ -26,24 +26,19 @@ Require Import PreMonoidalCenter. Require Import PreMonoidalCategories. Require Import BinoidalCategories. -Class GeneralizedArrow (K:Enrichment) {ce}(C:MonoidalEnrichment ce) := -{ ga_functor_obj : enr_v K -> ce -; ga_functor : Functor (enr_v_mon K) (enr_c_pm ce) ga_functor_obj -; ga_functor_monoidal : PreMonoidalFunctor (enr_v_mon K) (enr_c_pm ce) ga_functor +Class GeneralizedArrow (K:Enrichment)(C:Enrichment) := +{ ga_functor_obj : enr_v K -> C +; ga_functor : Functor (enr_v_mon K) (enr_c_pm C) ga_functor_obj +; ga_functor_monoidal : PreMonoidalFunctor (enr_v_mon K) (enr_c_pm C) ga_functor (* We require that the host language (but NOT the guest language) be pure, i.e. all morphisms central, to simplify * things. If this doesn't suit you, just consider the "host language" here to be the pure sublanguage of the * host language, and toss on the inclusion functor to the full language *) -; ga_host_lang_pure : CommutativeCat (enr_c_pm ce) - -(* -; ga_functor : Functor (enr_v_mon K) (Center_is_Monoidal (enr_c_pm ce)) ga_functor_obj -; ga_functor_monoidal : MonoidalFunctor (enr_v_mon K) (Center_is_Monoidal (enr_c_pm ce)) ga_functor -*) +; ga_host_lang_pure : CommutativeCat (enr_c_pm C) }. Coercion ga_functor_monoidal : GeneralizedArrow >-> PreMonoidalFunctor. -Implicit Arguments GeneralizedArrow [ [ce] ]. -Implicit Arguments ga_functor_obj [ K ce C ]. -Implicit Arguments ga_functor [ K ce C ]. -Implicit Arguments ga_functor_monoidal [ K ce C ]. +Implicit Arguments GeneralizedArrow [ ]. +Implicit Arguments ga_functor_obj [ K C ]. +Implicit Arguments ga_functor [ K C ]. +Implicit Arguments ga_functor_monoidal [ K C ]. diff --git a/src/GeneralizedArrowFromReification.v b/src/GeneralizedArrowFromReification.v index 9ff0d4d..b5e3147 100644 --- a/src/GeneralizedArrowFromReification.v +++ b/src/GeneralizedArrowFromReification.v @@ -916,7 +916,7 @@ Implicit Arguments mf_i [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] apply (fmor_respects (-⋉ F b)). apply iso_comp2. Qed. -*) + Lemma cancell_coherent (b:enr_v K) : #(pmon_cancell(PreMonoidalCat:=enr_c_pm C) (garrow_functor b)) ~~ (#(iso_id (enr_c_i C)) ⋉ garrow_functor b >>> @@ -1162,7 +1162,7 @@ Implicit Arguments mf_i [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] apply assoc_coherent. Defined. - Definition garrow_from_reification : GeneralizedArrow K CM := + Definition garrow_from_reification : GeneralizedArrow K C := {| ga_functor_monoidal := garrow_monoidal ; ga_host_lang_pure := reification_host_lang_pure _ _ _ reification |}. diff --git a/src/HaskProofFlattener.v b/src/HaskProofFlattener.v index fcc2a37..7b70e6e 100644 --- a/src/HaskProofFlattener.v +++ b/src/HaskProofFlattener.v @@ -116,13 +116,12 @@ Section HaskProofFlattener. admit. Defined. - Definition guestJudgmentAsGArrowType {Γ}{Δ}{ec}(lt:PCFJudg Γ Δ ec) : HaskType Γ ★ := + Definition guestJudgmentAsGArrowType {Γ}{Δ}(lt:PCFJudg Γ Δ) : HaskType Γ ★ := match lt with - pcfjudg x y => - (mkGA (tensorizeType x) (tensorizeType y)) + (x,y) => (mkGA (tensorizeType x) (tensorizeType y)) end. - Definition obact {Γ}{Δ} ec (X:Tree ??(PCFJudg Γ Δ ec)) : Tree ??(LeveledHaskType Γ ★) := + Definition obact {Γ}{Δ} (X:Tree ??(PCFJudg Γ Δ)) : Tree ??(LeveledHaskType Γ ★) := mapOptionTree guestJudgmentAsGArrowType X @@@ nil. Hint Constructors Rule_Flat. @@ -133,11 +132,11 @@ Section HaskProofFlattener. * it might help to have the definition for "Inductive ND" (see * NaturalDeduction.v) handy as a cross-reference. *) -(* + Hint Constructors Rule_Flat. Definition FlatteningFunctor_fmor {Γ}{Δ}{ec} : forall h c, - (h~~{JudgmentsL _ _ (PCF _ Γ Δ ec)}~~>c) -> - ((obact ec h)~~{TypesL _ _ (SystemFCa Γ Δ)}~~>(obact ec c)). + (h~~{JudgmentsL (PCF Γ Δ ec)}~~>c) -> + ((obact(Δ:=ec) h)~~{TypesL (SystemFCa Γ Δ)}~~>(obact(Δ:=ec) c)). set (@nil (HaskTyVar Γ ★)) as lev. @@ -146,40 +145,49 @@ Section HaskProofFlattener. induction X; simpl. (* the proof from no hypotheses of no conclusions (nd_id0) becomes RVoid *) - apply nd_rule; apply (org_fc _ _ (RVoid _ _ )). auto. + apply nd_rule; apply (org_fc _ _ [] [(_,_)] (RVoid _ _)). apply Flat_RVoid. (* the proof from hypothesis X of conclusion X (nd_id1) becomes RVar *) - apply nd_rule; apply (org_fc _ _ (RVar _ _ _ _)). auto. + apply nd_rule; apply (org_fc _ _ [] [(_,_)] (RVar _ _ _ _)). apply Flat_RVar. (* the proof from hypothesis X of no conclusions (nd_weak) becomes RWeak;;RVoid *) eapply nd_comp; [ idtac | eapply nd_rule - ; eapply (org_fc _ _ (RArrange _ _ _ _ _ (RWeak _))) + ; eapply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RWeak _))) ; auto ]. eapply nd_rule. - eapply (org_fc _ _ (RVoid _ _)); auto. - + eapply (org_fc _ _ [] [(_,_)] (RVoid _ _)); auto. apply Flat_RVoid. + apply Flat_RArrange. + (* the proof from hypothesis X of two identical conclusions X,,X (nd_copy) becomes RVar;;RJoin;;RCont *) - eapply nd_comp; [ idtac | eapply nd_rule; eapply (org_fc _ _ (RArrange _ _ _ _ _ (RCont _))) ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCont _))) ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. - set (snd_initial(SequentND:=@pl_snd _ _ _ _ (SystemFCa Γ Δ)) - (mapOptionTree guestJudgmentAsGArrowType h @@@ lev)) as q. + set (snd_initial(SequentND:=pl_snd(ProgrammingLanguage:=SystemFCa Γ Δ)) + (mapOptionTree (guestJudgmentAsGArrowType(Δ:=ec)) h @@@ lev)) as q. eapply nd_comp. eapply nd_prod. apply q. apply q. apply nd_rule. - eapply (org_fc _ _ (RJoin _ _ _ _ _ _ )). - auto. - auto. + eapply (org_fc _ _ ([(_,_)],,[(_,_)]) [(_,_)] (RJoin _ _ _ _ _ _ )). + destruct h; simpl. + destruct o. + simpl. + apply Flat_RJoin. + apply Flat_RJoin. + apply Flat_RJoin. + apply Flat_RArrange. (* nd_prod becomes nd_llecnac;;nd_prod;;RJoin *) eapply nd_comp. apply (nd_llecnac ;; nd_prod IHX1 IHX2). apply nd_rule. - eapply (org_fc _ _ (RJoin _ _ _ _ _ _ )). - auto. + eapply (org_fc _ _ ([(_,_)],,[(_,_)]) [(_,_)] (RJoin _ _ _ _ _ _ )). + apply (Flat_RJoin Γ Δ (mapOptionTree guestJudgmentAsGArrowType h1 @@@ nil) + (mapOptionTree guestJudgmentAsGArrowType h2 @@@ nil) + (mapOptionTree guestJudgmentAsGArrowType c1 @@@ nil) + (mapOptionTree guestJudgmentAsGArrowType c2 @@@ nil)). (* nd_comp becomes pl_subst (aka nd_cut) *) eapply nd_comp. @@ -192,39 +200,39 @@ Section HaskProofFlattener. (* nd_cancell becomes RVar;;RuCanL *) eapply nd_comp; - [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanL _))) ]. - apply (snd_initial(SequentND:=@pl_cnd _ _ _ _ (SystemFCa Γ Δ))). - auto. + [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RuCanL _))) ]. + apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))). + apply Flat_RArrange. (* nd_cancelr becomes RVar;;RuCanR *) eapply nd_comp; - [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanR _))) ]. - apply (snd_initial(SequentND:=@pl_cnd _ _ _ _ (SystemFCa Γ Δ))). - auto. + [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RuCanR _))) ]. + apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))). + apply Flat_RArrange. (* nd_llecnac becomes RVar;;RCanL *) eapply nd_comp; - [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanL _))) ]. - apply (snd_initial(SequentND:=@pl_cnd _ _ _ _ (SystemFCa Γ Δ))). - auto. + [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCanL _))) ]. + apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))). + apply Flat_RArrange. (* nd_rlecnac becomes RVar;;RCanR *) eapply nd_comp; - [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanR _))) ]. - apply (snd_initial(SequentND:=@pl_cnd _ _ _ _ (SystemFCa Γ Δ))). - auto. + [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCanR _))) ]. + apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))). + apply Flat_RArrange. (* nd_assoc becomes RVar;;RAssoc *) eapply nd_comp; - [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RAssoc _ _ _))) ]. - apply (snd_initial(SequentND:=@pl_cnd _ _ _ _ (SystemFCa Γ Δ))). - auto. + [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RAssoc _ _ _))) ]. + apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))). + apply Flat_RArrange. (* nd_cossa becomes RVar;;RCossa *) eapply nd_comp; - [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCossa _ _ _))) ]. - apply (snd_initial(SequentND:=@pl_cnd _ _ _ _ (SystemFCa Γ Δ))). - auto. + [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCossa _ _ _))) ]. + apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))). + apply Flat_RArrange. destruct r as [r rp]. refine (match rp as R in @Rule_PCF _ _ _ H C _ with @@ -316,9 +324,11 @@ Section HaskProofFlattener. destruct case_RNote. eapply nd_comp. eapply nd_rule. - eapply (org_fc _ _ (RVar _ _ _ _)) . auto. + eapply (org_fc _ _ [] [(_,_)] (RVar _ _ _ _)) . auto. + apply Flat_RVar. apply nd_rule. - apply (org_fc _ _ (RNote _ _ _ _ _ n)). auto. + apply (org_fc _ _ [(_,_)] [(_,_)] (RNote _ _ _ _ _ n)). auto. + apply Flat_RNote. destruct case_RVar. (* ga_id *) @@ -346,23 +356,23 @@ Section HaskProofFlattener. Defined. - Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL _ _ (PCF _ Γ Δ ec)) (TypesL _ _ (SystemFCa Γ Δ)) (obact ec) := + Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) := { fmor := FlatteningFunctor_fmor }. admit. admit. admit. Defined. -(* - Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg). - refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros. - unfold ReificationFunctor_fmor; simpl. - admit. - unfold ReificationFunctor_fmor; simpl. - admit. - unfold ReificationFunctor_fmor; simpl. - admit. - Defined. + (* + Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg). + refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros. + unfold ReificationFunctor_fmor; simpl. + admit. + unfold ReificationFunctor_fmor; simpl. + admit. + unfold ReificationFunctor_fmor; simpl. + admit. + Defined. Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME. refine {| plsmme_pl := PCF n Γ Δ |}. @@ -383,7 +393,7 @@ Section HaskProofFlattener. admit. (* ... and the retraction exists *) Defined. -*) + *) (* Any particular proof in HaskProof is only finitely large, so it uses only finitely many levels of nesting, so * it falls within (SystemFCa n) for some n. This function calculates that "n" and performs the translation *) (* @@ -391,8 +401,7 @@ Section HaskProofFlattener. forall h c (pf:ND Rule h c), { n:nat & h ~~{JudgmentsL (SystemFCa_SMME n)}~~> c }. *) - (* for every n we have a functor from the category of (n+1)-bounded proofs to the category of n-bounded proofs *) -*) + End HaskProofFlattener. diff --git a/src/HaskProofStratified.v b/src/HaskProofStratified.v index 5c5f68a..ee475da 100644 --- a/src/HaskProofStratified.v +++ b/src/HaskProofStratified.v @@ -55,18 +55,22 @@ Open Scope nd_scope. *) Section HaskProofStratified. + Section PCF. + Context (ndr_systemfc:@ND_Relation _ Rule). - Inductive PCFJudg Γ (Δ:CoercionEnv Γ) (ec:HaskTyVar Γ ★) := - pcfjudg : Tree ??(HaskType Γ ★) -> Tree ??(HaskType Γ ★) -> PCFJudg Γ Δ ec. - Implicit Arguments pcfjudg [ [Γ] [Δ] [ec] ]. + Context Γ (Δ:CoercionEnv Γ). + Definition PCFJudg (ec:HaskTyVar Γ ★) := + @prod (Tree ??(HaskType Γ ★)) (Tree ??(HaskType Γ ★)). + Definition pcfjudg (ec:HaskTyVar Γ ★) := + @pair (Tree ??(HaskType Γ ★)) (Tree ??(HaskType Γ ★)). (* given an PCFJudg at depth (ec::depth) we can turn it into an PCFJudg * from depth (depth) by wrapping brackets around everything in the * succedent and repopulating *) - Definition brakify {Γ}{Δ}{ec} (j:PCFJudg Γ Δ ec) : Judg := + Definition brakify {ec} (j:PCFJudg ec) : Judg := match j with - pcfjudg Σ τ => Γ > Δ > (Σ@@@(ec::nil)) |- (mapOptionTree (fun t => HaskBrak ec t) τ @@@ nil) + (Σ,τ) => Γ > Δ > (Σ@@@(ec::nil)) |- (mapOptionTree (fun t => HaskBrak ec t) τ @@@ nil) end. Definition pcf_vars {Γ}(ec:HaskTyVar Γ ★)(t:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★) @@ -77,13 +81,13 @@ Section HaskProofStratified. end end) t. - Inductive MatchingJudgments {Γ}{Δ}{ec} : Tree ??(PCFJudg Γ Δ ec) -> Tree ??Judg -> Type := + Inductive MatchingJudgments {ec} : Tree ??(PCFJudg ec) -> Tree ??Judg -> Type := | match_nil : MatchingJudgments [] [] | match_branch : forall a b c d, MatchingJudgments a b -> MatchingJudgments c d -> MatchingJudgments (a,,c) (b,,d) | match_leaf : forall Σ τ lev, MatchingJudgments - [pcfjudg (pcf_vars ec Σ) τ ] + [((pcf_vars ec Σ) , τ )] [Γ > Δ > Σ |- (mapOptionTree (HaskBrak ec) τ @@@ lev)]. Definition fc_vars {Γ}(ec:HaskTyVar Γ ★)(t:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★) @@ -94,56 +98,69 @@ Section HaskProofStratified. end end) t. - Definition pcfjudg2judg {Γ}{Δ:CoercionEnv Γ} ec (cj:PCFJudg Γ Δ ec) := - match cj with pcfjudg Σ τ => Γ > Δ > (Σ @@@ (ec::nil)) |- (τ @@@ (ec::nil)) end. + Definition pcfjudg2judg ec (cj:PCFJudg ec) := + match cj with (Σ,τ) => Γ > Δ > (Σ @@@ (ec::nil)) |- (τ @@@ (ec::nil)) end. (* Rules allowed in PCF; i.e. rules we know how to turn into GArrows *) (* Rule_PCF consists of the rules allowed in flat PCF: everything except *) (* AppT, AbsT, AppC, AbsC, Cast, Global, and some Case statements *) - Inductive Rule_PCF {Γ}{Δ:CoercionEnv Γ} (ec:HaskTyVar Γ ★) - : forall (h c:Tree ??(PCFJudg Γ Δ ec)), Rule (mapOptionTree (pcfjudg2judg ec) h) (mapOptionTree (pcfjudg2judg ec) c) -> Type := - | PCF_RArrange : ∀ x y t a, Rule_PCF ec [pcfjudg _ _ ] [ pcfjudg _ _ ] (RArrange Γ Δ (x@@@(ec::nil)) (y@@@(ec::nil)) (t@@@(ec::nil)) a) - | PCF_RLit : ∀ lit , Rule_PCF ec [ ] [ pcfjudg [] [_] ] (RLit Γ Δ lit (ec::nil)) - | PCF_RNote : ∀ Σ τ n , Rule_PCF ec [pcfjudg _ [_]] [ pcfjudg _ [_] ] (RNote Γ Δ (Σ@@@(ec::nil)) τ (ec::nil) n) - | PCF_RVar : ∀ σ , Rule_PCF ec [ ] [ pcfjudg [_] [_] ] (RVar Γ Δ σ (ec::nil) ) - | PCF_RLam : ∀ Σ tx te , Rule_PCF ec [pcfjudg (_,,[_]) [_] ] [ pcfjudg _ [_] ] (RLam Γ Δ (Σ@@@(ec::nil)) tx te (ec::nil) ) + Inductive Rule_PCF (ec:HaskTyVar Γ ★) + : forall (h c:Tree ??(PCFJudg ec)), Rule (mapOptionTree (pcfjudg2judg ec) h) (mapOptionTree (pcfjudg2judg ec) c) -> Type := + | PCF_RArrange : ∀ x y t a, Rule_PCF ec [(_, _)] [(_, _)] (RArrange Γ Δ (x@@@(ec::nil)) (y@@@(ec::nil)) (t@@@(ec::nil)) a) + | PCF_RLit : ∀ lit , Rule_PCF ec [ ] [ ([],[_]) ] (RLit Γ Δ lit (ec::nil)) + | PCF_RNote : ∀ Σ τ n , Rule_PCF ec [(_,[_])] [(_,[_])] (RNote Γ Δ (Σ@@@(ec::nil)) τ (ec::nil) n) + | PCF_RVar : ∀ σ , Rule_PCF ec [ ] [([_],[_])] (RVar Γ Δ σ (ec::nil) ) + | PCF_RLam : ∀ Σ tx te , Rule_PCF ec [((_,,[_]),[_])] [(_,[_])] (RLam Γ Δ (Σ@@@(ec::nil)) tx te (ec::nil) ) | PCF_RApp : ∀ Σ Σ' tx te , - Rule_PCF ec ([pcfjudg _ [_]],,[pcfjudg _ [_]]) [pcfjudg (_,,_) [_]] + Rule_PCF ec ([(_,[_])],,[(_,[_])]) [((_,,_),[_])] (RApp Γ Δ (Σ@@@(ec::nil))(Σ'@@@(ec::nil)) tx te (ec::nil)) | PCF_RLet : ∀ Σ Σ' σ₂ p, - Rule_PCF ec ([pcfjudg _ [_]],,[pcfjudg (_,,[_]) [_]]) [pcfjudg (_,,_) [_]] + Rule_PCF ec ([(_,[_])],,[((_,,[_]),[_])]) [((_,,_),[_])] (RLet Γ Δ (Σ@@@(ec::nil)) (Σ'@@@(ec::nil)) σ₂ p (ec::nil)) - | PCF_RVoid : Rule_PCF ec [ ] [ pcfjudg [] [] ] (RVoid Γ Δ ) + | PCF_RVoid : Rule_PCF ec [ ] [([],[])] (RVoid Γ Δ ) (*| PCF_RLetRec : ∀ Σ₁ τ₁ τ₂ , Rule_PCF (ec::nil) _ _ (RLetRec Γ Δ Σ₁ τ₁ τ₂ (ec::nil) )*) - | PCF_RJoin : ∀ Σ₁ Σ₂ τ₁ τ₂, Rule_PCF ec ([pcfjudg _ _],,[pcfjudg _ _]) [pcfjudg (_,,_) (_,,_)] + | PCF_RJoin : ∀ Σ₁ Σ₂ τ₁ τ₂, Rule_PCF ec ([(_,_)],,[(_,_)]) [((_,,_),(_,,_))] (RJoin Γ Δ (Σ₁@@@(ec::nil)) (Σ₂@@@(ec::nil)) (τ₁@@@(ec::nil)) (τ₂@@@(ec::nil))). (* need int/boolean case *) Implicit Arguments Rule_PCF [ ]. - Definition PCFRule Γ Δ lev h c := { r:_ & @Rule_PCF Γ Δ lev h c r }. + Definition PCFRule lev h c := { r:_ & @Rule_PCF lev h c r }. + End PCF. + + Definition FCJudg Γ (Δ:CoercionEnv Γ) := + @prod (Tree ??(LeveledHaskType Γ ★)) (Tree ??(LeveledHaskType Γ ★)). + Definition fcjudg2judg {Γ}{Δ}(fc:FCJudg Γ Δ) := + match fc with + (x,y) => Γ > Δ > x |- y + end. + Coercion fcjudg2judg : FCJudg >-> Judg. + + Definition pcfjudg2fcjudg {Γ}{Δ} ec (fc:PCFJudg Γ ec) : FCJudg Γ Δ := + match fc with + (x,y) => (x @@@ (ec::nil),y @@@ (ec::nil)) + end. (* An organized deduction has been reorganized into contiguous blocks whose * hypotheses (if any) and conclusion have the same Γ and Δ and a fixed nesting depth. The boolean * indicates if non-PCF rules have been used *) - Inductive OrgR : Tree ??Judg -> Tree ??Judg -> Type := + Inductive OrgR Γ Δ : Tree ??(FCJudg Γ Δ) -> Tree ??(FCJudg Γ Δ) -> Type := - | org_fc : forall h c (r:Rule h c), + | org_fc : forall (h c:Tree ??(FCJudg Γ Δ)) + (r:Rule (mapOptionTree fcjudg2judg h) (mapOptionTree fcjudg2judg c)), Rule_Flat r -> - OrgR h c + OrgR _ _ h c - | org_pcf : forall Γ Δ ec h h' c c', - MatchingJudgments h h' -> - MatchingJudgments c c' -> - ND (PCFRule Γ Δ ec) h c -> - OrgR h' c'. + | org_pcf : forall ec h c, + ND (PCFRule Γ Δ ec) h c -> + OrgR Γ Δ (mapOptionTree (pcfjudg2fcjudg ec) h) (mapOptionTree (pcfjudg2fcjudg ec) c). - Definition mkEsc {Γ}{Δ}{ec}(h:Tree ??(PCFJudg Γ Δ ec)) + Definition mkEsc Γ Δ ec (h:Tree ??(PCFJudg Γ ec)) : ND Rule - (mapOptionTree brakify h) - (mapOptionTree (pcfjudg2judg ec) h). + (mapOptionTree (brakify Γ Δ) h) + (mapOptionTree (pcfjudg2judg Γ Δ ec) h). apply nd_replicate; intros. destruct o; simpl in *. induction t0. @@ -154,10 +171,10 @@ Section HaskProofStratified. apply (Prelude_error "mkEsc got multi-leaf succedent"). Defined. - Definition mkBrak {Γ}{Δ}{ec}(h:Tree ??(PCFJudg Γ Δ ec)) + Definition mkBrak Γ Δ ec (h:Tree ??(PCFJudg Γ ec)) : ND Rule - (mapOptionTree (pcfjudg2judg ec) h) - (mapOptionTree brakify h). + (mapOptionTree (pcfjudg2judg Γ Δ ec) h) + (mapOptionTree (brakify Γ Δ) h). apply nd_replicate; intros. destruct o; simpl in *. induction t0. @@ -175,8 +192,8 @@ Section HaskProofStratified. pcf_vars ec Σ = snd vars }. *) - Definition pcfToND : forall Γ Δ ec h c, - ND (PCFRule Γ Δ ec) h c -> ND Rule (mapOptionTree (pcfjudg2judg ec) h) (mapOptionTree (pcfjudg2judg ec) c). + Definition pcfToND Γ Δ : forall ec h c, + ND (PCFRule Γ Δ ec) h c -> ND Rule (mapOptionTree (pcfjudg2judg Γ Δ ec) h) (mapOptionTree (pcfjudg2judg Γ Δ ec) c). intros. eapply (fun q => nd_map' _ q X). intros. @@ -186,19 +203,8 @@ Section HaskProofStratified. Defined. Instance OrgPCF Γ Δ lev : @ND_Relation _ (PCFRule Γ Δ lev) := - { ndr_eqv := fun a b f g => (pcfToND _ _ _ _ _ f) === (pcfToND _ _ _ _ _ g) }. - admit. - admit. - admit. - admit. - admit. - admit. - admit. - admit. - admit. - admit. - admit. - Defined. + { ndr_eqv := fun a b f g => (pcfToND _ _ _ _ _ f) === (pcfToND _ _ _ _ _ g) }. + Admitted. (* * An intermediate representation necessitated by Coq's termination @@ -218,8 +224,8 @@ Section HaskProofStratified. Alternating c | alt_pcf : forall Γ Δ ec h c h' c', - MatchingJudgments h h' -> - MatchingJudgments c c' -> + MatchingJudgments Γ Δ h h' -> + MatchingJudgments Γ Δ c c' -> Alternating h' -> ND (PCFRule Γ Δ ec) h c -> Alternating c'. @@ -229,8 +235,8 @@ Section HaskProofStratified. Lemma magic a b c d ec e : ClosedSIND(Rule:=Rule) [a > b > c |- [d @@ (ec :: e)]] -> ClosedSIND(Rule:=Rule) [a > b > pcf_vars ec c @@@ (ec :: nil) |- [d @@ (ec :: nil)]]. - admit. - Defined. + admit. + Defined. Definition orgify : forall Γ Δ Σ τ (pf:ClosedSIND(Rule:=Rule) [Γ > Δ > Σ |- τ]), Alternating [Γ > Δ > Σ |- τ]. @@ -243,8 +249,8 @@ Section HaskProofStratified. | T_Leaf (Some (Γ > Δ > Σ |- τ)) => let case_leaf := tt in fun eqpf => _ | T_Branch b1 b2 => let case_branch := tt in fun eqpf => _ end (refl_equal _)) - with orgify_pcf Γ Δ ec pcfj j (m:MatchingJudgments pcfj j) - (pf:ClosedSIND (mapOptionTree (pcfjudg2judg ec) pcfj)) {struct pf} : Alternating j := + with orgify_pcf Γ Δ ec pcfj j (m:MatchingJudgments Γ Δ pcfj j) + (pf:ClosedSIND (mapOptionTree (pcfjudg2judg Γ Δ ec) pcfj)) {struct pf} : Alternating j := let case_pcf := tt in _ for orgify_fc'). @@ -296,11 +302,11 @@ Section HaskProofStratified. Definition pcfify Γ Δ ec : forall Σ τ, ClosedSIND(Rule:=Rule) [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)] - -> ND (PCFRule Γ Δ ec) [] [pcfjudg Σ τ]. + -> ND (PCFRule Γ Δ ec) [] [(Σ,τ)]. refine (( fix pcfify Σ τ (pn:@ClosedSIND _ Rule [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)]) {struct pn} - : ND (PCFRule Γ Δ ec) [] [pcfjudg Σ τ] := + : ND (PCFRule Γ Δ ec) [] [(Σ,τ)] := (match pn in @ClosedSIND _ _ J return J=[Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)] -> _ with | cnd_weak => let case_nil := tt in _ | cnd_rule h c cnd' r => let case_rule := tt in _ @@ -314,13 +320,12 @@ Section HaskProofStratified. Admitted. (* any proof in organized form can be "dis-organized" *) - Definition unOrgR : forall h c, OrgR h c -> ND Rule h c. + (* + Definition unOrgR : forall Γ Δ h c, OrgR Γ Δ h c -> ND Rule h c. intros. - induction X. apply nd_rule. apply r. - eapply nd_comp. (* apply (mkEsc h). @@ -329,31 +334,16 @@ Section HaskProofStratified. apply n. *) Admitted. - - Definition unOrgND h c : ND OrgR h c -> ND Rule h c := nd_map unOrgR. + Definition unOrgND Γ Δ h c : ND (OrgR Γ Δ) h c -> ND Rule h c := nd_map (unOrgR Γ Δ). + *) - Instance OrgNDR : @ND_Relation _ OrgR := - { ndr_eqv := fun a b f g => (unOrgND _ _ f) === (unOrgND _ _ g) }. - admit. - admit. - admit. - admit. - admit. - admit. - admit. - admit. - admit. - admit. - admit. - Defined. - Hint Constructors Rule_Flat. - Definition PCF_Arrange {Γ}{Δ}{lev} : forall x y z, Arrange x y -> ND (PCFRule Γ Δ lev) [pcfjudg x z] [pcfjudg y z]. + Definition PCF_Arrange {Γ}{Δ}{lev} : forall x y z, Arrange x y -> ND (PCFRule Γ Δ lev) [(x,z)] [(y,z)]. admit. Defined. - Definition PCF_cut Γ Δ lev : forall a b c, ND (PCFRule Γ Δ lev) ([ pcfjudg a b ],,[ pcfjudg b c ]) [ pcfjudg a c ]. + Definition PCF_cut Γ Δ lev : forall a b c, ND (PCFRule Γ Δ lev) ([(a,b)],,[(b,c)]) [(a,c)]. intros. destruct b. destruct o. @@ -368,7 +358,7 @@ Section HaskProofStratified. apply RuCanL. eapply nd_comp; [ idtac | apply (PCF_Arrange ([],,a) a [h0]); apply RCanL ]. apply nd_rule. -(* + (* set (@RLet Γ Δ [] (a@@@(ec::nil)) h0 h (ec::nil)) as q. exists q. apply (PCF_RLet _ [] a h0 h). @@ -376,15 +366,10 @@ Section HaskProofStratified. apply (Prelude_error "cut rule invoked with [a|=[b]] [[b]|=[x,,y]]"). apply (Prelude_error "cut rule invoked with [a|=[]] [[]|=c]"). apply (Prelude_error "cut rule invoked with [a|=[b,,c]] [[b,,c]|=z]"). -*) - admit. - admit. - admit. - admit. - admit. - Defined. + *) + Admitted. - Instance PCF_sequents Γ Δ lev : @SequentND _ (PCFRule Γ Δ lev) _ pcfjudg := + Instance PCF_sequents Γ Δ lev ec : @SequentND _ (PCFRule Γ Δ lev) _ (pcfjudg Γ ec) := { snd_cut := PCF_cut Γ Δ lev }. apply Build_SequentND. intros. @@ -405,78 +390,69 @@ Section HaskProofStratified. admit. Defined. - Definition PCF_left Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [pcfjudg b c] [pcfjudg (a,,b) (a,,c)]. + Definition PCF_left Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [(b,c)] [((a,,b),(a,,c))]. eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ]. eapply nd_prod; [ apply snd_initial | apply nd_id ]. apply nd_rule. set (@PCF_RJoin Γ Δ lev a b a c) as q'. refine (existT _ _ _). apply q'. - Defined. + Admitted. - Definition PCF_right Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [pcfjudg b c] [pcfjudg (b,,a) (c,,a)]. + Definition PCF_right Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [(b,c)] [((b,,a),(c,,a))]. eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ]. eapply nd_prod; [ apply nd_id | apply snd_initial ]. apply nd_rule. set (@PCF_RJoin Γ Δ lev b a c a) as q'. refine (existT _ _ _). apply q'. - Defined. + Admitted. - Instance PCF_sequent_join Γ Δ lev : @ContextND _ (PCFRule Γ Δ lev) _ pcfjudg _ := + Instance PCF_sequent_join Γ Δ lev : @ContextND _ (PCFRule Γ Δ lev) _ (pcfjudg Γ lev) _ := { cnd_expand_left := fun a b c => PCF_left Γ Δ lev c a b ; cnd_expand_right := fun a b c => PCF_right Γ Δ lev c a b }. - admit. - admit. - admit. - admit. - admit. - admit. - Defined. - - Instance OrgPCF_SequentND_Relation Γ Δ lev : SequentND_Relation (PCF_sequent_join Γ Δ lev) OrgND. - admit. - Defined. - Instance OrgPCF_ContextND_Relation Γ Δ lev : ContextND_Relation (PCF_sequent_join Γ Δ lev). - admit. - Defined. -(* - (* 5.1.3 *) - Instance PCF Γ Δ lev : @ProgrammingLanguage _ pcfjudg (PCFRule Γ Δ lev) := - { pl_eqv := OrgPCF_ContextND_Relation Γ Δ lev - ; pl_snd := PCF_sequents Γ Δ lev - }. - (* - apply Build_TreeStructuralRules; intros; unfold eqv; unfold hom; simpl. - - apply nd_rule. unfold PCFRule. simpl. + intros; apply nd_rule. unfold PCFRule. simpl. exists (RArrange _ _ _ _ _ (RCossa _ _ _)). - apply (PCF_RArrange lev ((a,,b),,c) (a,,(b,,c)) x). + apply (PCF_RArrange _ _ lev ((a,,b),,c) (a,,(b,,c)) x). - apply nd_rule. unfold PCFRule. simpl. + intros; apply nd_rule. unfold PCFRule. simpl. exists (RArrange _ _ _ _ _ (RAssoc _ _ _)). - apply (PCF_RArrange lev (a,,(b,,c)) ((a,,b),,c) x). + apply (PCF_RArrange _ _ lev (a,,(b,,c)) ((a,,b),,c) x). - apply nd_rule. unfold PCFRule. simpl. + intros; apply nd_rule. unfold PCFRule. simpl. exists (RArrange _ _ _ _ _ (RCanL _)). - apply (PCF_RArrange lev ([],,a) _ _). + apply (PCF_RArrange _ _ lev ([],,a) _ _). - apply nd_rule. unfold PCFRule. simpl. + intros; apply nd_rule. unfold PCFRule. simpl. exists (RArrange _ _ _ _ _ (RCanR _)). - apply (PCF_RArrange lev (a,,[]) _ _). + apply (PCF_RArrange _ _ lev (a,,[]) _ _). - apply nd_rule. unfold PCFRule. simpl. + intros; apply nd_rule. unfold PCFRule. simpl. exists (RArrange _ _ _ _ _ (RuCanL _)). - apply (PCF_RArrange lev _ ([],,a) _). + apply (PCF_RArrange _ _ lev _ ([],,a) _). - apply nd_rule. unfold PCFRule. simpl. + intros; apply nd_rule. unfold PCFRule. simpl. exists (RArrange _ _ _ _ _ (RuCanR _)). - apply (PCF_RArrange lev _ (a,,[]) _). + apply (PCF_RArrange _ _ lev _ (a,,[]) _). Defined. -*) - Definition SystemFCa_cut Γ Δ : forall a b c, ND OrgR ([ Γ > Δ > a |- b ],,[ Γ > Δ > b |- c ]) [ Γ > Δ > a |- c ]. + Instance OrgPCF_SequentND_Relation Γ Δ lev : SequentND_Relation (PCF_sequent_join Γ Δ lev) (OrgPCF Γ Δ lev). + admit. + Defined. + + Definition OrgPCF_ContextND_Relation Γ Δ lev + : @ContextND_Relation _ _ _ _ _ (PCF_sequent_join Γ Δ lev) (OrgPCF Γ Δ lev) (OrgPCF_SequentND_Relation Γ Δ lev). + admit. + Defined. + + (* 5.1.3 *) + Instance PCF Γ Δ lev : ProgrammingLanguage := + { pl_cnd := PCF_sequent_join Γ Δ lev + ; pl_eqv := OrgPCF_ContextND_Relation Γ Δ lev + }. + + Definition SystemFCa_cut Γ Δ : forall a b c, ND (OrgR Γ Δ) ([(a,b)],,[(b,c)]) [(a,c)]. intros. destruct b. destruct o. @@ -484,11 +460,14 @@ Section HaskProofStratified. destruct o. (* when the cut is a single leaf and the RHS is a single leaf: *) + (* eapply nd_comp. eapply nd_prod. apply nd_id. eapply nd_rule. - apply org_fc with (r:=RArrange _ _ _ _ _ (RuCanL [l])). + set (@org_fc) as ofc. + set (RArrange Γ Δ _ _ _ (RuCanL [l0])) as rule. + apply org_fc with (r:=RArrange _ _ _ _ _ (RuCanL [_])). auto. eapply nd_comp; [ idtac | eapply nd_rule; apply org_fc with (r:=RArrange _ _ _ _ _ (RCanL _)) ]. apply nd_rule. @@ -499,18 +478,21 @@ Section HaskProofStratified. apply org_fc with (r:=@RLet Γ Δ [] a h1 h h2). auto. auto. + *) + admit. apply (Prelude_error "systemfc cut rule invoked with [a|=[b]] [[b]|=[]]"). apply (Prelude_error "systemfc cut rule invoked with [a|=[b]] [[b]|=[x,,y]]"). apply (Prelude_error "systemfc rule invoked with [a|=[]] [[]|=c]"). apply (Prelude_error "systemfc rule invoked with [a|=[b,,c]] [[b,,c]|=z]"). Defined. - Instance SystemFCa_sequents Γ Δ : @SequentND _ OrgR _ (mkJudg Γ Δ) := + Instance SystemFCa_sequents Γ Δ : @SequentND _ (OrgR Γ Δ) _ _ := { snd_cut := SystemFCa_cut Γ Δ }. apply Build_SequentND. intros. induction a. destruct a; simpl. + (* apply nd_rule. destruct l. apply org_fc with (r:=RVar _ _ _ _). @@ -525,51 +507,82 @@ Section HaskProofStratified. apply org_fc with (r:=RJoin _ _ _ _ _ _). auto. admit. - Defined. + *) + admit. + admit. + admit. + admit. + Defined. - Definition SystemFCa_left Γ Δ a b c : ND OrgR [Γ > Δ > b |- c] [Γ > Δ > (a,,b) |- (a,,c)]. + Definition SystemFCa_left Γ Δ a b c : ND (OrgR Γ Δ) [(b,c)] [((a,,b),(a,,c))]. + admit. + (* eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ]. eapply nd_prod; [ apply snd_initial | apply nd_id ]. apply nd_rule. apply org_fc with (r:=RJoin Γ Δ a b a c). auto. + *) Defined. - Definition SystemFCa_right Γ Δ a b c : ND OrgR [Γ > Δ > b |- c] [Γ > Δ > (b,,a) |- (c,,a)]. + Definition SystemFCa_right Γ Δ a b c : ND (OrgR Γ Δ) [(b,c)] [((b,,a),(c,,a))]. + admit. + (* eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ]. eapply nd_prod; [ apply nd_id | apply snd_initial ]. apply nd_rule. apply org_fc with (r:=RJoin Γ Δ b a c a). auto. + *) Defined. -(* - Instance SystemFCa_sequent_join Γ Δ : @SequentExpansion _ _ _ _ _ (SystemFCa_sequents Γ Δ) (SystemFCa_cutrule Γ Δ) := - { se_expand_left := SystemFCa_left Γ Δ - ; se_expand_right := SystemFCa_right Γ Δ }. - admit. - admit. + Instance SystemFCa_sequent_join Γ Δ : @ContextND _ _ _ _ (SystemFCa_sequents Γ Δ) := + { cnd_expand_left := fun a b c => SystemFCa_left Γ Δ c a b + ; cnd_expand_right := fun a b c => SystemFCa_right Γ Δ c a b }. + (* + intros; apply nd_rule. simpl. + apply (org_fc _ _ _ _ ((RArrange _ _ _ _ _ (RCossa _ _ _)))). + auto. + + intros; apply nd_rule. simpl. + apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RAssoc _ _ _))); auto. + + intros; apply nd_rule. simpl. + apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RCanL _))); auto. + + intros; apply nd_rule. simpl. + apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RCanR _))); auto. + + intros; apply nd_rule. simpl. + apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RuCanL _))); auto. + + intros; apply nd_rule. simpl. + apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RuCanR _))); auto. + *) + admit. + admit. + admit. + admit. + admit. + admit. + Defined. + + Instance OrgFC Γ Δ : @ND_Relation _ (OrgR Γ Δ). + Admitted. + + Instance OrgFC_SequentND_Relation Γ Δ : SequentND_Relation (SystemFCa_sequent_join Γ Δ) (OrgFC Γ Δ). admit. + Defined. + + Definition OrgFC_ContextND_Relation Γ Δ + : @ContextND_Relation _ _ _ _ _ (SystemFCa_sequent_join Γ Δ) (OrgFC Γ Δ) (OrgFC_SequentND_Relation Γ Δ). admit. Defined. -*) + (* 5.1.2 *) - Instance SystemFCa Γ Δ : @ProgrammingLanguage _ _ (mkJudg Γ Δ) OrgR. -(* - { pl_eqv := OrgNDR - ; pl_sn := SystemFCa_sequents Γ Δ - ; pl_subst := SystemFCa_cutrule Γ Δ - ; pl_sequent_join := SystemFCa_sequent_join Γ Δ + Instance SystemFCa Γ Δ : @ProgrammingLanguage (LeveledHaskType Γ ★) _ := + { pl_eqv := OrgFC_ContextND_Relation Γ Δ + ; pl_snd := SystemFCa_sequents Γ Δ }. - apply Build_TreeStructuralRules; intros; unfold eqv; unfold hom; simpl. - apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RCossa a b c))). apply Flat_RArrange. - apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RAssoc a b c))). apply Flat_RArrange. - apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanL a ))). apply Flat_RArrange. - apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanR a ))). apply Flat_RArrange. - apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanL a ))). apply Flat_RArrange. - apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanR a ))). apply Flat_RArrange. -*) -admit. - Defined. -*) + End HaskProofStratified. diff --git a/src/ProgrammingLanguage.v b/src/ProgrammingLanguage.v index e29903a..0636a6e 100644 --- a/src/ProgrammingLanguage.v +++ b/src/ProgrammingLanguage.v @@ -116,7 +116,7 @@ Section Programming_Language. simpl; eapply cndr_inert. apply pl_eqv. auto. auto. Defined. - Definition Types_binoidal : EBinoidalCat TypesL. + Definition Types_binoidal : EBinoidalCat TypesL (@T_Branch _). refine {| ebc_first := Types_first ; ebc_second := Types_second @@ -171,28 +171,28 @@ Section Programming_Language. Instance Types_assoc a b : Types_second a >>>> Types_first b <~~~> Types_first b >>>> Types_second a := { ni_iso := fun c => Types_assoc_iso a c b }. - admit. + admit. (* need to add this as an obligation in ProgrammingLanguage class *) Defined. Instance Types_cancelr : Types_first [] <~~~> functor_id _ := { ni_iso := Types_cancelr_iso }. intros; simpl. - admit. + admit. (* need to add this as an obligation in ProgrammingLanguage class *) Defined. Instance Types_cancell : Types_second [] <~~~> functor_id _ := { ni_iso := Types_cancell_iso }. - admit. + admit. (* need to add this as an obligation in ProgrammingLanguage class *) Defined. Instance Types_assoc_ll a b : Types_second (a,,b) <~~~> Types_second b >>>> Types_second a := { ni_iso := fun c => Types_assoc_iso a b c }. - admit. + admit. (* need to add this as an obligation in ProgrammingLanguage class *) Defined. Instance Types_assoc_rr a b : Types_first (a,,b) <~~~> Types_first a >>>> Types_first b := { ni_iso := fun c => iso_inv _ _ (Types_assoc_iso c a b) }. - admit. + admit. (* need to add this as an obligation in ProgrammingLanguage class *) Defined. Instance TypesL_PreMonoidal : PreMonoidalCat Types_binoidal [] := @@ -241,9 +241,9 @@ Section Programming_Language. auto. intros; simpl; reflexivity. intros; simpl; reflexivity. - admit. (* assoc central *) - admit. (* cancelr central *) - admit. (* cancell central *) + admit. (* assoc is central: need to add this as an obligation in ProgrammingLanguage class *) + admit. (* cancelr is central: need to add this as an obligation in ProgrammingLanguage class *) + admit. (* cancell is central: need to add this as an obligation in ProgrammingLanguage class *) Defined. Definition TypesEnrichedInJudgments : SurjectiveEnrichment. diff --git a/src/ProgrammingLanguageArrow.v b/src/ProgrammingLanguageArrow.v index f6a3940..5dbce6d 100644 --- a/src/ProgrammingLanguageArrow.v +++ b/src/ProgrammingLanguageArrow.v @@ -31,9 +31,8 @@ Require Import NaturalDeduction. Require Import NaturalDeductionCategory. Require Import ProgrammingLanguage. -Require Import ProgrammingLanguageGeneralizedArrow. Require Import FreydCategories. - +Require Import Enrichments. Require Import GeneralizedArrow. Section ArrowInLanguage. @@ -41,34 +40,36 @@ Section ArrowInLanguage. (* an Arrow In A Programming Language consists of... *) (* a host language: *) - Context `(Host:ProgrammingLanguage). + Context `(Host : ProgrammingLanguage). - (* ... for which Types(L) is cartesian: *) - Context (center_of_TypesL:MonoidalCat (TypesL_PreMonoidal Host)). + Context (Host_Monoidal : MonoidalCat (TypesL_PreMonoidal Host)). + Context (Host_Cartesian : CartesianCat Host_Monoidal). - (* along with a full subcategory of Z(Types(L)) *) - Context {P}(VK:FullSubcategory (Center (TypesL_PreMonoidal Host)) P). + Context + {P} + (Pobj_unit : P []) + (Pobj_closed : forall a b, P a → P b → P (bin_obj(BinoidalCat:=Center_is_PreMonoidal (TypesL_PreMonoidal Host)) a b)). - Context (Pobj_unit : P []). - Context (Pobj_closed : forall a b, P a → P b → P (bin_obj(BinoidalCat:=Center_is_PreMonoidal (TypesL_PreMonoidal Host)) a b)). - Definition VKM := - PreMonoidalFullSubcategory_PreMonoidal (Center_is_PreMonoidal (TypesL_PreMonoidal Host)) VK Pobj_unit Pobj_closed. + Context (VK : FullSubcategory Host_Cartesian P). - (* a premonoidal category enriched in aforementioned full subcategory *) - Context (Kehom:(Center (TypesL_PreMonoidal Host)) -> (Center (TypesL_PreMonoidal Host)) -> @ob _ _ VK). - Context (KE :@ECategory (@ob _ _ VK) (@hom _ _ VK) VK _ VKM (pmon_I VKM) VKM (Center (TypesL_PreMonoidal Host)) Kehom). - Context {kbo :(Center (TypesL_PreMonoidal Host)) -> (Center (TypesL_PreMonoidal Host)) -> (Center (TypesL_PreMonoidal Host))}. - Context (kbc :@BinoidalCat (Center (TypesL_PreMonoidal Host)) _ (Underlying KE) kbo). + Context ehom KE (K_bin:@EBinoidalCat _ _ VK _ _ _ + (PreMonoidalFullSubcategory_PreMonoidal Host_Cartesian VK Pobj_unit Pobj_closed) + (TypesL Host) ehom KE (bin_obj(BinoidalCat:=Host_Monoidal))). - Definition one' := @one _ _ _ (car_terminal(CartesianCat:=CC)) - Context (K :@PreMonoidalCat _ _ KE kbo kbc ). - Context (CC:CartesianCat (Center (TypesL_PreMonoidal Host))). + Context (K_premonoidal:PreMonoidalCat K_bin (one(TerminalObject:=Host_Cartesian))). Definition ArrowInProgrammingLanguage := - @FreydCategory _ _ _ _ _ _ (Center (TypesL_PreMonoidal Host)) _ _ _ _ K. + @FreydCategory _ _ _ _ _ _ _ _ Host_Cartesian _ _ K_bin K_premonoidal. + + Definition K_enrichment : Enrichment. + refine + {| enr_c_pm := K_premonoidal + ; enr_v_mon := MonoidalFullSubcategory_Monoidal Host_Cartesian _ _ VK + |}. + Defined. - Definition ArrowsAreGeneralizedArrows (arrow:ArrowInProgrammingLanguage) : GeneralizedArrow K_enrichment Host. - refine {| ga_functor_monoidal := inclusion_functor_monoidal VK |}. - Defined. + Instance ArrowsAreGeneralizedArrows : GeneralizedArrow K_enrichment (TypesEnrichedInJudgments Host) := + { ga_functor_monoidal := + PreMonoidalFullSubcategoryInclusionFunctor_PreMonoidal Host_Cartesian VK Pobj_unit Pobj_closed Host_Cartesian }. -End GArrowInLanguage. +End ArrowInLanguage. diff --git a/src/ProgrammingLanguageFlattening.v b/src/ProgrammingLanguageFlattening.v index f01621b..4438dd2 100644 --- a/src/ProgrammingLanguageFlattening.v +++ b/src/ProgrammingLanguageFlattening.v @@ -15,6 +15,8 @@ Require Import Enrichment_ch2_8. Require Import Subcategories_ch7_1. Require Import NaturalTransformations_ch7_4. Require Import NaturalIsomorphisms_ch7_5. +Require Import BinoidalCategories. +Require Import PreMonoidalCategories. Require Import MonoidalCategories_ch7_8. Require Import Coherence_ch7_8. Require Import Enrichment_ch2_8. @@ -25,51 +27,66 @@ Require Import Reification. Require Import NaturalDeduction. Require Import NaturalDeductionCategory. Require Import GeneralizedArrow. -Require Import GeneralizedArrowFromReification. Require Import ProgrammingLanguage. Require Import ProgrammingLanguageReification. +Require Import SectionRetract_ch2_4. +Require Import GeneralizedArrowFromReification. +Require Import Enrichments. Require Import ReificationsAndGeneralizedArrows. Section Flattening. - Context (Guest:ProgrammingLanguageSMME) (Host :ProgrammingLanguageSMME). + Context `(Guest:ProgrammingLanguage) `(Host :ProgrammingLanguage). Context (GuestHost:TwoLevelLanguage Guest Host). - Definition FlatObject (x:TypesL _ _ Host) := + Definition FlatObject (x:TypesL Host) := forall y1 y2, not ((reification_r_obj GuestHost y1 y2)=x). - Definition FlatSubCategory := FullSubcategory (TypesL _ _ Host) FlatObject. + Instance FlatSubCategory : FullSubcategory (TypesL Host) FlatObject. - Context (F:Retraction (TypesL _ _ Host) FlatSubCategory). + Context (F:RetractionOfCategories (TypesL Host) (FullSubCategoriesAreCategories FlatSubCategory)). - Definition FlatteningOfReification := - garrow_from_reification Guest Host GuestHost >>>> F. + Definition FlatteningOfReification HostMonic HostMonoidal := + (ga_functor + (@garrow_from_reification + (TypesEnrichedInJudgments Guest) + (TypesEnrichedInJudgments Host) + HostMonic HostMonoidal GuestHost)) + >>>> F. -(* - Lemma FlatteningIsNotDestructive : - FlatteningOfReification >>>> retraction_retraction F >>>> HomFunctor _ (me_i Host) ≃ GuestHost. + Lemma FlatteningIsNotDestructive HostMonic HostMonoidal : + FlatteningOfReification HostMonic HostMonoidal >>>> retraction_retraction F >>>> HomFunctor _ [] + ≃ (reification_rstar GuestHost). apply if_inv. - set (@roundtrip_reification_to_reification _ Guest _ _ Host GuestHost) as q. - unfold mf_f in *; simpl in *. - apply (if_comp q). + set (@roundtrip_reification_to_reification (TypesEnrichedInJudgments Guest) (TypesEnrichedInJudgments Host) + HostMonic HostMonoidal GuestHost) as q. + unfold mf_F in *; simpl in *. + eapply if_comp. + apply q. clear q. - unfold me_mf; simpl. - unfold mf_f; simpl. - refine (if_respects _ (if_id _)). + unfold mf_F; simpl. + unfold pmon_I. + apply (if_respects + (garrow_functor (TypesEnrichedInJudgments Guest) HostMonic HostMonoidal GuestHost) + (FlatteningOfReification HostMonic HostMonoidal >>>> retraction_retraction F) + (HomFunctor (TypesL Host) []) + (HomFunctor (TypesL Host) [])); [ idtac | apply (if_id _) ]. unfold FlatteningOfReification. - unfold mf_f; simpl. - eapply if_comp. - Focus 2. - eapply if_inv. - apply (if_associativity (garrow_functor Guest Host GuestHost) F (retraction_retraction F)). - eapply if_comp. - eapply if_inv. - apply if_right_identity. - refine (if_respects (if_id _) _). + unfold mf_F; simpl. apply if_inv. + eapply if_comp. + apply (if_associativity (garrow_functor (TypesEnrichedInJudgments Guest) HostMonic HostMonoidal GuestHost) F + (retraction_retraction F)). + eapply if_comp; [ idtac | apply if_right_identity ]. + apply (if_respects + (garrow_functor (TypesEnrichedInJudgments Guest) HostMonic HostMonoidal GuestHost) + (garrow_functor (TypesEnrichedInJudgments Guest) HostMonic HostMonoidal GuestHost) + (F >>>> retraction_retraction F) + (functor_id _)). + apply (if_id _). apply retraction_composes. Qed. -*) + End Flattening. diff --git a/src/ProgrammingLanguageReification.v b/src/ProgrammingLanguageReification.v index f6a2a8e..932c517 100644 --- a/src/ProgrammingLanguageReification.v +++ b/src/ProgrammingLanguageReification.v @@ -28,9 +28,29 @@ Require Import Reification. Require Import NaturalDeduction. Require Import NaturalDeductionCategory. Require Import ProgrammingLanguage. +Require Import Enrichments. + +Section ProgrammingLanguageReification. + + Definition TwoLevelLanguage `(Guest:ProgrammingLanguage) `(Host:ProgrammingLanguage) + := Reification (TypesEnrichedInJudgments Guest) (TypesEnrichedInJudgments Host) []. + + Inductive NLevelLanguage : forall (n:nat) `(PL:ProgrammingLanguage), Type := + | NLevelLanguage_zero : forall `(lang:ProgrammingLanguage), + NLevelLanguage O lang + | NLevelLanguage_succ : forall `(L1:ProgrammingLanguage) `(L2:ProgrammingLanguage) n, + TwoLevelLanguage L1 L2 -> NLevelLanguage n L1 -> NLevelLanguage (S n) L2. + + (* + Definition OmegaLevelLanguage : Type := + { f : nat -> ProgrammingLanguage + & forall n, TwoLevelLanguage (f n) (f (S n)) }. + *) + +End ProgrammingLanguageReification. (* - Structure ProgrammingLanguageSMME := + Structure ProgrammingLanguage := { plsmme_t : Type ; plsmme_judg : Type ; plsmme_sequent : Tree ??plsmme_t -> Tree ??plsmme_t -> plsmme_judg @@ -38,25 +58,6 @@ Require Import ProgrammingLanguage. ; plsmme_pl : @ProgrammingLanguage plsmme_t plsmme_judg plsmme_sequent plsmme_rule ; plsmme_smme : SurjectiveEnrichment (TypesEnrichedInJudgments _ _ plsmme_pl) }. - Coercion plsmme_pl : ProgrammingLanguageSMME >-> ProgrammingLanguage. - Coercion plsmme_smme : ProgrammingLanguageSMME >-> SurjectiveMonicMonoidalEnrichment. + Coercion plsmme_pl : ProgrammingLanguage >-> ProgrammingLanguage. + Coercion plsmme_smme : ProgrammingLanguage >-> SurjectiveMonicMonoidalEnrichment. *) - - Context - `(Guest : ProgrammingLanguage) - `(Host : ProgrammingLanguage) - (HostMonoidal : MonoidalEnrichment (TypesEnrichedInJudgments Host)) - (HostMonic : MonicEnrichment (TypesEnrichedInJudgments Host)). - -Definition TwoLevelLanguage (Guest Host:ProgrammingLanguageSMME) - := Reification Guest Host (me_i Host). - -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/ReificationFromGeneralizedArrow.v b/src/ReificationFromGeneralizedArrow.v index 1a5fea7..730d91d 100644 --- a/src/ReificationFromGeneralizedArrow.v +++ b/src/ReificationFromGeneralizedArrow.v @@ -26,7 +26,7 @@ Require Import RepresentableStructure_ch7_2. Require Import Reification. Require Import GeneralizedArrow. -Definition reification_from_garrow (K:Enrichment) {ce} (C:MonoidalEnrichment ce) (garrow : GeneralizedArrow K C) +Definition reification_from_garrow (K:Enrichment) {ce} (C:MonoidalEnrichment ce) (garrow : GeneralizedArrow K ce) : Reification K ce (enr_c_i ce). refine {| reification_r := fun k:K => HomFunctor K k >>>> ga_functor garrow diff --git a/src/ReificationsAndGeneralizedArrows.v b/src/ReificationsAndGeneralizedArrows.v index 4056c77..7924a43 100644 --- a/src/ReificationsAndGeneralizedArrows.v +++ b/src/ReificationsAndGeneralizedArrows.v @@ -71,9 +71,8 @@ Section ReificationsEquivalentToGeneralizedArrows. Qed. Lemma roundtrip_garrow_to_garrow - `(K:SurjectiveEnrichment) `(C:MonicEnrichment ce) (CM:MonoidalEnrichment ce) (garrow : GeneralizedArrow K CM) + `(K:SurjectiveEnrichment) `(C:MonicEnrichment ce) (CM:MonoidalEnrichment ce) (garrow : GeneralizedArrow K ce) : garrow ≃ garrow_from_reification K C CM (reification_from_garrow K CM garrow). - apply if_inv. eapply if_comp. eapply if_inv. diff --git a/src/categories b/src/categories index 1104780..0ecd73c 160000 --- a/src/categories +++ b/src/categories @@ -1 +1 @@ -Subproject commit 1104780d775bf36ff9f44ab287c22604ab47f0b5 +Subproject commit 0ecd73c172f67634fa956fb52b332e6effb5a04d -- 1.7.10.4