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