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