src/HaskProofCategory.v

   1 (*********************************************************************************************************************************)
   2 (* HaskProofCategory:                                                                                                            *)
   3 (*                                                                                                                               *)
   4 (*    Natural Deduction proofs of the well-typedness of a Haskell term form a category                                           *)
   5 (*                                                                                                                               *)
   6 (*********************************************************************************************************************************)
   7
   8 Generalizable All Variables.
   9 Require Import Preamble.
  10 Require Import General.
  11 Require Import NaturalDeduction.
  12 Require Import Coq.Strings.String.
  13 Require Import Coq.Lists.List.
  14
  15 Require Import HaskKinds.
  16 Require Import HaskCoreTypes.
  17 Require Import HaskLiteralsAndTyCons.
  18 Require Import HaskStrongTypes.
  19 Require Import HaskProof.
  20 Require Import NaturalDeduction.
  21 Require Import NaturalDeductionCategory.
  22
  23 Require Import Algebras_ch4.
  24 Require Import Categories_ch1_3.
  25 Require Import Functors_ch1_4.
  26 Require Import Isomorphisms_ch1_5.
  27 Require Import ProductCategories_ch1_6_1.
  28 Require Import OppositeCategories_ch1_6_2.
  29 Require Import Enrichment_ch2_8.
  30 Require Import Subcategories_ch7_1.
  31 Require Import NaturalTransformations_ch7_4.
  32 Require Import NaturalIsomorphisms_ch7_5.
  33 Require Import MonoidalCategories_ch7_8.
  34 Require Import Coherence_ch7_8.
  35
  36 Require Import HaskStrongTypes.
  37 Require Import HaskStrong.
  38 Require Import HaskProof.
  39 Require Import HaskStrongToProof.
  40 Require Import HaskProofToStrong.
  41 Require Import ProgrammingLanguage.
  42
  43 Section HaskProofCategory.
  44
  45   Definition unitType {Γ} : RawHaskType Γ ★.
  46     admit.
  47     Defined.
  48
  49   Definition brakifyType {Γ} (v:HaskTyVar Γ ★)(lt:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
  50     match lt with
  51       t @@ l => HaskBrak v t @@ l
  52     end.
  53
  54   Definition brakifyu {Γ}{Δ}(v:HaskTyVar Γ ★)(j:UJudg Γ Δ) : UJudg Γ Δ :=
  55     match j with
  56       mkUJudg Σ τ =>
  57         Γ >> Δ > mapOptionTree (brakifyType v) Σ |- mapOptionTree (brakifyType v) τ
  58     end.
  59
  60   Definition mkEsc {Γ}{Δ}(j:Tree ??(UJudg Γ Δ)) v h
  61     : ND Rule
  62     (mapOptionTree (@UJudg2judg Γ Δ) h)
  63     (mapOptionTree (fun j => @UJudg2judg Γ Δ (brakifyu v j)) h).
  64     admit.
  65     Defined.
  66
  67   Definition mkBrak {Γ}{Δ}(j:Tree ??(UJudg Γ Δ)) v h
  68     : ND Rule
  69     (mapOptionTree (fun j => @UJudg2judg Γ Δ (brakifyu v j)) h)
  70     (mapOptionTree (@UJudg2judg Γ Δ           ) h).
  71     admit.
  72     Defined.
  73
  74   Context (ndr_systemfc:@ND_Relation _ Rule).
  75
  76   Open Scope nd_scope.
  77
  78   (* Rules allowed in PCF; i.e. rules we know how to turn into GArrows *)
  79   (* Rule_PCF consists of the rules allowed in flat PCF: everything except
  80      * AppT, AbsT, AppC, AbsC, Cast, Global, and some Case statements *)
  81   Inductive Rule_PCF {Γ:TypeEnv}{Δ:CoercionEnv Γ} : forall {h}{c}, Rule h c -> Type :=
  82   | PCF_RURule           : ∀ h c r            ,  Rule_PCF (RURule Γ Δ  h c r)
  83   | PCF_RLit             : ∀ Σ τ              ,  Rule_PCF (RLit Γ Δ Σ τ  )
  84   | PCF_RNote            : ∀ Σ τ l n          ,  Rule_PCF (RNote Γ Δ Σ τ l n)
  85   | PCF_RVar             : ∀ σ               l,  Rule_PCF (RVar Γ Δ  σ         l)
  86   | PCF_RLam             : ∀ Σ tx te    q     ,  Rule_PCF (RLam Γ Δ  Σ tx te      q )
  87   | PCF_RApp             : ∀ Σ tx te   p     l,  Rule_PCF (RApp Γ Δ  Σ tx te   p l)
  88   | PCF_RLet             : ∀ Σ σ₁ σ₂   p     l,  Rule_PCF (RLet Γ Δ  Σ σ₁ σ₂   p l)
  89   | PCF_RBindingGroup    : ∀ q a b c d e      ,  Rule_PCF (RBindingGroup q a b c d e)
  90   | PCF_RCase            : ∀ T κlen κ θ l x   ,  Rule_PCF (RCase Γ Δ T κlen κ θ l x)   (* FIXME: only for boolean and int *)
  91   | PCF_REmptyGroup      : ∀ q a              ,  Rule_PCF (REmptyGroup q a)
  92   | PCF_RLetRec          : ∀ Σ₁ τ₁ τ₂ lev     ,  Rule_PCF (RLetRec Γ Δ Σ₁ τ₁ τ₂ lev).
  93   Implicit Arguments Rule_PCF [ ].
  94
  95   Definition PCFR Γ Δ h c := { r:_ & Rule_PCF Γ Δ h c r }.
  96
  97   (* An organized deduction has been reorganized into contiguous blocks whose
  98    * hypotheses (if any) and conclusion have the same Γ and Δ and a fixed nesting depth.  The boolean
  99    * indicates if non-PCF rules have been used *)
 100   Inductive OrgR : bool -> nat -> forall Γ Δ, Tree ??(UJudg Γ Δ) -> Tree ??(UJudg Γ Δ) -> Type :=
 101
 102   | org_pcf       : forall n Γ Δ h c b,
 103     PCFR Γ Δ (mapOptionTree UJudg2judg h) (mapOptionTree UJudg2judg c) -> OrgR b n Γ Δ h c
 104
 105   | org_fc        : forall n Γ Δ h c,
 106     ND Rule (mapOptionTree UJudg2judg h) (mapOptionTree UJudg2judg c) -> OrgR true n Γ Δ h c
 107
 108   | org_nest      : forall n Γ Δ h c b v,
 109     OrgR b    n  Γ Δ h c ->
 110     OrgR b (S n) _ _ (mapOptionTree (brakifyu v) h) (mapOptionTree (brakifyu v) c)
 111   .
 112
 113   Definition OrgND b n Γ Δ := ND (OrgR b n Γ Δ).
 114
 115   (* any proof in organized form can be "dis-organized" *)
 116   Definition unOrgR b n Γ Δ : forall h c, OrgR b n Γ Δ h c ->
 117     ND Rule (mapOptionTree (@UJudg2judg Γ Δ) h) (mapOptionTree (@UJudg2judg Γ Δ) c).
 118
 119     intros.
 120
 121     induction X.
 122       apply nd_rule.
 123       destruct p.
 124       apply x.
 125
 126     apply n0.
 127
 128     rewrite <- mapOptionTree_compose.
 129       rewrite <- mapOptionTree_compose.
 130       eapply nd_comp.
 131       apply (mkBrak h).
 132       eapply nd_comp; [ idtac |  apply (mkEsc c) ].
 133       apply IHX.
 134       Defined.
 135
 136     Definition unOrgND b n Γ Δ h c :
 137       ND (OrgR b n Γ Δ) h c -> ND Rule (mapOptionTree (@UJudg2judg Γ Δ) h) (mapOptionTree (@UJudg2judg Γ Δ) c)
 138       := nd_map' (@UJudg2judg Γ Δ) (unOrgR b n Γ Δ).
 139
 140     Instance OrgNDR b n Γ Δ : @ND_Relation _ (OrgR b n Γ Δ) :=
 141     { ndr_eqv := fun a b f g => (unOrgND _ _ _ _ _ _ f) === (unOrgND _ _ _ _ _ _ g) }.
 142       admit.
 143       admit.
 144       admit.
 145       admit.
 146       admit.
 147       admit.
 148       admit.
 149       admit.
 150       admit.
 151       admit.
 152       admit.
 153       admit.
 154       admit.
 155       Defined.
 156
 157       (*
 158     Hint Constructors Rule_Flat.
 159
 160     Definition SystemFC_SC n : @SequentCalculus _ (RuleSystemFCa n) _ (mkJudg Γ Δ).
 161       apply Build_SequentCalculus.
 162       intro a.
 163       induction a.
 164       destruct a.
 165       apply nd_rule.
 166       destruct l.
 167       apply sfc_flat with (r:=RVar _ _ _ _).
 168       auto.
 169       apply nd_rule.
 170       apply sfc_flat with (r:=REmptyGroup _ _).
 171       auto.
 172       eapply nd_comp; [ apply nd_llecnac | idtac ].
 173       eapply nd_comp; [ eapply nd_prod | idtac ].
 174       apply IHa1.
 175       apply IHa2.
 176       apply nd_rule.
 177       apply sfc_flat with (r:=RBindingGroup _ _ _ _ _ _ ).
 178       auto.
 179       Defined.
 180
 181     Existing Instance SystemFC_SC.
 182
 183     Lemma systemfc_cut n : ∀a b c,
 184            ND (RuleSystemFCa n) ([Γ > Δ > a |- b],, [Γ > Δ > b |- c]) [Γ > Δ > a |- c].
 185       intros.
 186       admit.
 187       Defined.
 188
 189     Lemma systemfc_cutrule n
 190       : @CutRule _ (RuleSystemFCa n) _ (mkJudg Γ Δ) (ndr_systemfc n) (SystemFC_SC n).
 191       apply Build_CutRule with (nd_cut:=systemfc_cut n).
 192       admit.
 193       admit.
 194       admit.
 195       Defined.
 196
 197     Definition systemfc_left n a b c : ND (RuleSystemFCa n) [Γ > Δ > b |- c] [Γ > Δ > a,, b |- a,, c].
 198       eapply nd_comp; [ apply nd_llecnac | idtac ].
 199       eapply nd_comp; [ eapply nd_prod | idtac ].
 200       Focus 3.
 201       apply nd_rule.
 202       apply sfc_flat with (r:=RBindingGroup _ _ _ _ _ _ ).
 203       auto.
 204       idtac.
 205       apply nd_seq_reflexive.
 206       apply nd_id.
 207       Defined.
 208
 209     Definition systemfc_right n a b c : ND (RuleSystemFCa n) [Γ > Δ > b |- c] [Γ > Δ > b,,a |- c,,a].
 210       eapply nd_comp; [ apply nd_rlecnac | idtac ].
 211       eapply nd_comp; [ eapply nd_prod | idtac ].
 212       apply nd_id.
 213       apply (nd_seq_reflexive a).
 214       apply nd_rule.
 215       apply sfc_flat with (r:=RBindingGroup _ _ _ _ _ _ ).
 216       auto.
 217       Defined.
 218 *)
 219 (*
 220     Definition systemfc_expansion n
 221       : @SequentExpansion _ (RuleSystemFCa n) _ (mkJudg Γ Δ) (ndr_systemfca n) (SystemFC_SC n) (systemfc_cutrule n).
 222     Check  (@Build_SequentExpansion).
 223 apply (@Build_SequentExpansion _ _ _ _ (ndr_systemfca n)  _ _ (systemfc_left n) (systemfc_right n)).
 224       refine {| se_expand_left:=systemfc_left n
 225         ; se_expand_right:=systemfc_right n |}.
 226
 227 *)
 228
 229     (* 5.1.2 *)
 230     Instance SystemFCa n Γ Δ : @ProgrammingLanguage _ _ (@mkUJudg Γ Δ) (OrgR true n Γ Δ) :=
 231     { pl_eqv                := OrgNDR true n Γ Δ
 232     ; pl_tsr                := _ (*@TreeStructuralRules Judg Rule T sequent*)
 233     ; pl_sc                 := _
 234     ; pl_subst              := _
 235     ; pl_sequent_join       := _
 236     }.
 237       apply Build_TreeStructuralRules; intros; unfold eqv; unfold hom; simpl.
 238       apply nd_rule; apply org_fc; apply nd_rule; simpl.  apply  (RURule _ _ _ _ (RCossa _ a b c)).
 239       apply nd_rule; apply org_fc; apply nd_rule; simpl;  apply  (RURule _ _ _ _ (RAssoc _ a b c)).
 240       apply nd_rule; apply org_fc; apply nd_rule; simpl;  apply  (RURule _ _ _ _ (RCanL  _ a    )).
 241       apply nd_rule; apply org_fc; apply nd_rule; simpl;  apply  (RURule _ _ _ _ (RCanR  _ a    )).
 242       apply nd_rule; apply org_fc; apply nd_rule; simpl;  apply  (RURule _ _ _ _ (RuCanL _ a    )).
 243       apply nd_rule; apply org_fc; apply nd_rule; simpl;  apply  (RURule _ _ _ _ (RuCanR _ a    )).
 244       Admitted.
 245
 246     (* "flat" SystemFC: no brackets allowed *)
 247     Instance SystemFC Γ Δ : @ProgrammingLanguage _ _ (@mkUJudg Γ Δ) (OrgR true O Γ Δ) :=
 248     { pl_eqv                := OrgNDR true O Γ Δ
 249     ; pl_tsr                := _ (*@TreeStructuralRules Judg Rule T sequent*)
 250     ; pl_sc                 := _
 251     ; pl_subst              := _
 252     ; pl_sequent_join       := _
 253     }.
 254       Admitted.
 255
 256     (* 5.1.3 *)
 257     Instance PCF n Γ Δ : @ProgrammingLanguage _ _ (@mkUJudg Γ Δ) (OrgR false n Γ Δ) :=
 258     { pl_eqv                := OrgNDR false n Γ Δ
 259     ; pl_tsr                := _ (*@TreeStructuralRules Judg Rule T sequent*)
 260     ; pl_sc                 := _
 261     ; pl_subst              := _
 262     ; pl_sequent_join       := _
 263     }.
 264       apply Build_TreeStructuralRules; intros; unfold eqv; unfold hom; simpl.
 265       apply nd_rule; apply org_pcf; simpl; exists (RCossa _ a b c); apply (PCF_RURule [_>>_>_|-_] [_>>_>_|-_]).
 266       apply nd_rule; apply org_pcf; simpl; exists (RAssoc _ a b c); apply (PCF_RURule [_>>_>_|-_] [_>>_>_|-_]).
 267       apply nd_rule; apply org_pcf; simpl; exists (RCanL  _ a    ); apply (PCF_RURule [_>>_>_|-_] [_>>_>_|-_]).
 268       apply nd_rule; apply org_pcf; simpl; exists (RCanR  _ a    ); apply (PCF_RURule [_>>_>_|-_] [_>>_>_|-_]).
 269       apply nd_rule; apply org_pcf; simpl; exists (RuCanL _ a    ); apply (PCF_RURule [_>>_>_|-_] [_>>_>_|-_]).
 270       apply nd_rule; apply org_pcf; simpl; exists (RuCanR _ a    ); apply (PCF_RURule [_>>_>_|-_] [_>>_>_|-_]).
 271     Admitted.
 272
 273   (* gathers a tree of guest-language types into a single host-language types via the tensor *)
 274   Definition tensorizeType {Γ} (lt:Tree ??(LeveledHaskType Γ ★)) : HaskType Γ ★.
 275     admit.
 276     Defined.
 277
 278   Definition mkGA {Γ} : HaskType Γ ★ -> HaskType Γ ★ -> HaskType Γ ★.
 279     admit.
 280     Defined.
 281
 282   Definition guestJudgmentAsGArrowType {Γ}{Δ} (lt:UJudg Γ Δ) : LeveledHaskType Γ ★ :=
 283     match lt with
 284       mkUJudg x y =>
 285       (mkGA (tensorizeType x) (tensorizeType y)) @@ nil
 286     end.
 287
 288   Fixpoint obact n {Γ}{Δ}(X:Tree ??(UJudg Γ Δ)) : Tree ??(LeveledHaskType Γ ★) :=
 289     match n with
 290       | 0    => mapOptionTree guestJudgmentAsGArrowType X
 291       | S n' => let t := obact n' X
 292                 in  [guestJudgmentAsGArrowType (Γ >> Δ > [] |- t )]
 293     end.
 294
 295 (*  Definition *)
 296
 297
 298   Definition magic {Γ}{Δ} h c n x :
 299 Rule_PCF Γ Δ (mapOptionTree (@UJudg2judg Γ Δ) h) (mapOptionTree (@UJudg2judg Γ Δ) c) x
 300 -> ND (OrgR true n Γ Δ) []
 301      [Γ >> Δ > mapOptionTree guestJudgmentAsGArrowType h
 302       |- mapOptionTree guestJudgmentAsGArrowType c].
 303   admit.
 304   Defined.
 305
 306   (*
 307    * Here it is, what you've all been waiting for!  When reading this,
 308    * it might help to have the definition for "Inductive ND" (see
 309    * NaturalDeduction.v) handy as a cross-reference.
 310    *)
 311   Definition FlatteningFunctor_fmor {Γ}{Δ}
 312     : forall h c,
 313       (h~~{JudgmentsL _ _ (PCF 0 Γ Δ)}~~>c) ->
 314       ((obact 0 h)~~{TypesL _ _ (SystemFC Γ Δ)}~~>(obact 0 c)).
 315     unfold hom; unfold ob; unfold ehom; simpl; unfold mon_i; unfold obact; intros.
 316
 317     induction X; simpl.
 318
 319     (* the proof from no hypotheses of no conclusions (nd_id0) becomes REmptyGroup *)
 320     apply nd_rule; apply org_fc; simpl. apply nd_rule. apply REmptyGroup.
 321
 322     (* the proof from hypothesis X of conclusion X (nd_id1) becomes RVar *)
 323     apply nd_rule; apply org_fc; simpl. apply nd_rule. destruct (guestJudgmentAsGArrowType h). apply RVar.
 324
 325     (* the proof from hypothesis X of no conclusions (nd_weak) becomes RWeak;;REmptyGroup *)
 326     apply nd_rule; apply org_fc; simpl.
 327       eapply nd_comp; [ idtac | apply (nd_rule (RURule _ _ _ _ (RWeak _ _))) ].
 328       apply nd_rule. apply REmptyGroup.
 329
 330     (* the proof from hypothesis X of two identical conclusions X,,X (nd_copy) becomes RVar;;RBindingGroup;;RCont *)
 331     eapply nd_comp; [ idtac | eapply nd_rule; eapply org_fc; apply (nd_rule (RURule _ _ _ _ (RCont _ _))) ].
 332       eapply nd_comp; [ apply nd_llecnac | idtac ].
 333       set (nd_seq_reflexive(SequentCalculus:=@pl_sc  _ _ _ _ (SystemFC Γ Δ)) (mapOptionTree guestJudgmentAsGArrowType h)) as q.
 334       eapply nd_comp.
 335       eapply nd_prod.
 336       apply q.
 337       apply q.
 338       apply nd_rule; eapply org_fc.
 339       simpl.
 340       apply nd_rule.
 341       apply RBindingGroup.
 342
 343     (* nd_prod becomes nd_llecnac;;nd_prod;;RBindingGroup *)
 344     eapply nd_comp.
 345       apply (nd_llecnac ;; nd_prod IHX1 IHX2).
 346       apply nd_rule; apply org_fc; simpl.
 347       eapply nd_rule. apply RBindingGroup.
 348
 349     (* nd_comp becomes pl_subst (aka nd_cut) *)
 350     eapply nd_comp.
 351       apply (nd_llecnac ;; nd_prod IHX1 IHX2).
 352       clear IHX1 IHX2 X1 X2.
 353       apply (@nd_cut _ _ _ _ _ _ (@pl_subst _ _ _ _ (SystemFC Γ Δ))).
 354
 355     (* nd_cancell becomes RVar;;RuCanL *)
 356     eapply nd_comp;
 357       [ idtac | eapply nd_rule; apply org_fc; simpl; apply nd_rule; apply (RURule _ _ _ _ (RuCanL _ _)) ].
 358       apply (nd_seq_reflexive(SequentCalculus:=@pl_sc  _ _ _ _ (SystemFC Γ Δ))).
 359
 360     (* nd_cancelr becomes RVar;;RuCanR *)
 361     eapply nd_comp;
 362       [ idtac | eapply nd_rule; apply org_fc; simpl; apply nd_rule; apply (RURule _ _ _ _ (RuCanR _ _)) ].
 363       apply (nd_seq_reflexive(SequentCalculus:=@pl_sc  _ _ _ _ (SystemFC Γ Δ))).
 364
 365     (* nd_llecnac becomes RVar;;RCanL *)
 366     eapply nd_comp;
 367       [ idtac | eapply nd_rule; apply org_fc; simpl; apply nd_rule; apply (RURule _ _ _ _ (RCanL _ _)) ].
 368       apply (nd_seq_reflexive(SequentCalculus:=@pl_sc  _ _ _ _ (SystemFC Γ Δ))).
 369
 370     (* nd_rlecnac becomes RVar;;RCanR *)
 371     eapply nd_comp;
 372       [ idtac | eapply nd_rule; apply org_fc; simpl; apply nd_rule; apply (RURule _ _ _ _ (RCanR _ _)) ].
 373       apply (nd_seq_reflexive(SequentCalculus:=@pl_sc  _ _ _ _ (SystemFC Γ Δ))).
 374
 375     (* nd_assoc becomes RVar;;RAssoc *)
 376     eapply nd_comp;
 377       [ idtac | eapply nd_rule; apply org_fc; simpl; apply nd_rule; apply (RURule _ _ _ _ (RAssoc _ _ _ _)) ].
 378       apply (nd_seq_reflexive(SequentCalculus:=@pl_sc  _ _ _ _ (SystemFC Γ Δ))).
 379
 380     (* nd_coss becomes RVar;;RCossa *)
 381     eapply nd_comp;
 382       [ idtac | eapply nd_rule; apply org_fc; simpl; apply nd_rule; apply (RURule _ _ _ _ (RCossa _ _ _ _)) ].
 383       apply (nd_seq_reflexive(SequentCalculus:=@pl_sc  _ _ _ _ (SystemFC Γ Δ))).
 384
 385     (* now, the interesting stuff: the inference rules of Judgments(PCF) become GArrow-parameterized terms *)
 386       refine (match r as R in OrgR B N G D H C return
 387                 match N with
 388                   | S _ => True
 389                   | O   => if B then True
 390                            else ND (OrgR true 0 G D)
 391                                   []
 392                                   [G >> D > mapOptionTree guestJudgmentAsGArrowType H |- mapOptionTree guestJudgmentAsGArrowType C]
 393                 end with
 394                 | org_pcf  n Γ Δ h c b r => _
 395                 | org_fc   n Γ Δ h c r => _
 396                 | org_nest n Γ Δ h c b v q => _
 397               end); destruct n; try destruct b; try apply I.
 398       destruct r0.
 399
 400       clear r h c Γ Δ.
 401       rename r0 into r; rename h0 into h; rename c0 into c; rename Γ0 into Γ; rename Δ0 into Δ.
 402
 403       refine (match r as R in Rule_PCF G D H C with
 404                 | PCF_RURule           h c r            => let case_RURule := tt in _
 405                 | PCF_RLit             Σ τ              => let case_RLit := tt in _
 406                 | PCF_RNote            Σ τ l n          => let case_RNote := tt in _
 407                 | PCF_RVar             σ               l=> let case_RVar := tt in _
 408                 | PCF_RLam             Σ tx te    q     => let case_RLam := tt in _
 409                 | PCF_RApp             Σ tx te   p     l=> let case_RApp := tt in _
 410                 | PCF_RLet             Σ σ₁ σ₂   p     l=> let case_RLet := tt in _
 411                 | PCF_RBindingGroup    q a b c d e      => let case_RBindingGroup := tt in _
 412                 | PCF_RCase            T κlen κ θ l x   => let case_RCase := tt in _
 413                 | PCF_REmptyGroup      q a              => let case_REmptyGroup := tt in _
 414                 | PCF_RLetRec          Σ₁ τ₁ τ₂ lev     => let case_RLetRec := tt in _
 415               end).
 416       rename Γ
 417
 418       apply (magic _ _ _ _ r0).
 419       Defined.
 420
 421   Instance FlatteningFunctor {n}{Γ}{Δ} : Functor (JudgmentsL _ _ (PCF n Γ Δ)) (TypesL _ _ (SystemFCa n Γ Δ)) obact :=
 422     { fmor := FlatteningFunctor_fmor }.
 423     unfold hom; unfold ob; unfold ehom; intros; simpl.
 424
 425
 426   Definition productifyType {Γ} (lt:Tree ??(LeveledHaskType Γ ★)) : LeveledHaskType Γ ★.
 427     admit.
 428     Defined.
 429
 430   Definition exponent {Γ} : LeveledHaskType Γ ★ -> LeveledHaskType Γ ★ -> LeveledHaskType Γ ★.
 431     admit.
 432     Defined.
 433
 434   Definition brakify {Γ}(Σ τ:Tree ??(LeveledHaskType Γ ★))  := exponent (productifyType Σ) (productifyType τ).
 435
 436   Definition brakifyJudg (j:Judg) : Judg :=
 437     match j with
 438       Γ > Δ > Σ |- τ =>
 439         Γ > Δ > [] |- [brakify Σ τ]
 440     end.
 441
 442   Definition brakifyUJudg (j:Judg) : Judg :=
 443     match j with
 444       Γ > Δ > Σ |- τ =>
 445         Γ > Δ > [] |- [brakify Σ τ]
 446     end.
 447   *)
 448
 449   End RuleSystemFC.
 450
 451   Context (ndr_pcf      :forall n Γ Δ, @ND_Relation _ (@RulePCF Γ Δ n)).
 452
 453
 454   Instance PCF n Γ Δ : @ProgrammingLanguage _ _ (mkJudg Γ Δ) (@RulePCF Γ Δ n) :=
 455   { pl_eqv                := _
 456   ; pl_tsr                := _ (*@TreeStructuralRules Judg Rule T sequent*)
 457   ; pl_sc                 := _ (*@SequentCalculus Judg Rule _ sequent*)
 458   ; pl_subst              := _ (*@CutRule Judg Rule _ sequent pl_eqv pl_sc*)
 459   ; pl_sequent_join       := _ (*@SequentExpansion Judg Rule T sequent pl_eqv pl_sc pl_subst*)
 460   }.
 461   Admitted.
 462
 463   Inductive RuleX : nat -> Tree ??Judg -> Tree ??Judg -> Type :=
 464   | x_flat : forall n     h c   (r:Rule h c), Rule_Flat r -> RuleX    n  h c
 465   | x_nest : forall n Γ Δ h c,  ND (@RulePCF Γ Δ n) h c   ->
 466     RuleX (S n) (mapOptionTree brakifyJudg h) (mapOptionTree brakifyJudg c).
 467
 468   Section X.
 469
 470     Context (n:nat).
 471     Context (ndr:@ND_Relation _ (RuleX (S n))).
 472
 473     Definition SystemFCa' := Judgments_Category ndr.
 474
 475     Definition ReificationFunctor_fmor Γ Δ
 476       : forall h c,
 477         (h~~{JudgmentsL _ _ (PCF n Γ Δ)}~~>c) ->
 478         ((mapOptionTree brakifyJudg h)~~{SystemFCa'}~~>(mapOptionTree brakifyJudg c)).
 479       unfold hom; unfold ob; simpl.
 480       intros.
 481       apply nd_rule.
 482       eapply x_nest.
 483       apply X.
 484       Defined.
 485
 486     Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
 487       refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
 488       unfold ReificationFunctor_fmor; simpl.
 489       admit.
 490       unfold ReificationFunctor_fmor; simpl.
 491       admit.
 492       unfold ReificationFunctor_fmor; simpl.
 493       admit.
 494       Defined.
 495
 496     Definition FlatteningFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakify).
 497       refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
 498       unfold ReificationFunctor_fmor; simpl.
 499       admit.
 500       unfold ReificationFunctor_fmor; simpl.
 501       admit.
 502       unfold ReificationFunctor_fmor; simpl.
 503       admit.
 504       Defined.
 505
 506   Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
 507     refine {| plsmme_pl := PCF n Γ Δ |}.
 508     admit.
 509     Defined.
 510
 511   Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
 512     refine {| plsmme_pl := SystemFCa n Γ Δ |}.
 513     admit.
 514     Defined.
 515
 516   Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
 517     admit.
 518     Defined.
 519
 520   (* 5.1.4 *)
 521   Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
 522     admit.
 523     (*  ... and the retraction exists *)
 524     Defined.
 525
 526   (* Any particular proof in HaskProof is only finitely large, so it uses only finitely many levels of nesting, so
 527    * it falls within (SystemFCa n) for some n.  This function calculates that "n" and performs the translation *)
 528   (*
 529   Definition HaskProof_to_SystemFCa :
 530     forall h c (pf:ND Rule h c),
 531       { n:nat & h ~~{JudgmentsL (SystemFCa_SMME n)}~~> c }.
 532       *)
 533
 534   (* for every n we have a functor from the category of (n+1)-bounded proofs to the category of n-bounded proofs *)
 535
 536
 537   Definition makeTree : Tree ??(LeveledHaskType Γ ★) -> HaskType Γ ★.
 538     admit.
 539     Defined.
 540
 541   Definition flattenType n (j:JudgmentsN n) : TypesN n.
 542     unfold eob_eob.
 543     unfold ob in j.
 544     refine (mapOptionTree _ j).
 545     clear j; intro j.
 546     destruct j as [ Γ' Δ' Σ τ ].
 547     assert (Γ'=Γ). admit.
 548     rewrite H in *.
 549     clear H Γ'.
 550     refine (_ @@ nil).
 551     refine (HaskBrak _ ( (makeTree Σ) ---> (makeTree τ) )); intros.
 552     admit.
 553     Defined.
 554
 555   Definition FlattenFunctor_fmor n :
 556     forall h c,
 557       (h~~{JudgmentsN n}~~>c) ->
 558       ((flattenType n h)~~{TypesN n}~~>(flattenType n c)).
 559     intros.
 560     unfold hom in *; simpl.
 561     unfold mon_i.
 562     unfold ehom.
 563     unfold TypesNmor.
 564
 565     admit.
 566     Defined.
 567
 568   Definition FlattenFunctor n : Functor (JudgmentsN n) (TypesN n) (flattenType n).
 569     refine {| fmor := FlattenFunctor_fmor n |}; intros.
 570     admit.
 571     admit.
 572     admit.
 573     Defined.
 574
 575   End RulePCF.
 576   Implicit Arguments Rule_PCF [ [h] [c] ].
 577   Implicit Arguments BoundedRule [ ].
 578
 579 *)
 580 (*
 581   Definition code2garrow0 {Γ}(ec t1 t2:RawHaskType Γ ★) : RawHaskType Γ ★.
 582     admit.
 583     Defined.
 584   Definition code2garrow Γ (ec t:RawHaskType Γ ★) :=
 585       match t with
 586 (*        | TApp ★ ★ (TApp _ ★ TArrow tx) t' => code2garrow0 ec tx       t'*)
 587         |                               _  => code2garrow0 ec unitType t
 588       end.
 589   Opaque code2garrow.
 590   Fixpoint typeMap {TV}{κ}(ty:@RawHaskType TV κ) : @RawHaskType TV κ :=
 591       match ty as TY in RawHaskType _ K return RawHaskType TV K with
 592         | TCode ec t        => code2garrow _ ec t
 593         | TApp _ _ t1 t2    => TApp (typeMap t1) (typeMap t2)
 594         | TAll _ f          => TAll _ (fun tv => typeMap (f tv))
 595         | TCoerc _ t1 t2 t3 => TCoerc (typeMap t1) (typeMap t2) (typeMap t3)
 596         | TVar   _ v        => TVar v
 597         | TArrow            => TArrow
 598         | TCon  tc          => TCon tc
 599         | TyFunApp  tf rhtl => (* FIXME *) TyFunApp tf rhtl
 600       end.
 601
 602   Definition typeMapL {Γ}(lht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★  :=
 603     match lht with
 604 (*      | t @@ nil       => (fun TV ite => typeMap (t TV ite)) @@ lev*)
 605       | t @@ lev => (fun TV ite => typeMap (t TV ite)) @@ lev
 606     end.
 607
 608   Definition coMap {Γ}(ck:HaskCoercionKind Γ) :=
 609     fun TV ite => match ck TV ite with
 610       | mkRawCoercionKind _ t1 t2 => mkRawCoercionKind _ (typeMap t1) (typeMap t2)
 611       end.
 612
 613   Definition flattenCoercion {Γ}{Δ}{ck}(hk:HaskCoercion Γ Δ ck) : HaskCoercion Γ (map coMap Δ) (coMap ck).
 614     admit.
 615     Defined.
 616
 617   Lemma update_typeMap Γ (lev:HaskLevel Γ) ξ v t
 618     : (typeMap ○ (update_ξ            ξ  lev ((⟨v, t ⟩)          :: nil)))
 619     = (           update_ξ (typeMap ○ ξ) lev ((⟨v, typeMap_ t ⟩) :: nil)).
 620     admit.
 621     Qed.
 622
 623   Lemma foo κ Γ σ τ : typeMap_ (substT σ τ) = substT(Γ:=Γ)(κ₁:=κ) (fun TV ite => typeMap ○ σ TV ite) τ.
 624     admit.
 625     Qed.
 626
 627   Lemma lit_lemma lit Γ : typeMap_ (literalType lit) = literalType(Γ:=Γ) lit.
 628     admit.
 629     Qed.
 630 *)
 631 (*
 632   Definition flatten : forall h c, Rule h c -> @ND Judg Rule (mapOptionTree flattenJudgment h) (mapOptionTree flattenJudgment c).
 633     intros h c r.
 634     refine (match r as R in Rule H C return ND Rule (mapOptionTree flattenJudgment H) (mapOptionTree flattenJudgment C) with
 635       | RURule  a b c d e             => let case_RURule := tt        in _
 636       | RNote   Γ Δ Σ τ l n           => let case_RNote := tt         in _
 637       | RLit    Γ Δ l     _           => let case_RLit := tt          in _
 638       | RVar    Γ Δ σ         p       => let case_RVar := tt          in _
 639       | RGlobal Γ Δ σ l wev           => let case_RGlobal := tt       in _
 640       | RLam    Γ Δ Σ tx te     x     => let case_RLam := tt          in _
 641       | RCast   Γ Δ Σ σ τ γ     x     => let case_RCast := tt         in _
 642       | RAbsT   Γ Δ Σ κ σ a           => let case_RAbsT := tt         in _
 643       | RAppT   Γ Δ Σ κ σ τ     y     => let case_RAppT := tt         in _
 644       | RAppCo  Γ Δ Σ κ σ₁ σ₂ γ σ l   => let case_RAppCo := tt        in _
 645       | RAbsCo  Γ Δ Σ κ σ  σ₁ σ₂  y   => let case_RAbsCo := tt        in _
 646       | RApp    Γ Δ Σ₁ Σ₂ tx te p     => let case_RApp := tt          in _
 647       | RLet    Γ Δ Σ₁ Σ₂ σ₁ σ₂ p     => let case_RLet := tt          in _
 648       | RBindingGroup Γ p lri m x q   => let case_RBindingGroup := tt in _
 649       | REmptyGroup _ _               => let case_REmptyGroup := tt   in _
 650       | RBrak   Σ a b c n m           => let case_RBrak := tt         in _
 651       | REsc    Σ a b c n m           => let case_REsc := tt          in _
 652       | RCase   Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
 653       | RLetRec Γ Δ lri x y t         => let case_RLetRec := tt       in _
 654       end).
 655
 656       destruct case_RURule.
 657         admit.
 658
 659       destruct case_RBrak.
 660         simpl.
 661         admit.
 662
 663       destruct case_REsc.
 664         simpl.
 665         admit.
 666
 667       destruct case_RNote.
 668         eapply nd_rule.  simpl.  apply RNote; auto.
 669
 670       destruct case_RLit.
 671         simpl.
 672
 673       set (@RNote Γ Δ Σ τ l) as q.
 674     Defined.
 675
 676   Definition flatten' {h}{c} (pf:ND Rule h c) := nd_map' flattenJudgment flatten pf.
 677
 678
 679     @ND Judgment1 Rule1 (mapOptionTree f h) (mapOptionTree f c).
 680
 681   refine (fix flatten : forall Γ Δ Σ τ
 682     (pf:SCND Rule [] [Γ > Δ >                       Σ |-                       τ ]) :
 683     SCND Rule [] [Γ > Δ > mapOptionTree typeMap Σ |- mapOptionTree typeMap τ ] :=
 684     match pf as SCND _ _
 685     | scnd_comp   : forall ht ct c , SCND ht ct -> Rule ct [c] -> SCND ht [c]
 686   | scnd_weak   : forall c       , SCND c  []
 687   | scnd_leaf   : forall ht c    , SCND ht [c]  -> SCND ht [c]
 688   | scnd_branch : forall ht c1 c2, SCND ht c1 -> SCND ht c2 -> SCND ht (c1,,c2)
 689   Expr Γ Δ ξ τ -> Expr Γ (map coMap Δ) (typeMap ○ ξ) (typeMap τ).
 690 *)
 691
 692 (*
 693   Lemma all_lemma Γ κ σ l :
 694 (@typeMap (κ :: Γ)
 695            (@HaskTApp (κ :: Γ) κ (@weakF Γ κ ★ σ) (@FreshHaskTyVar Γ κ) @@
 696             @weakL Γ κ l)) = (@typeMap Γ (@HaskTAll Γ κ σ @@  l)).
 697 *)
 698
 699 (*
 700   Definition flatten : forall Γ Δ ξ τ,  Expr Γ Δ ξ τ -> Expr Γ (map coMap Δ) (typeMap ○ ξ) (typeMap τ).
 701   refine (fix flatten Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') : Expr Γ' (map coMap Δ') (typeMap ○ ξ') (typeMap τ') :=
 702     match exp as E in Expr G D X T return Expr G (map coMap D) (typeMap ○ X) (typeMap T) with
 703     | EGlobal  Γ Δ ξ t wev                          => EGlobal _ _ _ _  wev
 704     | EVar     Γ Δ ξ ev                             => EVar    _ _ _    ev
 705     | ELit     Γ Δ ξ lit lev                        => let case_ELit    := tt in _
 706     | EApp     Γ Δ ξ t1 t2 lev e1 e2                => EApp _ _ _ _ _ _ (flatten _ _ _ _ e1) (flatten _ _ _ _ e2)
 707     | ELam     Γ Δ ξ t1 t2 lev v    e               => let case_ELam := tt in _
 708     | ELet     Γ Δ ξ tv t  l ev elet ebody          => let case_ELet    := tt in _
 709     | ELetRec  Γ Δ ξ lev t tree branches ebody      => let case_ELetRec := tt in _
 710     | ECast    Γ Δ ξ t1 t2 γ lev e                  => let case_ECast   := tt in _
 711     | ENote    Γ Δ ξ t n e                          => ENote _ _ _ _ n (flatten _ _ _ _ e)
 712     | ETyLam   Γ Δ ξ κ σ l e                        => let case_ETyLam  := tt in _
 713     | ECoLam   Γ Δ κ σ σ₁ σ₂ ξ l             e      => let case_ECoLam  := tt in _
 714     | ECoApp   Γ Δ κ σ₁ σ₂ γ σ ξ l e                => let case_ECoApp  := tt in _
 715     | ETyApp   Γ Δ κ σ τ ξ  l    e                  => let case_ETyApp  := tt in _
 716     | ECase    Γ Δ ξ l tc tbranches atypes e alts'  => let case_ECase   := tt in _
 717
 718     | EEsc     Γ Δ ξ ec t lev e                     => let case_EEsc    := tt in _
 719     | EBrak    Γ Δ ξ ec t lev e                     => let case_EBrak   := tt in _
 720     end); clear exp ξ' τ' Γ' Δ'.
 721
 722   destruct case_ELit.
 723     simpl.
 724     rewrite lit_lemma.
 725     apply ELit.
 726
 727   destruct case_ELam.
 728     set (flatten _ _ _ _ e) as q.
 729     rewrite update_typeMap in q.
 730     apply (@ELam _ _ _ _ _ _ _ _ v q).
 731
 732   destruct case_ELet.
 733     set (flatten _ _ _ _ ebody) as ebody'.
 734     set (flatten _ _ _ _ elet)  as elet'.
 735     rewrite update_typeMap in ebody'.
 736     apply (@ELet _ _ _ _ _ _ _ _ _ elet' ebody').
 737
 738   destruct case_EEsc.
 739     admit.
 740   destruct case_EBrak.
 741     admit.
 742
 743   destruct case_ECast.
 744     apply flatten in e.
 745     eapply ECast in e.
 746     apply e.
 747     apply flattenCoercion in γ.
 748     apply γ.
 749
 750   destruct case_ETyApp.
 751     apply flatten in e.
 752     simpl in e.
 753     unfold HaskTAll in e.
 754     unfold typeMap_ in e.
 755     simpl in e.
 756     eapply ETyApp in e.
 757     rewrite <- foo in e.
 758     apply e.
 759
 760   destruct case_ECoLam.
 761     apply flatten in e.
 762     simpl in e.
 763     set (@ECoLam _ _ _ _ _ _ _ _ _ _ e) as x.
 764     simpl in x.
 765     simpl.
 766     unfold typeMap_.
 767     simpl.
 768     apply x.
 769
 770   destruct case_ECoApp.
 771     simpl.
 772     apply flatten in e.
 773     eapply ECoApp.
 774     unfold mkHaskCoercionKind in *.
 775     simpl in γ.
 776     apply flattenCoercion in γ.
 777     unfold coMap in γ at 2.
 778     apply γ.
 779     apply e.
 780
 781   destruct case_ETyLam.
 782     apply flatten in e.
 783     set (@ETyLam Unique _ Γ (map coMap Δ) (typeMap ○ ξ) κ (fun ite x => typeMap (σ x ite))) as e'.
 784     unfold HaskTAll in *.
 785     unfold typeMap_ in *.
 786     rewrite <- foo in e'.
 787     unfold typeMap in e'.
 788     simpl in e'.
 789     apply ETyLam.
 790
 791 Set Printing Implicit.
 792 idtac.
 793 idtac.
 794
 795
 796     admit.
 797
 798   destruct case_ECase.
 799     admit.
 800
 801   destruct case_ELetRec.
 802     admit.
 803     Defined.
 804
 805   (* This proof will work for any dynamic semantics you like, so
 806    * long as those semantics are an ND_Relation (associativity,
 807    * neutrality, etc) *)
 808   Context (dynamic_semantics   : @ND_Relation _ Rule).
 809
 810   Section SystemFC_Category.
 811
 812     Context {Γ:TypeEnv}
 813             {Δ:CoercionEnv Γ}.
 814
 815     Definition Context := Tree ??(LeveledHaskType Γ ★).
 816
 817     Notation "a |= b" := (Γ >> Δ > a |- b).
 818
 819     (*
 820        SystemFCa
 821        PCF
 822        SystemFCa_two_level
 823        SystemFCa_initial_GArrow
 824      *)
 825
 826     Context (nd_eqv:@ND_Relation _ (@URule Γ Δ)).
 827     Check (@ProgrammingLanguage).
 828     Context (PL:@ProgrammingLanguage (LeveledHaskType Γ ★)
 829       (fun x y => match x with x1|=x2 => match y with y1|=y2 => @URule Γ Δ)).
 830     Definition JudgmentsFC := @Judgments_Category_CartesianCat _ (@URule Γ Δ) nd_eqv.
 831     Definition TypesFC     := @TypesL                          _ (@URule Γ Δ) nd_eqv.
 832
 833     (* The full subcategory of SystemFC(Γ,Δ) consisting only of judgments involving types at a fixed level.  Note that
 834      * code types are still permitted! *)
 835     Section SingleLevel.
 836       Context (lev:HaskLevel Γ).
 837
 838       Inductive ContextAtLevel : Context -> Prop :=
 839         | contextAtLevel_nil    :               ContextAtLevel []
 840         | contextAtLevel_leaf   : forall τ,     ContextAtLevel [τ @@ lev]
 841         | contextAtLevel_branch : forall b1 b2, ContextAtLevel b1 -> ContextAtLevel b2 -> ContextAtLevel (b1,,b2).
 842
 843       Inductive JudgmentsAtLevel : JudgmentsFC -> Prop :=
 844         | judgmentsAtLevel_nil    : JudgmentsAtLevel []
 845         | judgmentsAtLevel_leaf   : forall c1 c2, ContextAtLevel c1   -> ContextAtLevel c2   -> JudgmentsAtLevel [c1 |= c2]
 846         | judgmentsAtLevel_branch : forall j1 j2, JudgmentsAtLevel j1 -> JudgmentsAtLevel j2 -> JudgmentsAtLevel (j1,,j2).
 847
 848       Definition JudgmentsFCAtLevel := FullSubcategory JudgmentsFC JudgmentsAtLevel.
 849       Definition TypesFCAtLevel     := FullSubcategory TypesFC     ContextAtLevel.
 850     End SingleLevel.
 851
 852   End SystemFC_Category.
 853
 854   Implicit Arguments TypesFC [ ].
 855
 856 (*
 857     Section EscBrak_Functor.
 858       Context
 859         (past:@Past V)
 860         (n:V)
 861         (Σ₁:Tree ??(@LeveledHaskType V)).
 862
 863       Definition EscBrak_Functor_Fobj
 864         : SystemFC_Cat_Flat ((Σ₁,n)::past) -> SystemFC_Cat past
 865         := mapOptionTree (fun q:Tree ??(@CoreType V) * Tree ??(@CoreType V) =>
 866           let (a,s):=q in (Σ₁,,(``a)^^^n,[`<[ n |- encodeTypeTree_flat s ]>])).
 867
 868
 869       Definition EscBrak_Functor_Fmor
 870         : forall a b (f:a~~{SystemFC_Cat_Flat ((Σ₁,n)::past)}~~>b),
 871           (EscBrak_Functor_Fobj a)~~{SystemFC_Cat past}~~>(EscBrak_Functor_Fobj b).
 872         intros.
 873         eapply nd_comp.
 874         apply prepend_esc.
 875         eapply nd_comp.
 876         eapply Flat_to_ML.
 877         apply f.
 878         apply append_brak.
 879         Defined.
 880
 881       Lemma esc_then_brak_is_id : forall a,
 882        ndr_eqv(ND_Relation:=ml_dynamic_semantics V) (nd_comp prepend_esc append_brak)
 883          (nd_id (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj a))).
 884          admit.
 885          Qed.
 886
 887       Lemma brak_then_esc_is_id : forall a,
 888        ndr_eqv(ND_Relation:=ml_dynamic_semantics V) (nd_comp append_brak prepend_esc)
 889          (nd_id (mapOptionTree (ob2judgment_flat (((Σ₁,n)::past))) a)).
 890          admit.
 891          Qed.
 892
 893       Instance EscBrak_Functor
 894         : Functor (SystemFC_Cat_Flat ((Σ₁,n)::past)) (SystemFC_Cat past) EscBrak_Functor_Fobj :=
 895         { fmor := fun a b f => EscBrak_Functor_Fmor a b f }.
 896         intros; unfold EscBrak_Functor_Fmor; simpl in *.
 897           apply ndr_comp_respects; try reflexivity.
 898           apply ndr_comp_respects; try reflexivity.
 899           auto.
 900         intros; unfold EscBrak_Functor_Fmor; simpl in *.
 901           set (@ndr_comp_left_identity _ _ (ml_dynamic_semantics V)) as q.
 902           setoid_rewrite q.
 903           apply esc_then_brak_is_id.
 904         intros; unfold EscBrak_Functor_Fmor; simpl in *.
 905           set (@ndr_comp_associativity _ _ (ml_dynamic_semantics V)) as q.
 906           repeat setoid_rewrite q.
 907           apply ndr_comp_respects; try reflexivity.
 908           apply ndr_comp_respects; try reflexivity.
 909           repeat setoid_rewrite <- q.
 910           apply ndr_comp_respects; try reflexivity.
 911           setoid_rewrite brak_then_esc_is_id.
 912           clear q.
 913           set (@ndr_comp_left_identity _ _ (fc_dynamic_semantics V)) as q.
 914           setoid_rewrite q.
 915           reflexivity.
 916         Defined.
 917
 918     End EscBrak_Functor.
 919
 920
 921
 922   Ltac rule_helper_tactic' :=
 923     match goal with
 924     | [ H : ?A = ?A |- _ ] => clear H
 925     | [ H : [?A] = [] |- _ ] => inversion H; clear H
 926     | [ H : [] = [?A] |- _ ] => inversion H; clear H
 927     | [ H : ?A,,?B = [] |- _ ] => inversion H; clear H
 928     | [ H : ?A,,?B = [?Y] |- _ ] => inversion H; clear H
 929     | [ H: ?A :: ?B = ?B |- _ ] => apply symmetry in H; apply list_cannot_be_longer_than_itself in H; destruct H
 930     | [ H: ?B = ?A :: ?B |- _ ] => apply list_cannot_be_longer_than_itself in H; destruct H
 931     | [ H: ?A :: ?C :: ?B = ?B |- _ ] => apply symmetry in H; apply list_cannot_be_longer_than_itself' in H; destruct H
 932     | [ H: ?B = ?A :: ?C :: ?B |- _ ] => apply list_cannot_be_longer_than_itself' in H; destruct H
 933 (*  | [ H : Sequent T |- _ ] => destruct H *)
 934 (*  | [ H : ?D = levelize ?C (?A |= ?B) |- _ ] => inversion H; clear H*)
 935     | [ H : [?A] = [?B] |- _ ] => inversion H; clear H
 936     | [ H : [] = mapOptionTree ?B ?C |- _ ] => apply mapOptionTree_on_nil in H; subst
 937     | [ H : [?A] = mapOptionTree ?B ?C |- _ ] => destruct C as [C|]; simpl in H; [ | inversion H ]; destruct C; simpl in H; simpl
 938     | [ H : ?A,,?B = mapOptionTree ?C ?D |- _ ] => destruct D as [D|] ; [destruct D|idtac]; simpl in H; inversion H
 939     end.
 940
 941   Lemma fixit : forall a b f c1 c2, (@mapOptionTree a b f c1),,(mapOptionTree f c2) = mapOptionTree f (c1,,c2).
 942     admit.
 943     Defined.
 944
 945   Lemma grak a b f c : @mapOptionTree a b f c = [] -> [] = c.
 946     admit.
 947     Qed.
 948
 949   Definition append_brak_to_id : forall {c},
 950   @ND_FC V
 951       (mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past))  c )
 952       (mapOptionTree (ob2judgment past)  (EscBrak_Functor_Fobj c)).
 953   admit.
 954   Defined.
 955
 956   Definition append_brak : forall {h c}
 957     (pf:@ND_FC V
 958       h
 959       (mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past))  c )),
 960     @ND_FC V
 961        h
 962       (mapOptionTree (ob2judgment past)  (EscBrak_Functor_Fobj c)).
 963
 964       refine (fix append_brak h c nd {struct nd} :=
 965        ((match nd
 966             as nd'
 967             in @ND _ _ H C
 968             return
 969             (H=h) ->
 970             (C=mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past)) c) ->
 971             ND_FC h (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj c))
 972           with
 973           | nd_id0                     => let case_nd_id0     := tt in _
 974           | nd_id1     h               => let case_nd_id1     := tt in _
 975           | nd_weak    h               => let case_nd_weak    := tt in _
 976           | nd_copy    h               => let case_nd_copy    := tt in _
 977           | nd_prod    _ _ _ _ lpf rpf => let case_nd_prod    := tt in _
 978           | nd_comp    _ _ _   top bot => let case_nd_comp    := tt in _
 979           | nd_rule    _ _     rule    => let case_nd_rule    := tt in _
 980           | nd_cancell _               => let case_nd_cancell := tt in _
 981           | nd_cancelr _               => let case_nd_cancelr := tt in _
 982           | nd_llecnac _               => let case_nd_llecnac := tt in _
 983           | nd_rlecnac _               => let case_nd_rlecnac := tt in _
 984           | nd_assoc   _ _ _           => let case_nd_assoc   := tt in _
 985           | nd_cossa   _ _ _           => let case_nd_cossa   := tt in _
 986         end) (refl_equal _) (refl_equal _)
 987        ));
 988        simpl in *; intros; subst; simpl in *; try (repeat (rule_helper_tactic' || subst)); subst; simpl in *.
 989        destruct case_nd_id0. apply nd_id0.
 990        destruct case_nd_id1. apply nd_rule. destruct p. apply RBrak.
 991        destruct case_nd_weak. apply nd_weak.
 992
 993        destruct case_nd_copy.
 994          (*
 995          destruct c; try destruct o; simpl in *; try rule_helper_tactic'; try destruct p; try rule_helper_tactic'.
 996          inversion H0; subst.
 997          simpl.*)
 998          idtac.
 999          clear H0.
1000          admit.
1001
1002        destruct case_nd_prod.
1003          eapply nd_prod.
1004          apply (append_brak _ _ lpf).
1005          apply (append_brak _ _ rpf).
1006
1007        destruct case_nd_comp.
1008          apply append_brak in bot.
1009          apply (nd_comp top bot).
1010
1011        destruct case_nd_cancell.
1012          eapply nd_comp; [ apply nd_cancell | idtac ].
1013          apply append_brak_to_id.
1014
1015        destruct case_nd_cancelr.
1016          eapply nd_comp; [ apply nd_cancelr | idtac ].
1017          apply append_brak_to_id.
1018
1019        destruct case_nd_llecnac.
1020          eapply nd_comp; [ idtac | apply nd_llecnac ].
1021          apply append_brak_to_id.
1022
1023        destruct case_nd_rlecnac.
1024          eapply nd_comp; [ idtac | apply nd_rlecnac ].
1025          apply append_brak_to_id.
1026
1027        destruct case_nd_assoc.
1028          eapply nd_comp; [ apply nd_assoc | idtac ].
1029          repeat rewrite fixit.
1030          apply append_brak_to_id.
1031
1032        destruct case_nd_cossa.
1033          eapply nd_comp; [ idtac | apply nd_cossa ].
1034          repeat rewrite fixit.
1035          apply append_brak_to_id.
1036
1037        destruct case_nd_rule
1038
1039
1040
1041     Defined.
1042
1043   Definition append_brak {h c} : forall
1044       pf:@ND_FC V
1045         (fixify Γ ((⟨n, Σ₁ ⟩) :: past)                       h )
1046         c,
1047       @ND_FC V
1048         (fixify Γ                past  (EscBrak_Functor_Fobj h))
1049         c.
1050     admit.
1051     Defined.
1052 *)
1053 *)
1054 End HaskProofCategory.