src/ProgrammingLanguage.v

   1 (*********************************************************************************************************************************)
   2 (* NaturalDeduction:                                                                                                             *)
   3 (*                                                                                                                               *)
   4 (*   Structurally explicit natural deduction proofs.                                                                             *)
   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
  26
  27 (*
  28  *  Everything in the rest of this section is just groundwork meant to
  29  *  build up to the definition of the AcceptableLanguage class, which
  30  *  appears at the end of the section.  References to "the instance"
  31  *  mean instances of that class.  Think of this section as being one
  32  *  big Class { ... } definition, except that we declare most of the
  33  *  stuff outside the curly brackets in order to take advantage of
  34  *  Coq's section mechanism.
  35  *)
  36 Section Acceptable_Language.
  37
  38   (* Formalized Definition 4.1.1, production $\tau$ *)
  39   Context {T    : Type}.               (* types of the language *)
  40
  41   Inductive Sequent := sequent : Tree ??T -> Tree ??T -> Sequent.
  42      Notation "cs |= ss" := (sequent cs ss) : al_scope.
  43      (* Because of term irrelevance we need only store the *erased* (def
  44       * 4.4) trees; for this reason there is no Coq type directly
  45       * corresponding to productions $e$ and $x$ of 4.1.1, and TreeOT can
  46       * be used for productions $\Gamma$ and $\Sigma$ *)
  47
  48   (* to do: sequent calculus equals natural deduction over sequents, theorem equals sequent with null antecedent, *)
  49
  50   Context {Rule : Tree ??Sequent -> Tree ??Sequent -> Type}.
  51
  52   Notation "H /⋯⋯/ C" := (ND Rule H C) : al_scope.
  53
  54   Open Scope pf_scope.
  55   Open Scope nd_scope.
  56   Open Scope al_scope.
  57
  58   (* Formalized Definition 4.1
  59    *
  60    * Note that from this abstract interface, the terms (expressions)
  61    * in the proof are not accessible at all; they don't need to be --
  62    * so long as we have access to the equivalence relation upon
  63    * proof-conclusions.  Moreover, hiding the expressions actually
  64    * makes the encoding in CiC work out easier for two reasons:
  65    *
  66    *  1. Because the denotation function is provided a proof rather
  67    *     than a term, it is a total function (the denotation function is
  68    *     often undefined for ill-typed terms).
  69    *
  70    *  2. We can define arr_composition of proofs without having to know how
  71    *     to compose expressions.  The latter task is left up to the client
  72    *     function which extracts an expression from a completed proof.
  73    *
  74    * This also means that we don't need an explicit proof obligation for 4.1.2.
  75    *)
  76   Class AcceptableLanguage :=
  77
  78   (* Formalized Definition 4.1: denotational semantics equivalence relation on the conclusions of proofs *)
  79   { al_eqv                   : @ND_Relation Sequent Rule
  80                                      where "pf1 === pf2" := (@ndr_eqv _ _ al_eqv _ _ pf1 pf2)
  81
  82   (* Formalized Definition 4.1.3; note that t here is either $\top$ or a single type, not a Tree of types;
  83    * we rely on "completeness of atomic initial segments" (http://en.wikipedia.org/wiki/Completeness_of_atomic_initial_sequents)
  84    * to generate the rest *)
  85   ; al_reflexive_seq         : forall t, Rule [] [t|=t]
  86
  87   (* these can all be absorbed into a separate "sequent calculus" presentation *)
  88   ; al_ant_assoc     : forall {a b c d}, Rule [(a,,b),,c|=d]     [(a,,(b,,c))|=d]
  89   ; al_ant_cossa     : forall {a b c d}, Rule [a,,(b,,c)|=d]     [((a,,b),,c)|=d]
  90   ; al_ant_cancell   : forall {a b    }, Rule [  [],,a  |=b]     [        a  |=b]
  91   ; al_ant_cancelr   : forall {a b    }, Rule [a,,[]    |=b]     [        a  |=b]
  92   ; al_ant_llecnac   : forall {a b    }, Rule [      a  |=b]     [  [],,a    |=b]
  93   ; al_ant_rlecnac   : forall {a b    }, Rule [      a  |=b]     [  a,,[]    |=b]
  94   ; al_suc_assoc     : forall {a b c d}, Rule [d|=(a,,b),,c]     [d|=(a,,(b,,c))]
  95   ; al_suc_cossa     : forall {a b c d}, Rule [d|=a,,(b,,c)]     [d|=((a,,b),,c)]
  96   ; al_suc_cancell   : forall {a b    }, Rule [a|=[],,b    ]     [a|=      b    ]
  97   ; al_suc_cancelr   : forall {a b    }, Rule [a|=b,,[]    ]     [a|=      b    ]
  98   ; al_suc_llecnac   : forall {a b    }, Rule [a|=      b  ]     [a|=[],,b      ]
  99   ; al_suc_rlecnac   : forall {a b    }, Rule [a|=      b  ]     [a|=b,,[]      ]
 100
 101   ; al_horiz_expand_left            : forall tau {Gamma Sigma}, Rule [        Gamma |=        Sigma ] [tau,,Gamma|=tau,,Sigma]
 102   ; al_horiz_expand_right           : forall tau {Gamma Sigma}, Rule [        Gamma |=        Sigma ] [Gamma,,tau|=Sigma,,tau]
 103
 104   (* these are essentially one way of formalizing
 105    * "completeness of atomic initial segments" (http://en.wikipedia.org/wiki/Completeness_of_atomic_initial_sequents) *)
 106   ; al_horiz_expand_left_reflexive  : forall a b, [#al_reflexive_seq b#];;[#al_horiz_expand_left  a#]===[#al_reflexive_seq (a,,b)#]
 107   ; al_horiz_expand_right_reflexive : forall a b, [#al_reflexive_seq a#];;[#al_horiz_expand_right b#]===[#al_reflexive_seq (a,,b)#]
 108   ; al_horiz_expand_right_then_cancel : forall a,
 109     ((([#al_reflexive_seq (a,, [])#] ;; [#al_ant_cancelr#]);; [#al_suc_cancelr#]) === [#al_reflexive_seq a#])
 110
 111   ; al_vert_expand_ant_left       : forall x `(pf:[a|=b]/⋯⋯/[c|=d]),  [x,,a   |=   b   ]/⋯⋯/[x,,c   |=   d   ]
 112   ; al_vert_expand_ant_right      : forall x `(pf:[a|=b]/⋯⋯/[c|=d]),  [   a,,x|=   b   ]/⋯⋯/[   c,,x|=   d   ]
 113   ; al_vert_expand_suc_left       : forall x `(pf:[a|=b]/⋯⋯/[c|=d]),  [   a   |=x,,b   ]/⋯⋯/[   c   |=x,,d   ]
 114   ; al_vert_expand_suc_right      : forall x `(pf:[a|=b]/⋯⋯/[c|=d]),  [   a   |=   b,,x]/⋯⋯/[   c   |=   d,,x]
 115   ; al_vert_expand_ant_l_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]),
 116       f===g -> al_vert_expand_ant_left x f === al_vert_expand_ant_left  x g
 117   ; al_vert_expand_ant_r_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]),
 118     f===g -> al_vert_expand_ant_right  x f === al_vert_expand_ant_right x g
 119   ; al_vert_expand_suc_l_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]),
 120     f===g -> al_vert_expand_suc_left   x f === al_vert_expand_suc_left  x g
 121   ; al_vert_expand_suc_r_respects : forall x a b c d (f g:[a|=b]/⋯⋯/[c|=d]),
 122     f===g -> al_vert_expand_suc_right  x f === al_vert_expand_suc_right x g
 123   ; 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]
 124   ; 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]
 125   ; 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]
 126   ; 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]
 127   ; 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]),
 128     (al_vert_expand_ant_left x (h;;g)) === (al_vert_expand_ant_left x h);;(al_vert_expand_ant_left x g)
 129   ; 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]),
 130     (al_vert_expand_ant_right x (h;;g)) === (al_vert_expand_ant_right x h);;(al_vert_expand_ant_right x g)
 131   ; 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]),
 132     (al_vert_expand_suc_left x (h;;g)) === (al_vert_expand_suc_left x h);;(al_vert_expand_suc_left x g)
 133   ; 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]),
 134     (al_vert_expand_suc_right x (h;;g)) === (al_vert_expand_suc_right x h);;(al_vert_expand_suc_right x g)
 135
 136   ; al_subst                 : forall a b c,  [ a |= b ] ,, [ b |= c ] /⋯⋯/ [ a |= c ]
 137   ; al_subst_associativity : forall {a b c d},
 138       ((al_subst a b c) ** (nd_id1 (c|=d))) ;;
 139       (al_subst a c d)
 140       ===
 141       nd_assoc ;;
 142       ((nd_id1 (a|=b)) ** (al_subst b c d) ;;
 143       (al_subst a b d))
 144   ; al_subst_associativity' : forall {a b c d},
 145       nd_cossa ;;
 146       ((al_subst a b c) ** (nd_id1 (c|=d))) ;;
 147       (al_subst a c d)
 148       ===
 149       ((nd_id1 (a|=b)) ** (al_subst b c d) ;;
 150       (al_subst a b d))
 151
 152   ; al_subst_left_identity  : forall `(pf:h/⋯⋯/[t1|=t2]), nd_llecnac;;((    [#al_reflexive_seq t1#]**pf);; al_subst _ _ _) === pf
 153   ; al_subst_right_identity : forall `(pf:h/⋯⋯/[t1|=t2]), nd_rlecnac;;((pf**[#al_reflexive_seq t2#]    );; al_subst _ _ _) === pf
 154   ; al_subst_commutes_with_horiz_expand_left : forall a b c d,
 155     [#al_horiz_expand_left d#] ** [#al_horiz_expand_left d#];; al_subst (d,, a) (d,, b) (d,, c)
 156     === al_subst a b c;; [#al_horiz_expand_left d#]
 157   ; al_subst_commutes_with_horiz_expand_right : forall a b c d,
 158     [#al_horiz_expand_right d#] ** [#al_horiz_expand_right d#] ;; al_subst (a,, d) (b,, d) (c,, d)
 159     === al_subst a b c;; [#al_horiz_expand_right d#]
 160   ; al_subst_commutes_with_vertical_expansion : forall t0 t1 t2, forall (f:[[]|=t1]/⋯⋯/[[]|=t0])(g:[[]|=t0]/⋯⋯/[[]|=t2]),
 161    (((nd_rlecnac;;
 162       ((([#al_reflexive_seq (t1,, [])#];; al_vert_expand_ant_left t1 (al_vert_expand_suc_right [] f));;
 163         (nd_rule al_ant_cancelr));; (nd_rule al_suc_cancelr)) ** nd_id0);;
 164      (nd_id [t1 |= t0]) **
 165      ((([#al_reflexive_seq (t0,, [])#];; al_vert_expand_ant_left t0 (al_vert_expand_suc_right [] g));;
 166        (nd_rule al_ant_cancelr));; (nd_rule al_suc_cancelr)));;
 167     al_subst t1 t0 t2)
 168    ===
 169     ((([#al_reflexive_seq (t1,, [])#];;
 170           (al_vert_expand_ant_left t1 (al_vert_expand_suc_right [] f);;
 171            al_vert_expand_ant_left t1 (al_vert_expand_suc_right [] g)));;
 172          (nd_rule al_ant_cancelr));; (nd_rule al_suc_cancelr))
 173   }.
 174
 175   Notation "pf1 === pf2" := (@ndr_eqv _ _ al_eqv _ _ pf1 pf2) : temporary_scope3.
 176   Open Scope temporary_scope3.
 177
 178   Lemma al_subst_respects :
 179     forall {AL:AcceptableLanguage}{a b c},
 180       forall
 181       (f  : [] /⋯⋯/ [a |= b])
 182       (f' : [] /⋯⋯/ [a |= b])
 183       (g  : [] /⋯⋯/ [b |= c])
 184       (g' : [] /⋯⋯/ [b |= c]),
 185       (f === f') ->
 186       (g === g') ->
 187       (f ** g;; al_subst _ _ _) === (f' ** g';; al_subst _ _ _).
 188     intros.
 189     setoid_rewrite H.
 190     setoid_rewrite H0.
 191     reflexivity.
 192     Defined.
 193
 194   (* a contextually closed language *)
 195   (*
 196   Class ContextuallyClosedAcceptableLanguage :=
 197   { ccal_al                          :  AcceptableLanguage
 198   ; ccal_contextual_closure_operator :  Tree ??T -> Tree ??T -> Tree ??T
 199   where "a -~- b" := (ccal_contextual_closure_operator a b)
 200   ; ccal_contextual_closure          :  forall {a b c d}(f:[a|=b]/⋯⋯/[c|=d]),     [[]|=a-~-b]/⋯⋯/[[]|=c-~-d]
 201   ; ccal_contextual_closure_respects :  forall {a b c d}(f f':[a|=b]/⋯⋯/[c|=d]),
 202                                                   f===f' -> (ccal_contextual_closure f)===(ccal_contextual_closure f')
 203   ; ccal_contextual_closure_preserves_comp :  forall {a b c d e f}(f':[a|=b]/⋯⋯/[c|=d])(g':[c|=d]/⋯⋯/[e|=f]),
 204              (ccal_contextual_closure f');;(ccal_contextual_closure g') === (ccal_contextual_closure (f';;g'))
 205   ; ccal_contextual_closure_preserves_id :  forall {a b}, ccal_contextual_closure (nd_id [a|=b]) === nd_id [[]|=a-~-b]
 206   }.
 207   Coercion ccal_al : ContextuallyClosedAcceptableLanguage >-> AcceptableLanguage.
 208   *)
 209
 210   (* languages with unrestricted substructural rules (like that of Section 5) additionally implement this class *)
 211   Class AcceptableLanguageWithUnrestrictedSubstructuralRules :=
 212   { alwusr_al :> AcceptableLanguage
 213   ; al_contr  : forall a b,     Rule [a,,a |= b ]  [    a |= b]
 214   ; al_exch   : forall a b c,   Rule [a,,b |= c ]  [(b,,a)|= c]
 215   ; al_weak   : forall a b,     Rule [[] |= b ]  [    a |= b]
 216   }.
 217   Coercion alwusr_al : AcceptableLanguageWithUnrestrictedSubstructuralRules >-> AcceptableLanguage.
 218
 219   (* languages with a fixpoint operator *)
 220   Class AcceptableLanguageWithFixpointOperator `(al:AcceptableLanguage) :=
 221   { alwfpo_al := al
 222   ; al_fix    : forall a b x,   Rule [a,,x |= b,,x]  [a |= b]
 223   }.
 224   Coercion alwfpo_al : AcceptableLanguageWithFixpointOperator >-> AcceptableLanguage.
 225
 226   Close Scope temporary_scope3.
 227   Close Scope al_scope.
 228   Close Scope nd_scope.
 229   Close Scope pf_scope.
 230
 231 End Acceptable_Language.
 232
 233 Implicit Arguments ND [ Judgment ].
 234
 235 Open Scope nd_scope.
 236   Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_suc_right T Rule AL a b c d e)
 237   with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv)))
 238     as parametric_morphism_al_vert_expand_suc_right.
 239     intros; apply al_vert_expand_suc_r_respects; auto.
 240     Defined.
 241   Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_suc_left T Rule AL a b c d e)
 242   with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv)))
 243     as parametric_morphism_al_vert_expand_suc_left.
 244     intros; apply al_vert_expand_suc_l_respects; auto.
 245     Defined.
 246   Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_ant_right T Rule AL a b c d e)
 247   with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv)))
 248     as parametric_morphism_al_vert_expand_ant_right.
 249     intros; apply al_vert_expand_ant_r_respects; auto.
 250     Defined.
 251   Add Parametric Morphism {T Rule AL a b c d e} : (@al_vert_expand_ant_left T Rule AL a b c d e)
 252   with signature ((ndr_eqv(ND_Relation:=al_eqv)) ==> (ndr_eqv(ND_Relation:=al_eqv)))
 253     as parametric_morphism_al_vert_expand_ant_left.
 254     intros; apply al_vert_expand_ant_l_respects; auto.
 255     Defined.
 256 Close Scope nd_scope.
 257
 258 Notation "cs |= ss" := (@sequent _ cs ss) : al_scope.
 259 (*
 260 Definition mapSequent {T R:Type}(f:Tree ??T -> Tree ??R)(seq:@Sequent T) : @Sequent R :=
 261   match seq with sequentpair a b => pair (f a) (f b) end.
 262 Implicit Arguments Sequent [ ].
 263 *)
 264
 265
 266 (* proofs which are generic and apply to any acceptable langauge (most of section 4) *)
 267 Section Acceptable_Language_Facts.
 268
 269   (* the ambient language about which we are proving facts *)
 270   Context `(Lang : @AcceptableLanguage T Rule).
 271
 272   (* just for this section *)
 273   Open Scope nd_scope.
 274   Open Scope al_scope.
 275   Open Scope pf_scope.
 276   Notation "H /⋯⋯/ C" := (@ND Sequent Rule H C)     : temporary_scope4.
 277   Notation "a === b"  := (@ndr_eqv _ _ al_eqv _ _ a b)                   : temporary_scope4.
 278   Open Scope temporary_scope4.
 279
 280   Definition lang_al_eqv := al_eqv(AcceptableLanguage:=Lang).
 281   Existing Instance lang_al_eqv.
 282
 283   Ltac distribute :=
 284     match goal with
 285      [ |- ?G ] =>
 286       match G with
 287         context ct [(?A ** ?B) ;; (?C ** ?D)] =>
 288            setoid_rewrite <- (ndr_prod_preserves_comp A B C D)
 289       end
 290       end.
 291
 292   Ltac sequentialize_product A B :=
 293     match goal with
 294      [ |- ?G ] =>
 295       match G with
 296       | context ct [(A ** B)] =>
 297           setoid_replace (A ** B)
 298         with ((A ** (nd_id _)) ;; ((nd_id _) ** B))
 299         (*with ((A ** (nd_id _)) ;; ((nd_id _) ** B))*)
 300     end end.
 301   Ltac sequentialize_product' A B :=
 302     match goal with
 303      [ |- ?G ] =>
 304       match G with
 305       | context ct [(A ** B)] =>
 306           setoid_replace (A ** B)
 307         with (((nd_id _) ** B) ;; (A ** (nd_id _)))
 308         (*with ((A ** (nd_id _)) ;; ((nd_id _) ** B))*)
 309     end end.
 310   Ltac distribute' :=
 311     match goal with
 312      [ |- ?G ] =>
 313       match G with
 314         context ct [(?A ;; ?B) ** (?C ;; ?D)] =>
 315            setoid_rewrite (ndr_prod_preserves_comp A B C D)
 316       end
 317       end.
 318   Ltac distribute_left_product_with_id :=
 319     match goal with
 320      [ |- ?G ] =>
 321       match G with
 322         context ct [(nd_id ?A) ** (?C ;; ?D)] =>
 323            setoid_replace ((nd_id A) ** (C ;; D)) with ((nd_id A ;; nd_id A) ** (C ;; D));
 324         [ setoid_rewrite (ndr_prod_preserves_comp (nd_id A) C (nd_id A) D) | idtac ]
 325       end
 326       end.
 327   Ltac distribute_right_product_with_id :=
 328     match goal with
 329      [ |- ?G ] =>
 330       match G with
 331         context ct [(?C ;; ?D) ** (nd_id ?A)] =>
 332            setoid_replace ((C ;; D) ** (nd_id A)) with ((C ;; D) ** (nd_id A ;; nd_id A));
 333         [ setoid_rewrite (ndr_prod_preserves_comp C (nd_id A) D (nd_id A)) | idtac ]
 334       end
 335       end.
 336
 337   (* another phrasing of al_subst_associativity; obligations tend to show up in this form *)
 338   Lemma al_subst_associativity'' :
 339     forall (a b : T) (f : [] /⋯⋯/ [[a] |= [b]]) (c : T) (g : [] /⋯⋯/ [[b] |= [c]])
 340     (d : T) (h : [] /⋯⋯/ [[c] |= [d]]),
 341     nd_llecnac;; ((nd_llecnac;; (f ** g;; al_subst [a] [b] [c])) ** h;; al_subst [a] [c] [d]) ===
 342     nd_llecnac;; (f ** (nd_llecnac;; (g ** h;; al_subst [b] [c] [d]));; al_subst [a] [b] [d]).
 343     intros.
 344       sequentialize_product' (nd_llecnac;; (f ** g;; al_subst [a] [b] [c])) h.
 345       repeat setoid_rewrite <- ndr_comp_associativity.
 346       distribute_right_product_with_id.
 347       repeat setoid_rewrite ndr_comp_associativity.
 348       set (@al_subst_associativity) as q. setoid_rewrite q. clear q.
 349       apply ndr_comp_respects; try reflexivity.
 350       repeat setoid_rewrite <- ndr_comp_associativity.
 351       apply ndr_comp_respects; try reflexivity.
 352       sequentialize_product f ((nd_llecnac;; g ** h);; al_subst [b] [c] [d]).
 353       distribute_left_product_with_id.
 354       repeat setoid_rewrite <- ndr_comp_associativity.
 355       apply ndr_comp_respects; try reflexivity.
 356       setoid_rewrite <- ndr_prod_preserves_comp.
 357       repeat setoid_rewrite ndr_comp_left_identity.
 358       repeat setoid_rewrite ndr_comp_right_identity.
 359     admit.
 360     admit.
 361     admit.
 362     admit.
 363     admit.
 364     Qed.
 365
 366   (* Formalized Definition 4.6 *)
 367   Section Types1.
 368     Instance Types1 : Category T (fun t1 t2 => [ ] /⋯⋯/ [ [t1] |= [t2] ]) :=
 369     { eqv  := fun ta tb pf1 pf2                                            => pf1 === pf2
 370     ; id   := fun t                                                        => [#al_reflexive_seq [t]#]
 371     ; comp := fun {ta tb tc:T}(pf1:[]/⋯⋯/[[ta]|=[tb]])(pf2:[]/⋯⋯/[[tb]|=[tc]]) => nd_llecnac ;; ((pf1 ** pf2) ;; (al_subst _ _ _))
 372     }.
 373     intros; apply Build_Equivalence;
 374       [ unfold Reflexive; intros; reflexivity
 375       | unfold Symmetric; intros; symmetry; auto
 376       | unfold Transitive; intros; transitivity y; auto ].
 377     unfold Proper; unfold respectful; intros; simpl.
 378       apply ndr_comp_respects. reflexivity.
 379       apply al_subst_respects; auto.
 380     intros; simpl. apply al_subst_left_identity.
 381     intros; simpl.
 382       assert (@nd_llecnac _ Rule [] === @nd_rlecnac _ _ []).
 383       apply ndr_structural_indistinguishable; auto.
 384       setoid_rewrite H.
 385       apply al_subst_right_identity.
 386     intros; apply al_subst_associativity''.
 387     Defined.
 388   End Types1.
 389
 390   (* Formalized Definition 4.10 *)
 391   Instance Judgments : Category (Tree ??Sequent) (fun h c => h /⋯⋯/ c) :=
 392   { id   := fun h          => nd_id _
 393   ; comp := fun a b c f g  => f ;; g
 394   ; eqv  := fun a b f g    => f===g
 395   }.
 396   intros; apply Build_Equivalence;
 397     [ unfold Reflexive; intros; reflexivity
 398     | unfold Symmetric; intros; symmetry; auto
 399     | unfold Transitive; intros; transitivity y; auto ].
 400   unfold Proper; unfold respectful; intros; simpl; apply ndr_comp_respects; auto.
 401   intros; apply ndr_comp_left_identity.
 402   intros; apply ndr_comp_right_identity.
 403   intros; apply ndr_comp_associativity.
 404   Defined.
 405
 406   (* a "primitive" proof has exactly one hypothesis and one conclusion *)
 407   Inductive IsPrimitive : forall (h_:Tree ??(@Sequent T)), Type :=
 408     isPrimitive : forall h, IsPrimitive [h].
 409   Hint Constructors IsPrimitive.
 410   Instance IsPrimitiveSubCategory : SubCategory Judgments IsPrimitive (fun _ _ _ _ _ => True).
 411     apply Build_SubCategory; intros; auto.
 412     Defined.
 413
 414   (* The primitive judgments form a subcategory; nearly all of the
 415    * functors we build that go into Judgments will factor through the
 416    * inclusion functor for this subcategory.  Explicitly constructing
 417    * it makes the formalization easier, but distracts from what's
 418    * actually going on (from an expository perspective) *)
 419   Definition PrimitiveJudgments := SubCategoriesAreCategories Judgments IsPrimitiveSubCategory.
 420   Definition PrimitiveInclusion := InclusionFunctor           Judgments IsPrimitiveSubCategory.
 421
 422   Section Types0.
 423     Inductive IsNil    : Tree ??(@Sequent T) -> Prop := isnil    : IsNil [].
 424     Inductive IsClosed : Tree ??(@Sequent T) -> Prop := isclosed:forall t, IsClosed [[]|=[t]].
 425     Inductive IsIdentity : forall h c,  (h /⋯⋯/ c) -> Prop :=
 426       | isidentity0 : forall t,         IsIdentity t t (nd_id t)
 427       | isidentity1 : forall t pf1 pf2, IsIdentity t t pf1 -> IsIdentity t t pf2 -> IsIdentity t t (pf1 ;; pf2).
 428     Inductive IsInTypes0  (h c:Tree ??Sequent)(pf:h /⋯⋯/ c) : Prop :=
 429       | iit0_id0   : IsNil h    -> IsNil    c -> IsIdentity _ _ pf -> IsInTypes0 _ _ pf
 430       | iit0_id1   : @IsClosed  h -> @IsClosed   c -> IsIdentity _ _ pf -> IsInTypes0 _ _ pf
 431       | iit0_term  : IsNil h    -> @IsClosed c ->                      IsInTypes0 _ _ pf.
 432      Instance Types0P : SubCategory Judgments
 433         (fun x:Judgments => IsInTypes0 _ _ (id(Category:=Judgments) x))
 434         (fun h c _ _ f => IsInTypes0 h c f).
 435      intros.
 436        apply Build_SubCategory; intros; simpl.
 437         auto.
 438         inversion H0.
 439           inversion H1; subst.
 440           inversion H2; subst.
 441           inversion H; subst. inversion H4; subst.
 442           apply iit0_id0; auto. apply isidentity1; auto.
 443           inversion H5.
 444           inversion H5.
 445           inversion H1; subst.
 446           inversion H2; subst.
 447           inversion H3; subst. clear H8. clear H7.
 448             inversion H; subst. inversion H5.
 449             inversion H4; subst.
 450             inversion H6; subst.
 451             apply iit0_id1; auto. apply isidentity1; auto.
 452             clear H10. clear H8.
 453             apply iit0_id1; auto. apply isidentity1; auto.
 454             inversion H4; subst. inversion H; subst.
 455             inversion H8.
 456             inversion H6.
 457             apply iit0_term; auto.
 458         clear H7; subst.
 459           inversion H; subst.
 460           inversion H4; subst.
 461           apply iit0_term; auto.
 462           inversion H4; subst.
 463             inversion H7; subst. clear H14.
 464             apply iit0_id1; auto. apply isidentity1; auto.
 465             clear H13.
 466             apply iit0_id1; auto. apply isidentity1; auto.
 467             inversion H4; subst.
 468             inversion H; subst.
 469             inversion H10.
 470             inversion H7.
 471             apply iit0_term; auto.
 472         inversion H1; subst.
 473         inversion H; subst.
 474           inversion H3; subst. apply iit0_term; auto.
 475           inversion H4.
 476           inversion H4.
 477        Qed.
 478
 479     (* Formalized Definition 4.8 *)
 480     Definition Types0 := SubCategoriesAreCategories Judgments Types0P.
 481   End Types0.
 482
 483   (* Formalized Definition 4.11 *)
 484   Instance Judgments_binoidal : BinoidalCat Judgments (fun a b:Tree ??Sequent => a,,b) :=
 485   { bin_first  := fun x => @Build_Functor _ _ Judgments _ _ Judgments (fun a => a,,x)   (fun a b (f:a/⋯⋯/b) => f**(nd_id x)) _ _ _
 486   ; bin_second := fun x => @Build_Functor _ _ Judgments _ _ Judgments (fun a => x,,a)   (fun a b (f:a/⋯⋯/b) => (nd_id x)**f) _ _ _
 487   }.
 488     intros. simpl. simpl in H. setoid_rewrite H. reflexivity.
 489     intros. simpl. reflexivity.
 490     intros. simpl. setoid_rewrite <- ndr_prod_preserves_comp. setoid_rewrite ndr_comp_left_identity. reflexivity.
 491     intros. simpl. simpl in H. setoid_rewrite H. reflexivity.
 492     intros. simpl. reflexivity.
 493     intros. simpl. setoid_rewrite <- ndr_prod_preserves_comp. setoid_rewrite ndr_comp_left_identity. reflexivity.
 494     Defined.
 495
 496   Definition jud_assoc_iso (a b c:Judgments) : @Isomorphic _ _ Judgments ((a,,b),,c) (a,,(b,,c)).
 497     apply (@Build_Isomorphic _ _ Judgments _ _ nd_assoc nd_cossa); simpl; auto.
 498     Defined.
 499   Definition jud_cancelr_iso (a:Judgments) : @Isomorphic _ _ Judgments (a,,[]) a.
 500     apply (@Build_Isomorphic _ _ Judgments _ _ nd_cancelr nd_rlecnac); simpl; auto.
 501     Defined.
 502   Definition jud_cancell_iso (a:Judgments) : @Isomorphic _ _ Judgments ([],,a) a.
 503     apply (@Build_Isomorphic _ _ Judgments _ _ nd_cancell nd_llecnac); simpl; auto.
 504     Defined.
 505
 506   (* just for this section *)
 507   Notation "a ⊗ b"  := (@bin_obj    _ _ Judgments _ Judgments_binoidal a b).
 508   Notation "c ⋊ -"  := (@bin_second _ _ Judgments _ Judgments_binoidal c).
 509   Notation "- ⋉ c"  := (@bin_first  _ _ Judgments _ Judgments_binoidal c).
 510   Notation "c ⋊ f"  := ((c ⋊ -) \ f).
 511   Notation "g ⋉ c"  := ((- ⋉ c) \ g).
 512
 513   Hint Extern 1 => apply (@nd_structural_id0 _ Rule).
 514   Hint Extern 1 => apply (@nd_structural_id1 _ Rule).
 515   Hint Extern 1 => apply (@nd_structural_weak _ Rule).
 516   Hint Extern 1 => apply (@nd_structural_copy _ Rule).
 517   Hint Extern 1 => apply (@nd_structural_prod _ Rule).
 518   Hint Extern 1 => apply (@nd_structural_comp _ Rule).
 519   Hint Extern 1 => apply (@nd_structural_cancell _ Rule).
 520   Hint Extern 1 => apply (@nd_structural_cancelr _ Rule).
 521   Hint Extern 1 => apply (@nd_structural_llecnac _ Rule).
 522   Hint Extern 1 => apply (@nd_structural_rlecnac _ Rule).
 523   Hint Extern 1 => apply (@nd_structural_assoc _ Rule).
 524   Hint Extern 1 => apply (@nd_structural_cossa _ Rule).
 525   Hint Extern 2 => apply (@ndr_structural_indistinguishable _ Rule).
 526
 527   Program Instance Judgments_premonoidal  : PreMonoidalCat Judgments_binoidal [ ] :=
 528   { pmon_assoc     := fun a b => @Build_NaturalIsomorphism _ _ _ _ _ _ _ _ _ _ (fun x => (jud_assoc_iso a x b))   _
 529   ; pmon_cancell   :=            @Build_NaturalIsomorphism _ _ _ _ _ _ _ _ _ _ (fun x => (jud_cancell_iso x))     _
 530   ; pmon_cancelr   :=            @Build_NaturalIsomorphism _ _ _ _ _ _ _ _ _ _ (fun x => (jud_cancelr_iso x))     _
 531   ; pmon_assoc_rr  := fun a b => @Build_NaturalIsomorphism _ _ _ _ _ _ _ _ _ _ (fun x => (jud_assoc_iso x a b)⁻¹) _
 532   ; pmon_assoc_ll  := fun a b => @Build_NaturalIsomorphism _ _ _ _ _ _ _ _ _ _ (fun x => jud_assoc_iso a b x)     _
 533   }.
 534   Next Obligation.
 535     setoid_rewrite (ndr_prod_associativity (nd_id a) f (nd_id b)).
 536     repeat setoid_rewrite ndr_comp_associativity.
 537     apply ndr_comp_respects; try reflexivity.
 538     symmetry.
 539     eapply transitivity; [ idtac | apply ndr_comp_right_identity ].
 540     apply ndr_comp_respects; try reflexivity; simpl; auto.
 541     Defined.
 542   Next Obligation.
 543     setoid_rewrite (ndr_prod_right_identity f).
 544     repeat setoid_rewrite ndr_comp_associativity.
 545     apply ndr_comp_respects; try reflexivity.
 546     symmetry.
 547     eapply transitivity; [ idtac | apply ndr_comp_right_identity ].
 548     apply ndr_comp_respects; try reflexivity; simpl; auto.
 549     Defined.
 550   Next Obligation.
 551     setoid_rewrite (ndr_prod_left_identity f).
 552     repeat setoid_rewrite ndr_comp_associativity.
 553     apply ndr_comp_respects; try reflexivity.
 554     symmetry.
 555     eapply transitivity; [ idtac | apply ndr_comp_right_identity ].
 556     apply ndr_comp_respects; try reflexivity; simpl; auto.
 557     Defined.
 558   Next Obligation.
 559     apply Build_Pentagon; intros.
 560     simpl; apply ndr_structural_indistinguishable; auto.
 561     Defined.
 562   Next Obligation.
 563     apply Build_Triangle; intros;
 564     simpl; apply ndr_structural_indistinguishable; auto.
 565     Defined.
 566   Next Obligation.
 567     setoid_rewrite (ndr_prod_associativity f (nd_id a) (nd_id b)).
 568     repeat setoid_rewrite <- ndr_comp_associativity.
 569     apply ndr_comp_respects; try reflexivity.
 570     eapply transitivity; [ idtac | apply ndr_comp_left_identity ].
 571     apply ndr_comp_respects; try reflexivity; simpl; auto.
 572     Defined.
 573   Next Obligation.
 574     setoid_rewrite (ndr_prod_associativity (nd_id a) (nd_id b) f).
 575     repeat setoid_rewrite ndr_comp_associativity.
 576     apply ndr_comp_respects; try reflexivity.
 577     symmetry.
 578     eapply transitivity; [ idtac | apply ndr_comp_right_identity ].
 579     apply ndr_comp_respects; try reflexivity; simpl; auto.
 580     Defined.
 581     Check (@Judgments_premonoidal).  (* to force Coq to verify that we've finished all the obligations *)
 582
 583   Definition Judgments_monoidal_endofunctor_fobj : Judgments ×× Judgments -> Judgments :=
 584     (fun xy =>
 585      match xy with
 586      | pair_obj x y => T_Branch x y
 587      end).
 588   Definition Judgments_monoidal_endofunctor_fmor :
 589            forall a b, (a~~{Judgments ×× Judgments}~~>b) ->
 590            ((Judgments_monoidal_endofunctor_fobj a)~~{Judgments}~~>(Judgments_monoidal_endofunctor_fobj b)).
 591      intros.
 592      destruct a.
 593      destruct b.
 594      destruct X.
 595      exact (h**h0).
 596      Defined.
 597   Definition Judgments_monoidal_endofunctor : Functor (Judgments ×× Judgments) Judgments Judgments_monoidal_endofunctor_fobj.
 598     refine {| fmor := Judgments_monoidal_endofunctor_fmor |}; intros; simpl.
 599     abstract (destruct a; destruct b; destruct f; destruct f'; auto; destruct H; apply ndr_prod_respects; auto).
 600     abstract (destruct a; simpl; reflexivity).
 601     abstract (destruct a; destruct b; destruct c; destruct f; destruct g; symmetry; apply ndr_prod_preserves_comp).
 602     Defined.
 603
 604   Instance Judgments_monoidal  : MonoidalCat _ _ Judgments_monoidal_endofunctor [ ].
 605     admit.
 606     Defined.
 607
 608   (* all morphisms in the category of Judgments are central; there's probably a very short route from here to CartesianCat *)
 609   Lemma all_central : forall a b:Judgments, forall (f:a~>b), CentralMorphism f.
 610     intros; apply Build_CentralMorphism; intros.
 611     simpl.
 612       setoid_rewrite <- (ndr_prod_preserves_comp f (nd_id _) (nd_id _) g).
 613       setoid_rewrite <- (ndr_prod_preserves_comp (nd_id _) g f (nd_id _)).
 614       setoid_rewrite ndr_comp_left_identity.
 615       setoid_rewrite ndr_comp_right_identity.
 616       reflexivity.
 617     simpl.
 618       setoid_rewrite <- (ndr_prod_preserves_comp g (nd_id _) (nd_id _) f).
 619       setoid_rewrite <- (ndr_prod_preserves_comp (nd_id _) f g (nd_id _)).
 620       setoid_rewrite ndr_comp_left_identity.
 621       setoid_rewrite ndr_comp_right_identity.
 622       reflexivity.
 623     Defined.
 624
 625   (*
 626   Instance NoHigherOrderFunctionTypes : SubCategory Judgments
 627   Instance            NoFunctionTypes : SubCategory Judgments
 628   Lemma first_order_functions_eliminable : IsomorphicCategories NoHigherOrderFunctionTypes NoFunctionTypes
 629   *)
 630
 631   (* Formalized Theorem 4.19 *)
 632   Instance Types_omega_e : ECategory Judgments_monoidal (Tree ??T) (fun tt1 tt2 => [ tt1 |= tt2 ]) :=
 633   { eid             := fun tt      => [#al_reflexive_seq tt#]
 634   ; ecomp           := fun a b c   => al_subst a b c
 635   }.
 636     admit.
 637     admit.
 638     admit.
 639     admit.
 640     admit.
 641     Defined.
 642
 643   Definition Types_omega_monoidal_functor
 644     : Functor (Types_omega_e ×× Types_omega_e) Types_omega_e (fun a => match a with pair_obj a1 a2 => a1,,a2 end).
 645     admit.
 646     Defined.
 647
 648   Instance Types_omega_monoidal : MonoidalCat Types_omega_e _ Types_omega_monoidal_functor [].
 649     admit.
 650     Defined.
 651
 652   Definition AL_Enrichment : Enrichment.
 653     refine {| enr_c   := Types_omega_e |}.
 654     Defined.
 655
 656   Definition AL_SurjectiveEnrichment : SurjectiveEnrichment.
 657     refine {| se_enr  := AL_Enrichment |}.
 658     unfold treeDecomposition.
 659     intros; induction d; simpl.
 660     destruct a.
 661     destruct s.
 662     exists [pair t t0]; auto.
 663     exists []; auto.
 664     destruct IHd1.
 665     destruct IHd2.
 666     exists (x,,x0); subst; auto.
 667     Defined.
 668
 669   Definition AL_MonoidalEnrichment : MonoidalEnrichment.
 670     refine {| me_enr := AL_SurjectiveEnrichment ; me_mon := Types_omega_monoidal |}.
 671     admit.
 672     Defined.
 673
 674   Definition AL_MonicMonoidalEnrichment : MonicMonoidalEnrichment.
 675     refine {| ffme_enr := AL_MonoidalEnrichment |}.
 676     admit.
 677     admit.
 678     admit.
 679     Defined.
 680
 681   (*
 682   Instance Types_omega_be : BinoidalECategory Types_omega_e :=
 683   { bec_obj     := fun tt1 tt2 => tt1,,tt2
 684   ; bec_efirst  := fun a b c   => nd_rule (@al_horiz_expand_right _ _ Lang _ _ _)
 685   ; bec_esecond := fun a b c   => nd_rule (@al_horiz_expand_left  _ _ Lang _ _ _)
 686   }.
 687     intros; apply all_central.
 688     intros; apply all_central.
 689     intros. unfold eid. simpl.
 690       setoid_rewrite <- al_horiz_expand_right_reflexive.
 691       reflexivity.
 692     intros. unfold eid. simpl.
 693       setoid_rewrite <- al_horiz_expand_left_reflexive.
 694       reflexivity.
 695     intros. simpl.
 696       set (@al_subst_commutes_with_horiz_expand_right _ _ _ a b c d) as q.
 697       setoid_rewrite <- q. clear q.
 698       apply ndr_comp_respects; try reflexivity.
 699       distribute.
 700       apply ndr_prod_respects.
 701       eapply transitivity; [ idtac | apply ndr_comp_right_identity ].
 702       apply ndr_comp_respects; reflexivity.
 703       eapply transitivity; [ idtac | apply ndr_comp_left_identity ].
 704       apply ndr_comp_respects; reflexivity.
 705     intros. simpl.
 706       set (@al_subst_commutes_with_horiz_expand_left _ _ _ a b c d) as q.
 707       setoid_rewrite <- q. clear q.
 708       apply ndr_comp_respects; try reflexivity.
 709       distribute.
 710       apply ndr_prod_respects.
 711       eapply transitivity; [ idtac | apply ndr_comp_right_identity ].
 712       apply ndr_comp_respects; reflexivity.
 713       eapply transitivity; [ idtac | apply ndr_comp_left_identity ].
 714       apply ndr_comp_respects; reflexivity.
 715       Defined.
 716   *)
 717
 718   Definition Types_omega : Category _ (fun tt1 tt2 => [ ]/⋯⋯/[ tt1 |= tt2 ]) := Underlying Types_omega_e.
 719   Existing Instance Types_omega.
 720
 721   (*
 722   Definition Types_omega_binoidal : BinoidalCat Types_omega (fun tt1 tt2 => tt1,,tt2) := Underlying_binoidal Types_omega_be.
 723   Existing Instance Types_omega_binoidal.
 724   *)
 725
 726   (* takes an "operation in the context" (proof from [b|=Top]/⋯⋯/[a|=Top]) and turns it into a function a-->b; note the variance *)
 727   Definition context_operation_as_function
 728     : forall {a}{b} (f:[b|=[]]~~{Judgments}~~>[a|=[]]), []~~{Judgments}~~>[a|=b].
 729     intros.
 730     apply (@al_vert_expand_suc_right _ _ _ b _ _) in f.
 731     simpl in f.
 732     apply (@al_vert_expand_ant_left  _ _ _ [] _ _) in f.
 733     simpl in f.
 734     set ([#al_reflexive_seq _#] ;; f ;; [#al_ant_cancell#] ;; [#al_suc_cancell#]) as f'.
 735     exact f'.
 736     Defined.
 737
 738   (* takes an "operation in the context" (proof from [Top|=a]/⋯⋯/[Top|=b]) and turns it into a function a-->b; note the variance *)
 739   Definition cocontext_operation_as_function
 740     : forall {a}{b} (f:[[]|=a]~~{Judgments}~~>[[]|=b]), []~~{Judgments}~~>[a|=b].
 741     intros. unfold hom. unfold hom in f.
 742     apply al_vert_expand_ant_right with (x:=a) in f.
 743     simpl in f.
 744     apply al_vert_expand_suc_left with (x:=[]) in f.
 745     simpl in f.
 746     set ([#al_reflexive_seq _#] ;; f ;; [#al_ant_cancell#] ;; [#al_suc_cancell#]) as f'.
 747     exact f'.
 748     Defined.
 749
 750
 751   Definition function_as_context_operation
 752     : forall {a}{b}{c} (f:[]~~{Judgments}~~>[a|=b]), [b|=c]~~{Judgments}~~>[a|=c]
 753     := fun a b c f => RepresentableFunctorºᑭ Types_omega_e c \ f.
 754   Definition function_as_cocontext_operation
 755     : forall {a}{b}{c} (f:[]/⋯⋯/[a|=b]), [c|=a]~~{Judgments}~~>[c|=b]
 756     := fun a b c f => RepresentableFunctor Types_omega_e c \ f.
 757
 758   Close Scope temporary_scope4.
 759   Close Scope al_scope.
 760   Close Scope nd_scope.
 761   Close Scope pf_scope.
 762   Close Scope isomorphism_scope.
 763 End Acceptable_Language_Facts.
 764
 765 Coercion AL_SurjectiveEnrichment    : AcceptableLanguage >-> SurjectiveEnrichment.
 766 Coercion AL_MonicMonoidalEnrichment : AcceptableLanguage >-> MonicMonoidalEnrichment.