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