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 Functors_ch1_4.
  13 Require Import Isomorphisms_ch1_5.
  14 Require Import ProductCategories_ch1_6_1.
  15 Require Import OppositeCategories_ch1_6_2.
  16 Require Import Enrichment_ch2_8.
  17 Require Import Subcategories_ch7_1.
  18 Require Import NaturalTransformations_ch7_4.
  19 Require Import NaturalIsomorphisms_ch7_5.
  20 Require Import MonoidalCategories_ch7_8.
  21 Require Import Coherence_ch7_8.
  22 Require Import Enrichment_ch2_8.
  23 Require Import RepresentableStructure_ch7_2.
  24 Require Import NaturalDeduction.
  25 Require Import NaturalDeductionCategory.
  26 Require Import Reification.
  27 Require Import FreydCategories.
  28 Require Import InitialTerminal_ch2_2.
  29 Require Import FunctorCategories_ch7_7.
  30 Require Import GeneralizedArrowFromReification.
  31 Require Import GeneralizedArrow.
  32
  33
  34 (*
  35  *  Everything in the rest of this section is just groundwork meant to
  36  *  build up to the definition of the ProgrammingLanguage class, which
  37  *  appears at the end of the section.  References to "the instance"
  38  *  mean instances of that class.  Think of this section as being one
  39  *  big Class { ... } definition, except that we declare most of the
  40  *  stuff outside the curly brackets in order to take advantage of
  41  *  Coq's section mechanism.
  42  *)
  43 Section Programming_Language.
  44
  45   (* Formalized Definition 4.1.1, production $\tau$ *)
  46   Context {T    : Type}.               (* types of the language *)
  47
  48   Context (Judg : Type).
  49   Context (sequent : Tree ??T -> Tree ??T -> Judg).
  50      Notation "cs |= ss" := (sequent cs ss) : al_scope.
  51      (* Because of term irrelevance we need only store the *erased* (def
  52       * 4.4) trees; for this reason there is no Coq type directly
  53       * corresponding to productions $e$ and $x$ of 4.1.1, and TreeOT can
  54       * be used for productions $\Gamma$ and $\Sigma$ *)
  55
  56   (* to do: sequent calculus equals natural deduction over sequents, theorem equals sequent with null antecedent, *)
  57
  58   Context {Rule : Tree ??Judg -> Tree ??Judg -> Type}.
  59
  60   Notation "H /⋯⋯/ C" := (ND Rule H C) : al_scope.
  61
  62   Open Scope pf_scope.
  63   Open Scope nd_scope.
  64   Open Scope al_scope.
  65
  66   (* Formalized Definition 4.1
  67    *
  68    * Note that from this abstract interface, the terms (expressions)
  69    * in the proof are not accessible at all; they don't need to be --
  70    * so long as we have access to the equivalence relation upon
  71    * proof-conclusions.  Moreover, hiding the expressions actually
  72    * makes the encoding in CiC work out easier for two reasons:
  73    *
  74    *  1. Because the denotation function is provided a proof rather
  75    *     than a term, it is a total function (the denotation function is
  76    *     often undefined for ill-typed terms).
  77    *
  78    *  2. We can define arr_composition of proofs without having to know how
  79    *     to compose expressions.  The latter task is left up to the client
  80    *     function which extracts an expression from a completed proof.
  81    *
  82    * This also means that we don't need an explicit proof obligation for 4.1.2.
  83    *)
  84   Class ProgrammingLanguage :=
  85
  86   (* Formalized Definition 4.1: denotational semantics equivalence relation on the conclusions of proofs *)
  87   { al_eqv                   : @ND_Relation Judg Rule
  88                                      where "pf1 === pf2" := (@ndr_eqv _ _ al_eqv _ _ pf1 pf2)
  89
  90   (* Formalized Definition 4.1.3; note that t here is either $\top$ or a single type, not a Tree of types;
  91    * we rely on "completeness of atomic initial segments" (http://en.wikipedia.org/wiki/Completeness_of_atomic_initial_sequents)
  92    * to generate the rest *)
  93   ; al_reflexive_seq         : forall t, Rule [] [t|=t]
  94
  95   (* these can all be absorbed into a separate "sequent calculus" presentation *)
  96   ; al_ant_assoc     : forall {a b c d}, Rule [(a,,b),,c|=d]     [(a,,(b,,c))|=d]
  97   ; al_ant_cossa     : forall {a b c d}, Rule [a,,(b,,c)|=d]     [((a,,b),,c)|=d]
  98   ; al_ant_cancell   : forall {a b    }, Rule [  [],,a  |=b]     [        a  |=b]
  99   ; al_ant_cancelr   : forall {a b    }, Rule [a,,[]    |=b]     [        a  |=b]
 100   ; al_ant_llecnac   : forall {a b    }, Rule [      a  |=b]     [  [],,a    |=b]
 101   ; al_ant_rlecnac   : forall {a b    }, Rule [      a  |=b]     [  a,,[]    |=b]
 102   ; al_suc_assoc     : forall {a b c d}, Rule [d|=(a,,b),,c]     [d|=(a,,(b,,c))]
 103   ; al_suc_cossa     : forall {a b c d}, Rule [d|=a,,(b,,c)]     [d|=((a,,b),,c)]
 104   ; al_suc_cancell   : forall {a b    }, Rule [a|=[],,b    ]     [a|=      b    ]
 105   ; al_suc_cancelr   : forall {a b    }, Rule [a|=b,,[]    ]     [a|=      b    ]
 106   ; al_suc_llecnac   : forall {a b    }, Rule [a|=      b  ]     [a|=[],,b      ]
 107   ; al_suc_rlecnac   : forall {a b    }, Rule [a|=      b  ]     [a|=b,,[]      ]
 108
 109   ; al_horiz_expand_left            : forall tau {Gamma Sigma}, Rule [        Gamma |=        Sigma ] [tau,,Gamma|=tau,,Sigma]
 110   ; al_horiz_expand_right           : forall tau {Gamma Sigma}, Rule [        Gamma |=        Sigma ] [Gamma,,tau|=Sigma,,tau]
 111
 112   (* these are essentially one way of formalizing
 113    * "completeness of atomic initial segments" (http://en.wikipedia.org/wiki/Completeness_of_atomic_initial_sequents) *)
 114   ; al_horiz_expand_left_reflexive  : forall a b, [#al_reflexive_seq b#];;[#al_horiz_expand_left  a#]===[#al_reflexive_seq (a,,b)#]
 115   ; al_horiz_expand_right_reflexive : forall a b, [#al_reflexive_seq a#];;[#al_horiz_expand_right b#]===[#al_reflexive_seq (a,,b)#]
 116   ; al_horiz_expand_right_then_cancel : forall a,
 117     ((([#al_reflexive_seq (a,, [])#] ;; [#al_ant_cancelr#]);; [#al_suc_cancelr#]) === [#al_reflexive_seq a#])
 118
 119   ; al_vert_expand_ant_left       : forall x `(pf:[a|=b]/⋯⋯/[c|=d]),  [x,,a   |=   b   ]/⋯⋯/[x,,c   |=   d   ]
 120   ; al_vert_expand_ant_right      : forall x `(pf:[a|=b]/⋯⋯/[c|=d]),  [   a,,x|=   b   ]/⋯⋯/[   c,,x|=   d   ]
 121   ; al_vert_expand_suc_left       : forall x `(pf:[a|=b]/⋯⋯/[c|=d]),  [   a   |=x,,b   ]/⋯⋯/[   c   |=x,,d   ]
 122   ; al_vert_expand_suc_right      : forall x `(pf:[a|=b]/⋯⋯/[c|=d]),  [   a   |=   b,,x]/⋯⋯/[   c   |=   d,,x]
 123   ; al_vert_expand_ant_l_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]),
 124       f===g -> al_vert_expand_ant_left x f === al_vert_expand_ant_left  x g
 125   ; al_vert_expand_ant_r_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]),
 126     f===g -> al_vert_expand_ant_right  x f === al_vert_expand_ant_right x g
 127   ; al_vert_expand_suc_l_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]),
 128     f===g -> al_vert_expand_suc_left   x f === al_vert_expand_suc_left  x g
 129   ; al_vert_expand_suc_r_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]),
 130     f===g -> al_vert_expand_suc_right  x f === al_vert_expand_suc_right x g
 131   ; 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]
 132   ; 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]
 133   ; 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]
 134   ; 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]
 135   ; 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]),
 136     (al_vert_expand_ant_left x (h;;g)) === (al_vert_expand_ant_left x h);;(al_vert_expand_ant_left x g)
 137   ; 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]),
 138     (al_vert_expand_ant_right x (h;;g)) === (al_vert_expand_ant_right x h);;(al_vert_expand_ant_right x g)
 139   ; 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]),
 140     (al_vert_expand_suc_left x (h;;g)) === (al_vert_expand_suc_left x h);;(al_vert_expand_suc_left x g)
 141   ; 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]),
 142     (al_vert_expand_suc_right x (h;;g)) === (al_vert_expand_suc_right x h);;(al_vert_expand_suc_right x g)
 143
 144   ; al_subst                 : forall a b c,  [ a |= b ] ,, [ b |= c ] /⋯⋯/ [ a |= c ]
 145   ; al_subst_associativity : forall {a b c d},
 146       ((al_subst a b c) ** (nd_id1 (c|=d))) ;;
 147       (al_subst a c d)
 148       ===
 149       nd_assoc ;;
 150       ((nd_id1 (a|=b)) ** (al_subst b c d) ;;
 151       (al_subst a b d))
 152   ; al_subst_associativity' : forall {a b c d},
 153       nd_cossa ;;
 154       ((al_subst a b c) ** (nd_id1 (c|=d))) ;;
 155       (al_subst a c d)
 156       ===
 157       ((nd_id1 (a|=b)) ** (al_subst b c d) ;;
 158       (al_subst a b d))
 159
 160   ; al_subst_left_identity  : forall a b, ((    [#al_reflexive_seq a#]**(nd_id _));; al_subst _ _ b) === nd_cancell
 161   ; al_subst_right_identity : forall a b, (((nd_id _)**[#al_reflexive_seq a#]    );; al_subst b _ _) === nd_cancelr
 162   ; al_subst_commutes_with_horiz_expand_left : forall a b c d,
 163     [#al_horiz_expand_left d#] ** [#al_horiz_expand_left d#];; al_subst (d,, a) (d,, b) (d,, c)
 164     === al_subst a b c;; [#al_horiz_expand_left d#]
 165   ; al_subst_commutes_with_horiz_expand_right : forall a b c d,
 166     [#al_horiz_expand_right d#] ** [#al_horiz_expand_right d#] ;; al_subst (a,, d) (b,, d) (c,, d)
 167     === al_subst a b c;; [#al_horiz_expand_right d#]
 168   ; al_subst_commutes_with_vertical_expansion : forall t0 t1 t2, forall (f:[[]|=t1]/⋯⋯/[[]|=t0])(g:[[]|=t0]/⋯⋯/[[]|=t2]),
 169    (((nd_rlecnac;;
 170       ((([#al_reflexive_seq (t1,, [])#];; al_vert_expand_ant_left t1 (al_vert_expand_suc_right [] f));;
 171         (nd_rule al_ant_cancelr));; (nd_rule al_suc_cancelr)) ** nd_id0);;
 172      (nd_id [t1 |= t0]) **
 173      ((([#al_reflexive_seq (t0,, [])#];; al_vert_expand_ant_left t0 (al_vert_expand_suc_right [] g));;
 174        (nd_rule al_ant_cancelr));; (nd_rule al_suc_cancelr)));;
 175     al_subst t1 t0 t2)
 176    ===
 177     ((([#al_reflexive_seq (t1,, [])#];;
 178           (al_vert_expand_ant_left t1 (al_vert_expand_suc_right [] f);;
 179            al_vert_expand_ant_left t1 (al_vert_expand_suc_right [] g)));;
 180          (nd_rule al_ant_cancelr));; (nd_rule al_suc_cancelr))
 181   }.
 182
 183   Notation "pf1 === pf2" := (@ndr_eqv _ _ al_eqv _ _ pf1 pf2) : temporary_scope3.
 184   Open Scope temporary_scope3.
 185
 186   Lemma al_subst_respects {PL:ProgrammingLanguage} :
 187     forall {a b c},
 188       forall
 189       (f  : [] /⋯⋯/ [a |= b])
 190       (f' : [] /⋯⋯/ [a |= b])
 191       (g  : [] /⋯⋯/ [b |= c])
 192       (g' : [] /⋯⋯/ [b |= c]),
 193       (f === f') ->
 194       (g === g') ->
 195       (f ** g;; al_subst _ _ _) === (f' ** g';; al_subst _ _ _).
 196     intros.
 197     setoid_rewrite H.
 198     setoid_rewrite H0.
 199     reflexivity.
 200     Defined.
 201
 202   (* languages with unrestricted substructural rules (like that of Section 5) additionally implement this class *)
 203   Class ProgrammingLanguageWithUnrestrictedSubstructuralRules :=
 204   { alwusr_al :> ProgrammingLanguage
 205   ; al_contr  : forall a b,     Rule [a,,a |= b ]  [    a |= b]
 206   ; al_exch   : forall a b c,   Rule [a,,b |= c ]  [(b,,a)|= c]
 207   ; al_weak   : forall a b,     Rule [[] |= b ]  [    a |= b]
 208   }.
 209   Coercion alwusr_al : ProgrammingLanguageWithUnrestrictedSubstructuralRules >-> ProgrammingLanguage.
 210
 211   (* languages with a fixpoint operator *)
 212   Class ProgrammingLanguageWithFixpointOperator `(al:ProgrammingLanguage) :=
 213   { alwfpo_al := al
 214   ; al_fix    : forall a b x,   Rule [a,,x |= b,,x]  [a |= b]
 215   }.
 216   Coercion alwfpo_al : ProgrammingLanguageWithFixpointOperator >-> ProgrammingLanguage.
 217
 218   Section LanguageCategory.
 219
 220     Context (PL:ProgrammingLanguage).
 221
 222     (* category of judgments in a fixed type/coercion context *)
 223     Definition JudgmentsL :=@Judgments_Category_monoidal _ Rule al_eqv.
 224
 225     Definition identityProof t : [] ~~{JudgmentsL}~~> [t |= t].
 226       unfold hom; simpl.
 227       apply nd_rule.
 228       apply al_reflexive_seq.
 229       Defined.
 230
 231     Definition cutProof a b c : [a |= b],,[b |= c] ~~{JudgmentsL}~~> [a |= c].
 232       unfold hom; simpl.
 233       apply al_subst.
 234       Defined.
 235
 236     Definition TypesLFC : ECategory JudgmentsL (Tree ??T) (fun x y => [x|=y]).
 237       refine
 238       {| eid   := identityProof
 239        ; ecomp := cutProof
 240       |}; intros.
 241       apply MonoidalCat_all_central.
 242       apply MonoidalCat_all_central.
 243       unfold identityProof; unfold cutProof; simpl.
 244       apply al_subst_left_identity.
 245       unfold identityProof; unfold cutProof; simpl.
 246       apply al_subst_right_identity.
 247       unfold identityProof; unfold cutProof; simpl.
 248       apply al_subst_associativity'.
 249       Defined.
 250
 251     Definition TypesEnrichedInJudgments : Enrichment.
 252       refine {| enr_c := TypesLFC |}.
 253       Defined.
 254
 255     Definition Types_first c : EFunctor TypesLFC TypesLFC (fun x => x,,c ).
 256 (*
 257       eapply Build_EFunctor; intros.
 258       eapply MonoidalCat_all_central.
 259       unfold eqv.
 260       simpl.
 261 *)
 262       admit.
 263       Defined.
 264
 265     Definition Types_second c : EFunctor TypesLFC TypesLFC (fun x => c,,x ).
 266       admit.
 267       Defined.
 268
 269     Definition Types_binoidal : BinoidalCat TypesLFC (@T_Branch _).
 270       refine
 271         {| bin_first  := TypesL_first
 272          ; bin_second := TypesL_second
 273          |}.
 274       Defined.
 275
 276     Definition Pairing : prod_obj TypesL_binoidal TypesL_binoidal -> TypesL_binoidal.
 277       admit.
 278       Defined.
 279     Definition Pairing_Functor : Functor (TypesL_binoidal ×× TypesL_binoidal) TypesL_binoidal Pairing.
 280       admit.
 281       Defined.
 282     Definition TypesL : MonoidalCat TypesL_binoidal Pairing Pairing_Functor [].
 283       admit.
 284       Defined.
 285
 286     Definition TypesLEnrichedInJudgments1 : SurjectiveEnrichment.
 287       refine {| se_enr := TypesLEnrichedInJudgments0 |}.
 288       simpl.
 289       admit.
 290       Defined.
 291
 292     Definition TypesLEnrichedInJudgments2 : MonoidalEnrichment.
 293       refine {| me_enr := TypesLEnrichedInJudgments0 ; me_mon := TypesL |}.
 294       simpl.
 295       admit.
 296       Defined.
 297
 298     Definition TypesLEnrichedInJudgments3 : MonicMonoidalEnrichment.
 299       refine {| ffme_enr := TypesLEnrichedInJudgments2 |}; simpl.
 300       admit.
 301       admit.
 302       admit.
 303       Defined.
 304
 305   End LanguageCategory.
 306
 307   (*
 308   Definition ArrowInProgrammingLanguage (L:ProgrammingLanguage)(tc:Terminal (TypesL L)) :=
 309     FreydCategory (TypesL L) (TypesL L).
 310     *)
 311
 312   Definition TwoLevelLanguage (L1 L2:ProgrammingLanguage) :=
 313     Reification (TypesLEnrichedInJudgments1 L1) (TypesLEnrichedInJudgments3 L2) (me_i (TypesLEnrichedInJudgments3 L2)).
 314
 315   Inductive NLevelLanguage : nat -> ProgrammingLanguage -> Type :=
 316   | NLevelLanguage_zero : forall lang,    NLevelLanguage O lang
 317   | NLevelLanguage_succ : forall L1 L2 n, TwoLevelLanguage L1 L2 -> NLevelLanguage n L1 -> NLevelLanguage (S n) L2.
 318
 319   Definition OmegaLevelLanguage (PL:ProgrammingLanguage) : Type :=
 320     forall n:nat, NLevelLanguage n PL.
 321
 322   Section TwoLevelLanguage.
 323     Context `(L12:TwoLevelLanguage L1 L2).
 324
 325     Definition FlatObject (x:TypesL L2) :=
 326       forall y1 y2, not ((reification_r_obj L12 y1 y2)=x).
 327
 328     Definition FlatSubCategory := FullSubcategory (TypesL L2) FlatObject.
 329
 330     Context `(retraction      :@Functor _ _ (TypesL L2) _ _ FlatSubCategory retract_obj).
 331     Context `(retraction_inv  :@Functor _ _ FlatSubCategory _ _ (TypesL L2) retract_inv_obj).
 332     Context  (retraction_works:retraction >>>> retraction_inv ~~~~ functor_id _).
 333
 334     Definition FlatteningOfReification :=
 335       (garrow_from_reification (TypesLEnrichedInJudgments1 L1) (TypesLEnrichedInJudgments3 L2) L12) >>>> retraction.
 336
 337     Lemma FlatteningIsNotDestructive :
 338       FlatteningOfReification >>>> retraction_inv >>>> RepresentableFunctor _ (me_i (TypesLEnrichedInJudgments3 L2)) ~~~~ L12.
 339       admit.
 340       Qed.
 341
 342   End TwoLevelLanguage.
 343
 344   Close Scope temporary_scope3.
 345   Close Scope al_scope.
 346   Close Scope nd_scope.
 347   Close Scope pf_scope.
 348
 349 End Programming_Language.
 350
 351 Implicit Arguments ND [ Judgment ].
 352
 353 (*
 354 Open Scope nd_scope.
 355   Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_suc_right T Rule AL a b c d e)
 356   with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv)))
 357     as parametric_morphism_al_vert_expand_suc_right.
 358     intros; apply al_vert_expand_suc_r_respects; auto.
 359     Defined.
 360   Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_suc_left T Rule AL a b c d e)
 361   with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv)))
 362     as parametric_morphism_al_vert_expand_suc_left.
 363     intros; apply al_vert_expand_suc_l_respects; auto.
 364     Defined.
 365   Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_ant_right T Rule AL a b c d e)
 366   with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv)))
 367     as parametric_morphism_al_vert_expand_ant_right.
 368     intros; apply al_vert_expand_ant_r_respects; auto.
 369     Defined.
 370   Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_ant_left T Rule AL a b c d e)
 371   with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv)))
 372     as parametric_morphism_al_vert_expand_ant_left.
 373     intros; apply al_vert_expand_ant_l_respects; auto.
 374     Defined.
 375 Close Scope nd_scope.
 376
 377 Notation "cs |= ss" := (@sequent _ cs ss) : al_scope.
 378 (*
 379 Definition mapJudg {T R:Type}(f:Tree ??T -> Tree ??R)(seq:@Judg T) : @Judg R :=
 380   match seq with sequentpair a b => pair (f a) (f b) end.
 381 Implicit Arguments Judg [ ].
 382 *)
 383
 384
 385 (* proofs which are generic and apply to any acceptable langauge (most of section 4) *)
 386 Section Programming_Language_Facts.
 387
 388   (* the ambient language about which we are proving facts *)
 389   Context `(Lang : @ProgrammingLanguage T Rule).
 390
 391   (* just for this section *)
 392   Open Scope nd_scope.
 393   Open Scope al_scope.
 394   Open Scope pf_scope.
 395   Notation "H /⋯⋯/ C" := (@ND Judg Rule H C)     : temporary_scope4.
 396   Notation "a === b"  := (@ndr_eqv _ _ al_eqv _ _ a b)                   : temporary_scope4.
 397   Open Scope temporary_scope4.
 398
 399   Definition lang_al_eqv := al_eqv(ProgrammingLanguage:=Lang).
 400   Existing Instance lang_al_eqv.
 401
 402   Ltac distribute :=
 403     match goal with
 404      [ |- ?G ] =>
 405       match G with
 406         context ct [(?A ** ?B) ;; (?C ** ?D)] =>
 407            setoid_rewrite <- (ndr_prod_preserves_comp A B C D)
 408       end
 409       end.
 410
 411   Ltac sequentialize_product A B :=
 412     match goal with
 413      [ |- ?G ] =>
 414       match G with
 415       | context ct [(A ** B)] =>
 416           setoid_replace (A ** B)
 417         with ((A ** (nd_id _)) ;; ((nd_id _) ** B))
 418         (*with ((A ** (nd_id _)) ;; ((nd_id _) ** B))*)
 419     end end.
 420   Ltac sequentialize_product' A B :=
 421     match goal with
 422      [ |- ?G ] =>
 423       match G with
 424       | context ct [(A ** B)] =>
 425           setoid_replace (A ** B)
 426         with (((nd_id _) ** B) ;; (A ** (nd_id _)))
 427         (*with ((A ** (nd_id _)) ;; ((nd_id _) ** B))*)
 428     end end.
 429   Ltac distribute' :=
 430     match goal with
 431      [ |- ?G ] =>
 432       match G with
 433         context ct [(?A ;; ?B) ** (?C ;; ?D)] =>
 434            setoid_rewrite (ndr_prod_preserves_comp A B C D)
 435       end
 436       end.
 437   Ltac distribute_left_product_with_id :=
 438     match goal with
 439      [ |- ?G ] =>
 440       match G with
 441         context ct [(nd_id ?A) ** (?C ;; ?D)] =>
 442            setoid_replace ((nd_id A) ** (C ;; D)) with ((nd_id A ;; nd_id A) ** (C ;; D));
 443         [ setoid_rewrite (ndr_prod_preserves_comp (nd_id A) C (nd_id A) D) | idtac ]
 444       end
 445       end.
 446   Ltac distribute_right_product_with_id :=
 447     match goal with
 448      [ |- ?G ] =>
 449       match G with
 450         context ct [(?C ;; ?D) ** (nd_id ?A)] =>
 451            setoid_replace ((C ;; D) ** (nd_id A)) with ((C ;; D) ** (nd_id A ;; nd_id A));
 452         [ setoid_rewrite (ndr_prod_preserves_comp C (nd_id A) D (nd_id A)) | idtac ]
 453       end
 454       end.
 455
 456   (* another phrasing of al_subst_associativity; obligations tend to show up in this form *)
 457   Lemma al_subst_associativity'' :
 458     forall (a b : T) (f : [] /⋯⋯/ [[a] |= [b]]) (c : T) (g : [] /⋯⋯/ [[b] |= [c]])
 459     (d : T) (h : [] /⋯⋯/ [[c] |= [d]]),
 460     nd_llecnac;; ((nd_llecnac;; (f ** g;; al_subst [a] [b] [c])) ** h;; al_subst [a] [c] [d]) ===
 461     nd_llecnac;; (f ** (nd_llecnac;; (g ** h;; al_subst [b] [c] [d]));; al_subst [a] [b] [d]).
 462     intros.
 463       sequentialize_product' (nd_llecnac;; (f ** g;; al_subst [a] [b] [c])) h.
 464       repeat setoid_rewrite <- ndr_comp_associativity.
 465       distribute_right_product_with_id.
 466       repeat setoid_rewrite ndr_comp_associativity.
 467       set (@al_subst_associativity) as q. setoid_rewrite q. clear q.
 468       apply ndr_comp_respects; try reflexivity.
 469       repeat setoid_rewrite <- ndr_comp_associativity.
 470       apply ndr_comp_respects; try reflexivity.
 471       sequentialize_product f ((nd_llecnac;; g ** h);; al_subst [b] [c] [d]).
 472       distribute_left_product_with_id.
 473       repeat setoid_rewrite <- ndr_comp_associativity.
 474       apply ndr_comp_respects; try reflexivity.
 475       setoid_rewrite <- ndr_prod_preserves_comp.
 476       repeat setoid_rewrite ndr_comp_left_identity.
 477       repeat setoid_rewrite ndr_comp_right_identity.
 478     admit.
 479     admit.
 480     admit.
 481     admit.
 482     admit.
 483     Qed.
 484
 485   Close Scope temporary_scope4.
 486   Close Scope al_scope.
 487   Close Scope nd_scope.
 488   Close Scope pf_scope.
 489   Close Scope isomorphism_scope.
 490 End Programming_Language_Facts.
 491
 492 (*Coercion AL_SurjectiveEnrichment    : ProgrammingLanguage >-> SurjectiveEnrichment.*)
 493 (*Coercion AL_MonicMonoidalEnrichment : ProgrammingLanguage >-> MonicMonoidalEnrichment.*)
 494 *)