src/HaskProofCategory.v

   1 (*********************************************************************************************************************************)
   2 (* HaskProofCategory:                                                                                                            *)
   3 (*                                                                                                                               *)
   4 (*    Natural Deduction proofs of the well-typedness of a Haskell term form a category                                           *)
   5 (*                                                                                                                               *)
   6 (*********************************************************************************************************************************)
   7
   8 Generalizable All Variables.
   9 Require Import Preamble.
  10 Require Import General.
  11 Require Import NaturalDeduction.
  12 Require Import Coq.Strings.String.
  13 Require Import Coq.Lists.List.
  14
  15 Require Import HaskKinds.
  16 Require Import HaskCoreTypes.
  17 Require Import HaskLiteralsAndTyCons.
  18 Require Import HaskStrongTypes.
  19 Require Import HaskProof.
  20 Require Import NaturalDeduction.
  21 Require Import NaturalDeductionCategory.
  22
  23 Require Import Algebras_ch4.
  24 Require Import Categories_ch1_3.
  25 Require Import Functors_ch1_4.
  26 Require Import Isomorphisms_ch1_5.
  27 Require Import ProductCategories_ch1_6_1.
  28 Require Import OppositeCategories_ch1_6_2.
  29 Require Import Enrichment_ch2_8.
  30 Require Import Subcategories_ch7_1.
  31 Require Import NaturalTransformations_ch7_4.
  32 Require Import NaturalIsomorphisms_ch7_5.
  33 Require Import MonoidalCategories_ch7_8.
  34 Require Import Coherence_ch7_8.
  35
  36 Require Import HaskStrongTypes.
  37 Require Import HaskStrong.
  38 Require Import HaskProof.
  39 Require Import HaskStrongToProof.
  40 Require Import HaskProofToStrong.
  41 Require Import ProgrammingLanguage.
  42
  43 Open Scope nd_scope.
  44
  45
  46 (*
  47  *  The flattening transformation.  Currently only TWO-level languages are
  48  *  supported, and the level-1 sublanguage is rather limited.
  49  *
  50  *
  51  *  This file abuses terminology pretty badly.  For purposes of this file,
  52  *  "PCF" means "the level-1 sublanguage" and "FC" (aka System FC) means
  53  *  the whole language (level-0 language including bracketed level-1 terms)
  54  *)
  55 Section HaskProofCategory.
  56
  57   Context (ndr_systemfc:@ND_Relation _ Rule).
  58
  59   Inductive PCFJudg Γ (Δ:CoercionEnv Γ) (ec:HaskTyVar Γ ★) :=
  60     pcfjudg : Tree ??(HaskType Γ ★) -> Tree ??(HaskType Γ ★) -> PCFJudg Γ Δ ec.
  61     Implicit Arguments pcfjudg [ [Γ] [Δ] [ec] ].
  62
  63   (* given an PCFJudg at depth (ec::depth) we can turn it into an PCFJudg
  64    * from depth (depth) by wrapping brackets around everything in the
  65    * succedent and repopulating *)
  66   Definition brakify {Γ}{Δ}{ec} (j:PCFJudg Γ Δ ec) : Judg :=
  67     match j with
  68       pcfjudg Σ τ => Γ > Δ > (Σ@@@(ec::nil)) |- (mapOptionTree (fun t => HaskBrak ec t) τ @@@ nil)
  69       end.
  70
  71   Definition pcf_vars {Γ}(ec:HaskTyVar Γ ★)(t:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★)
  72     := mapOptionTreeAndFlatten (fun lt =>
  73       match lt with t @@ l => match l with
  74                                 | ec'::nil => if eqd_dec ec ec' then [t] else []
  75                                 | _ => []
  76                               end
  77       end) t.
  78
  79   Inductive MatchingJudgments {Γ}{Δ}{ec} : Tree ??(PCFJudg Γ Δ ec) -> Tree ??Judg -> Type :=
  80     | match_nil    : MatchingJudgments [] []
  81     | match_branch : forall a b c d, MatchingJudgments a b -> MatchingJudgments c d -> MatchingJudgments (a,,c) (b,,d)
  82     | match_leaf   :
  83       forall Σ τ lev,
  84         MatchingJudgments
  85           [pcfjudg (pcf_vars ec Σ)                               τ         ]
  86           [Γ > Δ >              Σ  |- (mapOptionTree (HaskBrak ec) τ @@@ lev)].
  87
  88   Definition fc_vars {Γ}(ec:HaskTyVar Γ ★)(t:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★)
  89     := mapOptionTreeAndFlatten (fun lt =>
  90       match lt with t @@ l => match l with
  91                                 | ec'::nil => if eqd_dec ec ec' then [] else [t]
  92                                 | _ => []
  93                               end
  94       end) t.
  95
  96   Definition pcfjudg2judg {Γ}{Δ:CoercionEnv Γ} ec (cj:PCFJudg Γ Δ ec) :=
  97     match cj with pcfjudg Σ τ => Γ > Δ > (Σ @@@ (ec::nil)) |- (τ @@@ (ec::nil)) end.
  98
  99   (* Rules allowed in PCF; i.e. rules we know how to turn into GArrows     *)
 100   (* Rule_PCF consists of the rules allowed in flat PCF: everything except *)
 101   (* AppT, AbsT, AppC, AbsC, Cast, Global, and some Case statements        *)
 102   Inductive Rule_PCF {Γ}{Δ:CoercionEnv Γ} (ec:HaskTyVar Γ ★)
 103     : forall (h c:Tree ??(PCFJudg Γ Δ ec)), Rule (mapOptionTree (pcfjudg2judg ec) h) (mapOptionTree (pcfjudg2judg ec) c) -> Type :=
 104   | PCF_RArrange    : ∀ x y t     a,  Rule_PCF ec [pcfjudg _  _ ] [ pcfjudg _  _  ] (RArrange Γ Δ (x@@@(ec::nil)) (y@@@(ec::nil)) (t@@@(ec::nil)) a)
 105   | PCF_RLit        : ∀ lit        ,  Rule_PCF ec [           ] [ pcfjudg [] [_] ] (RLit   Γ Δ  lit (ec::nil))
 106   | PCF_RNote       : ∀ Σ τ   n    ,  Rule_PCF ec [pcfjudg _ [_]] [ pcfjudg _ [_] ] (RNote  Γ Δ  (Σ@@@(ec::nil)) τ         (ec::nil) n)
 107   | PCF_RVar        : ∀ σ          ,  Rule_PCF ec [           ] [ pcfjudg [_] [_] ] (RVar   Γ Δ    σ         (ec::nil)  )
 108   | PCF_RLam        : ∀ Σ tx te    ,  Rule_PCF ec [pcfjudg (_,,[_]) [_] ] [ pcfjudg _ [_] ] (RLam   Γ Δ  (Σ@@@(ec::nil)) tx te  (ec::nil)  )
 109
 110   | PCF_RApp             : ∀ Σ Σ' tx te ,
 111     Rule_PCF ec ([pcfjudg _ [_]],,[pcfjudg _ [_]]) [pcfjudg (_,,_) [_]]
 112     (RApp Γ Δ (Σ@@@(ec::nil))(Σ'@@@(ec::nil)) tx te (ec::nil))
 113
 114   | PCF_RLet             : ∀ Σ Σ' σ₂   p,
 115     Rule_PCF ec ([pcfjudg _ [_]],,[pcfjudg (_,,[_]) [_]]) [pcfjudg (_,,_) [_]]
 116     (RLet Γ Δ (Σ@@@(ec::nil)) (Σ'@@@(ec::nil)) σ₂ p (ec::nil))
 117
 118   | PCF_REmptyGroup      :                 Rule_PCF ec [           ] [ pcfjudg []  [] ] (REmptyGroup   Γ Δ  )
 119 (*| PCF_RLetRec          : ∀ Σ₁ τ₁ τ₂   ,  Rule_PCF (ec::nil) _ _ (RLetRec Γ Δ Σ₁ τ₁ τ₂ (ec::nil) )*)
 120   | PCF_RBindingGroup    : ∀ Σ₁ Σ₂ τ₁ τ₂,  Rule_PCF ec ([pcfjudg _ _],,[pcfjudg _ _]) [pcfjudg (_,,_) (_,,_)]
 121     (RBindingGroup Γ Δ (Σ₁@@@(ec::nil)) (Σ₂@@@(ec::nil)) (τ₁@@@(ec::nil)) (τ₂@@@(ec::nil))).
 122   (* need int/boolean case *)
 123   Implicit Arguments Rule_PCF [ ].
 124
 125   Definition PCFRule Γ Δ lev h c := { r:_ & @Rule_PCF Γ Δ lev h c r }.
 126
 127   (* An organized deduction has been reorganized into contiguous blocks whose
 128    * hypotheses (if any) and conclusion have the same Γ and Δ and a fixed nesting depth.  The boolean
 129    * indicates if non-PCF rules have been used *)
 130   Inductive OrgR : Tree ??Judg -> Tree ??Judg -> Type :=
 131
 132   | org_fc        : forall h c (r:Rule h c),
 133     Rule_Flat r ->
 134     OrgR h c
 135
 136   | org_pcf      : forall Γ Δ ec h h' c c',
 137     MatchingJudgments    h  h' ->
 138     MatchingJudgments    c  c' ->
 139     ND (PCFRule Γ Δ ec)  h  c  ->
 140     OrgR                 h' c'.
 141
 142   Definition mkEsc {Γ}{Δ}{ec}(h:Tree ??(PCFJudg Γ Δ ec))
 143     : ND Rule
 144     (mapOptionTree brakify h)
 145     (mapOptionTree (pcfjudg2judg ec) h).
 146     apply nd_replicate; intros.
 147     destruct o; simpl in *.
 148     induction t0.
 149     destruct a; simpl.
 150     apply nd_rule.
 151     apply REsc.
 152     apply nd_id.
 153     apply (Prelude_error "mkEsc got multi-leaf succedent").
 154     Defined.
 155
 156   Definition mkBrak {Γ}{Δ}{ec}(h:Tree ??(PCFJudg Γ Δ ec))
 157     : ND Rule
 158     (mapOptionTree (pcfjudg2judg ec) h)
 159     (mapOptionTree brakify h).
 160     apply nd_replicate; intros.
 161     destruct o; simpl in *.
 162     induction t0.
 163     destruct a; simpl.
 164     apply nd_rule.
 165     apply RBrak.
 166     apply nd_id.
 167     apply (Prelude_error "mkBrak got multi-leaf succedent").
 168     Defined.
 169
 170     (*
 171   Definition Partition {Γ} ec (Σ:Tree ??(LeveledHaskType Γ ★)) :=
 172     { vars:(_ * _) |
 173       fc_vars  ec Σ = fst vars /\
 174       pcf_vars ec Σ = snd vars }.
 175       *)
 176
 177   Definition pcfToND : forall Γ Δ ec h c,
 178     ND (PCFRule Γ Δ ec) h c -> ND Rule (mapOptionTree (pcfjudg2judg ec) h) (mapOptionTree (pcfjudg2judg ec) c).
 179     intros.
 180     eapply (fun q => nd_map' _ q X).
 181     intros.
 182     destruct X0.
 183     apply nd_rule.
 184     apply x.
 185     Defined.
 186
 187   Instance OrgPCF Γ Δ lev : @ND_Relation _ (PCFRule Γ Δ lev) :=
 188     { ndr_eqv := fun a b f g => (pcfToND _ _ _ _ _ f) === (pcfToND _ _ _ _ _ g) }.
 189       admit.
 190       admit.
 191       admit.
 192       admit.
 193       admit.
 194       admit.
 195       admit.
 196       admit.
 197       admit.
 198       admit.
 199       admit.
 200       admit.
 201       admit.
 202       Defined.
 203
 204   (*
 205    * An intermediate representation necessitated by Coq's termination
 206    * conditions.  This is basically a tree where each node is a
 207    * subproof which is either entirely level-1 or entirely level-0
 208    *)
 209   Inductive Alternating : Tree ??Judg -> Type :=
 210
 211     | alt_nil    : Alternating []
 212
 213     | alt_branch : forall a b,
 214       Alternating a -> Alternating b -> Alternating (a,,b)
 215
 216     | alt_fc     : forall h c,
 217       Alternating h ->
 218       ND Rule h c ->
 219       Alternating c
 220
 221     | alt_pcf    : forall Γ Δ ec h c h' c',
 222       MatchingJudgments    h  h' ->
 223       MatchingJudgments    c  c' ->
 224       Alternating h' ->
 225       ND (PCFRule Γ Δ ec) h c ->
 226       Alternating c'.
 227
 228   Require Import Coq.Logic.Eqdep.
 229
 230   Lemma magic a b c d ec e :
 231     ClosedND(Rule:=Rule) [a > b > c |- [d @@  (ec :: e)]] ->
 232     ClosedND(Rule:=Rule) [a > b > pcf_vars ec c @@@ (ec :: nil) |- [d @@  (ec :: nil)]].
 233   admit.
 234   Defined.
 235
 236   Definition orgify : forall Γ Δ Σ τ (pf:ClosedND(Rule:=Rule) [Γ > Δ > Σ |- τ]), Alternating [Γ > Δ > Σ |- τ].
 237
 238     refine (
 239       fix  orgify_fc' Γ Δ Σ τ (pf:ClosedND [Γ > Δ > Σ |- τ]) {struct pf} : Alternating [Γ > Δ > Σ |- τ] :=
 240         let case_main := tt in _
 241       with orgify_fc c (pf:ClosedND c) {struct pf} : Alternating c :=
 242       (match c as C return C=c -> Alternating C with
 243         | T_Leaf None                    => fun _ => alt_nil
 244         | T_Leaf (Some (Γ > Δ > Σ |- τ)) => let case_leaf := tt in fun eqpf => _
 245         | T_Branch b1 b2                 => let case_branch := tt in fun eqpf => _
 246       end (refl_equal _))
 247       with orgify_pcf   Γ Δ ec pcfj j (m:MatchingJudgments pcfj j)
 248         (pf:ClosedND (mapOptionTree (pcfjudg2judg ec) pcfj)) {struct pf} : Alternating j :=
 249         let case_pcf := tt in _
 250       for orgify_fc').
 251
 252       destruct case_main.
 253       inversion pf; subst.
 254       set (alt_fc _ _ (orgify_fc _ X) (nd_rule X0)) as backup.
 255       refine (match X0 as R in Rule H C return
 256                 match C with
 257                   | T_Leaf (Some (Γ > Δ > Σ |- τ)) =>
 258                     h=H -> Alternating [Γ > Δ > Σ |- τ] -> Alternating [Γ > Δ > Σ |- τ]
 259                   | _                              => True
 260                 end
 261                  with
 262                 | RBrak   Σ a b c n m           => let case_RBrak := tt         in fun pf' backup => _
 263                 | REsc    Σ a b c n m           => let case_REsc := tt          in fun pf' backup => _
 264                 | _ => fun pf' x => x
 265               end (refl_equal _) backup).
 266       clear backup0 backup.
 267
 268       destruct case_RBrak.
 269         rename c into ec.
 270         set (@match_leaf Σ0 a ec n [b] m) as q.
 271         set (orgify_pcf Σ0 a ec _ _ q) as q'.
 272         apply q'.
 273         simpl.
 274         rewrite pf' in X.
 275         apply magic in X.
 276         apply X.
 277
 278       destruct case_REsc.
 279         apply (Prelude_error "encountered Esc in wrong side of mkalt").
 280
 281     destruct case_leaf.
 282       apply orgify_fc'.
 283       rewrite eqpf.
 284       apply pf.
 285
 286     destruct case_branch.
 287       rewrite <- eqpf in pf.
 288       inversion pf; subst.
 289       apply no_rules_with_multiple_conclusions in X0.
 290       inversion X0.
 291       exists b1. exists b2.
 292       auto.
 293       apply (alt_branch _ _ (orgify_fc _ X) (orgify_fc _ X0)).
 294
 295     destruct case_pcf.
 296     Admitted.
 297
 298   Definition pcfify Γ Δ ec : forall Σ τ,
 299     ClosedND(Rule:=Rule) [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)]
 300       -> ND (PCFRule Γ Δ ec) [] [pcfjudg Σ τ].
 301
 302     refine ((
 303       fix pcfify Σ τ (pn:@ClosedND _ Rule [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)]) {struct pn}
 304       : ND (PCFRule Γ Δ ec) [] [pcfjudg Σ τ] :=
 305      (match pn in @ClosedND _ _ J return J=[Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)] -> _ with
 306       | cnd_weak             => let case_nil    := tt in _
 307       | cnd_rule h c cnd' r  => let case_rule   := tt in _
 308       | cnd_branch _ _ c1 c2 => let case_branch := tt in _
 309       end (refl_equal _)))).
 310       intros.
 311       inversion H.
 312       intros.
 313       destruct c; try destruct o; inversion H.
 314       destruct j.
 315       Admitted.
 316
 317   (* any proof in organized form can be "dis-organized" *)
 318   Definition unOrgR : forall h c, OrgR h c -> ND Rule h c.
 319     intros.
 320
 321     induction X.
 322       apply nd_rule.
 323       apply r.
 324
 325     eapply nd_comp.
 326       (*
 327       apply (mkEsc h).
 328       eapply nd_comp; [ idtac |  apply (mkBrak c) ].
 329       apply pcfToND.
 330       apply n.
 331       *)
 332       Admitted.
 333
 334   Definition unOrgND h c :  ND OrgR h c -> ND Rule h c := nd_map unOrgR.
 335
 336   Instance OrgNDR : @ND_Relation _ OrgR :=
 337     { ndr_eqv := fun a b f g => (unOrgND _ _ f) === (unOrgND _ _ g) }.
 338       admit.
 339       admit.
 340       admit.
 341       admit.
 342       admit.
 343       admit.
 344       admit.
 345       admit.
 346       admit.
 347       admit.
 348       admit.
 349       admit.
 350       admit.
 351       Defined.
 352
 353   Hint Constructors Rule_Flat.
 354
 355   Instance PCF_sequents Γ Δ lev : @SequentCalculus _ (PCFRule Γ Δ lev) _ pcfjudg.
 356     apply Build_SequentCalculus.
 357     intros.
 358     induction a.
 359     destruct a; simpl.
 360     apply nd_rule.
 361       exists (RVar _ _ _ _).
 362       apply PCF_RVar.
 363     apply nd_rule.
 364       exists (REmptyGroup _ _ ).
 365       apply PCF_REmptyGroup.
 366     eapply nd_comp.
 367       eapply nd_comp; [ apply nd_llecnac | idtac ].
 368       apply (nd_prod IHa1 IHa2).
 369       apply nd_rule.
 370         exists (RBindingGroup _ _ _ _ _ _).
 371         apply PCF_RBindingGroup.
 372         Defined.
 373
 374   Definition PCF_Arrange {Γ}{Δ}{lev} : forall x y z, Arrange x y -> ND (PCFRule Γ Δ lev) [pcfjudg x z] [pcfjudg y z].
 375     admit.
 376     Defined.
 377
 378   Definition PCF_cut Γ Δ lev : forall a b c, ND (PCFRule Γ Δ lev) ([ pcfjudg a b ],,[ pcfjudg b c ]) [ pcfjudg a c ].
 379     intros.
 380     destruct b.
 381     destruct o.
 382     destruct c.
 383     destruct o.
 384
 385     (* when the cut is a single leaf and the RHS is a single leaf: *)
 386     eapply nd_comp.
 387       eapply nd_prod.
 388       apply nd_id.
 389       apply (PCF_Arrange [h] ([],,[h]) [h0]).
 390       apply RuCanL.
 391       eapply nd_comp; [ idtac | apply (PCF_Arrange ([],,a) a [h0]); apply RCanL ].
 392       apply nd_rule.
 393 (*
 394       set (@RLet Γ Δ [] (a@@@(ec::nil)) h0 h (ec::nil)) as q.
 395       exists q.
 396       apply (PCF_RLet _ [] a h0 h).
 397     apply (Prelude_error "cut rule invoked with [a|=[b]] [[b]|=[]]").
 398     apply (Prelude_error "cut rule invoked with [a|=[b]] [[b]|=[x,,y]]").
 399     apply (Prelude_error "cut rule invoked with [a|=[]]  [[]|=c]").
 400     apply (Prelude_error "cut rule invoked with [a|=[b,,c]] [[b,,c]|=z]").
 401 *)
 402     admit.
 403     admit.
 404     admit.
 405     admit.
 406     admit.
 407     Defined.
 408
 409   Instance PCF_cutrule Γ Δ lev : CutRule (PCF_sequents Γ Δ lev) :=
 410     { nd_cut := PCF_cut Γ Δ lev }.
 411     admit.
 412     admit.
 413     admit.
 414     Defined.
 415
 416   Definition PCF_left Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [pcfjudg b c] [pcfjudg (a,,b) (a,,c)].
 417     eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ].
 418     eapply nd_prod; [ apply nd_seq_reflexive | apply nd_id ].
 419     apply nd_rule.
 420     set (@PCF_RBindingGroup Γ Δ lev a b a c) as q'.
 421     refine (existT _ _ _).
 422     apply q'.
 423     Defined.
 424
 425   Definition PCF_right Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [pcfjudg b c] [pcfjudg (b,,a) (c,,a)].
 426     eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ].
 427     eapply nd_prod; [ apply nd_id | apply nd_seq_reflexive ].
 428     apply nd_rule.
 429     set (@PCF_RBindingGroup Γ Δ lev b a c a) as q'.
 430     refine (existT _ _ _).
 431     apply q'.
 432     Defined.
 433
 434   Instance PCF_sequent_join Γ Δ lev : @SequentExpansion _ _ _ _ _ (PCF_sequents Γ Δ lev) (PCF_cutrule Γ Δ lev) :=
 435   { se_expand_left  := PCF_left  Γ Δ lev
 436   ; se_expand_right := PCF_right Γ Δ lev }.
 437     admit.
 438     admit.
 439     admit.
 440     admit.
 441     Defined.
 442
 443   (* 5.1.3 *)
 444   Instance PCF Γ Δ lev : @ProgrammingLanguage _ _ pcfjudg (PCFRule Γ Δ lev) :=
 445   { pl_eqv                := OrgPCF Γ Δ lev
 446   ; pl_sc                 := PCF_sequents Γ Δ lev
 447   ; pl_subst              := PCF_cutrule Γ Δ lev
 448   ; pl_sequent_join       := PCF_sequent_join Γ Δ lev
 449   }.
 450     apply Build_TreeStructuralRules; intros; unfold eqv; unfold hom; simpl.
 451
 452     apply nd_rule. unfold PCFRule. simpl.
 453       exists (RArrange _ _ _ _ _ (RCossa _ _ _)).
 454       apply (PCF_RArrange lev ((a,,b),,c) (a,,(b,,c)) x).
 455
 456     apply nd_rule. unfold PCFRule. simpl.
 457       exists (RArrange _ _ _ _ _ (RAssoc _ _ _)).
 458       apply (PCF_RArrange lev (a,,(b,,c)) ((a,,b),,c) x).
 459
 460     apply nd_rule. unfold PCFRule. simpl.
 461       exists (RArrange _ _ _ _ _ (RCanL _)).
 462       apply (PCF_RArrange lev ([],,a) _ _).
 463
 464     apply nd_rule. unfold PCFRule. simpl.
 465       exists (RArrange _ _ _ _ _ (RCanR _)).
 466       apply (PCF_RArrange lev (a,,[]) _ _).
 467
 468     apply nd_rule. unfold PCFRule. simpl.
 469       exists (RArrange _ _ _ _ _ (RuCanL _)).
 470       apply (PCF_RArrange lev _ ([],,a) _).
 471
 472     apply nd_rule. unfold PCFRule. simpl.
 473       exists (RArrange _ _ _ _ _ (RuCanR _)).
 474       apply (PCF_RArrange lev _ (a,,[]) _).
 475       Defined.
 476
 477   Instance SystemFCa_sequents Γ Δ : @SequentCalculus _ OrgR _ (mkJudg Γ Δ).
 478     apply Build_SequentCalculus.
 479     intros.
 480     induction a.
 481     destruct a; simpl.
 482     apply nd_rule.
 483       destruct l.
 484       apply org_fc with (r:=RVar _ _ _ _).
 485       auto.
 486     apply nd_rule.
 487       apply org_fc with (r:=REmptyGroup _ _ ).
 488       auto.
 489     eapply nd_comp.
 490       eapply nd_comp; [ apply nd_llecnac | idtac ].
 491       apply (nd_prod IHa1 IHa2).
 492       apply nd_rule.
 493         apply org_fc with (r:=RBindingGroup _ _ _ _ _ _).
 494         auto.
 495         Defined.
 496
 497   Definition SystemFCa_cut Γ Δ : forall a b c, ND OrgR ([ Γ > Δ > a |- b ],,[ Γ > Δ > b |- c ]) [ Γ > Δ > a |- c ].
 498     intros.
 499     destruct b.
 500     destruct o.
 501     destruct c.
 502     destruct o.
 503
 504     (* when the cut is a single leaf and the RHS is a single leaf: *)
 505     eapply nd_comp.
 506       eapply nd_prod.
 507       apply nd_id.
 508       eapply nd_rule.
 509       apply org_fc with (r:=RArrange _ _ _ _ _ (RuCanL [l])).
 510       auto.
 511       eapply nd_comp; [ idtac | eapply nd_rule; apply org_fc with (r:=RArrange _ _ _ _ _ (RCanL _)) ].
 512       apply nd_rule.
 513       destruct l.
 514       destruct l0.
 515       assert (h0=h2). admit.
 516       subst.
 517       apply org_fc with (r:=@RLet Γ Δ [] a h1 h h2).
 518       auto.
 519       auto.
 520     apply (Prelude_error "systemfc cut rule invoked with [a|=[b]] [[b]|=[]]").
 521     apply (Prelude_error "systemfc cut rule invoked with [a|=[b]] [[b]|=[x,,y]]").
 522     apply (Prelude_error "systemfc rule invoked with [a|=[]]  [[]|=c]").
 523     apply (Prelude_error "systemfc rule invoked with [a|=[b,,c]] [[b,,c]|=z]").
 524     Defined.
 525
 526   Instance SystemFCa_cutrule Γ Δ : CutRule (SystemFCa_sequents Γ Δ) :=
 527     { nd_cut := SystemFCa_cut Γ Δ }.
 528     admit.
 529     admit.
 530     admit.
 531     Defined.
 532
 533   Definition SystemFCa_left Γ Δ a b c : ND OrgR [Γ > Δ > b |- c] [Γ > Δ > (a,,b) |- (a,,c)].
 534     eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ].
 535     eapply nd_prod; [ apply nd_seq_reflexive | apply nd_id ].
 536     apply nd_rule.
 537     apply org_fc with (r:=RBindingGroup Γ Δ a b a c).
 538     auto.
 539     Defined.
 540
 541   Definition SystemFCa_right Γ Δ a b c : ND OrgR [Γ > Δ > b |- c] [Γ > Δ > (b,,a) |- (c,,a)].
 542     eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ].
 543     eapply nd_prod; [ apply nd_id | apply nd_seq_reflexive ].
 544     apply nd_rule.
 545     apply org_fc with (r:=RBindingGroup Γ Δ b a c a).
 546     auto.
 547     Defined.
 548
 549   Instance SystemFCa_sequent_join Γ Δ : @SequentExpansion _ _ _ _ _ (SystemFCa_sequents Γ Δ) (SystemFCa_cutrule Γ Δ) :=
 550   { se_expand_left  := SystemFCa_left  Γ Δ
 551   ; se_expand_right := SystemFCa_right Γ Δ }.
 552     admit.
 553     admit.
 554     admit.
 555     admit.
 556     Defined.
 557
 558   (* 5.1.2 *)
 559   Instance SystemFCa Γ Δ : @ProgrammingLanguage _ _ (mkJudg Γ Δ) OrgR :=
 560   { pl_eqv                := OrgNDR
 561   ; pl_sc                 := SystemFCa_sequents     Γ Δ
 562   ; pl_subst              := SystemFCa_cutrule      Γ Δ
 563   ; pl_sequent_join       := SystemFCa_sequent_join Γ Δ
 564   }.
 565     apply Build_TreeStructuralRules; intros; unfold eqv; unfold hom; simpl.
 566     apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RCossa a b c))). apply Flat_RArrange.
 567     apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RAssoc a b c))). apply Flat_RArrange.
 568     apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanL  a    ))). apply Flat_RArrange.
 569     apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanR  a    ))). apply Flat_RArrange.
 570     apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanL a    ))). apply Flat_RArrange.
 571     apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanR a    ))). apply Flat_RArrange.
 572     Defined.
 573
 574
 575 (*
 576   Definition code2garrow Γ (ec t:RawHaskType Γ ★) :=
 577       match t with
 578 (*        | TApp ★ ★ (TApp _ ★ TArrow tx) t' => code2garrow0 ec tx       t'*)
 579         |                               _  => code2garrow0 ec unitType t
 580       end.
 581   Opaque code2garrow.
 582   Fixpoint typeMap {TV}{κ}(ty:@RawHaskType TV κ) : @RawHaskType TV κ :=
 583       match ty as TY in RawHaskType _ K return RawHaskType TV K with
 584         | TCode ec t        => code2garrow _ ec t
 585         | TApp _ _ t1 t2    => TApp (typeMap t1) (typeMap t2)
 586         | TAll _ f          => TAll _ (fun tv => typeMap (f tv))
 587         | TCoerc _ t1 t2 t3 => TCoerc (typeMap t1) (typeMap t2) (typeMap t3)
 588         | TVar   _ v        => TVar v
 589         | TArrow            => TArrow
 590         | TCon  tc          => TCon tc
 591         | TyFunApp  tf rhtl => (* FIXME *) TyFunApp tf rhtl
 592       end.
 593
 594   Definition typeMapL {Γ}(lht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★  :=
 595     match lht with
 596 (*      | t @@ nil       => (fun TV ite => typeMap (t TV ite)) @@ lev*)
 597       | t @@ lev => (fun TV ite => typeMap (t TV ite)) @@ lev
 598     end.
 599 *)
 600
 601   (* gathers a tree of guest-language types into a single host-language types via the tensor *)
 602   Definition tensorizeType {Γ} (lt:Tree ??(HaskType Γ ★)) : HaskType Γ ★.
 603     admit.
 604     Defined.
 605
 606   Definition mkGA {Γ} : HaskType Γ ★ -> HaskType Γ ★ -> HaskType Γ ★.
 607     admit.
 608     Defined.
 609
 610   Definition guestJudgmentAsGArrowType {Γ}{Δ}{ec}(lt:PCFJudg Γ Δ ec) : HaskType Γ ★ :=
 611     match lt with
 612       pcfjudg x y =>
 613       (mkGA (tensorizeType x) (tensorizeType y))
 614     end.
 615
 616   Definition obact {Γ}{Δ} ec (X:Tree ??(PCFJudg Γ Δ ec)) : Tree ??(LeveledHaskType Γ ★) :=
 617     mapOptionTree guestJudgmentAsGArrowType X @@@ nil.
 618
 619   (*
 620    * Here it is, what you've all been waiting for!  When reading this,
 621    * it might help to have the definition for "Inductive ND" (see
 622    * NaturalDeduction.v) handy as a cross-reference.
 623    *)
 624   Definition FlatteningFunctor_fmor {Γ}{Δ}{ec}
 625     : forall h c,
 626       (h~~{JudgmentsL _ _ (PCF Γ Δ ec)}~~>c) ->
 627       ((obact ec h)~~{TypesL _ _ (SystemFCa Γ Δ)}~~>(obact ec c)).
 628
 629     set (@nil (HaskTyVar Γ ★)) as lev.
 630
 631     unfold hom; unfold ob; unfold ehom; simpl; unfold mon_i; unfold obact; intros.
 632
 633     induction X; simpl.
 634
 635     (* the proof from no hypotheses of no conclusions (nd_id0) becomes REmptyGroup *)
 636     apply nd_rule; apply (org_fc _ _ (REmptyGroup _ _ )). auto.
 637
 638     (* the proof from hypothesis X of conclusion X (nd_id1) becomes RVar *)
 639     apply nd_rule; apply (org_fc _ _ (RVar _ _ _ _)). auto.
 640
 641     (* the proof from hypothesis X of no conclusions (nd_weak) becomes RWeak;;REmptyGroup *)
 642     eapply nd_comp;
 643       [ idtac
 644       | eapply nd_rule
 645       ; eapply (org_fc  _ _ (RArrange _ _ _ _ _ (RWeak _)))
 646       ; auto ].
 647       eapply nd_rule.
 648       eapply (org_fc _ _ (REmptyGroup _ _)); auto.
 649
 650     (* the proof from hypothesis X of two identical conclusions X,,X (nd_copy) becomes RVar;;RBindingGroup;;RCont *)
 651     eapply nd_comp; [ idtac | eapply nd_rule; eapply (org_fc _ _ (RArrange _ _ _ _ _ (RCont _))) ].
 652       eapply nd_comp; [ apply nd_llecnac | idtac ].
 653       set (nd_seq_reflexive(SequentCalculus:=@pl_sc  _ _ _ _ (SystemFCa Γ Δ))
 654         (mapOptionTree guestJudgmentAsGArrowType h @@@ lev)) as q.
 655       eapply nd_comp.
 656       eapply nd_prod.
 657       apply q.
 658       apply q.
 659       apply nd_rule.
 660       eapply (org_fc _ _ (RBindingGroup _ _ _ _ _ _ )).
 661       auto.
 662       auto.
 663
 664     (* nd_prod becomes nd_llecnac;;nd_prod;;RBindingGroup *)
 665     eapply nd_comp.
 666       apply (nd_llecnac ;; nd_prod IHX1 IHX2).
 667       apply nd_rule.
 668       eapply (org_fc _ _ (RBindingGroup _ _ _ _ _ _ )).
 669       auto.
 670
 671     (* nd_comp becomes pl_subst (aka nd_cut) *)
 672     eapply nd_comp.
 673       apply (nd_llecnac ;; nd_prod IHX1 IHX2).
 674       clear IHX1 IHX2 X1 X2.
 675       apply (@nd_cut _ _ _ _ _ _ (@pl_subst _ _ _ _ (SystemFCa Γ Δ))).
 676
 677     (* nd_cancell becomes RVar;;RuCanL *)
 678     eapply nd_comp;
 679       [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanL _))) ].
 680       apply (nd_seq_reflexive(SequentCalculus:=@pl_sc  _ _ _ _ (SystemFCa Γ Δ))).
 681       auto.
 682
 683     (* nd_cancelr becomes RVar;;RuCanR *)
 684     eapply nd_comp;
 685       [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanR _))) ].
 686       apply (nd_seq_reflexive(SequentCalculus:=@pl_sc  _ _ _ _ (SystemFCa Γ Δ))).
 687       auto.
 688
 689     (* nd_llecnac becomes RVar;;RCanL *)
 690     eapply nd_comp;
 691       [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanL _))) ].
 692       apply (nd_seq_reflexive(SequentCalculus:=@pl_sc  _ _ _ _ (SystemFCa Γ Δ))).
 693       auto.
 694
 695     (* nd_rlecnac becomes RVar;;RCanR *)
 696     eapply nd_comp;
 697       [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanR _))) ].
 698       apply (nd_seq_reflexive(SequentCalculus:=@pl_sc  _ _ _ _ (SystemFCa Γ Δ))).
 699       auto.
 700
 701     (* nd_assoc becomes RVar;;RAssoc *)
 702     eapply nd_comp;
 703       [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RAssoc _ _ _))) ].
 704       apply (nd_seq_reflexive(SequentCalculus:=@pl_sc  _ _ _ _ (SystemFCa Γ Δ))).
 705       auto.
 706
 707     (* nd_cossa becomes RVar;;RCossa *)
 708     eapply nd_comp;
 709       [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCossa _ _ _))) ].
 710       apply (nd_seq_reflexive(SequentCalculus:=@pl_sc  _ _ _ _ (SystemFCa Γ Δ))).
 711       auto.
 712
 713       destruct r as [r rp].
 714       refine (match rp as R in Rule_PCF _ _ _ H C _ with
 715                 | PCF_RArrange         h c r q          => let case_RURule        := tt in _
 716                 | PCF_RLit             lit              => let case_RLit          := tt in _
 717                 | PCF_RNote            Σ τ   n          => let case_RNote         := tt in _
 718                 | PCF_RVar             σ                => let case_RVar          := tt in _
 719                 | PCF_RLam             Σ tx te          => let case_RLam          := tt in _
 720                 | PCF_RApp             Σ tx te   p      => let case_RApp          := tt in _
 721                 | PCF_RLet             Σ σ₁ σ₂   p      => let case_RLet          := tt in _
 722                 | PCF_RBindingGroup    b c d e          => let case_RBindingGroup := tt in _
 723                 | PCF_REmptyGroup                       => let case_REmptyGroup   := tt in _
 724               (*| PCF_RCase            T κlen κ θ l x   => let case_RCase         := tt in _*)
 725               (*| PCF_RLetRec          Σ₁ τ₁ τ₂ lev     => let case_RLetRec       := tt in _*)
 726               end); simpl in *.
 727       clear rp.
 728       clear r h c.
 729       rename r0 into r; rename h0 into h; rename c0 into c.
 730
 731       destruct case_RURule.
 732         refine (match q with
 733           | RLeft   a b c r => let case_RLeft  := tt in _
 734           | RRight  a b c r => let case_RRight := tt in _
 735           | RCanL     b     => let case_RCanL  := tt in _
 736           | RCanR     b     => let case_RCanR  := tt in _
 737           | RuCanL    b     => let case_RuCanL := tt in _
 738           | RuCanR    b     => let case_RuCanR := tt in _
 739           | RAssoc    b c d => let case_RAssoc := tt in _
 740           | RCossa    b c d => let case_RCossa := tt in _
 741           | RExch     b c   => let case_RExch  := tt in _
 742           | RWeak     b     => let case_RWeak  := tt in _
 743           | RCont     b     => let case_RCont  := tt in _
 744           | RComp a b c f g => let case_RComp  := tt in _
 745         end).
 746
 747       destruct case_RCanL.
 748         (* ga_cancell *)
 749         admit.
 750
 751       destruct case_RCanR.
 752         (* ga_cancelr *)
 753         admit.
 754
 755       destruct case_RuCanL.
 756         (* ga_uncancell *)
 757         admit.
 758
 759       destruct case_RuCanR.
 760         (* ga_uncancelr *)
 761         admit.
 762
 763       destruct case_RAssoc.
 764         (* ga_assoc *)
 765         admit.
 766
 767       destruct case_RCossa.
 768         (* ga_unassoc *)
 769         admit.
 770
 771       destruct case_RExch.
 772         (* ga_swap *)
 773         admit.
 774
 775       destruct case_RWeak.
 776         (* ga_drop *)
 777         admit.
 778
 779       destruct case_RCont.
 780         (* ga_copy *)
 781         admit.
 782
 783       destruct case_RLeft.
 784         (* ga_second *)
 785         admit.
 786
 787       destruct case_RRight.
 788         (* ga_first *)
 789         admit.
 790
 791       destruct case_RComp.
 792         (* ga_comp *)
 793         admit.
 794
 795       destruct case_RLit.
 796         (* ga_literal *)
 797         admit.
 798
 799       (* hey cool, I figured out how to pass CoreNote's through... *)
 800       destruct case_RNote.
 801         eapply nd_comp.
 802         eapply nd_rule.
 803         eapply (org_fc _ _ (RVar _ _ _ _)) . auto.
 804         apply nd_rule.
 805         apply (org_fc _ _ (RNote _ _ _ _ _ n)). auto.
 806
 807       destruct case_RVar.
 808         (* ga_id *)
 809         admit.
 810
 811       destruct case_RLam.
 812         (* ga_curry, but try to avoid this someday in the future if the argument type isn't a function *)
 813         admit.
 814
 815       destruct case_RApp.
 816         (* ga_apply *)
 817         admit.
 818
 819       destruct case_RLet.
 820         (* ga_comp! perhaps this means the ga_curry avoidance can be done by turning lambdas into lets? *)
 821         admit.
 822
 823       destruct case_REmptyGroup.
 824         (* ga_id u *)
 825         admit.
 826
 827       destruct case_RBindingGroup.
 828         (* ga_first+ga_second; technically this assumes a specific evaluation order, which is bad *)
 829         admit.
 830
 831       Defined.
 832
 833   Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL _ _ (PCF Γ Δ ec)) (TypesL _ _ (SystemFCa Γ Δ)) (obact ec) :=
 834     { fmor := FlatteningFunctor_fmor }.
 835     admit.
 836     admit.
 837     admit.
 838     Defined.
 839 (*
 840     Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
 841       refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
 842       unfold ReificationFunctor_fmor; simpl.
 843       admit.
 844       unfold ReificationFunctor_fmor; simpl.
 845       admit.
 846       unfold ReificationFunctor_fmor; simpl.
 847       admit.
 848       Defined.
 849
 850
 851   Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
 852     refine {| plsmme_pl := PCF n Γ Δ |}.
 853     admit.
 854     Defined.
 855
 856   Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
 857     refine {| plsmme_pl := SystemFCa n Γ Δ |}.
 858     admit.
 859     Defined.
 860
 861   Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
 862     admit.
 863     Defined.
 864
 865   (* 5.1.4 *)
 866   Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
 867     admit.
 868     (*  ... and the retraction exists *)
 869     Defined.
 870 *)
 871   (* Any particular proof in HaskProof is only finitely large, so it uses only finitely many levels of nesting, so
 872    * it falls within (SystemFCa n) for some n.  This function calculates that "n" and performs the translation *)
 873   (*
 874   Definition HaskProof_to_SystemFCa :
 875     forall h c (pf:ND Rule h c),
 876       { n:nat & h ~~{JudgmentsL (SystemFCa_SMME n)}~~> c }.
 877       *)
 878
 879   (* for every n we have a functor from the category of (n+1)-bounded proofs to the category of n-bounded proofs *)
 880
 881
 882
 883 End HaskProofCategory.
 884
 885 (*
 886   Definition code2garrow0 {Γ}(ec t1 t2:RawHaskType Γ ★) : RawHaskType Γ ★.
 887     admit.
 888     Defined.
 889   Definition code2garrow Γ (ec t:RawHaskType Γ ★) :=
 890       match t with
 891 (*        | TApp ★ ★ (TApp _ ★ TArrow tx) t' => code2garrow0 ec tx       t'*)
 892         |                               _  => code2garrow0 ec unitType t
 893       end.
 894   Opaque code2garrow.
 895   Fixpoint typeMap {TV}{κ}(ty:@RawHaskType TV κ) : @RawHaskType TV κ :=
 896       match ty as TY in RawHaskType _ K return RawHaskType TV K with
 897         | TCode ec t        => code2garrow _ ec t
 898         | TApp _ _ t1 t2    => TApp (typeMap t1) (typeMap t2)
 899         | TAll _ f          => TAll _ (fun tv => typeMap (f tv))
 900         | TCoerc _ t1 t2 t3 => TCoerc (typeMap t1) (typeMap t2) (typeMap t3)
 901         | TVar   _ v        => TVar v
 902         | TArrow            => TArrow
 903         | TCon  tc          => TCon tc
 904         | TyFunApp  tf rhtl => (* FIXME *) TyFunApp tf rhtl
 905       end.
 906 *)
 907
 908