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 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
*)
Section Programming_Language.
- (* Formalized Definition 4.1.1, production $\tau$ *)
Context {T : Type}. (* types of the language *)
Context (Judg : Type).
Context (sequent : Tree ??T -> Tree ??T -> Judg).
- Notation "cs |= ss" := (sequent cs ss) : al_scope.
+ Notation "cs |= ss" := (sequent cs ss) : pl_scope.
(* Because of term irrelevance we need only store the *erased* (def
* 4.4) trees; for this reason there is no Coq type directly
* corresponding to productions $e$ and $x$ of 4.1.1, and TreeOT can
Context {Rule : Tree ??Judg -> Tree ??Judg -> Type}.
- Notation "H /⋯⋯/ C" := (ND Rule H C) : al_scope.
+ Notation "H /⋯⋯/ C" := (ND Rule H C) : pl_scope.
Open Scope pf_scope.
Open Scope nd_scope.
- Open Scope al_scope.
+ Open Scope pl_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 --
* 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))
- }.
-
- 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]
+ { pl_eqv : @ND_Relation Judg Rule where "pf1 === pf2" := (@ndr_eqv _ _ pl_eqv _ _ pf1 pf2)
+ ; pl_tsr :> @TreeStructuralRules Judg Rule T sequent
+ ; pl_sc :> @SequentCalculus Judg Rule _ sequent
+ ; pl_subst :> @CutRule Judg Rule _ sequent pl_eqv pl_sc
+ ; pl_sequent_join :> @SequentExpansion Judg Rule T sequent pl_eqv pl_sc pl_subst
}.
- 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.
+ Notation "pf1 === pf2" := (@ndr_eqv _ _ pl_eqv _ _ pf1 pf2) : temporary_scope3.
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 pl_eqv.
+
+ Definition JudgmentsL := Judgments_cartesian.
Definition identityProof t : [] ~~{JudgmentsL}~~> [t |= t].
unfold hom; simpl.
- apply nd_rule.
- apply al_reflexive_seq.
+ apply nd_seq_reflexive.
Defined.
Definition cutProof a b c : [a |= b],,[b |= c] ~~{JudgmentsL}~~> [a |= c].
unfold hom; simpl.
- apply al_subst.
+ apply pl_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
apply MonoidalCat_all_central.
apply MonoidalCat_all_central.
unfold identityProof; unfold cutProof; simpl.
- apply al_subst_left_identity.
+ apply nd_cut_left_identity.
unfold identityProof; unfold cutProof; simpl.
- apply al_subst_right_identity.
+ apply nd_cut_right_identity.
unfold identityProof; unfold cutProof; simpl.
- apply al_subst_associativity'.
+ symmetry.
+ apply nd_cut_associativity.
Defined.
- Definition TypesLEnrichedInJudgments0 : Enrichment.
- refine {| enr_c := TypesLFC |}.
+ Definition Types_first c : EFunctor TypesL TypesL (fun x => x,,c ).
+ refine {| efunc := fun x y => (nd_rule (@se_expand_right _ _ _ _ _ _ _ (@pl_sequent_join PL) c x y)) |}.
+ intros; apply MonoidalCat_all_central.
+ intros. unfold ehom. unfold hom. unfold identityProof. unfold eid. simpl. unfold identityProof.
+ apply se_reflexive_right.
+ intros. unfold ehom. unfold comp. simpl. unfold cutProof.
+ rewrite <- (@ndr_prod_preserves_comp _ _ pl_eqv _ _ [#se_expand_right _ c#] _ _ (nd_id1 (b|=c0))
+ _ (nd_id1 (a,,c |= b,,c)) _ [#se_expand_right _ c#]).
+ setoid_rewrite (@ndr_comp_right_identity _ _ pl_eqv _ [a,, c |= b,, c]).
+ setoid_rewrite (@ndr_comp_left_identity _ _ pl_eqv [b |= c0]).
+ apply se_cut_right.
Defined.
- Definition TypesL_first c : EFunctor TypesLFC TypesLFC (fun x => x,,c ).
-(*
- eapply Build_EFunctor; intros.
- eapply MonoidalCat_all_central.
- unfold eqv.
- simpl.
-*)
- admit.
- Defined.
-
- Definition TypesL_second c : EFunctor TypesLFC TypesLFC (fun x => c,,x ).
- admit.
+ Definition Types_second c : EFunctor TypesL TypesL (fun x => c,,x).
+ eapply Build_EFunctor.
+ instantiate (1:=(fun x y => (nd_rule (@se_expand_left _ _ _ _ _ _ _ (@pl_sequent_join PL) c x y)))).
+ intros; apply MonoidalCat_all_central.
+ intros. unfold ehom. unfold hom. unfold identityProof. unfold eid. simpl. unfold identityProof.
+ apply se_reflexive_left.
+ intros. unfold ehom. unfold comp. simpl. unfold cutProof.
+ rewrite <- (@ndr_prod_preserves_comp _ _ pl_eqv _ _ [#se_expand_left _ c#] _ _ (nd_id1 (b|=c0))
+ _ (nd_id1 (c,,a |= c,,b)) _ [#se_expand_left _ c#]).
+ setoid_rewrite (@ndr_comp_right_identity _ _ pl_eqv _ [c,,a |= c,,b]).
+ setoid_rewrite (@ndr_comp_left_identity _ _ pl_eqv [b |= c0]).
+ apply se_cut_left.
Defined.
- Definition TypesL_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 [].
+ Definition Types_PreMonoidal : PreMonoidalCat Types_binoidal [].
admit.
Defined.
- Definition TypesLEnrichedInJudgments1 : SurjectiveEnrichment.
- refine {| se_enr := TypesLEnrichedInJudgments0 |}.
- simpl.
- admit.
+ Definition TypesEnrichedInJudgments : Enrichment.
+ refine {| enr_c := TypesL |}.
Defined.
- Definition TypesLEnrichedInJudgments2 : MonoidalEnrichment.
- refine {| me_enr := TypesLEnrichedInJudgments0 ; me_mon := TypesL |}.
- simpl.
- admit.
- Defined.
+ Structure HasProductTypes :=
+ {
+ }.
- Definition TypesLEnrichedInJudgments3 : MonicMonoidalEnrichment.
- refine {| ffme_enr := TypesLEnrichedInJudgments2 |}; simpl.
- admit.
- admit.
+ (* 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).
- *)
- Definition TwoLevelLanguage (L1 L2:ProgrammingLanguage) :=
- Reification (TypesLEnrichedInJudgments1 L1) (TypesLEnrichedInJudgments3 L2) (me_i (TypesLEnrichedInJudgments3 L2)).
+ 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).
- 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.
+ Context (GuestHost:TwoLevelLanguage).
- Definition OmegaLevelLanguage (PL:ProgrammingLanguage) : Type :=
- forall n:nat, NLevelLanguage n PL.
+ Definition FlatObject (x:TypesL Host) :=
+ forall y1 y2, not ((reification_r_obj GuestHost y1 y2)=x).
- Section TwoLevelLanguage.
- Context `(L12:TwoLevelLanguage L1 L2).
+ Definition FlatSubCategory := FullSubcategory (TypesL Host) FlatObject.
- Definition FlatObject (x:TypesL L2) :=
- forall y1 y2, not ((reification_r_obj L12 y1 y2)=x).
+ Section Flattening.
- Definition FlatSubCategory := FullSubcategory (TypesL L2) FlatObject.
+ 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.
- 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 Flattening.
- Definition FlatteningOfReification :=
- (garrow_from_reification (TypesLEnrichedInJudgments1 L1) (TypesLEnrichedInJudgments3 L2) L12) >>>> retraction.
+ End GArrowInLanguage.
- 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.
+ Close Scope pl_scope.
Close Scope nd_scope.
Close Scope pf_scope.
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
projects / coq-hetmet.git / blobdiff