src/ProgrammingLanguage.v

   1 (*********************************************************************************************************************************)
   2 (* ProgrammingLanguage                                                                                                           *)
   3 (*                                                                                                                               *)
   4 (*   Basic assumptions about programming languages .                                                                             *)
   5 (*                                                                                                                               *)
   6 (*********************************************************************************************************************************)
   7
   8 Generalizable All Variables.
   9 Require Import Preamble.
  10 Require Import General.
  11 Require Import Categories_ch1_3.
  12 Require Import InitialTerminal_ch2_2.
  13 Require Import Functors_ch1_4.
  14 Require Import Isomorphisms_ch1_5.
  15 Require Import ProductCategories_ch1_6_1.
  16 Require Import OppositeCategories_ch1_6_2.
  17 Require Import Enrichment_ch2_8.
  18 Require Import Subcategories_ch7_1.
  19 Require Import NaturalTransformations_ch7_4.
  20 Require Import NaturalIsomorphisms_ch7_5.
  21 Require Import MonoidalCategories_ch7_8.
  22 Require Import Coherence_ch7_8.
  23 Require Import Enrichment_ch2_8.
  24 Require Import RepresentableStructure_ch7_2.
  25 Require Import FunctorCategories_ch7_7.
  26
  27 Require Import NaturalDeduction.
  28 Require Import NaturalDeductionCategory.
  29
  30 Require Import FreydCategories.
  31
  32 Require Import Reification.
  33 Require Import GeneralizedArrow.
  34 Require Import GeneralizedArrowFromReification.
  35 Require Import ReificationFromGeneralizedArrow.
  36
  37 (*
  38  *  Everything in the rest of this section is just groundwork meant to
  39  *  build up to the definition of the ProgrammingLanguage class, which
  40  *  appears at the end of the section.  References to "the instance"
  41  *  mean instances of that class.  Think of this section as being one
  42  *  big Class { ... } definition, except that we declare most of the
  43  *  stuff outside the curly brackets in order to take advantage of
  44  *  Coq's section mechanism.
  45  *)
  46 Section Programming_Language.
  47
  48   Context {T    : Type}.               (* types of the language *)
  49
  50   Context (Judg : Type).
  51   Context (sequent : Tree ??T -> Tree ??T -> Judg).
  52      Notation "cs |= ss" := (sequent cs ss) : pl_scope.
  53      (* Because of term irrelevance we need only store the *erased* (def
  54       * 4.4) trees; for this reason there is no Coq type directly
  55       * corresponding to productions $e$ and $x$ of 4.1.1, and TreeOT can
  56       * be used for productions $\Gamma$ and $\Sigma$ *)
  57
  58   (* to do: sequent calculus equals natural deduction over sequents, theorem equals sequent with null antecedent, *)
  59
  60   Context {Rule : Tree ??Judg -> Tree ??Judg -> Type}.
  61
  62   Notation "H /⋯⋯/ C" := (ND Rule H C) : pl_scope.
  63
  64   Open Scope pf_scope.
  65   Open Scope nd_scope.
  66   Open Scope pl_scope.
  67
  68   (*
  69    *
  70    * Note that from this abstract interface, the terms (expressions)
  71    * in the proof are not accessible at all; they don't need to be --
  72    * so long as we have access to the equivalence relation upon
  73    * proof-conclusions.  Moreover, hiding the expressions actually
  74    * makes the encoding in CiC work out easier for two reasons:
  75    *
  76    *  1. Because the denotation function is provided a proof rather
  77    *     than a term, it is a total function (the denotation function is
  78    *     often undefined for ill-typed terms).
  79    *
  80    *  2. We can define arr_composition of proofs without having to know how
  81    *     to compose expressions.  The latter task is left up to the client
  82    *     function which extracts an expression from a completed proof.
  83    *
  84    * This also means that we don't need an explicit proof obligation for 4.1.2.
  85    *)
  86   Class ProgrammingLanguage :=
  87   { pl_eqv                :  @ND_Relation Judg Rule where "pf1 === pf2" := (@ndr_eqv _ _ pl_eqv _ _ pf1 pf2)
  88   ; pl_tsr                :> @TreeStructuralRules Judg Rule T sequent
  89   ; pl_sc                 :> @SequentCalculus Judg Rule _ sequent
  90   ; pl_subst              :> @CutRule Judg Rule _ sequent pl_eqv pl_sc
  91   ; pl_sequent_join       :> @SequentExpansion Judg Rule T sequent pl_eqv pl_sc pl_subst
  92   }.
  93   Notation "pf1 === pf2" := (@ndr_eqv _ _ pl_eqv _ _ pf1 pf2) : temporary_scope3.
  94
  95   Section LanguageCategory.
  96
  97     Context (PL:ProgrammingLanguage).
  98
  99     (* category of judgments in a fixed type/coercion context *)
 100     Definition Judgments_cartesian := @Judgments_Category_CartesianCat _ Rule pl_eqv.
 101
 102     Definition JudgmentsL          := Judgments_cartesian.
 103
 104     Definition identityProof t : [] ~~{JudgmentsL}~~> [t |= t].
 105       unfold hom; simpl.
 106       apply nd_seq_reflexive.
 107       Defined.
 108
 109     Definition cutProof a b c : [a |= b],,[b |= c] ~~{JudgmentsL}~~> [a |= c].
 110       unfold hom; simpl.
 111       apply pl_subst.
 112       Defined.
 113
 114     Definition TypesL : ECategory JudgmentsL (Tree ??T) (fun x y => [x|=y]).
 115       refine
 116       {| eid   := identityProof
 117        ; ecomp := cutProof
 118       |}; intros.
 119       apply MonoidalCat_all_central.
 120       apply MonoidalCat_all_central.
 121       unfold identityProof; unfold cutProof; simpl.
 122       apply nd_cut_left_identity.
 123       unfold identityProof; unfold cutProof; simpl.
 124       apply nd_cut_right_identity.
 125       unfold identityProof; unfold cutProof; simpl.
 126       symmetry.
 127       apply nd_cut_associativity.
 128       Defined.
 129
 130     Definition Types_first c : EFunctor TypesL TypesL (fun x => x,,c ).
 131       refine {| efunc := fun x y => (nd_rule (@se_expand_right _ _ _ _ _ _ _ (@pl_sequent_join PL) c x y)) |}.
 132       intros; apply MonoidalCat_all_central.
 133       intros. unfold ehom. unfold hom. unfold identityProof. unfold eid. simpl. unfold identityProof.
 134       apply se_reflexive_right.
 135       intros. unfold ehom. unfold comp. simpl. unfold cutProof.
 136       rewrite <- (@ndr_prod_preserves_comp _ _ pl_eqv _ _ [#se_expand_right _ c#] _ _ (nd_id1 (b|=c0))
 137                   _ (nd_id1 (a,,c |= b,,c))  _ [#se_expand_right _ c#]).
 138       setoid_rewrite (@ndr_comp_right_identity _ _ pl_eqv _ [a,, c |= b,, c]).
 139       setoid_rewrite (@ndr_comp_left_identity  _ _ pl_eqv [b |= c0]).
 140       apply se_cut_right.
 141       Defined.
 142
 143     Definition Types_second c : EFunctor TypesL TypesL (fun x => c,,x).
 144       eapply Build_EFunctor.
 145       instantiate (1:=(fun x y => (nd_rule (@se_expand_left _ _ _ _ _ _ _ (@pl_sequent_join PL) c x y)))).
 146       intros; apply MonoidalCat_all_central.
 147       intros. unfold ehom. unfold hom. unfold identityProof. unfold eid. simpl. unfold identityProof.
 148       apply se_reflexive_left.
 149       intros. unfold ehom. unfold comp. simpl. unfold cutProof.
 150       rewrite <- (@ndr_prod_preserves_comp _ _ pl_eqv _ _ [#se_expand_left _ c#] _ _ (nd_id1 (b|=c0))
 151                   _ (nd_id1 (c,,a |= c,,b))  _ [#se_expand_left _ c#]).
 152       setoid_rewrite (@ndr_comp_right_identity _ _ pl_eqv _ [c,,a |= c,,b]).
 153       setoid_rewrite (@ndr_comp_left_identity  _ _ pl_eqv [b |= c0]).
 154       apply se_cut_left.
 155       Defined.
 156
 157     Definition Types_binoidal : BinoidalCat TypesL (@T_Branch _).
 158       refine
 159         {| bin_first  := Types_first
 160          ; bin_second := Types_second
 161          |}.
 162       Defined.
 163
 164     Definition Types_PreMonoidal : PreMonoidalCat Types_binoidal [].
 165       admit.
 166       Defined.
 167
 168     Definition TypesEnrichedInJudgments : Enrichment.
 169       refine {| enr_c := TypesL |}.
 170       Defined.
 171
 172     Structure HasProductTypes :=
 173     {
 174     }.
 175
 176     (* need to prove that if we have cartesian tuples we have cartesian contexts *)
 177     Definition LanguagesWithProductsAreSMME : HasProductTypes -> SurjectiveMonicMonoidalEnrichment TypesEnrichedInJudgments.
 178       admit.
 179       Defined.
 180
 181   End LanguageCategory.
 182 End Programming_Language.
 183
 184 Structure ProgrammingLanguageSMME :=
 185 { plsmme_t       : Type
 186 ; plsmme_judg    : Type
 187 ; plsmme_sequent : Tree ??plsmme_t -> Tree ??plsmme_t -> plsmme_judg
 188 ; plsmme_rule    : Tree ??plsmme_judg -> Tree ??plsmme_judg -> Type
 189 ; plsmme_pl      : @ProgrammingLanguage plsmme_t plsmme_judg plsmme_sequent plsmme_rule
 190 ; plsmme_smme    : SurjectiveMonicMonoidalEnrichment (TypesEnrichedInJudgments _ _ plsmme_pl)
 191 }.
 192 Coercion plsmme_pl   : ProgrammingLanguageSMME >-> ProgrammingLanguage.
 193 Coercion plsmme_smme : ProgrammingLanguageSMME >-> SurjectiveMonicMonoidalEnrichment.
 194
 195 Section ArrowInLanguage.
 196   Context  (Host:ProgrammingLanguageSMME).
 197   Context `(CC:CartesianCat (me_mon Host)).
 198   Context `(K:@ECategory _ _ _ _ _ _ (@car_mn _ _ _ _ _ _ _ CC) C Kehom).
 199   Context `(pmc:PreMonoidalCat K bobj mobj (@one _ _ _ (cartesian_terminal C))).
 200     (* FIXME *)
 201     (*
 202     Definition ArrowInProgrammingLanguage :=
 203       @FreydCategory _ _ _ _ _ _ (@car_mn _ _ _ _ _ _ _ CC) _ _ _ _ pmc.
 204       *)
 205 End ArrowInLanguage.
 206
 207 Section GArrowInLanguage.
 208   Context (Guest:ProgrammingLanguageSMME).
 209   Context (Host :ProgrammingLanguageSMME).
 210   Definition GeneralizedArrowInLanguage := GeneralizedArrow Guest Host.
 211
 212   (* FIXME
 213   Definition ArrowsAreGeneralizedArrows : ArrowInProgrammingLanguage -> GeneralizedArrowInLanguage.
 214   *)
 215   Definition TwoLevelLanguage := Reification Guest Host (me_i Host).
 216
 217   Context (GuestHost:TwoLevelLanguage).
 218
 219   Definition FlatObject (x:TypesL _ _ Host) :=
 220     forall y1 y2, not ((reification_r_obj GuestHost y1 y2)=x).
 221
 222   Definition FlatSubCategory := FullSubcategory (TypesL _ _ Host) FlatObject.
 223
 224   Section Flattening.
 225
 226     Context  (F:Retraction (TypesL _ _ Host) FlatSubCategory).
 227     Definition FlatteningOfReification := garrow_from_reification Guest Host GuestHost >>>> F.
 228     Lemma FlatteningIsNotDestructive :
 229       FlatteningOfReification >>>> retraction_retraction F >>>> RepresentableFunctor _ (me_i Host) ~~~~ GuestHost.
 230       admit.
 231       Qed.
 232
 233   End Flattening.
 234
 235 End GArrowInLanguage.
 236
 237 Inductive NLevelLanguage : nat -> ProgrammingLanguageSMME -> Type :=
 238 | NLevelLanguage_zero : forall lang,    NLevelLanguage O lang
 239 | NLevelLanguage_succ : forall (L1 L2:ProgrammingLanguageSMME) n,
 240                           TwoLevelLanguage L1 L2 -> NLevelLanguage n L1 -> NLevelLanguage (S n) L2.
 241
 242 Definition OmegaLevelLanguage : Type :=
 243   { f : nat -> ProgrammingLanguageSMME
 244   & forall n, TwoLevelLanguage (f n) (f (S n)) }.
 245
 246 Implicit Arguments ND [ Judgment ].