src/HaskProofCategory.v

   1 (*********************************************************************************************************************************)
   2 (* HaskProofCategory:                                                                                                            *)
   3 (*                                                                                                                               *)
   4 (*    Natural Deduction proofs of the well-typedness of a Haskell term form a category                                           *)
   5 (*                                                                                                                               *)
   6 (*********************************************************************************************************************************)
   7
   8 Generalizable All Variables.
   9 Require Import Preamble.
  10 Require Import General.
  11 Require Import NaturalDeduction.
  12 Require Import Coq.Strings.String.
  13 Require Import Coq.Lists.List.
  14
  15 Require Import HaskKinds.
  16 Require Import HaskCoreTypes.
  17 Require Import HaskLiteralsAndTyCons.
  18 Require Import HaskStrongTypes.
  19 Require Import HaskProof.
  20 Require Import NaturalDeduction.
  21 Require Import NaturalDeductionCategory.
  22
  23 Require Import Algebras_ch4.
  24 Require Import Categories_ch1_3.
  25 Require Import Functors_ch1_4.
  26 Require Import Isomorphisms_ch1_5.
  27 Require Import ProductCategories_ch1_6_1.
  28 Require Import OppositeCategories_ch1_6_2.
  29 Require Import Enrichment_ch2_8.
  30 Require Import Subcategories_ch7_1.
  31 Require Import NaturalTransformations_ch7_4.
  32 Require Import NaturalIsomorphisms_ch7_5.
  33 Require Import MonoidalCategories_ch7_8.
  34 Require Import Coherence_ch7_8.
  35
  36 Require Import HaskStrongTypes.
  37 Require Import HaskStrong.
  38 Require Import HaskProof.
  39 Require Import HaskStrongToProof.
  40 Require Import HaskProofToStrong.
  41 Require Import ProgrammingLanguage.
  42
  43 Section HaskProofCategory.
  44
  45   Definition unitType {Γ} : RawHaskType Γ ★.
  46     admit.
  47     Defined.
  48
  49   Definition brakifyType {Γ} (lt:LeveledHaskType Γ ★) : LeveledHaskType (★ ::Γ) ★ :=
  50     match lt with
  51       t @@ l => HaskBrak (FreshHaskTyVar ★) (weakT t) @@ weakL l
  52     end.
  53
  54   Definition brakify (j:Judg) : Judg :=
  55     match j with
  56       Γ > Δ > Σ |- τ =>
  57         (★ ::Γ) > weakCE Δ > mapOptionTree brakifyType Σ |- mapOptionTree brakifyType τ
  58     end.
  59
  60   (* Rules allowed in PCF; i.e. rules we know how to turn into GArrows *)
  61   Section RulePCF.
  62
  63     Context {Γ:TypeEnv}{Δ:CoercionEnv Γ}.
  64
  65     (* Rule_PCF consists of the rules allowed in flat PCF: everything except
  66      * AppT, AbsT, AppC, AbsC, Cast, Global, and some Case statements *)
  67     Inductive Rule_PCF : forall {h}{c}, Rule h c -> Prop :=
  68     | PCF_RURule           : ∀ h c r            ,  Rule_PCF (RURule Γ Δ  h c r)
  69     | PCF_RLit             : ∀ Γ Δ Σ τ          ,  Rule_PCF (RLit Γ Δ Σ τ  )
  70     | PCF_RNote            : ∀ Σ τ l n          ,  Rule_PCF (RNote Γ Δ Σ τ l n)
  71     | PCF_RVar             : ∀ σ               l,  Rule_PCF (RVar Γ Δ  σ         l)
  72     | PCF_RLam             : ∀ Σ tx te    q     ,  Rule_PCF (RLam Γ Δ  Σ tx te      q )
  73     | PCF_RApp             : ∀ Σ tx te   p     l,  Rule_PCF (RApp Γ Δ  Σ tx te   p l)
  74     | PCF_RLet             : ∀ Σ σ₁ σ₂   p     l,  Rule_PCF (RLet Γ Δ  Σ σ₁ σ₂   p l)
  75     | PCF_RBindingGroup    : ∀ q a b c d e      ,  Rule_PCF (RBindingGroup q a b c d e)
  76     | PCF_RCase            : ∀ T κlen κ θ l x   ,  Rule_PCF (RCase Γ Δ T κlen κ θ l x)   (* FIXME: only for boolean and int *)
  77     | Flat_REmptyGroup     : ∀ q a              ,  Rule_PCF (REmptyGroup q a)
  78     | Flat_RLetRec         : ∀ Γ Δ Σ₁ τ₁ τ₂ lev ,  Rule_PCF (RLetRec Γ Δ Σ₁ τ₁ τ₂ lev).
  79
  80     (* "RulePCF n" is the type of rules permitted in PCF with n-level deep nesting (so, "RulePCF 0" is flat PCF) *)
  81     Inductive RulePCF : nat -> Tree ??Judg -> Tree ??Judg -> Type :=
  82
  83     (* any proof using only PCF rules is an n-bounded proof for any n>0 *)
  84     | pcf_flat : forall n h c (r:Rule h c), Rule_PCF  r  -> RulePCF n h c
  85
  86     (* any n-bounded proof may be used as an (n+1)-bounded proof by prepending Esc and appending Brak *)
  87     | pfc_nest : forall n h c, ND (RulePCF n) h c    -> RulePCF (S n) (mapOptionTree brakify h) (mapOptionTree brakify c)
  88     .
  89   End RulePCF.
  90
  91   Section RuleSystemFC.
  92
  93     Context {Γ:TypeEnv}{Δ:CoercionEnv Γ}.
  94
  95     (* "RuleSystemFCa n" is the type of rules permitted in SystemFC^\alpha with n-level-deep nesting
  96      * in a fixed Γ,Δ context.  This is a subcategory of the "complete" SystemFCa, but it's enough to
  97      * do the flattening transformation *)
  98     Inductive RuleSystemFCa : nat -> Tree ??Judg -> Tree ??Judg -> Type :=
  99     | sfc_flat : forall n h c   (r:Rule h c), Rule_Flat r -> RuleSystemFCa    n  h c
 100     | sfc_nest : forall n h c,  ND (@RulePCF Γ Δ n) h c  -> RuleSystemFCa (S n) h c
 101     .
 102
 103     Context (ndr_systemfca:forall n, @ND_Relation _ (RuleSystemFCa n)).
 104
 105     Hint Constructors Rule_Flat.
 106
 107     Definition SystemFC_SC n : @SequentCalculus _ (RuleSystemFCa n) _ (mkJudg Γ Δ).
 108       apply Build_SequentCalculus.
 109       intro a.
 110       induction a.
 111       destruct a.
 112       apply nd_rule.
 113       destruct l.
 114       apply sfc_flat with (r:=RVar _ _ _ _).
 115       auto.
 116       apply nd_rule.
 117       apply sfc_flat with (r:=REmptyGroup _ _).
 118       auto.
 119       eapply nd_comp; [ apply nd_llecnac | idtac ].
 120       eapply nd_comp; [ eapply nd_prod | idtac ].
 121       apply IHa1.
 122       apply IHa2.
 123       apply nd_rule.
 124       apply sfc_flat with (r:=RBindingGroup _ _ _ _ _ _ ).
 125       auto.
 126       Defined.
 127
 128     Existing Instance SystemFC_SC.
 129
 130     Lemma systemfc_cut n : ∀a b c,
 131            ND (RuleSystemFCa n) ([Γ > Δ > a |- b],, [Γ > Δ > b |- c]) [Γ > Δ > a |- c].
 132       intros.
 133       admit.
 134       Defined.
 135
 136     Lemma systemfc_cutrule n
 137       : @CutRule _ (RuleSystemFCa n) _ (mkJudg Γ Δ) (ndr_systemfca n) (SystemFC_SC n).
 138       apply Build_CutRule with (nd_cut:=systemfc_cut n).
 139       admit.
 140       admit.
 141       admit.
 142       Defined.
 143
 144     Definition systemfc_left n a b c : ND (RuleSystemFCa n) [Γ > Δ > b |- c] [Γ > Δ > a,, b |- a,, c].
 145       eapply nd_comp; [ apply nd_llecnac | idtac ].
 146       eapply nd_comp; [ eapply nd_prod | idtac ].
 147       Focus 3.
 148       apply nd_rule.
 149       apply sfc_flat with (r:=RBindingGroup _ _ _ _ _ _ ).
 150       auto.
 151       idtac.
 152       apply nd_seq_reflexive.
 153       apply nd_id.
 154       Defined.
 155
 156     Definition systemfc_right n a b c : ND (RuleSystemFCa n) [Γ > Δ > b |- c] [Γ > Δ > b,,a |- c,,a].
 157       eapply nd_comp; [ apply nd_rlecnac | idtac ].
 158       eapply nd_comp; [ eapply nd_prod | idtac ].
 159       apply nd_id.
 160       apply (nd_seq_reflexive a).
 161       apply nd_rule.
 162       apply sfc_flat with (r:=RBindingGroup _ _ _ _ _ _ ).
 163       auto.
 164       Defined.
 165
 166     Definition systemfc_expansion n
 167       : @SequentExpansion _ (RuleSystemFCa n) _ (mkJudg Γ Δ) (ndr_systemfca n) (SystemFC_SC n) (systemfc_cutrule n).
 168     Check  (@Build_SequentExpansion).
 169 apply (@Build_SequentExpansion _ _ _ _ (ndr_systemfca n)  _ _ (systemfc_left n) (systemfc_right n)).
 170       refine {| se_expand_left:=systemfc_left n
 171         ; se_expand_right:=systemfc_right n |}.
 172
 173
 174     (* 5.1.2 *)
 175     Instance SystemFCa n : @ProgrammingLanguage _ Judg (mkJudg Γ Δ) (RuleSystemFCa n) :=
 176     { pl_eqv                := ndr_systemfca n
 177     ; pl_tsr                := _ (*@TreeStructuralRules Judg Rule T sequent*)
 178     ; pl_sc                 := SystemFC_SC n
 179     ; pl_subst              := systemfc_cutrule n
 180     ; pl_sequent_join       := systemfc_expansion n
 181     }.
 182       apply Build_TreeStructuralRules; intros; unfold eqv; unfold hom; simpl.
 183       apply sfc_flat with (r:=RURule _ _ _ _ (RCossa _ a b c)); auto. apply Flat_RURule.
 184       apply sfc_flat with (r:=RURule _ _ _ _ (RAssoc _ a b c)); auto. apply Flat_RURule.
 185       apply sfc_flat with (r:=RURule _ _ _ _ (RCanL  _ a    )); auto. apply Flat_RURule.
 186       apply sfc_flat with (r:=RURule _ _ _ _ (RCanR  _ a    )); auto. apply Flat_RURule.
 187       apply sfc_flat with (r:=RURule _ _ _ _ (RuCanL _ a    )); auto. apply Flat_RURule.
 188       apply sfc_flat with (r:=RURule _ _ _ _ (RuCanR _ a    )); auto. apply Flat_RURule.
 189 Show Existentials.
 190
 191   Admitted.
 192
 193   End RuleSystemFC.
 194
 195   Context (ndr_pcf      :forall n Γ Δ, @ND_Relation _ (@RulePCF Γ Δ n)).
 196
 197   (* 5.1.3 *)
 198   Instance PCF n Γ Δ : @ProgrammingLanguage _ _ (mkJudg Γ Δ) (@RulePCF Γ Δ n) :=
 199   { pl_eqv                := _ (*@ND_Relation Judg Rule where "pf1 === pf2" := (@ndr_eqv _ _ pl_eqv _ _ pf1 pf2)*)
 200   ; pl_tsr                := _ (*@TreeStructuralRules Judg Rule T sequent*)
 201   ; pl_sc                 := _ (*@SequentCalculus Judg Rule _ sequent*)
 202   ; pl_subst              := _ (*@CutRule Judg Rule _ sequent pl_eqv pl_sc*)
 203   ; pl_sequent_join       := _ (*@SequentExpansion Judg Rule T sequent pl_eqv pl_sc pl_subst*)
 204   }.
 205   Admitted.
 206
 207
 208   Definition ReificationFunctor n : Functor (JudgmentsN n) (JudgmentsN (S n)) (mapOptionTree brakify).
 209     refine {| fmor := fun h c (f:h~~{JudgmentsN n}~~>c) => nd_rule (br_nest _ _ _ f) |}; intros; simpl.
 210     admit.
 211     admit.
 212     admit.
 213     Defined.
 214
 215   Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
 216     refine {| plsmme_pl := PCF n Γ Δ |}.
 217     admit.
 218     Defined.
 219
 220   Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
 221     refine {| plsmme_pl := SystemFCa n Γ Δ |}.
 222     admit.
 223     Defined.
 224
 225   Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
 226     admit.
 227     Defined.
 228
 229   (* 5.1.4 *)
 230   Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
 231     admit.
 232     (*  ... and the retraction exists *)
 233     Defined.
 234
 235   (* Any particular proof in HaskProof is only finitely large, so it uses only finitely many levels of nesting, so
 236    * it falls within (SystemFCa n) for some n.  This function calculates that "n" and performs the translation *)
 237   (*
 238   Definition HaskProof_to_SystemFCa :
 239     forall h c (pf:ND Rule h c),
 240       { n:nat & h ~~{JudgmentsL (SystemFCa_SMME n)}~~> c }.
 241       *)
 242
 243   (* for every n we have a functor from the category of (n+1)-bounded proofs to the category of n-bounded proofs *)
 244
 245
 246   Definition makeTree : Tree ??(LeveledHaskType Γ ★) -> HaskType Γ ★.
 247     admit.
 248     Defined.
 249
 250   Definition flattenType n (j:JudgmentsN n) : TypesN n.
 251     unfold eob_eob.
 252     unfold ob in j.
 253     refine (mapOptionTree _ j).
 254     clear j; intro j.
 255     destruct j as [ Γ' Δ' Σ τ ].
 256     assert (Γ'=Γ). admit.
 257     rewrite H in *.
 258     clear H Γ'.
 259     refine (_ @@ nil).
 260     refine (HaskBrak _ ( (makeTree Σ) ---> (makeTree τ) )); intros.
 261     admit.
 262     Defined.
 263
 264   Definition FlattenFunctor_fmor n :
 265     forall h c,
 266       (h~~{JudgmentsN n}~~>c) ->
 267       ((flattenType n h)~~{TypesN n}~~>(flattenType n c)).
 268     intros.
 269     unfold hom in *; simpl.
 270     unfold mon_i.
 271     unfold ehom.
 272     unfold TypesNmor.
 273
 274     admit.
 275     Defined.
 276
 277   Definition FlattenFunctor n : Functor (JudgmentsN n) (TypesN n) (flattenType n).
 278     refine {| fmor := FlattenFunctor_fmor n |}; intros.
 279     admit.
 280     admit.
 281     admit.
 282     Defined.
 283
 284   End RulePCF.
 285   Implicit Arguments Rule_PCF [ [h] [c] ].
 286   Implicit Arguments BoundedRule [ ].
 287
 288 *)
 289 (*
 290   Definition code2garrow0 {Γ}(ec t1 t2:RawHaskType Γ ★) : RawHaskType Γ ★.
 291     admit.
 292     Defined.
 293   Definition code2garrow Γ (ec t:RawHaskType Γ ★) :=
 294       match t with
 295 (*        | TApp ★ ★ (TApp _ ★ TArrow tx) t' => code2garrow0 ec tx       t'*)
 296         |                               _  => code2garrow0 ec unitType t
 297       end.
 298   Opaque code2garrow.
 299   Fixpoint typeMap {TV}{κ}(ty:@RawHaskType TV κ) : @RawHaskType TV κ :=
 300       match ty as TY in RawHaskType _ K return RawHaskType TV K with
 301         | TCode ec t        => code2garrow _ ec t
 302         | TApp _ _ t1 t2    => TApp (typeMap t1) (typeMap t2)
 303         | TAll _ f          => TAll _ (fun tv => typeMap (f tv))
 304         | TCoerc _ t1 t2 t3 => TCoerc (typeMap t1) (typeMap t2) (typeMap t3)
 305         | TVar   _ v        => TVar v
 306         | TArrow            => TArrow
 307         | TCon  tc          => TCon tc
 308         | TyFunApp  tf rhtl => (* FIXME *) TyFunApp tf rhtl
 309       end.
 310
 311   Definition typeMapL {Γ}(lht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★  :=
 312     match lht with
 313 (*      | t @@ nil       => (fun TV ite => typeMap (t TV ite)) @@ lev*)
 314       | t @@ lev => (fun TV ite => typeMap (t TV ite)) @@ lev
 315     end.
 316
 317   Definition coMap {Γ}(ck:HaskCoercionKind Γ) :=
 318     fun TV ite => match ck TV ite with
 319       | mkRawCoercionKind _ t1 t2 => mkRawCoercionKind _ (typeMap t1) (typeMap t2)
 320       end.
 321
 322   Definition flattenCoercion {Γ}{Δ}{ck}(hk:HaskCoercion Γ Δ ck) : HaskCoercion Γ (map coMap Δ) (coMap ck).
 323     admit.
 324     Defined.
 325
 326   Lemma update_typeMap Γ (lev:HaskLevel Γ) ξ v t
 327     : (typeMap ○ (update_ξ            ξ  lev ((⟨v, t ⟩)          :: nil)))
 328     = (           update_ξ (typeMap ○ ξ) lev ((⟨v, typeMap_ t ⟩) :: nil)).
 329     admit.
 330     Qed.
 331
 332   Lemma foo κ Γ σ τ : typeMap_ (substT σ τ) = substT(Γ:=Γ)(κ₁:=κ) (fun TV ite => typeMap ○ σ TV ite) τ.
 333     admit.
 334     Qed.
 335
 336   Lemma lit_lemma lit Γ : typeMap_ (literalType lit) = literalType(Γ:=Γ) lit.
 337     admit.
 338     Qed.
 339 *)
 340 (*
 341   Definition flatten : forall h c, Rule h c -> @ND Judg Rule (mapOptionTree flattenJudgment h) (mapOptionTree flattenJudgment c).
 342     intros h c r.
 343     refine (match r as R in Rule H C return ND Rule (mapOptionTree flattenJudgment H) (mapOptionTree flattenJudgment C) with
 344       | RURule  a b c d e             => let case_RURule := tt        in _
 345       | RNote   Γ Δ Σ τ l n           => let case_RNote := tt         in _
 346       | RLit    Γ Δ l     _           => let case_RLit := tt          in _
 347       | RVar    Γ Δ σ         p       => let case_RVar := tt          in _
 348       | RGlobal Γ Δ σ l wev           => let case_RGlobal := tt       in _
 349       | RLam    Γ Δ Σ tx te     x     => let case_RLam := tt          in _
 350       | RCast   Γ Δ Σ σ τ γ     x     => let case_RCast := tt         in _
 351       | RAbsT   Γ Δ Σ κ σ a           => let case_RAbsT := tt         in _
 352       | RAppT   Γ Δ Σ κ σ τ     y     => let case_RAppT := tt         in _
 353       | RAppCo  Γ Δ Σ κ σ₁ σ₂ γ σ l   => let case_RAppCo := tt        in _
 354       | RAbsCo  Γ Δ Σ κ σ  σ₁ σ₂  y   => let case_RAbsCo := tt        in _
 355       | RApp    Γ Δ Σ₁ Σ₂ tx te p     => let case_RApp := tt          in _
 356       | RLet    Γ Δ Σ₁ Σ₂ σ₁ σ₂ p     => let case_RLet := tt          in _
 357       | RBindingGroup Γ p lri m x q   => let case_RBindingGroup := tt in _
 358       | REmptyGroup _ _               => let case_REmptyGroup := tt   in _
 359       | RBrak   Σ a b c n m           => let case_RBrak := tt         in _
 360       | REsc    Σ a b c n m           => let case_REsc := tt          in _
 361       | RCase   Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
 362       | RLetRec Γ Δ lri x y t         => let case_RLetRec := tt       in _
 363       end).
 364
 365       destruct case_RURule.
 366         admit.
 367
 368       destruct case_RBrak.
 369         simpl.
 370         admit.
 371
 372       destruct case_REsc.
 373         simpl.
 374         admit.
 375
 376       destruct case_RNote.
 377         eapply nd_rule.  simpl.  apply RNote; auto.
 378
 379       destruct case_RLit.
 380         simpl.
 381
 382       set (@RNote Γ Δ Σ τ l) as q.
 383     Defined.
 384
 385   Definition flatten' {h}{c} (pf:ND Rule h c) := nd_map' flattenJudgment flatten pf.
 386
 387
 388     @ND Judgment1 Rule1 (mapOptionTree f h) (mapOptionTree f c).
 389
 390   refine (fix flatten : forall Γ Δ Σ τ
 391     (pf:SCND Rule [] [Γ > Δ >                       Σ |-                       τ ]) :
 392     SCND Rule [] [Γ > Δ > mapOptionTree typeMap Σ |- mapOptionTree typeMap τ ] :=
 393     match pf as SCND _ _
 394     | scnd_comp   : forall ht ct c , SCND ht ct -> Rule ct [c] -> SCND ht [c]
 395   | scnd_weak   : forall c       , SCND c  []
 396   | scnd_leaf   : forall ht c    , SCND ht [c]  -> SCND ht [c]
 397   | scnd_branch : forall ht c1 c2, SCND ht c1 -> SCND ht c2 -> SCND ht (c1,,c2)
 398   Expr Γ Δ ξ τ -> Expr Γ (map coMap Δ) (typeMap ○ ξ) (typeMap τ).
 399 *)
 400
 401 (*
 402   Lemma all_lemma Γ κ σ l :
 403 (@typeMap (κ :: Γ)
 404            (@HaskTApp (κ :: Γ) κ (@weakF Γ κ ★ σ) (@FreshHaskTyVar Γ κ) @@
 405             @weakL Γ κ l)) = (@typeMap Γ (@HaskTAll Γ κ σ @@  l)).
 406 *)
 407
 408 (*
 409   Definition flatten : forall Γ Δ ξ τ,  Expr Γ Δ ξ τ -> Expr Γ (map coMap Δ) (typeMap ○ ξ) (typeMap τ).
 410   refine (fix flatten Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') : Expr Γ' (map coMap Δ') (typeMap ○ ξ') (typeMap τ') :=
 411     match exp as E in Expr G D X T return Expr G (map coMap D) (typeMap ○ X) (typeMap T) with
 412     | EGlobal  Γ Δ ξ t wev                          => EGlobal _ _ _ _  wev
 413     | EVar     Γ Δ ξ ev                             => EVar    _ _ _    ev
 414     | ELit     Γ Δ ξ lit lev                        => let case_ELit    := tt in _
 415     | EApp     Γ Δ ξ t1 t2 lev e1 e2                => EApp _ _ _ _ _ _ (flatten _ _ _ _ e1) (flatten _ _ _ _ e2)
 416     | ELam     Γ Δ ξ t1 t2 lev v    e               => let case_ELam := tt in _
 417     | ELet     Γ Δ ξ tv t  l ev elet ebody          => let case_ELet    := tt in _
 418     | ELetRec  Γ Δ ξ lev t tree branches ebody      => let case_ELetRec := tt in _
 419     | ECast    Γ Δ ξ t1 t2 γ lev e                  => let case_ECast   := tt in _
 420     | ENote    Γ Δ ξ t n e                          => ENote _ _ _ _ n (flatten _ _ _ _ e)
 421     | ETyLam   Γ Δ ξ κ σ l e                        => let case_ETyLam  := tt in _
 422     | ECoLam   Γ Δ κ σ σ₁ σ₂ ξ l             e      => let case_ECoLam  := tt in _
 423     | ECoApp   Γ Δ κ σ₁ σ₂ γ σ ξ l e                => let case_ECoApp  := tt in _
 424     | ETyApp   Γ Δ κ σ τ ξ  l    e                  => let case_ETyApp  := tt in _
 425     | ECase    Γ Δ ξ l tc tbranches atypes e alts'  => let case_ECase   := tt in _
 426
 427     | EEsc     Γ Δ ξ ec t lev e                     => let case_EEsc    := tt in _
 428     | EBrak    Γ Δ ξ ec t lev e                     => let case_EBrak   := tt in _
 429     end); clear exp ξ' τ' Γ' Δ'.
 430
 431   destruct case_ELit.
 432     simpl.
 433     rewrite lit_lemma.
 434     apply ELit.
 435
 436   destruct case_ELam.
 437     set (flatten _ _ _ _ e) as q.
 438     rewrite update_typeMap in q.
 439     apply (@ELam _ _ _ _ _ _ _ _ v q).
 440
 441   destruct case_ELet.
 442     set (flatten _ _ _ _ ebody) as ebody'.
 443     set (flatten _ _ _ _ elet)  as elet'.
 444     rewrite update_typeMap in ebody'.
 445     apply (@ELet _ _ _ _ _ _ _ _ _ elet' ebody').
 446
 447   destruct case_EEsc.
 448     admit.
 449   destruct case_EBrak.
 450     admit.
 451
 452   destruct case_ECast.
 453     apply flatten in e.
 454     eapply ECast in e.
 455     apply e.
 456     apply flattenCoercion in γ.
 457     apply γ.
 458
 459   destruct case_ETyApp.
 460     apply flatten in e.
 461     simpl in e.
 462     unfold HaskTAll in e.
 463     unfold typeMap_ in e.
 464     simpl in e.
 465     eapply ETyApp in e.
 466     rewrite <- foo in e.
 467     apply e.
 468
 469   destruct case_ECoLam.
 470     apply flatten in e.
 471     simpl in e.
 472     set (@ECoLam _ _ _ _ _ _ _ _ _ _ e) as x.
 473     simpl in x.
 474     simpl.
 475     unfold typeMap_.
 476     simpl.
 477     apply x.
 478
 479   destruct case_ECoApp.
 480     simpl.
 481     apply flatten in e.
 482     eapply ECoApp.
 483     unfold mkHaskCoercionKind in *.
 484     simpl in γ.
 485     apply flattenCoercion in γ.
 486     unfold coMap in γ at 2.
 487     apply γ.
 488     apply e.
 489
 490   destruct case_ETyLam.
 491     apply flatten in e.
 492     set (@ETyLam Unique _ Γ (map coMap Δ) (typeMap ○ ξ) κ (fun ite x => typeMap (σ x ite))) as e'.
 493     unfold HaskTAll in *.
 494     unfold typeMap_ in *.
 495     rewrite <- foo in e'.
 496     unfold typeMap in e'.
 497     simpl in e'.
 498     apply ETyLam.
 499
 500 Set Printing Implicit.
 501 idtac.
 502 idtac.
 503
 504
 505     admit.
 506
 507   destruct case_ECase.
 508     admit.
 509
 510   destruct case_ELetRec.
 511     admit.
 512     Defined.
 513
 514   (* This proof will work for any dynamic semantics you like, so
 515    * long as those semantics are an ND_Relation (associativity,
 516    * neutrality, etc) *)
 517   Context (dynamic_semantics   : @ND_Relation _ Rule).
 518
 519   Section SystemFC_Category.
 520
 521     Context {Γ:TypeEnv}
 522             {Δ:CoercionEnv Γ}.
 523
 524     Definition Context := Tree ??(LeveledHaskType Γ ★).
 525
 526     Notation "a |= b" := (Γ >> Δ > a |- b).
 527
 528     (*
 529        SystemFCa
 530        PCF
 531        SystemFCa_two_level
 532        SystemFCa_initial_GArrow
 533      *)
 534
 535     Context (nd_eqv:@ND_Relation _ (@URule Γ Δ)).
 536     Check (@ProgrammingLanguage).
 537     Context (PL:@ProgrammingLanguage (LeveledHaskType Γ ★)
 538       (fun x y => match x with x1|=x2 => match y with y1|=y2 => @URule Γ Δ)).
 539     Definition JudgmentsFC := @Judgments_Category_CartesianCat _ (@URule Γ Δ) nd_eqv.
 540     Definition TypesFC     := @TypesL                          _ (@URule Γ Δ) nd_eqv.
 541
 542     (* The full subcategory of SystemFC(Γ,Δ) consisting only of judgments involving types at a fixed level.  Note that
 543      * code types are still permitted! *)
 544     Section SingleLevel.
 545       Context (lev:HaskLevel Γ).
 546
 547       Inductive ContextAtLevel : Context -> Prop :=
 548         | contextAtLevel_nil    :               ContextAtLevel []
 549         | contextAtLevel_leaf   : forall τ,     ContextAtLevel [τ @@ lev]
 550         | contextAtLevel_branch : forall b1 b2, ContextAtLevel b1 -> ContextAtLevel b2 -> ContextAtLevel (b1,,b2).
 551
 552       Inductive JudgmentsAtLevel : JudgmentsFC -> Prop :=
 553         | judgmentsAtLevel_nil    : JudgmentsAtLevel []
 554         | judgmentsAtLevel_leaf   : forall c1 c2, ContextAtLevel c1   -> ContextAtLevel c2   -> JudgmentsAtLevel [c1 |= c2]
 555         | judgmentsAtLevel_branch : forall j1 j2, JudgmentsAtLevel j1 -> JudgmentsAtLevel j2 -> JudgmentsAtLevel (j1,,j2).
 556
 557       Definition JudgmentsFCAtLevel := FullSubcategory JudgmentsFC JudgmentsAtLevel.
 558       Definition TypesFCAtLevel     := FullSubcategory TypesFC     ContextAtLevel.
 559     End SingleLevel.
 560
 561   End SystemFC_Category.
 562
 563   Implicit Arguments TypesFC [ ].
 564
 565 (*
 566     Section EscBrak_Functor.
 567       Context
 568         (past:@Past V)
 569         (n:V)
 570         (Σ₁:Tree ??(@LeveledHaskType V)).
 571
 572       Definition EscBrak_Functor_Fobj
 573         : SystemFC_Cat_Flat ((Σ₁,n)::past) -> SystemFC_Cat past
 574         := mapOptionTree (fun q:Tree ??(@CoreType V) * Tree ??(@CoreType V) =>
 575           let (a,s):=q in (Σ₁,,(``a)^^^n,[`<[ n |- encodeTypeTree_flat s ]>])).
 576
 577       Definition append_brak
 578       : forall {c}, ND_ML
 579           (mapOptionTree (ob2judgment_flat ((⟨Σ₁,n⟩) :: past))                        c )
 580           (mapOptionTree (ob2judgment                   past )  (EscBrak_Functor_Fobj c)).
 581         intros.
 582         unfold ND_ML.
 583         unfold EscBrak_Functor_Fobj.
 584         rewrite mapOptionTree_comp.
 585         simpl in *.
 586         apply nd_replicate.
 587         intro o; destruct o.
 588         apply nd_rule.
 589         apply MLRBrak.
 590         Defined.
 591
 592       Definition prepend_esc
 593       : forall {h}, ND_ML
 594           (mapOptionTree (ob2judgment                  past )  (EscBrak_Functor_Fobj h))
 595           (mapOptionTree (ob2judgment_flat ((⟨Σ₁,n⟩) :: past))                        h ).
 596         intros.
 597         unfold ND_ML.
 598         unfold EscBrak_Functor_Fobj.
 599         rewrite mapOptionTree_comp.
 600         simpl in *.
 601         apply nd_replicate.
 602         intro o; destruct o.
 603         apply nd_rule.
 604         apply MLREsc.
 605         Defined.
 606
 607       Definition EscBrak_Functor_Fmor
 608         : forall a b (f:a~~{SystemFC_Cat_Flat ((Σ₁,n)::past)}~~>b),
 609           (EscBrak_Functor_Fobj a)~~{SystemFC_Cat past}~~>(EscBrak_Functor_Fobj b).
 610         intros.
 611         eapply nd_comp.
 612         apply prepend_esc.
 613         eapply nd_comp.
 614         eapply Flat_to_ML.
 615         apply f.
 616         apply append_brak.
 617         Defined.
 618
 619       Lemma esc_then_brak_is_id : forall a,
 620        ndr_eqv(ND_Relation:=ml_dynamic_semantics V) (nd_comp prepend_esc append_brak)
 621          (nd_id (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj a))).
 622          admit.
 623          Qed.
 624
 625       Lemma brak_then_esc_is_id : forall a,
 626        ndr_eqv(ND_Relation:=ml_dynamic_semantics V) (nd_comp append_brak prepend_esc)
 627          (nd_id (mapOptionTree (ob2judgment_flat (((Σ₁,n)::past))) a)).
 628          admit.
 629          Qed.
 630
 631       Instance EscBrak_Functor
 632         : Functor (SystemFC_Cat_Flat ((Σ₁,n)::past)) (SystemFC_Cat past) EscBrak_Functor_Fobj :=
 633         { fmor := fun a b f => EscBrak_Functor_Fmor a b f }.
 634         intros; unfold EscBrak_Functor_Fmor; simpl in *.
 635           apply ndr_comp_respects; try reflexivity.
 636           apply ndr_comp_respects; try reflexivity.
 637           auto.
 638         intros; unfold EscBrak_Functor_Fmor; simpl in *.
 639           set (@ndr_comp_left_identity _ _ (ml_dynamic_semantics V)) as q.
 640           setoid_rewrite q.
 641           apply esc_then_brak_is_id.
 642         intros; unfold EscBrak_Functor_Fmor; simpl in *.
 643           set (@ndr_comp_associativity _ _ (ml_dynamic_semantics V)) as q.
 644           repeat setoid_rewrite q.
 645           apply ndr_comp_respects; try reflexivity.
 646           apply ndr_comp_respects; try reflexivity.
 647           repeat setoid_rewrite <- q.
 648           apply ndr_comp_respects; try reflexivity.
 649           setoid_rewrite brak_then_esc_is_id.
 650           clear q.
 651           set (@ndr_comp_left_identity _ _ (fc_dynamic_semantics V)) as q.
 652           setoid_rewrite q.
 653           reflexivity.
 654         Defined.
 655
 656     End EscBrak_Functor.
 657
 658
 659
 660   Ltac rule_helper_tactic' :=
 661     match goal with
 662     | [ H : ?A = ?A |- _ ] => clear H
 663     | [ H : [?A] = [] |- _ ] => inversion H; clear H
 664     | [ H : [] = [?A] |- _ ] => inversion H; clear H
 665     | [ H : ?A,,?B = [] |- _ ] => inversion H; clear H
 666     | [ H : ?A,,?B = [?Y] |- _ ] => inversion H; clear H
 667     | [ H: ?A :: ?B = ?B |- _ ] => apply symmetry in H; apply list_cannot_be_longer_than_itself in H; destruct H
 668     | [ H: ?B = ?A :: ?B |- _ ] => apply list_cannot_be_longer_than_itself in H; destruct H
 669     | [ H: ?A :: ?C :: ?B = ?B |- _ ] => apply symmetry in H; apply list_cannot_be_longer_than_itself' in H; destruct H
 670     | [ H: ?B = ?A :: ?C :: ?B |- _ ] => apply list_cannot_be_longer_than_itself' in H; destruct H
 671 (*  | [ H : Sequent T |- _ ] => destruct H *)
 672 (*  | [ H : ?D = levelize ?C (?A |= ?B) |- _ ] => inversion H; clear H*)
 673     | [ H : [?A] = [?B] |- _ ] => inversion H; clear H
 674     | [ H : [] = mapOptionTree ?B ?C |- _ ] => apply mapOptionTree_on_nil in H; subst
 675     | [ H : [?A] = mapOptionTree ?B ?C |- _ ] => destruct C as [C|]; simpl in H; [ | inversion H ]; destruct C; simpl in H; simpl
 676     | [ H : ?A,,?B = mapOptionTree ?C ?D |- _ ] => destruct D as [D|] ; [destruct D|idtac]; simpl in H; inversion H
 677     end.
 678
 679   Lemma fixit : forall a b f c1 c2, (@mapOptionTree a b f c1),,(mapOptionTree f c2) = mapOptionTree f (c1,,c2).
 680     admit.
 681     Defined.
 682
 683   Lemma grak a b f c : @mapOptionTree a b f c = [] -> [] = c.
 684     admit.
 685     Qed.
 686
 687   Definition append_brak_to_id : forall {c},
 688   @ND_FC V
 689       (mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past))  c )
 690       (mapOptionTree (ob2judgment past)  (EscBrak_Functor_Fobj c)).
 691   admit.
 692   Defined.
 693
 694   Definition append_brak : forall {h c}
 695     (pf:@ND_FC V
 696       h
 697       (mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past))  c )),
 698     @ND_FC V
 699        h
 700       (mapOptionTree (ob2judgment past)  (EscBrak_Functor_Fobj c)).
 701
 702       refine (fix append_brak h c nd {struct nd} :=
 703        ((match nd
 704             as nd'
 705             in @ND _ _ H C
 706             return
 707             (H=h) ->
 708             (C=mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past)) c) ->
 709             ND_FC h (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj c))
 710           with
 711           | nd_id0                     => let case_nd_id0     := tt in _
 712           | nd_id1     h               => let case_nd_id1     := tt in _
 713           | nd_weak    h               => let case_nd_weak    := tt in _
 714           | nd_copy    h               => let case_nd_copy    := tt in _
 715           | nd_prod    _ _ _ _ lpf rpf => let case_nd_prod    := tt in _
 716           | nd_comp    _ _ _   top bot => let case_nd_comp    := tt in _
 717           | nd_rule    _ _     rule    => let case_nd_rule    := tt in _
 718           | nd_cancell _               => let case_nd_cancell := tt in _
 719           | nd_cancelr _               => let case_nd_cancelr := tt in _
 720           | nd_llecnac _               => let case_nd_llecnac := tt in _
 721           | nd_rlecnac _               => let case_nd_rlecnac := tt in _
 722           | nd_assoc   _ _ _           => let case_nd_assoc   := tt in _
 723           | nd_cossa   _ _ _           => let case_nd_cossa   := tt in _
 724         end) (refl_equal _) (refl_equal _)
 725        ));
 726        simpl in *; intros; subst; simpl in *; try (repeat (rule_helper_tactic' || subst)); subst; simpl in *.
 727        destruct case_nd_id0. apply nd_id0.
 728        destruct case_nd_id1. apply nd_rule. destruct p. apply RBrak.
 729        destruct case_nd_weak. apply nd_weak.
 730
 731        destruct case_nd_copy.
 732          (*
 733          destruct c; try destruct o; simpl in *; try rule_helper_tactic'; try destruct p; try rule_helper_tactic'.
 734          inversion H0; subst.
 735          simpl.*)
 736          idtac.
 737          clear H0.
 738          admit.
 739
 740        destruct case_nd_prod.
 741          eapply nd_prod.
 742          apply (append_brak _ _ lpf).
 743          apply (append_brak _ _ rpf).
 744
 745        destruct case_nd_comp.
 746          apply append_brak in bot.
 747          apply (nd_comp top bot).
 748
 749        destruct case_nd_cancell.
 750          eapply nd_comp; [ apply nd_cancell | idtac ].
 751          apply append_brak_to_id.
 752
 753        destruct case_nd_cancelr.
 754          eapply nd_comp; [ apply nd_cancelr | idtac ].
 755          apply append_brak_to_id.
 756
 757        destruct case_nd_llecnac.
 758          eapply nd_comp; [ idtac | apply nd_llecnac ].
 759          apply append_brak_to_id.
 760
 761        destruct case_nd_rlecnac.
 762          eapply nd_comp; [ idtac | apply nd_rlecnac ].
 763          apply append_brak_to_id.
 764
 765        destruct case_nd_assoc.
 766          eapply nd_comp; [ apply nd_assoc | idtac ].
 767          repeat rewrite fixit.
 768          apply append_brak_to_id.
 769
 770        destruct case_nd_cossa.
 771          eapply nd_comp; [ idtac | apply nd_cossa ].
 772          repeat rewrite fixit.
 773          apply append_brak_to_id.
 774
 775        destruct case_nd_rule
 776
 777
 778
 779     Defined.
 780
 781   Definition append_brak {h c} : forall
 782       pf:@ND_FC V
 783         (fixify Γ ((⟨n, Σ₁ ⟩) :: past)                       h )
 784         c,
 785       @ND_FC V
 786         (fixify Γ                past  (EscBrak_Functor_Fobj h))
 787         c.
 788     admit.
 789     Defined.
 790 *)
 791 *)
 792 End HaskProofCategory.