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   (* "RuleSystemFCa n" is the type of rules permitted in SystemFC^\alpha with n-level-deep nesting
  92    * (so, "RuleSystemFCa 0" is damn close to System FC) *)
  93   Inductive RuleSystemFCa : nat -> Tree ??Judg -> Tree ??Judg -> Type :=
  94   | sfc_flat : forall n h c     (r:Rule h c), Rule_Flat r -> RuleSystemFCa    n  h c
  95   | sfc_nest : forall n h c Γ Δ, ND (@RulePCF Γ Δ n) h c  -> RuleSystemFCa (S n) h c
  96   .
  97
  98   Context (ndr_pcf      :forall n Γ Δ, @ND_Relation _ (@RulePCF Γ Δ n)).
  99   Context (ndr_systemfca:forall n, @ND_Relation _ (RuleSystemFCa n)).
 100
 101   (* 5.1.3 *)
 102   Instance PCF n Γ Δ : @ProgrammingLanguage _ _ (mkJudg Γ Δ) (@RulePCF Γ Δ n) :=
 103   { pl_eqv                := _ (*@ND_Relation Judg Rule where "pf1 === pf2" := (@ndr_eqv _ _ pl_eqv _ _ pf1 pf2)*)
 104   ; pl_tsr                := _ (*@TreeStructuralRules Judg Rule T sequent*)
 105   ; pl_sc                 := _ (*@SequentCalculus Judg Rule _ sequent*)
 106   ; pl_subst              := _ (*@CutRule Judg Rule _ sequent pl_eqv pl_sc*)
 107   ; pl_sequent_join       := _ (*@SequentExpansion Judg Rule T sequent pl_eqv pl_sc pl_subst*)
 108   }.
 109   Admitted.
 110
 111   (* 5.1.2 *)
 112   Instance SystemFCa n Γ Δ : @ProgrammingLanguage _ _ (mkJudg Γ Δ) (RuleSystemFCa n) :=
 113   { pl_eqv                := _ (*@ND_Relation Judg Rule where "pf1 === pf2" := (@ndr_eqv _ _ pl_eqv _ _ pf1 pf2)*)
 114   ; pl_tsr                := _ (*@TreeStructuralRules Judg Rule T sequent*)
 115   ; pl_sc                 := _ (*@SequentCalculus Judg Rule _ sequent*)
 116   ; pl_subst              := _ (*@CutRule Judg Rule _ sequent pl_eqv pl_sc*)
 117   ; pl_sequent_join       := _ (*@SequentExpansion Judg Rule T sequent pl_eqv pl_sc pl_subst*)
 118   }.
 119   Admitted.
 120
 121   Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
 122     refine {| plsmme_pl := PCF n Γ Δ |}.
 123     admit.
 124     Defined.
 125
 126   Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
 127     refine {| plsmme_pl := SystemFCa n Γ Δ |}.
 128     admit.
 129     Defined.
 130
 131   (* 5.1.4 *)
 132   Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
 133     admit.
 134     Defined.
 135   (*  ... and the retraction exists *)
 136
 137   (* Any particular proof in HaskProof is only finitely large, so it uses only finitely many levels of nesting, so
 138    * it falls within (SystemFCa n) for some n.  This function calculates that "n" and performs the translation *)
 139   (*Definition HaskProof_to_SystemFCa :
 140     forall h c (pf:ND Judg h c),
 141       { n:nat & h ~~{JudgmentsL SystemFCa_SMME n *)
 142
 143   (* for every n we have a functor from the category of (n+1)-bounded proofs to the category of n-bounded proofs *)
 144     (*
 145   Definition ReificationFunctor n : Functor (JudgmentsN n) (JudgmentsN (S n)) (mapOptionTree brakify).
 146     refine {| fmor := fun h c (f:h~~{JudgmentsN n}~~>c) => nd_rule (br_nest _ _ _ f) |}; intros; simpl.
 147     admit.
 148     admit.
 149     admit.
 150     Defined.
 151
 152   Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
 153     admit.
 154     Defined.
 155
 156   Definition makeTree : Tree ??(LeveledHaskType Γ ★) -> HaskType Γ ★.
 157     admit.
 158     Defined.
 159
 160   Definition flattenType n (j:JudgmentsN n) : TypesN n.
 161     unfold eob_eob.
 162     unfold ob in j.
 163     refine (mapOptionTree _ j).
 164     clear j; intro j.
 165     destruct j as [ Γ' Δ' Σ τ ].
 166     assert (Γ'=Γ). admit.
 167     rewrite H in *.
 168     clear H Γ'.
 169     refine (_ @@ nil).
 170     refine (HaskBrak _ ( (makeTree Σ) ---> (makeTree τ) )); intros.
 171     admit.
 172     Defined.
 173
 174   Definition FlattenFunctor_fmor n :
 175     forall h c,
 176       (h~~{JudgmentsN n}~~>c) ->
 177       ((flattenType n h)~~{TypesN n}~~>(flattenType n c)).
 178     intros.
 179     unfold hom in *; simpl.
 180     unfold mon_i.
 181     unfold ehom.
 182     unfold TypesNmor.
 183
 184     admit.
 185     Defined.
 186
 187   Definition FlattenFunctor n : Functor (JudgmentsN n) (TypesN n) (flattenType n).
 188     refine {| fmor := FlattenFunctor_fmor n |}; intros.
 189     admit.
 190     admit.
 191     admit.
 192     Defined.
 193
 194   End RulePCF.
 195   Implicit Arguments Rule_PCF [ [h] [c] ].
 196   Implicit Arguments BoundedRule [ ].
 197
 198 *)
 199 (*
 200   Definition code2garrow0 {Γ}(ec t1 t2:RawHaskType Γ ★) : RawHaskType Γ ★.
 201     admit.
 202     Defined.
 203   Definition code2garrow Γ (ec t:RawHaskType Γ ★) :=
 204       match t with
 205 (*        | TApp ★ ★ (TApp _ ★ TArrow tx) t' => code2garrow0 ec tx       t'*)
 206         |                               _  => code2garrow0 ec unitType t
 207       end.
 208   Opaque code2garrow.
 209   Fixpoint typeMap {TV}{κ}(ty:@RawHaskType TV κ) : @RawHaskType TV κ :=
 210       match ty as TY in RawHaskType _ K return RawHaskType TV K with
 211         | TCode ec t        => code2garrow _ ec t
 212         | TApp _ _ t1 t2    => TApp (typeMap t1) (typeMap t2)
 213         | TAll _ f          => TAll _ (fun tv => typeMap (f tv))
 214         | TCoerc _ t1 t2 t3 => TCoerc (typeMap t1) (typeMap t2) (typeMap t3)
 215         | TVar   _ v        => TVar v
 216         | TArrow            => TArrow
 217         | TCon  tc          => TCon tc
 218         | TyFunApp  tf rhtl => (* FIXME *) TyFunApp tf rhtl
 219       end.
 220
 221   Definition typeMapL {Γ}(lht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★  :=
 222     match lht with
 223 (*      | t @@ nil       => (fun TV ite => typeMap (t TV ite)) @@ lev*)
 224       | t @@ lev => (fun TV ite => typeMap (t TV ite)) @@ lev
 225     end.
 226
 227   Definition coMap {Γ}(ck:HaskCoercionKind Γ) :=
 228     fun TV ite => match ck TV ite with
 229       | mkRawCoercionKind _ t1 t2 => mkRawCoercionKind _ (typeMap t1) (typeMap t2)
 230       end.
 231
 232   Definition flattenCoercion {Γ}{Δ}{ck}(hk:HaskCoercion Γ Δ ck) : HaskCoercion Γ (map coMap Δ) (coMap ck).
 233     admit.
 234     Defined.
 235
 236   Lemma update_typeMap Γ (lev:HaskLevel Γ) ξ v t
 237     : (typeMap ○ (update_ξ            ξ  lev ((⟨v, t ⟩)          :: nil)))
 238     = (           update_ξ (typeMap ○ ξ) lev ((⟨v, typeMap_ t ⟩) :: nil)).
 239     admit.
 240     Qed.
 241
 242   Lemma foo κ Γ σ τ : typeMap_ (substT σ τ) = substT(Γ:=Γ)(κ₁:=κ) (fun TV ite => typeMap ○ σ TV ite) τ.
 243     admit.
 244     Qed.
 245
 246   Lemma lit_lemma lit Γ : typeMap_ (literalType lit) = literalType(Γ:=Γ) lit.
 247     admit.
 248     Qed.
 249 *)
 250 (*
 251   Definition flatten : forall h c, Rule h c -> @ND Judg Rule (mapOptionTree flattenJudgment h) (mapOptionTree flattenJudgment c).
 252     intros h c r.
 253     refine (match r as R in Rule H C return ND Rule (mapOptionTree flattenJudgment H) (mapOptionTree flattenJudgment C) with
 254       | RURule  a b c d e             => let case_RURule := tt        in _
 255       | RNote   Γ Δ Σ τ l n           => let case_RNote := tt         in _
 256       | RLit    Γ Δ l     _           => let case_RLit := tt          in _
 257       | RVar    Γ Δ σ         p       => let case_RVar := tt          in _
 258       | RGlobal Γ Δ σ l wev           => let case_RGlobal := tt       in _
 259       | RLam    Γ Δ Σ tx te     x     => let case_RLam := tt          in _
 260       | RCast   Γ Δ Σ σ τ γ     x     => let case_RCast := tt         in _
 261       | RAbsT   Γ Δ Σ κ σ a           => let case_RAbsT := tt         in _
 262       | RAppT   Γ Δ Σ κ σ τ     y     => let case_RAppT := tt         in _
 263       | RAppCo  Γ Δ Σ κ σ₁ σ₂ γ σ l   => let case_RAppCo := tt        in _
 264       | RAbsCo  Γ Δ Σ κ σ  σ₁ σ₂  y   => let case_RAbsCo := tt        in _
 265       | RApp    Γ Δ Σ₁ Σ₂ tx te p     => let case_RApp := tt          in _
 266       | RLet    Γ Δ Σ₁ Σ₂ σ₁ σ₂ p     => let case_RLet := tt          in _
 267       | RBindingGroup Γ p lri m x q   => let case_RBindingGroup := tt in _
 268       | REmptyGroup _ _               => let case_REmptyGroup := tt   in _
 269       | RBrak   Σ a b c n m           => let case_RBrak := tt         in _
 270       | REsc    Σ a b c n m           => let case_REsc := tt          in _
 271       | RCase   Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
 272       | RLetRec Γ Δ lri x y t         => let case_RLetRec := tt       in _
 273       end).
 274
 275       destruct case_RURule.
 276         admit.
 277
 278       destruct case_RBrak.
 279         simpl.
 280         admit.
 281
 282       destruct case_REsc.
 283         simpl.
 284         admit.
 285
 286       destruct case_RNote.
 287         eapply nd_rule.  simpl.  apply RNote; auto.
 288
 289       destruct case_RLit.
 290         simpl.
 291
 292       set (@RNote Γ Δ Σ τ l) as q.
 293     Defined.
 294
 295   Definition flatten' {h}{c} (pf:ND Rule h c) := nd_map' flattenJudgment flatten pf.
 296
 297
 298     @ND Judgment1 Rule1 (mapOptionTree f h) (mapOptionTree f c).
 299
 300   refine (fix flatten : forall Γ Δ Σ τ
 301     (pf:SCND Rule [] [Γ > Δ >                       Σ |-                       τ ]) :
 302     SCND Rule [] [Γ > Δ > mapOptionTree typeMap Σ |- mapOptionTree typeMap τ ] :=
 303     match pf as SCND _ _
 304     | scnd_comp   : forall ht ct c , SCND ht ct -> Rule ct [c] -> SCND ht [c]
 305   | scnd_weak   : forall c       , SCND c  []
 306   | scnd_leaf   : forall ht c    , SCND ht [c]  -> SCND ht [c]
 307   | scnd_branch : forall ht c1 c2, SCND ht c1 -> SCND ht c2 -> SCND ht (c1,,c2)
 308   Expr Γ Δ ξ τ -> Expr Γ (map coMap Δ) (typeMap ○ ξ) (typeMap τ).
 309 *)
 310
 311 (*
 312   Lemma all_lemma Γ κ σ l :
 313 (@typeMap (κ :: Γ)
 314            (@HaskTApp (κ :: Γ) κ (@weakF Γ κ ★ σ) (@FreshHaskTyVar Γ κ) @@
 315             @weakL Γ κ l)) = (@typeMap Γ (@HaskTAll Γ κ σ @@  l)).
 316 *)
 317
 318 (*
 319   Definition flatten : forall Γ Δ ξ τ,  Expr Γ Δ ξ τ -> Expr Γ (map coMap Δ) (typeMap ○ ξ) (typeMap τ).
 320   refine (fix flatten Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') : Expr Γ' (map coMap Δ') (typeMap ○ ξ') (typeMap τ') :=
 321     match exp as E in Expr G D X T return Expr G (map coMap D) (typeMap ○ X) (typeMap T) with
 322     | EGlobal  Γ Δ ξ t wev                          => EGlobal _ _ _ _  wev
 323     | EVar     Γ Δ ξ ev                             => EVar    _ _ _    ev
 324     | ELit     Γ Δ ξ lit lev                        => let case_ELit    := tt in _
 325     | EApp     Γ Δ ξ t1 t2 lev e1 e2                => EApp _ _ _ _ _ _ (flatten _ _ _ _ e1) (flatten _ _ _ _ e2)
 326     | ELam     Γ Δ ξ t1 t2 lev v    e               => let case_ELam := tt in _
 327     | ELet     Γ Δ ξ tv t  l ev elet ebody          => let case_ELet    := tt in _
 328     | ELetRec  Γ Δ ξ lev t tree branches ebody      => let case_ELetRec := tt in _
 329     | ECast    Γ Δ ξ t1 t2 γ lev e                  => let case_ECast   := tt in _
 330     | ENote    Γ Δ ξ t n e                          => ENote _ _ _ _ n (flatten _ _ _ _ e)
 331     | ETyLam   Γ Δ ξ κ σ l e                        => let case_ETyLam  := tt in _
 332     | ECoLam   Γ Δ κ σ σ₁ σ₂ ξ l             e      => let case_ECoLam  := tt in _
 333     | ECoApp   Γ Δ κ σ₁ σ₂ γ σ ξ l e                => let case_ECoApp  := tt in _
 334     | ETyApp   Γ Δ κ σ τ ξ  l    e                  => let case_ETyApp  := tt in _
 335     | ECase    Γ Δ ξ l tc tbranches atypes e alts'  => let case_ECase   := tt in _
 336
 337     | EEsc     Γ Δ ξ ec t lev e                     => let case_EEsc    := tt in _
 338     | EBrak    Γ Δ ξ ec t lev e                     => let case_EBrak   := tt in _
 339     end); clear exp ξ' τ' Γ' Δ'.
 340
 341   destruct case_ELit.
 342     simpl.
 343     rewrite lit_lemma.
 344     apply ELit.
 345
 346   destruct case_ELam.
 347     set (flatten _ _ _ _ e) as q.
 348     rewrite update_typeMap in q.
 349     apply (@ELam _ _ _ _ _ _ _ _ v q).
 350
 351   destruct case_ELet.
 352     set (flatten _ _ _ _ ebody) as ebody'.
 353     set (flatten _ _ _ _ elet)  as elet'.
 354     rewrite update_typeMap in ebody'.
 355     apply (@ELet _ _ _ _ _ _ _ _ _ elet' ebody').
 356
 357   destruct case_EEsc.
 358     admit.
 359   destruct case_EBrak.
 360     admit.
 361
 362   destruct case_ECast.
 363     apply flatten in e.
 364     eapply ECast in e.
 365     apply e.
 366     apply flattenCoercion in γ.
 367     apply γ.
 368
 369   destruct case_ETyApp.
 370     apply flatten in e.
 371     simpl in e.
 372     unfold HaskTAll in e.
 373     unfold typeMap_ in e.
 374     simpl in e.
 375     eapply ETyApp in e.
 376     rewrite <- foo in e.
 377     apply e.
 378
 379   destruct case_ECoLam.
 380     apply flatten in e.
 381     simpl in e.
 382     set (@ECoLam _ _ _ _ _ _ _ _ _ _ e) as x.
 383     simpl in x.
 384     simpl.
 385     unfold typeMap_.
 386     simpl.
 387     apply x.
 388
 389   destruct case_ECoApp.
 390     simpl.
 391     apply flatten in e.
 392     eapply ECoApp.
 393     unfold mkHaskCoercionKind in *.
 394     simpl in γ.
 395     apply flattenCoercion in γ.
 396     unfold coMap in γ at 2.
 397     apply γ.
 398     apply e.
 399
 400   destruct case_ETyLam.
 401     apply flatten in e.
 402     set (@ETyLam Unique _ Γ (map coMap Δ) (typeMap ○ ξ) κ (fun ite x => typeMap (σ x ite))) as e'.
 403     unfold HaskTAll in *.
 404     unfold typeMap_ in *.
 405     rewrite <- foo in e'.
 406     unfold typeMap in e'.
 407     simpl in e'.
 408     apply ETyLam.
 409
 410 Set Printing Implicit.
 411 idtac.
 412 idtac.
 413
 414
 415     admit.
 416
 417   destruct case_ECase.
 418     admit.
 419
 420   destruct case_ELetRec.
 421     admit.
 422     Defined.
 423
 424   (* This proof will work for any dynamic semantics you like, so
 425    * long as those semantics are an ND_Relation (associativity,
 426    * neutrality, etc) *)
 427   Context (dynamic_semantics   : @ND_Relation _ Rule).
 428
 429   Section SystemFC_Category.
 430
 431     Context {Γ:TypeEnv}
 432             {Δ:CoercionEnv Γ}.
 433
 434     Definition Context := Tree ??(LeveledHaskType Γ ★).
 435
 436     Notation "a |= b" := (Γ >> Δ > a |- b).
 437
 438     (*
 439        SystemFCa
 440        PCF
 441        SystemFCa_two_level
 442        SystemFCa_initial_GArrow
 443      *)
 444
 445     Context (nd_eqv:@ND_Relation _ (@URule Γ Δ)).
 446     Check (@ProgrammingLanguage).
 447     Context (PL:@ProgrammingLanguage (LeveledHaskType Γ ★)
 448       (fun x y => match x with x1|=x2 => match y with y1|=y2 => @URule Γ Δ)).
 449     Definition JudgmentsFC := @Judgments_Category_CartesianCat _ (@URule Γ Δ) nd_eqv.
 450     Definition TypesFC     := @TypesL                          _ (@URule Γ Δ) nd_eqv.
 451
 452     (* The full subcategory of SystemFC(Γ,Δ) consisting only of judgments involving types at a fixed level.  Note that
 453      * code types are still permitted! *)
 454     Section SingleLevel.
 455       Context (lev:HaskLevel Γ).
 456
 457       Inductive ContextAtLevel : Context -> Prop :=
 458         | contextAtLevel_nil    :               ContextAtLevel []
 459         | contextAtLevel_leaf   : forall τ,     ContextAtLevel [τ @@ lev]
 460         | contextAtLevel_branch : forall b1 b2, ContextAtLevel b1 -> ContextAtLevel b2 -> ContextAtLevel (b1,,b2).
 461
 462       Inductive JudgmentsAtLevel : JudgmentsFC -> Prop :=
 463         | judgmentsAtLevel_nil    : JudgmentsAtLevel []
 464         | judgmentsAtLevel_leaf   : forall c1 c2, ContextAtLevel c1   -> ContextAtLevel c2   -> JudgmentsAtLevel [c1 |= c2]
 465         | judgmentsAtLevel_branch : forall j1 j2, JudgmentsAtLevel j1 -> JudgmentsAtLevel j2 -> JudgmentsAtLevel (j1,,j2).
 466
 467       Definition JudgmentsFCAtLevel := FullSubcategory JudgmentsFC JudgmentsAtLevel.
 468       Definition TypesFCAtLevel     := FullSubcategory TypesFC     ContextAtLevel.
 469     End SingleLevel.
 470
 471   End SystemFC_Category.
 472
 473   Implicit Arguments TypesFC [ ].
 474
 475 (*
 476     Section EscBrak_Functor.
 477       Context
 478         (past:@Past V)
 479         (n:V)
 480         (Σ₁:Tree ??(@LeveledHaskType V)).
 481
 482       Definition EscBrak_Functor_Fobj
 483         : SystemFC_Cat_Flat ((Σ₁,n)::past) -> SystemFC_Cat past
 484         := mapOptionTree (fun q:Tree ??(@CoreType V) * Tree ??(@CoreType V) =>
 485           let (a,s):=q in (Σ₁,,(``a)^^^n,[`<[ n |- encodeTypeTree_flat s ]>])).
 486
 487       Definition append_brak
 488       : forall {c}, ND_ML
 489           (mapOptionTree (ob2judgment_flat ((⟨Σ₁,n⟩) :: past))                        c )
 490           (mapOptionTree (ob2judgment                   past )  (EscBrak_Functor_Fobj c)).
 491         intros.
 492         unfold ND_ML.
 493         unfold EscBrak_Functor_Fobj.
 494         rewrite mapOptionTree_comp.
 495         simpl in *.
 496         apply nd_replicate.
 497         intro o; destruct o.
 498         apply nd_rule.
 499         apply MLRBrak.
 500         Defined.
 501
 502       Definition prepend_esc
 503       : forall {h}, ND_ML
 504           (mapOptionTree (ob2judgment                  past )  (EscBrak_Functor_Fobj h))
 505           (mapOptionTree (ob2judgment_flat ((⟨Σ₁,n⟩) :: past))                        h ).
 506         intros.
 507         unfold ND_ML.
 508         unfold EscBrak_Functor_Fobj.
 509         rewrite mapOptionTree_comp.
 510         simpl in *.
 511         apply nd_replicate.
 512         intro o; destruct o.
 513         apply nd_rule.
 514         apply MLREsc.
 515         Defined.
 516
 517       Definition EscBrak_Functor_Fmor
 518         : forall a b (f:a~~{SystemFC_Cat_Flat ((Σ₁,n)::past)}~~>b),
 519           (EscBrak_Functor_Fobj a)~~{SystemFC_Cat past}~~>(EscBrak_Functor_Fobj b).
 520         intros.
 521         eapply nd_comp.
 522         apply prepend_esc.
 523         eapply nd_comp.
 524         eapply Flat_to_ML.
 525         apply f.
 526         apply append_brak.
 527         Defined.
 528
 529       Lemma esc_then_brak_is_id : forall a,
 530        ndr_eqv(ND_Relation:=ml_dynamic_semantics V) (nd_comp prepend_esc append_brak)
 531          (nd_id (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj a))).
 532          admit.
 533          Qed.
 534
 535       Lemma brak_then_esc_is_id : forall a,
 536        ndr_eqv(ND_Relation:=ml_dynamic_semantics V) (nd_comp append_brak prepend_esc)
 537          (nd_id (mapOptionTree (ob2judgment_flat (((Σ₁,n)::past))) a)).
 538          admit.
 539          Qed.
 540
 541       Instance EscBrak_Functor
 542         : Functor (SystemFC_Cat_Flat ((Σ₁,n)::past)) (SystemFC_Cat past) EscBrak_Functor_Fobj :=
 543         { fmor := fun a b f => EscBrak_Functor_Fmor a b f }.
 544         intros; unfold EscBrak_Functor_Fmor; simpl in *.
 545           apply ndr_comp_respects; try reflexivity.
 546           apply ndr_comp_respects; try reflexivity.
 547           auto.
 548         intros; unfold EscBrak_Functor_Fmor; simpl in *.
 549           set (@ndr_comp_left_identity _ _ (ml_dynamic_semantics V)) as q.
 550           setoid_rewrite q.
 551           apply esc_then_brak_is_id.
 552         intros; unfold EscBrak_Functor_Fmor; simpl in *.
 553           set (@ndr_comp_associativity _ _ (ml_dynamic_semantics V)) as q.
 554           repeat setoid_rewrite q.
 555           apply ndr_comp_respects; try reflexivity.
 556           apply ndr_comp_respects; try reflexivity.
 557           repeat setoid_rewrite <- q.
 558           apply ndr_comp_respects; try reflexivity.
 559           setoid_rewrite brak_then_esc_is_id.
 560           clear q.
 561           set (@ndr_comp_left_identity _ _ (fc_dynamic_semantics V)) as q.
 562           setoid_rewrite q.
 563           reflexivity.
 564         Defined.
 565
 566     End EscBrak_Functor.
 567
 568
 569
 570   Ltac rule_helper_tactic' :=
 571     match goal with
 572     | [ H : ?A = ?A |- _ ] => clear H
 573     | [ H : [?A] = [] |- _ ] => inversion H; clear H
 574     | [ H : [] = [?A] |- _ ] => inversion H; clear H
 575     | [ H : ?A,,?B = [] |- _ ] => inversion H; clear H
 576     | [ H : ?A,,?B = [?Y] |- _ ] => inversion H; clear H
 577     | [ H: ?A :: ?B = ?B |- _ ] => apply symmetry in H; apply list_cannot_be_longer_than_itself in H; destruct H
 578     | [ H: ?B = ?A :: ?B |- _ ] => apply list_cannot_be_longer_than_itself in H; destruct H
 579     | [ H: ?A :: ?C :: ?B = ?B |- _ ] => apply symmetry in H; apply list_cannot_be_longer_than_itself' in H; destruct H
 580     | [ H: ?B = ?A :: ?C :: ?B |- _ ] => apply list_cannot_be_longer_than_itself' in H; destruct H
 581 (*  | [ H : Sequent T |- _ ] => destruct H *)
 582 (*  | [ H : ?D = levelize ?C (?A |= ?B) |- _ ] => inversion H; clear H*)
 583     | [ H : [?A] = [?B] |- _ ] => inversion H; clear H
 584     | [ H : [] = mapOptionTree ?B ?C |- _ ] => apply mapOptionTree_on_nil in H; subst
 585     | [ H : [?A] = mapOptionTree ?B ?C |- _ ] => destruct C as [C|]; simpl in H; [ | inversion H ]; destruct C; simpl in H; simpl
 586     | [ H : ?A,,?B = mapOptionTree ?C ?D |- _ ] => destruct D as [D|] ; [destruct D|idtac]; simpl in H; inversion H
 587     end.
 588
 589   Lemma fixit : forall a b f c1 c2, (@mapOptionTree a b f c1),,(mapOptionTree f c2) = mapOptionTree f (c1,,c2).
 590     admit.
 591     Defined.
 592
 593   Lemma grak a b f c : @mapOptionTree a b f c = [] -> [] = c.
 594     admit.
 595     Qed.
 596
 597   Definition append_brak_to_id : forall {c},
 598   @ND_FC V
 599       (mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past))  c )
 600       (mapOptionTree (ob2judgment past)  (EscBrak_Functor_Fobj c)).
 601   admit.
 602   Defined.
 603
 604   Definition append_brak : forall {h c}
 605     (pf:@ND_FC V
 606       h
 607       (mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past))  c )),
 608     @ND_FC V
 609        h
 610       (mapOptionTree (ob2judgment past)  (EscBrak_Functor_Fobj c)).
 611
 612       refine (fix append_brak h c nd {struct nd} :=
 613        ((match nd
 614             as nd'
 615             in @ND _ _ H C
 616             return
 617             (H=h) ->
 618             (C=mapOptionTree (ob2judgment ((⟨Σ₁,n⟩) :: past)) c) ->
 619             ND_FC h (mapOptionTree (ob2judgment past) (EscBrak_Functor_Fobj c))
 620           with
 621           | nd_id0                     => let case_nd_id0     := tt in _
 622           | nd_id1     h               => let case_nd_id1     := tt in _
 623           | nd_weak    h               => let case_nd_weak    := tt in _
 624           | nd_copy    h               => let case_nd_copy    := tt in _
 625           | nd_prod    _ _ _ _ lpf rpf => let case_nd_prod    := tt in _
 626           | nd_comp    _ _ _   top bot => let case_nd_comp    := tt in _
 627           | nd_rule    _ _     rule    => let case_nd_rule    := tt in _
 628           | nd_cancell _               => let case_nd_cancell := tt in _
 629           | nd_cancelr _               => let case_nd_cancelr := tt in _
 630           | nd_llecnac _               => let case_nd_llecnac := tt in _
 631           | nd_rlecnac _               => let case_nd_rlecnac := tt in _
 632           | nd_assoc   _ _ _           => let case_nd_assoc   := tt in _
 633           | nd_cossa   _ _ _           => let case_nd_cossa   := tt in _
 634         end) (refl_equal _) (refl_equal _)
 635        ));
 636        simpl in *; intros; subst; simpl in *; try (repeat (rule_helper_tactic' || subst)); subst; simpl in *.
 637        destruct case_nd_id0. apply nd_id0.
 638        destruct case_nd_id1. apply nd_rule. destruct p. apply RBrak.
 639        destruct case_nd_weak. apply nd_weak.
 640
 641        destruct case_nd_copy.
 642          (*
 643          destruct c; try destruct o; simpl in *; try rule_helper_tactic'; try destruct p; try rule_helper_tactic'.
 644          inversion H0; subst.
 645          simpl.*)
 646          idtac.
 647          clear H0.
 648          admit.
 649
 650        destruct case_nd_prod.
 651          eapply nd_prod.
 652          apply (append_brak _ _ lpf).
 653          apply (append_brak _ _ rpf).
 654
 655        destruct case_nd_comp.
 656          apply append_brak in bot.
 657          apply (nd_comp top bot).
 658
 659        destruct case_nd_cancell.
 660          eapply nd_comp; [ apply nd_cancell | idtac ].
 661          apply append_brak_to_id.
 662
 663        destruct case_nd_cancelr.
 664          eapply nd_comp; [ apply nd_cancelr | idtac ].
 665          apply append_brak_to_id.
 666
 667        destruct case_nd_llecnac.
 668          eapply nd_comp; [ idtac | apply nd_llecnac ].
 669          apply append_brak_to_id.
 670
 671        destruct case_nd_rlecnac.
 672          eapply nd_comp; [ idtac | apply nd_rlecnac ].
 673          apply append_brak_to_id.
 674
 675        destruct case_nd_assoc.
 676          eapply nd_comp; [ apply nd_assoc | idtac ].
 677          repeat rewrite fixit.
 678          apply append_brak_to_id.
 679
 680        destruct case_nd_cossa.
 681          eapply nd_comp; [ idtac | apply nd_cossa ].
 682          repeat rewrite fixit.
 683          apply append_brak_to_id.
 684
 685        destruct case_nd_rule
 686
 687
 688
 689     Defined.
 690
 691   Definition append_brak {h c} : forall
 692       pf:@ND_FC V
 693         (fixify Γ ((⟨n, Σ₁ ⟩) :: past)                       h )
 694         c,
 695       @ND_FC V
 696         (fixify Γ                past  (EscBrak_Functor_Fobj h))
 697         c.
 698     admit.
 699     Defined.
 700 *)
 701 *)
 702 End HaskProofCategory.