From 992203bb4a221ea2f415c0d14bb34d35af2ee637 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sat, 26 Mar 2011 00:02:29 -0700 Subject: [PATCH] re-arrange NaturalDeduction --- src/ExtractionMain.v | 5 +- src/GeneralizedArrow.v | 10 +- src/GeneralizedArrowCategory.v | 21 +- src/GeneralizedArrowFromReification.v | 6 +- src/NaturalDeduction.v | 45 +++ src/NaturalDeductionCategory.v | 35 -- src/Preamble.v | 7 +- src/ProgrammingLanguage.v | 428 +++++------------------ src/ReificationCategory.v | 21 +- src/ReificationFromGeneralizedArrow.v | 2 +- src/ReificationsEquivalentToGeneralizedArrows.v | 4 + 11 files changed, 187 insertions(+), 397 deletions(-) diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index 2b65a18..61993a1 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -34,12 +34,13 @@ Require Import HaskStrongToWeak. Require Import HaskWeakToCore. Require Import HaskProofToStrong. +Require Import ProgrammingLanguage. + Require Import HaskProofCategory. (* Require Import HaskStrongCategory. -Require Import ReificationsEquivalentToGeneralizedArrows. -Require Import ProgrammingLanguage. *) +Require Import ReificationsEquivalentToGeneralizedArrows. Open Scope string_scope. Extraction Language Haskell. diff --git a/src/GeneralizedArrow.v b/src/GeneralizedArrow.v index f246567..bf7743b 100644 --- a/src/GeneralizedArrow.v +++ b/src/GeneralizedArrow.v @@ -22,14 +22,14 @@ Require Import Coherence_ch7_8. Require Import Enrichment_ch2_8. Require Import RepresentableStructure_ch7_2. -Class GeneralizedArrow (K:Enrichment) (C:MonoidalEnrichment) := +Class GeneralizedArrow (K:Enrichment) {ce}(C:MonoidalEnrichment ce) := { ga_functor_obj : enr_v_mon K -> C ; ga_functor : Functor (enr_v_mon K) C ga_functor_obj ; ga_functor_monoidal : MonoidalFunctor (enr_v_mon K) C ga_functor }. Coercion ga_functor_monoidal : GeneralizedArrow >-> MonoidalFunctor. -Implicit Arguments GeneralizedArrow [ ]. -Implicit Arguments ga_functor_obj [ K C ]. -Implicit Arguments ga_functor [ K C ]. -Implicit Arguments ga_functor_monoidal [ K C ]. +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 ]. diff --git a/src/GeneralizedArrowCategory.v b/src/GeneralizedArrowCategory.v index cd43282..d98f85a 100644 --- a/src/GeneralizedArrowCategory.v +++ b/src/GeneralizedArrowCategory.v @@ -9,6 +9,21 @@ Generalizable All Variables. Require Import Preamble. Require Import General. -Require Import NaturalDeduction. -Require Import Coq.Strings.String. -Require Import Coq.Lists.List. +Require Import Categories_ch1_3. +Require Import Functors_ch1_4. +Require Import Isomorphisms_ch1_5. +Require Import ProductCategories_ch1_6_1. +Require Import OppositeCategories_ch1_6_2. +Require Import 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 GeneralizedArrow. + +Instance CategoryOfGeneralizedArrows : Category SMME GeneralizedArrow. + admit. + Qed. diff --git a/src/GeneralizedArrowFromReification.v b/src/GeneralizedArrowFromReification.v index 6aeaace..e6d3cbd 100644 --- a/src/GeneralizedArrowFromReification.v +++ b/src/GeneralizedArrowFromReification.v @@ -26,7 +26,7 @@ Require Import GeneralizedArrow. Section GArrowFromReification. - Context (K:SurjectiveEnrichment) (C:MonicMonoidalEnrichment) (reification : Reification K C (me_i C)). + Context `(K:SurjectiveEnrichment ke) `(C:MonicMonoidalEnrichment ce cme) (reification : Reification K C (me_i C)). Fixpoint garrow_fobj_ vk : C := match vk with @@ -35,13 +35,13 @@ Section GArrowFromReification. | t1,,t2 => me_f C (pair_obj (garrow_fobj_ t1) (garrow_fobj_ t2)) end. - Definition garrow_fobj vk := garrow_fobj_ (projT1 (se_decomp K vk)). + Definition garrow_fobj vk := garrow_fobj_ (projT1 (se_decomp _ K vk)). Definition homset_tensor_iso : forall vk:enr_v_mon K, (reification_rstar reification vk) ≅ ehom(ECategory:=C) (me_i C) (garrow_fobj vk). intros. unfold garrow_fobj. - set (se_decomp K vk) as sevk. + set (se_decomp _ K vk) as sevk. destruct sevk. simpl in *. rewrite e. diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v index 855b66a..06b6efe 100644 --- a/src/NaturalDeduction.v +++ b/src/NaturalDeduction.v @@ -333,11 +333,56 @@ Section Natural_Deduction. | cnd_branch c1 c2 cnd1 cnd2 => nd_llecnac ;; nd_prod (closedNDtoNormalND cnd1) (closedNDtoNormalND cnd2) end. + Section Sequents. + Context {S:Type}. (* type of sequent components *) + Context (sequent:S->S->Judgment). + Context (ndr:ND_Relation). + Notation "a |= b" := (sequent a b). + Notation "a === b" := (@ndr_eqv ndr _ _ a b) : nd_scope. + + Class SequentCalculus := + { nd_seq_reflexive : forall a, ND [ ] [ a |= a ] + }. + + 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 + ; nd_cut_right_identity : forall a b, (((nd_id _)**(nd_seq_reflexive a) );; nd_cut b _ _) === nd_cancelr + ; nd_cut_associativity : forall {a b c d}, + (nd_cut a b c ** nd_id1 (c|=d)) ;; (nd_cut a c d) === nd_assoc ;; (nd_id1 (a|=b) ** nd_cut b c d) ;; nd_cut a b d + }. + + End Sequents. + + Section SequentsOfTrees. + Context {T:Type}{sequent:Tree ??T -> Tree ??T -> Judgment}(sc:SequentCalculus sequent). + Context (ndr:ND_Relation). + Notation "a |= b" := (sequent a b). + Notation "a === b" := (@ndr_eqv ndr _ _ a b) : nd_scope. + + Class TreeStructuralRules := + { tsr_ant_assoc : forall {x a b c}, Rule [((a,,b),,c) |= x] [(a,,(b,,c)) |= x] + ; tsr_ant_cossa : forall {x a b c}, Rule [(a,,(b,,c)) |= x] [((a,,b),,c) |= x] + ; tsr_ant_cancell : forall {x a }, Rule [ [],,a |= x] [ a |= x] + ; tsr_ant_cancelr : forall {x a }, Rule [a,,[] |= x] [ a |= x] + ; tsr_ant_llecnac : forall {x a }, Rule [ a |= x] [ [],,a |= x] + ; tsr_ant_rlecnac : forall {x a }, Rule [ a |= x] [ a,,[] |= x] + }. + + Class SequentExpansion := + { se_expand_left : forall tau {Gamma Sigma}, Rule [ Gamma |= Sigma ] [tau,,Gamma|=tau,,Sigma] + ; se_expand_right : forall tau {Gamma Sigma}, Rule [ Gamma |= Sigma ] [Gamma,,tau|=Sigma,,tau] + }. + End SequentsOfTrees. + Close Scope nd_scope. Open Scope pf_scope. End Natural_Deduction. +Coercion nd_cut : CutRule >-> Funclass. + Implicit Arguments ND [ Judgment ]. Hint Constructors Structural. Hint Extern 1 => apply nd_id_structural. diff --git a/src/NaturalDeductionCategory.v b/src/NaturalDeductionCategory.v index 5e3432b..b64ac4b 100644 --- a/src/NaturalDeductionCategory.v +++ b/src/NaturalDeductionCategory.v @@ -201,41 +201,6 @@ Section Judgments_Category. apply nd_structural_cancelr; auto. Defined. - (* Given some mapping "rep" that turns a (Tree ??T) intoto Judgment, - * this asserts that we have sensible structural rules with respect - * to that mapping. Doing all of this "with respect to a mapping" - * lets us avoid duplicating code for both the antecedent and - * succedent of sequent deductions. *) - Class TreeStructuralRules {T:Type}(rep:Tree ??T -> Judgment) := - { tsr_eqv : @ND_Relation Judgment Rule where "pf1 === pf2" := (@ndr_eqv _ _ tsr_eqv _ _ pf1 pf2) - ; tsr_ant_assoc : forall {a b c}, Rule [rep ((a,,b),,c)] [rep ((a,,(b,,c)))] - ; tsr_ant_cossa : forall {a b c}, Rule [rep (a,,(b,,c))] [rep (((a,,b),,c))] - ; tsr_ant_cancell : forall {a }, Rule [rep ( [],,a )] [rep ( a )] - ; tsr_ant_cancelr : forall {a }, Rule [rep (a,,[] )] [rep ( a )] - ; tsr_ant_llecnac : forall {a }, Rule [rep ( a )] [rep ( [],,a )] - ; tsr_ant_rlecnac : forall {a }, Rule [rep ( a )] [rep ( a,,[] )] - }. - - Section Sequents. - Context {S:Type}. (* type of sequent components *) - Context (sequent:S->S->Judgment). - Notation "a |= b" := (sequent a b). - - Class SequentCalculus := - { nd_seq_reflexive : forall a, ND Rule [ ] [ a |= a ] - }. - - Class CutRule := - { nd_cutrule_seq :> SequentCalculus - ; nd_cut : forall a b c, [ a |= b ] ,, [ b |= c ] /⋯⋯/ [ a |= c ] - ; nd_cut_associativity : forall {a b c d}, - ((nd_cut a b c) ** (nd_id1 (c|=d))) ;; (nd_cut a c d) - === - nd_assoc ;; ((nd_id1 (a|=b)) ** (nd_cut b c d) ;; (nd_cut a b d)) - ; nd_cut_left_identity : forall a b, (( (nd_seq_reflexive a)**(nd_id _));; nd_cut _ _ b) === nd_cancell - ; nd_cut_right_identity : forall a b, (((nd_id _)**(nd_seq_reflexive a) );; nd_cut b _ _) === nd_cancelr - }. - End Sequents. (* Structure ExpressionAlgebra (sig:Signature) := *) diff --git a/src/Preamble.v b/src/Preamble.v index f83d9a1..453027a 100644 --- a/src/Preamble.v +++ b/src/Preamble.v @@ -16,8 +16,11 @@ Export Coq.Setoids.Setoid. Set Printing Width 130. (* Proof General seems to add an extra two columns of overhead *) Generalizable All Variables. +Reserved Notation "a ** b" (at level 40). +Reserved Notation "a ;; b" (at level 45). + Reserved Notation "a -~- b" (at level 10). -Reserved Notation "a ** b" (at level 10). +Reserved Notation "pf1 === pf2" (at level 80). Reserved Notation "?? x" (at level 1). Reserved Notation "a ,, b" (at level 50). Reserved Notation "!! f" (at level 3). @@ -52,7 +55,6 @@ Reserved Notation "A ⋊ f" (at level 40). Reserved Notation "- ⋉ A" (at level 40). Reserved Notation "A ⋊ -" (at level 40). Reserved Notation "a *** b" (at level 40). -Reserved Notation "a ;; b" (at level 45). Reserved Notation "[# f #]" (at level 2). Reserved Notation "a ---> b" (at level 11, right associativity). Reserved Notation "a <- b" (at level 100, only parsing). @@ -69,7 +71,6 @@ Reserved Notation "f ○ g" (at level 100). Reserved Notation "a ==[ n ]==> b" (at level 20). Reserved Notation "a ==[ h | c ]==> b" (at level 20). Reserved Notation "H /⋯⋯/ C" (at level 70). -Reserved Notation "pf1 === pf2" (at level 80). Reserved Notation "a |== b @@ c" (at level 100). Reserved Notation "f >>>> g" (at level 45). Reserved Notation "a >>[ n ]<< b" (at level 100). diff --git a/src/ProgrammingLanguage.v b/src/ProgrammingLanguage.v index b00d1ad..7630440 100644 --- a/src/ProgrammingLanguage.v +++ b/src/ProgrammingLanguage.v @@ -9,6 +9,7 @@ Generalizable All Variables. Require Import Preamble. Require Import General. Require Import Categories_ch1_3. +Require Import InitialTerminal_ch2_2. Require Import Functors_ch1_4. Require Import Isomorphisms_ch1_5. Require Import ProductCategories_ch1_6_1. @@ -21,15 +22,17 @@ 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 Reification. + Require Import FreydCategories. -Require Import InitialTerminal_ch2_2. -Require Import FunctorCategories_ch7_7. -Require Import GeneralizedArrowFromReification. -Require Import GeneralizedArrow. +Require Import Reification. +Require Import GeneralizedArrow. +Require Import GeneralizedArrowFromReification. +Require Import ReificationFromGeneralizedArrow. (* * Everything in the rest of this section is just groundwork meant to @@ -42,7 +45,6 @@ Require Import GeneralizedArrow. *) Section Programming_Language. - (* Formalized Definition 4.1.1, production $\tau$ *) Context {T : Type}. (* types of the language *) Context (Judg : Type). @@ -63,7 +65,7 @@ Section Programming_Language. Open Scope nd_scope. Open Scope al_scope. - (* Formalized Definition 4.1 + (* * * Note that from this abstract interface, the terms (expressions) * in the proof are not accessible at all; they don't need to be -- @@ -82,145 +84,21 @@ Section Programming_Language. * This also means that we don't need an explicit proof obligation for 4.1.2. *) Class ProgrammingLanguage := - - (* Formalized Definition 4.1: denotational semantics equivalence relation on the conclusions of proofs *) - { al_eqv : @ND_Relation Judg Rule - where "pf1 === pf2" := (@ndr_eqv _ _ al_eqv _ _ pf1 pf2) - - (* Formalized Definition 4.1.3; note that t here is either $\top$ or a single type, not a Tree of types; - * we rely on "completeness of atomic initial segments" (http://en.wikipedia.org/wiki/Completeness_of_atomic_initial_sequents) - * to generate the rest *) - ; al_reflexive_seq : forall t, Rule [] [t|=t] - - (* these can all be absorbed into a separate "sequent calculus" presentation *) - ; al_ant_assoc : forall {a b c d}, Rule [(a,,b),,c|=d] [(a,,(b,,c))|=d] - ; al_ant_cossa : forall {a b c d}, Rule [a,,(b,,c)|=d] [((a,,b),,c)|=d] - ; al_ant_cancell : forall {a b }, Rule [ [],,a |=b] [ a |=b] - ; al_ant_cancelr : forall {a b }, Rule [a,,[] |=b] [ a |=b] - ; al_ant_llecnac : forall {a b }, Rule [ a |=b] [ [],,a |=b] - ; al_ant_rlecnac : forall {a b }, Rule [ a |=b] [ a,,[] |=b] - ; al_suc_assoc : forall {a b c d}, Rule [d|=(a,,b),,c] [d|=(a,,(b,,c))] - ; al_suc_cossa : forall {a b c d}, Rule [d|=a,,(b,,c)] [d|=((a,,b),,c)] - ; al_suc_cancell : forall {a b }, Rule [a|=[],,b ] [a|= b ] - ; al_suc_cancelr : forall {a b }, Rule [a|=b,,[] ] [a|= b ] - ; al_suc_llecnac : forall {a b }, Rule [a|= b ] [a|=[],,b ] - ; al_suc_rlecnac : forall {a b }, Rule [a|= b ] [a|=b,,[] ] - - ; al_horiz_expand_left : forall tau {Gamma Sigma}, Rule [ Gamma |= Sigma ] [tau,,Gamma|=tau,,Sigma] - ; al_horiz_expand_right : forall tau {Gamma Sigma}, Rule [ Gamma |= Sigma ] [Gamma,,tau|=Sigma,,tau] - - (* these are essentially one way of formalizing - * "completeness of atomic initial segments" (http://en.wikipedia.org/wiki/Completeness_of_atomic_initial_sequents) *) - ; al_horiz_expand_left_reflexive : forall a b, [#al_reflexive_seq b#];;[#al_horiz_expand_left a#]===[#al_reflexive_seq (a,,b)#] - ; al_horiz_expand_right_reflexive : forall a b, [#al_reflexive_seq a#];;[#al_horiz_expand_right b#]===[#al_reflexive_seq (a,,b)#] - ; al_horiz_expand_right_then_cancel : forall a, - ((([#al_reflexive_seq (a,, [])#] ;; [#al_ant_cancelr#]);; [#al_suc_cancelr#]) === [#al_reflexive_seq a#]) - - ; al_vert_expand_ant_left : forall x `(pf:[a|=b]/⋯⋯/[c|=d]), [x,,a |= b ]/⋯⋯/[x,,c |= d ] - ; al_vert_expand_ant_right : forall x `(pf:[a|=b]/⋯⋯/[c|=d]), [ a,,x|= b ]/⋯⋯/[ c,,x|= d ] - ; al_vert_expand_suc_left : forall x `(pf:[a|=b]/⋯⋯/[c|=d]), [ a |=x,,b ]/⋯⋯/[ c |=x,,d ] - ; al_vert_expand_suc_right : forall x `(pf:[a|=b]/⋯⋯/[c|=d]), [ a |= b,,x]/⋯⋯/[ c |= d,,x] - ; al_vert_expand_ant_l_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]), - f===g -> al_vert_expand_ant_left x f === al_vert_expand_ant_left x g - ; al_vert_expand_ant_r_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]), - f===g -> al_vert_expand_ant_right x f === al_vert_expand_ant_right x g - ; al_vert_expand_suc_l_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]), - f===g -> al_vert_expand_suc_left x f === al_vert_expand_suc_left x g - ; al_vert_expand_suc_r_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]), - f===g -> al_vert_expand_suc_right x f === al_vert_expand_suc_right x g - ; al_vert_expand_ant_l_preserves_id : forall x a b, al_vert_expand_ant_left x (nd_id [a|=b]) === nd_id [x,,a|=b] - ; al_vert_expand_ant_r_preserves_id : forall x a b, al_vert_expand_ant_right x (nd_id [a|=b]) === nd_id [a,,x|=b] - ; al_vert_expand_suc_l_preserves_id : forall x a b, al_vert_expand_suc_left x (nd_id [a|=b]) === nd_id [a|=x,,b] - ; al_vert_expand_suc_r_preserves_id : forall x a b, al_vert_expand_suc_right x (nd_id [a|=b]) === nd_id [a|=b,,x] - ; al_vert_expand_ant_l_preserves_comp : forall x a b c d e f (h:[a|=b]/⋯⋯/[c|=d])(g:[c|=d]/⋯⋯/[e|=f]), - (al_vert_expand_ant_left x (h;;g)) === (al_vert_expand_ant_left x h);;(al_vert_expand_ant_left x g) - ; al_vert_expand_ant_r_preserves_comp : forall x a b c d e f (h:[a|=b]/⋯⋯/[c|=d])(g:[c|=d]/⋯⋯/[e|=f]), - (al_vert_expand_ant_right x (h;;g)) === (al_vert_expand_ant_right x h);;(al_vert_expand_ant_right x g) - ; al_vert_expand_suc_l_preserves_comp : forall x a b c d e f (h:[a|=b]/⋯⋯/[c|=d])(g:[c|=d]/⋯⋯/[e|=f]), - (al_vert_expand_suc_left x (h;;g)) === (al_vert_expand_suc_left x h);;(al_vert_expand_suc_left x g) - ; al_vert_expand_suc_r_preserves_comp : forall x a b c d e f (h:[a|=b]/⋯⋯/[c|=d])(g:[c|=d]/⋯⋯/[e|=f]), - (al_vert_expand_suc_right x (h;;g)) === (al_vert_expand_suc_right x h);;(al_vert_expand_suc_right x g) - - ; al_subst : forall a b c, [ a |= b ] ,, [ b |= c ] /⋯⋯/ [ a |= c ] - ; al_subst_associativity : forall {a b c d}, - ((al_subst a b c) ** (nd_id1 (c|=d))) ;; - (al_subst a c d) - === - nd_assoc ;; - ((nd_id1 (a|=b)) ** (al_subst b c d) ;; - (al_subst a b d)) - ; al_subst_associativity' : forall {a b c d}, - nd_cossa ;; - ((al_subst a b c) ** (nd_id1 (c|=d))) ;; - (al_subst a c d) - === - ((nd_id1 (a|=b)) ** (al_subst b c d) ;; - (al_subst a b d)) - - ; al_subst_left_identity : forall a b, (( [#al_reflexive_seq a#]**(nd_id _));; al_subst _ _ b) === nd_cancell - ; al_subst_right_identity : forall a b, (((nd_id _)**[#al_reflexive_seq a#] );; al_subst b _ _) === nd_cancelr - ; al_subst_commutes_with_horiz_expand_left : forall a b c d, - [#al_horiz_expand_left d#] ** [#al_horiz_expand_left d#];; al_subst (d,, a) (d,, b) (d,, c) - === al_subst a b c;; [#al_horiz_expand_left d#] - ; al_subst_commutes_with_horiz_expand_right : forall a b c d, - [#al_horiz_expand_right d#] ** [#al_horiz_expand_right d#] ;; al_subst (a,, d) (b,, d) (c,, d) - === al_subst a b c;; [#al_horiz_expand_right d#] - ; al_subst_commutes_with_vertical_expansion : forall t0 t1 t2, forall (f:[[]|=t1]/⋯⋯/[[]|=t0])(g:[[]|=t0]/⋯⋯/[[]|=t2]), - (((nd_rlecnac;; - ((([#al_reflexive_seq (t1,, [])#];; al_vert_expand_ant_left t1 (al_vert_expand_suc_right [] f));; - (nd_rule al_ant_cancelr));; (nd_rule al_suc_cancelr)) ** nd_id0);; - (nd_id [t1 |= t0]) ** - ((([#al_reflexive_seq (t0,, [])#];; al_vert_expand_ant_left t0 (al_vert_expand_suc_right [] g));; - (nd_rule al_ant_cancelr));; (nd_rule al_suc_cancelr)));; - al_subst t1 t0 t2) - === - ((([#al_reflexive_seq (t1,, [])#];; - (al_vert_expand_ant_left t1 (al_vert_expand_suc_right [] f);; - al_vert_expand_ant_left t1 (al_vert_expand_suc_right [] g)));; - (nd_rule al_ant_cancelr));; (nd_rule al_suc_cancelr)) + { al_eqv : @ND_Relation Judg Rule where "pf1 === pf2" := (@ndr_eqv _ _ al_eqv _ _ pf1 pf2) + ; al_tsr : TreeStructuralRules + ; al_subst : CutRule + ; al_sequent_join : SequentJoin }. - Notation "pf1 === pf2" := (@ndr_eqv _ _ al_eqv _ _ pf1 pf2) : temporary_scope3. - Open Scope temporary_scope3. - - Lemma al_subst_respects {PL:ProgrammingLanguage} : - forall {a b c}, - forall - (f : [] /⋯⋯/ [a |= b]) - (f' : [] /⋯⋯/ [a |= b]) - (g : [] /⋯⋯/ [b |= c]) - (g' : [] /⋯⋯/ [b |= c]), - (f === f') -> - (g === g') -> - (f ** g;; al_subst _ _ _) === (f' ** g';; al_subst _ _ _). - intros. - setoid_rewrite H. - setoid_rewrite H0. - reflexivity. - Defined. - - (* languages with unrestricted substructural rules (like that of Section 5) additionally implement this class *) - Class ProgrammingLanguageWithUnrestrictedSubstructuralRules := - { alwusr_al :> ProgrammingLanguage - ; al_contr : forall a b, Rule [a,,a |= b ] [ a |= b] - ; al_exch : forall a b c, Rule [a,,b |= c ] [(b,,a)|= c] - ; al_weak : forall a b, Rule [[] |= b ] [ a |= b] - }. - Coercion alwusr_al : ProgrammingLanguageWithUnrestrictedSubstructuralRules >-> ProgrammingLanguage. - - (* languages with a fixpoint operator *) - Class ProgrammingLanguageWithFixpointOperator `(al:ProgrammingLanguage) := - { alwfpo_al := al - ; al_fix : forall a b x, Rule [a,,x |= b,,x] [a |= b] - }. - Coercion alwfpo_al : ProgrammingLanguageWithFixpointOperator >-> ProgrammingLanguage. Section LanguageCategory. Context (PL:ProgrammingLanguage). (* category of judgments in a fixed type/coercion context *) - Definition JudgmentsL :=@Judgments_Category_monoidal _ Rule al_eqv. + Definition Judgments_cartesian := @Judgments_Category_CartesianCat _ Rule al_eqv. + + Definition JudgmentsL := Judgments_cartesian. Definition identityProof t : [] ~~{JudgmentsL}~~> [t |= t]. unfold hom; simpl. @@ -233,7 +111,7 @@ Section Programming_Language. apply al_subst. Defined. - Definition TypesLFC : ECategory JudgmentsL (Tree ??T) (fun x y => [x|=y]). + Definition TypesL : ECategory JudgmentsL (Tree ??T) (fun x y => [x|=y]). refine {| eid := identityProof ; ecomp := cutProof @@ -248,98 +126,107 @@ Section Programming_Language. apply al_subst_associativity'. Defined. - Definition TypesEnrichedInJudgments : Enrichment. - refine {| enr_c := TypesLFC |}. - Defined. - - Definition Types_first c : EFunctor TypesLFC TypesLFC (fun x => x,,c ). -(* + Definition Types_first c : EFunctor TypesL TypesL (fun x => x,,c ). + (* eapply Build_EFunctor; intros. eapply MonoidalCat_all_central. unfold eqv. simpl. -*) + *) admit. Defined. - Definition Types_second c : EFunctor TypesLFC TypesLFC (fun x => c,,x ). + Definition Types_second c : EFunctor TypesL TypesL (fun x => c,,x ). admit. Defined. - Definition Types_binoidal : BinoidalCat TypesLFC (@T_Branch _). + Definition Types_binoidal : BinoidalCat TypesL (@T_Branch _). refine - {| bin_first := TypesL_first - ; bin_second := TypesL_second + {| bin_first := Types_first + ; bin_second := Types_second |}. Defined. - Definition Pairing : prod_obj TypesL_binoidal TypesL_binoidal -> TypesL_binoidal. - admit. - Defined. - Definition Pairing_Functor : Functor (TypesL_binoidal ×× TypesL_binoidal) TypesL_binoidal Pairing. - admit. - Defined. - Definition TypesL : MonoidalCat TypesL_binoidal Pairing Pairing_Functor []. - admit. - Defined. + Definition TypesL_binoidal : BinoidalCat TypesL (@T_Branch _). + admit. + Defined. - Definition TypesLEnrichedInJudgments1 : SurjectiveEnrichment. - refine {| se_enr := TypesLEnrichedInJudgments0 |}. - simpl. - admit. - Defined. + Definition Types_PreMonoidal : PreMonoidalCat TypesL_binoidal []. + admit. + Defined. - Definition TypesLEnrichedInJudgments2 : MonoidalEnrichment. - refine {| me_enr := TypesLEnrichedInJudgments0 ; me_mon := TypesL |}. - simpl. - admit. + Definition TypesEnrichedInJudgments : Enrichment. + refine {| enr_c := TypesL |}. Defined. - Definition TypesLEnrichedInJudgments3 : MonicMonoidalEnrichment. - refine {| ffme_enr := TypesLEnrichedInJudgments2 |}; simpl. - admit. - admit. + Structure HasProductTypes := + { + }. + + (* need to prove that if we have cartesian tuples we have cartesian contexts *) + Definition LanguagesWithProductsAreSMME : HasProductTypes -> SurjectiveMonicMonoidalEnrichment TypesEnrichedInJudgments. admit. Defined. End LanguageCategory. - - (* - Definition ArrowInProgrammingLanguage (L:ProgrammingLanguage)(tc:Terminal (TypesL L)) := - FreydCategory (TypesL L) (TypesL L). + + Structure ProgrammingLanguageSMME := + { plsmme_pl : ProgrammingLanguage + ; plsmme_smme : SurjectiveMonicMonoidalEnrichment (TypesEnrichedInJudgments plsmme_pl) + }. + 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). - Definition TwoLevelLanguage (L1 L2:ProgrammingLanguage) := - Reification (TypesLEnrichedInJudgments1 L1) (TypesLEnrichedInJudgments3 L2) (me_i (TypesLEnrichedInJudgments3 L2)). + Context (GuestHost:TwoLevelLanguage). - Inductive NLevelLanguage : nat -> ProgrammingLanguage -> Type := - | NLevelLanguage_zero : forall lang, NLevelLanguage O lang - | NLevelLanguage_succ : forall L1 L2 n, TwoLevelLanguage L1 L2 -> NLevelLanguage n L1 -> NLevelLanguage (S n) L2. + Definition FlatObject (x:TypesL Host) := + forall y1 y2, not ((reification_r_obj GuestHost y1 y2)=x). - Definition OmegaLevelLanguage (PL:ProgrammingLanguage) : Type := - forall n:nat, NLevelLanguage n PL. + Definition FlatSubCategory := FullSubcategory (TypesL Host) FlatObject. - Section TwoLevelLanguage. - Context `(L12:TwoLevelLanguage L1 L2). + Section Flattening. - Definition FlatObject (x:TypesL L2) := - forall y1 y2, not ((reification_r_obj L12 y1 y2)=x). + 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. - Definition FlatSubCategory := FullSubcategory (TypesL L2) FlatObject. + End Flattening. - Context `(retraction :@Functor _ _ (TypesL L2) _ _ FlatSubCategory retract_obj). - Context `(retraction_inv :@Functor _ _ FlatSubCategory _ _ (TypesL L2) retract_inv_obj). - Context (retraction_works:retraction >>>> retraction_inv ~~~~ functor_id _). + End GArrowInLanguage. - Definition FlatteningOfReification := - (garrow_from_reification (TypesLEnrichedInJudgments1 L1) (TypesLEnrichedInJudgments3 L2) L12) >>>> retraction. - - Lemma FlatteningIsNotDestructive : - FlatteningOfReification >>>> retraction_inv >>>> RepresentableFunctor _ (me_i (TypesLEnrichedInJudgments3 L2)) ~~~~ L12. - admit. - Qed. + 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. - End TwoLevelLanguage. + Definition OmegaLevelLanguage : Type := + { f : nat -> ProgrammingLanguageSMME + & forall n, TwoLevelLanguage (f n) (f (S n)) }. Close Scope temporary_scope3. Close Scope al_scope. @@ -349,146 +236,3 @@ Section Programming_Language. End Programming_Language. Implicit Arguments ND [ Judgment ]. - -(* -Open Scope nd_scope. - Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_suc_right T Rule AL a b c d e) - with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv))) - as parametric_morphism_al_vert_expand_suc_right. - intros; apply al_vert_expand_suc_r_respects; auto. - Defined. - Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_suc_left T Rule AL a b c d e) - with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv))) - as parametric_morphism_al_vert_expand_suc_left. - intros; apply al_vert_expand_suc_l_respects; auto. - Defined. - Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_ant_right T Rule AL a b c d e) - with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv))) - as parametric_morphism_al_vert_expand_ant_right. - intros; apply al_vert_expand_ant_r_respects; auto. - Defined. - Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_ant_left T Rule AL a b c d e) - with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv))) - as parametric_morphism_al_vert_expand_ant_left. - intros; apply al_vert_expand_ant_l_respects; auto. - Defined. -Close Scope nd_scope. - -Notation "cs |= ss" := (@sequent _ cs ss) : al_scope. -(* -Definition mapJudg {T R:Type}(f:Tree ??T -> Tree ??R)(seq:@Judg T) : @Judg R := - match seq with sequentpair a b => pair (f a) (f b) end. -Implicit Arguments Judg [ ]. -*) - - -(* proofs which are generic and apply to any acceptable langauge (most of section 4) *) -Section Programming_Language_Facts. - - (* the ambient language about which we are proving facts *) - Context `(Lang : @ProgrammingLanguage T Rule). - - (* just for this section *) - Open Scope nd_scope. - Open Scope al_scope. - Open Scope pf_scope. - Notation "H /⋯⋯/ C" := (@ND Judg Rule H C) : temporary_scope4. - Notation "a === b" := (@ndr_eqv _ _ al_eqv _ _ a b) : temporary_scope4. - Open Scope temporary_scope4. - - Definition lang_al_eqv := al_eqv(ProgrammingLanguage:=Lang). - Existing Instance lang_al_eqv. - - Ltac distribute := - match goal with - [ |- ?G ] => - match G with - context ct [(?A ** ?B) ;; (?C ** ?D)] => - setoid_rewrite <- (ndr_prod_preserves_comp A B C D) - end - end. - - Ltac sequentialize_product A B := - match goal with - [ |- ?G ] => - match G with - | context ct [(A ** B)] => - setoid_replace (A ** B) - with ((A ** (nd_id _)) ;; ((nd_id _) ** B)) - (*with ((A ** (nd_id _)) ;; ((nd_id _) ** B))*) - end end. - Ltac sequentialize_product' A B := - match goal with - [ |- ?G ] => - match G with - | context ct [(A ** B)] => - setoid_replace (A ** B) - with (((nd_id _) ** B) ;; (A ** (nd_id _))) - (*with ((A ** (nd_id _)) ;; ((nd_id _) ** B))*) - end end. - Ltac distribute' := - match goal with - [ |- ?G ] => - match G with - context ct [(?A ;; ?B) ** (?C ;; ?D)] => - setoid_rewrite (ndr_prod_preserves_comp A B C D) - end - end. - Ltac distribute_left_product_with_id := - match goal with - [ |- ?G ] => - match G with - context ct [(nd_id ?A) ** (?C ;; ?D)] => - setoid_replace ((nd_id A) ** (C ;; D)) with ((nd_id A ;; nd_id A) ** (C ;; D)); - [ setoid_rewrite (ndr_prod_preserves_comp (nd_id A) C (nd_id A) D) | idtac ] - end - end. - Ltac distribute_right_product_with_id := - match goal with - [ |- ?G ] => - match G with - context ct [(?C ;; ?D) ** (nd_id ?A)] => - setoid_replace ((C ;; D) ** (nd_id A)) with ((C ;; D) ** (nd_id A ;; nd_id A)); - [ setoid_rewrite (ndr_prod_preserves_comp C (nd_id A) D (nd_id A)) | idtac ] - end - end. - - (* another phrasing of al_subst_associativity; obligations tend to show up in this form *) - Lemma al_subst_associativity'' : - forall (a b : T) (f : [] /⋯⋯/ [[a] |= [b]]) (c : T) (g : [] /⋯⋯/ [[b] |= [c]]) - (d : T) (h : [] /⋯⋯/ [[c] |= [d]]), - nd_llecnac;; ((nd_llecnac;; (f ** g;; al_subst [a] [b] [c])) ** h;; al_subst [a] [c] [d]) === - nd_llecnac;; (f ** (nd_llecnac;; (g ** h;; al_subst [b] [c] [d]));; al_subst [a] [b] [d]). - intros. - sequentialize_product' (nd_llecnac;; (f ** g;; al_subst [a] [b] [c])) h. - repeat setoid_rewrite <- ndr_comp_associativity. - distribute_right_product_with_id. - repeat setoid_rewrite ndr_comp_associativity. - set (@al_subst_associativity) as q. setoid_rewrite q. clear q. - apply ndr_comp_respects; try reflexivity. - repeat setoid_rewrite <- ndr_comp_associativity. - apply ndr_comp_respects; try reflexivity. - sequentialize_product f ((nd_llecnac;; g ** h);; al_subst [b] [c] [d]). - distribute_left_product_with_id. - repeat setoid_rewrite <- ndr_comp_associativity. - apply ndr_comp_respects; try reflexivity. - setoid_rewrite <- ndr_prod_preserves_comp. - repeat setoid_rewrite ndr_comp_left_identity. - repeat setoid_rewrite ndr_comp_right_identity. - admit. - admit. - admit. - admit. - admit. - Qed. - - Close Scope temporary_scope4. - Close Scope al_scope. - Close Scope nd_scope. - Close Scope pf_scope. - Close Scope isomorphism_scope. -End Programming_Language_Facts. - -(*Coercion AL_SurjectiveEnrichment : ProgrammingLanguage >-> SurjectiveEnrichment.*) -(*Coercion AL_MonicMonoidalEnrichment : ProgrammingLanguage >-> MonicMonoidalEnrichment.*) -*) \ No newline at end of file diff --git a/src/ReificationCategory.v b/src/ReificationCategory.v index 4d83b78..eb6b5fd 100644 --- a/src/ReificationCategory.v +++ b/src/ReificationCategory.v @@ -9,6 +9,21 @@ Generalizable All Variables. Require Import Preamble. Require Import General. -Require Import NaturalDeduction. -Require Import Coq.Strings.String. -Require Import Coq.Lists.List. +Require Import Categories_ch1_3. +Require Import Functors_ch1_4. +Require Import Isomorphisms_ch1_5. +Require Import ProductCategories_ch1_6_1. +Require Import OppositeCategories_ch1_6_2. +Require Import 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 Reification. + +Instance CategoryOfReifications : Category SMME Reification. + admit. + Qed. \ No newline at end of file diff --git a/src/ReificationFromGeneralizedArrow.v b/src/ReificationFromGeneralizedArrow.v index 678de5c..8d94dca 100644 --- a/src/ReificationFromGeneralizedArrow.v +++ b/src/ReificationFromGeneralizedArrow.v @@ -24,7 +24,7 @@ Require Import RepresentableStructure_ch7_2. Require Import Reification. Require Import GeneralizedArrow. -Definition reification_from_garrow (K:Enrichment) (C:MonoidalEnrichment) (garrow : GeneralizedArrow K C) +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 diff --git a/src/ReificationsEquivalentToGeneralizedArrows.v b/src/ReificationsEquivalentToGeneralizedArrows.v index a81c895..1b626a2 100644 --- a/src/ReificationsEquivalentToGeneralizedArrows.v +++ b/src/ReificationsEquivalentToGeneralizedArrows.v @@ -83,4 +83,8 @@ Section ReificationsEquivalentToGeneralizedArrows. apply (step1_niso K C (reification_from_garrow K C garrow)). Qed. + Theorem ReificationsAreGArrows : IsomorphicCategories CategoryOfReifications CategoryOfGeneralizedArrows. + admit. + Qed. + End ReificationsEquivalentToGeneralizedArrows. -- 1.7.10.4