(*********************************************************************************************************************************)
(* ProgrammingLanguage *)
(* *)
-(* Basic assumptions about programming languages . *)
+(* Basic assumptions about programming languages. *)
(* *)
(*********************************************************************************************************************************)
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 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.
Require Import RepresentableStructure_ch7_2.
+Require Import FunctorCategories_ch7_7.
+
+Require Import Enrichments.
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.
-
-
-(*
- * Everything in the rest of this section is just groundwork meant to
- * build up to the definition of the ProgrammingLanguage class, which
- * appears at the end of the section. References to "the instance"
- * mean instances of that class. Think of this section as being one
- * big Class { ... } definition, except that we declare most of the
- * stuff outside the curly brackets in order to take advantage of
- * Coq's section mechanism.
- *)
+
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.
- (* 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
- * be used for productions $\Gamma$ and $\Sigma$ *)
+ Definition PLJudg := (Tree ??T) * (Tree ??T).
+ Definition sequent := @pair (Tree ??T) (Tree ??T).
+ Notation "cs |= ss" := (sequent cs ss) : pl_scope.
- (* to do: sequent calculus equals natural deduction over sequents, theorem equals sequent with null antecedent, *)
+ Context {Rule : Tree ??PLJudg -> Tree ??PLJudg -> Type}.
- 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.
-
- (* 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 --
- * so long as we have access to the equivalence relation upon
- * proof-conclusions. Moreover, hiding the expressions actually
- * makes the encoding in CiC work out easier for two reasons:
- *
- * 1. Because the denotation function is provided a proof rather
- * than a term, it is a total function (the denotation function is
- * often undefined for ill-typed terms).
- *
- * 2. We can define arr_composition of proofs without having to know how
- * to compose expressions. The latter task is left up to the client
- * function which extracts an expression from a completed proof.
- *
- * 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]
- }.
- Coercion alwusr_al : ProgrammingLanguageWithUnrestrictedSubstructuralRules >-> ProgrammingLanguage.
+ Open Scope pl_scope.
- (* 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]
+ Class ProgrammingLanguage :=
+ { pl_eqv0 : @ND_Relation PLJudg Rule
+ ; pl_snd :> @SequentND PLJudg Rule _ sequent
+ ; pl_cnd :> @ContextND PLJudg Rule T sequent pl_snd
+ ; pl_eqv1 :> @SequentND_Relation PLJudg Rule _ sequent pl_snd pl_eqv0
+ ; pl_eqv :> @ContextND_Relation PLJudg Rule _ sequent pl_snd pl_cnd pl_eqv0 pl_eqv1
}.
- 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 snd_initial.
Defined.
Definition cutProof a b c : [a |= b],,[b |= c] ~~{JudgmentsL}~~> [a |= c].
unfold hom; simpl.
- apply al_subst.
+ apply snd_cut.
Defined.
- Definition TypesLFC : ECategory JudgmentsL (Tree ??T) (fun x y => [x|=y]).
+ Existing Instance pl_eqv.
+
+ Definition TypesL : ECategory JudgmentsL (Tree ??T) (fun x y => [x|=y]).
refine
{| eid := identityProof
; ecomp := cutProof
|}; intros.
- apply MonoidalCat_all_central.
- apply MonoidalCat_all_central.
- unfold identityProof; unfold cutProof; simpl.
- apply al_subst_left_identity.
- unfold identityProof; unfold cutProof; simpl.
- apply al_subst_right_identity.
- unfold identityProof; unfold cutProof; simpl.
- apply al_subst_associativity'.
+ apply (mon_commutative(MonoidalCat:=JudgmentsL)).
+ apply (mon_commutative(MonoidalCat:=JudgmentsL)).
+ unfold identityProof; unfold cutProof; simpl; eapply cndr_inert. apply pl_eqv. auto. auto.
+ unfold identityProof; unfold cutProof; simpl; eapply cndr_inert. apply pl_eqv. auto. auto.
+ unfold identityProof; unfold cutProof; simpl; eapply cndr_inert. apply pl_eqv. auto. auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
Defined.
- Definition TypesEnrichedInJudgments : Enrichment.
- refine {| enr_c := TypesLFC |}.
+ Instance Types_first c : EFunctor TypesL TypesL (fun x => x,,c ) :=
+ { efunc := fun x y => cnd_expand_right(ContextND:=pl_cnd) x y c }.
+ intros; apply (mon_commutative(MonoidalCat:=JudgmentsL)).
+ intros. unfold ehom. unfold hom. unfold identityProof. unfold eid. simpl. unfold identityProof.
+ apply (cndr_inert pl_cnd); auto.
+ intros. unfold ehom. unfold comp. simpl. unfold cutProof.
+ rewrite <- (@ndr_prod_preserves_comp _ _ pl_eqv _ _ (cnd_expand_right _ _ c) _ _ (nd_id1 (b|=c0))
+ _ (nd_id1 (a,,c |= b,,c)) _ (cnd_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]).
+ simpl; eapply cndr_inert. apply pl_eqv. auto. auto.
Defined.
- Definition Types_first c : EFunctor TypesLFC TypesLFC (fun x => x,,c ).
-(*
- eapply Build_EFunctor; intros.
- eapply MonoidalCat_all_central.
- unfold eqv.
- simpl.
-*)
- admit.
+ Instance Types_second c : EFunctor TypesL TypesL (fun x => c,,x) :=
+ { efunc := fun x y => ((@cnd_expand_left _ _ _ _ _ _ x y c)) }.
+ intros; apply (mon_commutative(MonoidalCat:=JudgmentsL)).
+ intros. unfold ehom. unfold hom. unfold identityProof. unfold eid. simpl. unfold identityProof.
+ eapply cndr_inert; auto. apply pl_eqv.
+ intros. unfold ehom. unfold comp. simpl. unfold cutProof.
+ rewrite <- (@ndr_prod_preserves_comp _ _ pl_eqv _ _ (cnd_expand_left _ _ c) _ _ (nd_id1 (b|=c0))
+ _ (nd_id1 (c,,a |= c,,b)) _ (cnd_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]).
+ simpl; eapply cndr_inert. apply pl_eqv. auto. auto.
Defined.
- Definition Types_second c : EFunctor TypesLFC TypesLFC (fun x => c,,x ).
- admit.
- Defined.
-
- Definition Types_binoidal : BinoidalCat TypesLFC (@T_Branch _).
+ Definition Types_binoidal : EBinoidalCat TypesL.
refine
- {| bin_first := TypesL_first
- ; bin_second := TypesL_second
+ {| ebc_first := Types_first
+ ; ebc_second := Types_second
|}.
Defined.
- Definition Pairing : prod_obj TypesL_binoidal TypesL_binoidal -> TypesL_binoidal.
- admit.
+ Instance Types_assoc_iso a b c : Isomorphic(C:=TypesL) ((a,,b),,c) (a,,(b,,c)) :=
+ { iso_forward := snd_initial _ ;; cnd_ant_cossa _ a b c
+ ; iso_backward := snd_initial _ ;; cnd_ant_assoc _ a b c
+ }.
+ simpl; eapply cndr_inert. unfold identityProof; apply pl_eqv. auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ auto.
+ simpl; eapply cndr_inert. unfold identityProof; apply pl_eqv. auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ auto.
+ Defined.
+
+ Instance Types_cancelr_iso a : Isomorphic(C:=TypesL) (a,,[]) a :=
+ { iso_forward := snd_initial _ ;; cnd_ant_rlecnac _ a
+ ; iso_backward := snd_initial _ ;; cnd_ant_cancelr _ a
+ }.
+ unfold eqv; unfold comp; simpl.
+ eapply cndr_inert. apply pl_eqv. auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ auto.
+ unfold eqv; unfold comp; simpl.
+ eapply cndr_inert. apply pl_eqv. auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ auto.
Defined.
- Definition Pairing_Functor : Functor (TypesL_binoidal ×× TypesL_binoidal) TypesL_binoidal Pairing.
- admit.
+
+ Instance Types_cancell_iso a : Isomorphic(C:=TypesL) ([],,a) a :=
+ { iso_forward := snd_initial _ ;; cnd_ant_llecnac _ a
+ ; iso_backward := snd_initial _ ;; cnd_ant_cancell _ a
+ }.
+ unfold eqv; unfold comp; simpl.
+ eapply cndr_inert. apply pl_eqv. auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ auto.
+ unfold eqv; unfold comp; simpl.
+ eapply cndr_inert. apply pl_eqv. auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ auto.
Defined.
- Definition TypesL : MonoidalCat TypesL_binoidal Pairing Pairing_Functor [].
+
+ 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.
Defined.
- Definition TypesLEnrichedInJudgments1 : SurjectiveEnrichment.
- refine {| se_enr := TypesLEnrichedInJudgments0 |}.
- simpl.
+ Instance Types_cancelr : Types_first [] <~~~> functor_id _ :=
+ { ni_iso := Types_cancelr_iso }.
+ intros; simpl.
admit.
Defined.
- Definition TypesLEnrichedInJudgments2 : MonoidalEnrichment.
- refine {| me_enr := TypesLEnrichedInJudgments0 ; me_mon := TypesL |}.
- simpl.
+ Instance Types_cancell : Types_second [] <~~~> functor_id _ :=
+ { ni_iso := Types_cancell_iso }.
admit.
Defined.
- Definition TypesLEnrichedInJudgments3 : MonicMonoidalEnrichment.
- refine {| ffme_enr := TypesLEnrichedInJudgments2 |}; simpl.
- admit.
- admit.
+ 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.
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)).
-
- 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 OmegaLevelLanguage (PL:ProgrammingLanguage) : Type :=
- forall n:nat, NLevelLanguage n PL.
-
- Section TwoLevelLanguage.
- Context `(L12:TwoLevelLanguage L1 L2).
-
- Definition FlatObject (x:TypesL L2) :=
- forall y1 y2, not ((reification_r_obj L12 y1 y2)=x).
-
- Definition FlatSubCategory := FullSubcategory (TypesL L2) FlatObject.
-
- 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 _).
+ 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.
+ Defined.
- Definition FlatteningOfReification :=
- (garrow_from_reification (TypesLEnrichedInJudgments1 L1) (TypesLEnrichedInJudgments3 L2) L12) >>>> retraction.
+ Instance TypesL_PreMonoidal : PreMonoidalCat Types_binoidal [] :=
+ { pmon_assoc := Types_assoc
+ ; pmon_cancell := Types_cancell
+ ; pmon_cancelr := Types_cancelr
+ ; pmon_assoc_rr := Types_assoc_rr
+ ; pmon_assoc_ll := Types_assoc_ll
+ }.
+ apply Build_Pentagon.
+ intros; simpl.
+ eapply cndr_inert. apply pl_eqv.
+ apply ndpc_comp.
+ apply ndpc_comp.
+ auto.
+ apply ndpc_comp.
+ apply ndpc_prod.
+ apply ndpc_comp.
+ apply ndpc_comp.
+ auto.
+ apply ndpc_comp.
+ auto.
+ auto.
+ auto.
+ auto.
+ auto.
+ auto.
+ apply ndpc_comp.
+ apply ndpc_comp.
+ auto.
+ apply ndpc_comp.
+ auto.
+ auto.
+ auto.
+ apply Build_Triangle; intros; simpl.
+ eapply cndr_inert. apply pl_eqv.
+ auto.
+ apply ndpc_comp.
+ apply ndpc_comp.
+ auto.
+ apply ndpc_comp.
+ auto.
+ auto.
+ auto.
+ eapply cndr_inert. apply pl_eqv. auto.
+ auto.
+ intros; simpl; reflexivity.
+ intros; simpl; reflexivity.
+ admit. (* assoc central *)
+ admit. (* cancelr central *)
+ admit. (* cancell central *)
+ Defined.
- Lemma FlatteningIsNotDestructive :
- FlatteningOfReification >>>> retraction_inv >>>> RepresentableFunctor _ (me_i (TypesLEnrichedInJudgments3 L2)) ~~~~ L12.
- admit.
- Qed.
+ Definition TypesEnrichedInJudgments : SurjectiveEnrichment.
+ refine
+ {| senr_c_pm := TypesL_PreMonoidal
+ ; senr_v := JudgmentsL
+ ; senr_v_bin := Judgments_Category_binoidal _
+ ; senr_v_pmon := Judgments_Category_premonoidal _
+ ; senr_v_mon := Judgments_Category_monoidal _
+ ; senr_c_bin := Types_binoidal
+ ; senr_c := TypesL
+ |}.
+ Defined.
- End TwoLevelLanguage.
-
- Close Scope temporary_scope3.
- Close Scope al_scope.
- Close Scope nd_scope.
- Close Scope pf_scope.
+ End LanguageCategory.
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