src/HaskProofStratified.v

   1 (*********************************************************************************************************************************)
   2 (* HaskProofStratified:                                                                                                          *)
   3 (*                                                                                                                               *)
   4 (*    An alternate representation for HaskProof which ensures that deductions on a given level are grouped into contiguous       *)
   5 (*    blocks.  This representation lacks the attractive compositionality properties of HaskProof, but makes it easier to         *)
   6 (*    perform the flattening process.                                                                                            *)
   7 (*                                                                                                                               *)
   8 (*********************************************************************************************************************************)
   9
  10 Generalizable All Variables.
  11 Require Import Preamble.
  12 Require Import General.
  13 Require Import NaturalDeduction.
  14 Require Import Coq.Strings.String.
  15 Require Import Coq.Lists.List.
  16
  17 Require Import HaskKinds.
  18 Require Import HaskCoreTypes.
  19 Require Import HaskLiteralsAndTyCons.
  20 Require Import HaskStrongTypes.
  21 Require Import HaskProof.
  22 Require Import NaturalDeduction.
  23 Require Import NaturalDeductionCategory.
  24
  25 Require Import Algebras_ch4.
  26 Require Import Categories_ch1_3.
  27 Require Import Functors_ch1_4.
  28 Require Import Isomorphisms_ch1_5.
  29 Require Import ProductCategories_ch1_6_1.
  30 Require Import OppositeCategories_ch1_6_2.
  31 Require Import Enrichment_ch2_8.
  32 Require Import Subcategories_ch7_1.
  33 Require Import NaturalTransformations_ch7_4.
  34 Require Import NaturalIsomorphisms_ch7_5.
  35 Require Import MonoidalCategories_ch7_8.
  36 Require Import Coherence_ch7_8.
  37
  38 Require Import HaskStrongTypes.
  39 Require Import HaskStrong.
  40 Require Import HaskProof.
  41 Require Import HaskStrongToProof.
  42 Require Import HaskProofToStrong.
  43 Require Import ProgrammingLanguage.
  44
  45 Open Scope nd_scope.
  46
  47
  48 (*
  49  *  The flattening transformation.  Currently only TWO-level languages are
  50  *  supported, and the level-1 sublanguage is rather limited.
  51 *
  52  *  This file abuses terminology pretty badly.  For purposes of this file,
  53  *  "PCF" means "the level-1 sublanguage" and "FC" (aka System FC) means
  54  *  the whole language (level-0 language including bracketed level-1 terms)
  55  *)
  56 Section HaskProofStratified.
  57
  58   Context (ndr_systemfc:@ND_Relation _ Rule).
  59
  60   Inductive PCFJudg Γ (Δ:CoercionEnv Γ) (ec:HaskTyVar Γ ★) :=
  61     pcfjudg : Tree ??(HaskType Γ ★) -> Tree ??(HaskType Γ ★) -> PCFJudg Γ Δ ec.
  62     Implicit Arguments pcfjudg [ [Γ] [Δ] [ec] ].
  63
  64   (* given an PCFJudg at depth (ec::depth) we can turn it into an PCFJudg
  65    * from depth (depth) by wrapping brackets around everything in the
  66    * succedent and repopulating *)
  67   Definition brakify {Γ}{Δ}{ec} (j:PCFJudg Γ Δ ec) : Judg :=
  68     match j with
  69       pcfjudg Σ τ => Γ > Δ > (Σ@@@(ec::nil)) |- (mapOptionTree (fun t => HaskBrak ec t) τ @@@ nil)
  70       end.
  71
  72   Definition pcf_vars {Γ}(ec:HaskTyVar Γ ★)(t:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★)
  73     := mapOptionTreeAndFlatten (fun lt =>
  74       match lt with t @@ l => match l with
  75                                 | ec'::nil => if eqd_dec ec ec' then [t] else []
  76                                 | _ => []
  77                               end
  78       end) t.
  79
  80   Inductive MatchingJudgments {Γ}{Δ}{ec} : Tree ??(PCFJudg Γ Δ ec) -> Tree ??Judg -> Type :=
  81     | match_nil    : MatchingJudgments [] []
  82     | match_branch : forall a b c d, MatchingJudgments a b -> MatchingJudgments c d -> MatchingJudgments (a,,c) (b,,d)
  83     | match_leaf   :
  84       forall Σ τ lev,
  85         MatchingJudgments
  86           [pcfjudg (pcf_vars ec Σ)                               τ         ]
  87           [Γ > Δ >              Σ  |- (mapOptionTree (HaskBrak ec) τ @@@ lev)].
  88
  89   Definition fc_vars {Γ}(ec:HaskTyVar Γ ★)(t:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★)
  90     := mapOptionTreeAndFlatten (fun lt =>
  91       match lt with t @@ l => match l with
  92                                 | ec'::nil => if eqd_dec ec ec' then [] else [t]
  93                                 | _ => []
  94                               end
  95       end) t.
  96
  97   Definition pcfjudg2judg {Γ}{Δ:CoercionEnv Γ} ec (cj:PCFJudg Γ Δ ec) :=
  98     match cj with pcfjudg Σ τ => Γ > Δ > (Σ @@@ (ec::nil)) |- (τ @@@ (ec::nil)) end.
  99
 100   (* Rules allowed in PCF; i.e. rules we know how to turn into GArrows     *)
 101   (* Rule_PCF consists of the rules allowed in flat PCF: everything except *)
 102   (* AppT, AbsT, AppC, AbsC, Cast, Global, and some Case statements        *)
 103   Inductive Rule_PCF {Γ}{Δ:CoercionEnv Γ} (ec:HaskTyVar Γ ★)
 104     : forall (h c:Tree ??(PCFJudg Γ Δ ec)), Rule (mapOptionTree (pcfjudg2judg ec) h) (mapOptionTree (pcfjudg2judg ec) c) -> Type :=
 105   | PCF_RArrange    : ∀ x y t     a,  Rule_PCF ec [pcfjudg _  _ ] [ pcfjudg _  _  ] (RArrange Γ Δ (x@@@(ec::nil)) (y@@@(ec::nil)) (t@@@(ec::nil)) a)
 106   | PCF_RLit        : ∀ lit        ,  Rule_PCF ec [           ] [ pcfjudg [] [_] ] (RLit   Γ Δ  lit (ec::nil))
 107   | PCF_RNote       : ∀ Σ τ   n    ,  Rule_PCF ec [pcfjudg _ [_]] [ pcfjudg _ [_] ] (RNote  Γ Δ  (Σ@@@(ec::nil)) τ         (ec::nil) n)
 108   | PCF_RVar        : ∀ σ          ,  Rule_PCF ec [           ] [ pcfjudg [_] [_] ] (RVar   Γ Δ    σ         (ec::nil)  )
 109   | PCF_RLam        : ∀ Σ tx te    ,  Rule_PCF ec [pcfjudg (_,,[_]) [_] ] [ pcfjudg _ [_] ] (RLam   Γ Δ  (Σ@@@(ec::nil)) tx te  (ec::nil)  )
 110
 111   | PCF_RApp             : ∀ Σ Σ' tx te ,
 112     Rule_PCF ec ([pcfjudg _ [_]],,[pcfjudg _ [_]]) [pcfjudg (_,,_) [_]]
 113     (RApp Γ Δ (Σ@@@(ec::nil))(Σ'@@@(ec::nil)) tx te (ec::nil))
 114
 115   | PCF_RLet             : ∀ Σ Σ' σ₂   p,
 116     Rule_PCF ec ([pcfjudg _ [_]],,[pcfjudg (_,,[_]) [_]]) [pcfjudg (_,,_) [_]]
 117     (RLet Γ Δ (Σ@@@(ec::nil)) (Σ'@@@(ec::nil)) σ₂ p (ec::nil))
 118
 119   | PCF_RVoid      :                 Rule_PCF ec [           ] [ pcfjudg []  [] ] (RVoid   Γ Δ  )
 120 (*| PCF_RLetRec          : ∀ Σ₁ τ₁ τ₂   ,  Rule_PCF (ec::nil) _ _ (RLetRec Γ Δ Σ₁ τ₁ τ₂ (ec::nil) )*)
 121   | PCF_RJoin    : ∀ Σ₁ Σ₂ τ₁ τ₂,  Rule_PCF ec ([pcfjudg _ _],,[pcfjudg _ _]) [pcfjudg (_,,_) (_,,_)]
 122     (RJoin Γ Δ (Σ₁@@@(ec::nil)) (Σ₂@@@(ec::nil)) (τ₁@@@(ec::nil)) (τ₂@@@(ec::nil))).
 123   (* need int/boolean case *)
 124   Implicit Arguments Rule_PCF [ ].
 125
 126   Definition PCFRule Γ Δ lev h c := { r:_ & @Rule_PCF Γ Δ lev h c r }.
 127
 128   (* An organized deduction has been reorganized into contiguous blocks whose
 129    * hypotheses (if any) and conclusion have the same Γ and Δ and a fixed nesting depth.  The boolean
 130    * indicates if non-PCF rules have been used *)
 131   Inductive OrgR : Tree ??Judg -> Tree ??Judg -> Type :=
 132
 133   | org_fc        : forall h c (r:Rule h c),
 134     Rule_Flat r ->
 135     OrgR h c
 136
 137   | org_pcf      : forall Γ Δ ec h h' c c',
 138     MatchingJudgments    h  h' ->
 139     MatchingJudgments    c  c' ->
 140     ND (PCFRule Γ Δ ec)  h  c  ->
 141     OrgR                 h' c'.
 142
 143   Definition mkEsc {Γ}{Δ}{ec}(h:Tree ??(PCFJudg Γ Δ ec))
 144     : ND Rule
 145     (mapOptionTree brakify h)
 146     (mapOptionTree (pcfjudg2judg ec) h).
 147     apply nd_replicate; intros.
 148     destruct o; simpl in *.
 149     induction t0.
 150     destruct a; simpl.
 151     apply nd_rule.
 152     apply REsc.
 153     apply nd_id.
 154     apply (Prelude_error "mkEsc got multi-leaf succedent").
 155     Defined.
 156
 157   Definition mkBrak {Γ}{Δ}{ec}(h:Tree ??(PCFJudg Γ Δ ec))
 158     : ND Rule
 159     (mapOptionTree (pcfjudg2judg ec) h)
 160     (mapOptionTree brakify h).
 161     apply nd_replicate; intros.
 162     destruct o; simpl in *.
 163     induction t0.
 164     destruct a; simpl.
 165     apply nd_rule.
 166     apply RBrak.
 167     apply nd_id.
 168     apply (Prelude_error "mkBrak got multi-leaf succedent").
 169     Defined.
 170
 171     (*
 172   Definition Partition {Γ} ec (Σ:Tree ??(LeveledHaskType Γ ★)) :=
 173     { vars:(_ * _) |
 174       fc_vars  ec Σ = fst vars /\
 175       pcf_vars ec Σ = snd vars }.
 176       *)
 177
 178   Definition pcfToND : forall Γ Δ ec h c,
 179     ND (PCFRule Γ Δ ec) h c -> ND Rule (mapOptionTree (pcfjudg2judg ec) h) (mapOptionTree (pcfjudg2judg ec) c).
 180     intros.
 181     eapply (fun q => nd_map' _ q X).
 182     intros.
 183     destruct X0.
 184     apply nd_rule.
 185     apply x.
 186     Defined.
 187
 188   Instance OrgPCF Γ Δ lev : @ND_Relation _ (PCFRule Γ Δ lev) :=
 189     { ndr_eqv := fun a b f g => (pcfToND _ _ _ _ _ f) === (pcfToND _ _ _ _ _ g) }.
 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       admit.
 203       Defined.
 204
 205   (*
 206    * An intermediate representation necessitated by Coq's termination
 207    * conditions.  This is basically a tree where each node is a
 208    * subproof which is either entirely level-1 or entirely level-0
 209    *)
 210   Inductive Alternating : Tree ??Judg -> Type :=
 211
 212     | alt_nil    : Alternating []
 213
 214     | alt_branch : forall a b,
 215       Alternating a -> Alternating b -> Alternating (a,,b)
 216
 217     | alt_fc     : forall h c,
 218       Alternating h ->
 219       ND Rule h c ->
 220       Alternating c
 221
 222     | alt_pcf    : forall Γ Δ ec h c h' c',
 223       MatchingJudgments    h  h' ->
 224       MatchingJudgments    c  c' ->
 225       Alternating h' ->
 226       ND (PCFRule Γ Δ ec) h c ->
 227       Alternating c'.
 228
 229   Require Import Coq.Logic.Eqdep.
 230
 231   Lemma magic a b c d ec e :
 232     ClosedSIND(Rule:=Rule) [a > b > c |- [d @@  (ec :: e)]] ->
 233     ClosedSIND(Rule:=Rule) [a > b > pcf_vars ec c @@@ (ec :: nil) |- [d @@  (ec :: nil)]].
 234   admit.
 235   Defined.
 236
 237   Definition orgify : forall Γ Δ Σ τ (pf:ClosedSIND(Rule:=Rule) [Γ > Δ > Σ |- τ]), Alternating [Γ > Δ > Σ |- τ].
 238
 239     refine (
 240       fix  orgify_fc' Γ Δ Σ τ (pf:ClosedSIND [Γ > Δ > Σ |- τ]) {struct pf} : Alternating [Γ > Δ > Σ |- τ] :=
 241         let case_main := tt in _
 242       with orgify_fc c (pf:ClosedSIND c) {struct pf} : Alternating c :=
 243       (match c as C return C=c -> Alternating C with
 244         | T_Leaf None                    => fun _ => alt_nil
 245         | T_Leaf (Some (Γ > Δ > Σ |- τ)) => let case_leaf := tt in fun eqpf => _
 246         | T_Branch b1 b2                 => let case_branch := tt in fun eqpf => _
 247       end (refl_equal _))
 248       with orgify_pcf   Γ Δ ec pcfj j (m:MatchingJudgments pcfj j)
 249         (pf:ClosedSIND (mapOptionTree (pcfjudg2judg ec) pcfj)) {struct pf} : Alternating j :=
 250         let case_pcf := tt in _
 251       for orgify_fc').
 252
 253       destruct case_main.
 254       inversion pf; subst.
 255       set (alt_fc _ _ (orgify_fc _ X) (nd_rule X0)) as backup.
 256       refine (match X0 as R in Rule H C return
 257                 match C with
 258                   | T_Leaf (Some (Γ > Δ > Σ |- τ)) =>
 259                     h=H -> Alternating [Γ > Δ > Σ |- τ] -> Alternating [Γ > Δ > Σ |- τ]
 260                   | _                              => True
 261                 end
 262                  with
 263                 | RBrak   Σ a b c n m           => let case_RBrak := tt         in fun pf' backup => _
 264                 | REsc    Σ a b c n m           => let case_REsc := tt          in fun pf' backup => _
 265                 | _ => fun pf' x => x
 266               end (refl_equal _) backup).
 267       clear backup0 backup.
 268
 269       destruct case_RBrak.
 270         rename c into ec.
 271         set (@match_leaf Σ0 a ec n [b] m) as q.
 272         set (orgify_pcf Σ0 a ec _ _ q) as q'.
 273         apply q'.
 274         simpl.
 275         rewrite pf' in X.
 276         apply magic in X.
 277         apply X.
 278
 279       destruct case_REsc.
 280         apply (Prelude_error "encountered Esc in wrong side of mkalt").
 281
 282     destruct case_leaf.
 283       apply orgify_fc'.
 284       rewrite eqpf.
 285       apply pf.
 286
 287     destruct case_branch.
 288       rewrite <- eqpf in pf.
 289       inversion pf; subst.
 290       apply no_rules_with_multiple_conclusions in X0.
 291       inversion X0.
 292       exists b1. exists b2.
 293       auto.
 294       apply (alt_branch _ _ (orgify_fc _ X) (orgify_fc _ X0)).
 295
 296     destruct case_pcf.
 297     Admitted.
 298
 299   Definition pcfify Γ Δ ec : forall Σ τ,
 300     ClosedSIND(Rule:=Rule) [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)]
 301       -> ND (PCFRule Γ Δ ec) [] [pcfjudg Σ τ].
 302
 303     refine ((
 304       fix pcfify Σ τ (pn:@ClosedSIND _ Rule [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)]) {struct pn}
 305       : ND (PCFRule Γ Δ ec) [] [pcfjudg Σ τ] :=
 306      (match pn in @ClosedSIND _ _ J return J=[Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)] -> _ with
 307       | cnd_weak             => let case_nil    := tt in _
 308       | cnd_rule h c cnd' r  => let case_rule   := tt in _
 309       | cnd_branch _ _ c1 c2 => let case_branch := tt in _
 310       end (refl_equal _)))).
 311       intros.
 312       inversion H.
 313       intros.
 314       destruct c; try destruct o; inversion H.
 315       destruct j.
 316       Admitted.
 317
 318   (* any proof in organized form can be "dis-organized" *)
 319   Definition unOrgR : forall h c, OrgR h c -> ND Rule h c.
 320     intros.
 321
 322     induction X.
 323       apply nd_rule.
 324       apply r.
 325
 326     eapply nd_comp.
 327       (*
 328       apply (mkEsc h).
 329       eapply nd_comp; [ idtac |  apply (mkBrak c) ].
 330       apply pcfToND.
 331       apply n.
 332       *)
 333       Admitted.
 334
 335   Definition unOrgND h c :  ND OrgR h c -> ND Rule h c := nd_map unOrgR.
 336
 337   Instance OrgNDR : @ND_Relation _ OrgR :=
 338     { ndr_eqv := fun a b f g => (unOrgND _ _ f) === (unOrgND _ _ g) }.
 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       admit.
 352       Defined.
 353
 354   Hint Constructors Rule_Flat.
 355
 356   Instance PCF_sequents Γ Δ lev : @SequentCalculus _ (PCFRule Γ Δ lev) _ pcfjudg.
 357     apply Build_SequentCalculus.
 358     intros.
 359     induction a.
 360     destruct a; simpl.
 361     apply nd_rule.
 362       exists (RVar _ _ _ _).
 363       apply PCF_RVar.
 364     apply nd_rule.
 365       exists (RVoid _ _ ).
 366       apply PCF_RVoid.
 367     eapply nd_comp.
 368       eapply nd_comp; [ apply nd_llecnac | idtac ].
 369       apply (nd_prod IHa1 IHa2).
 370       apply nd_rule.
 371         exists (RJoin _ _ _ _ _ _).
 372         apply PCF_RJoin.
 373         Defined.
 374
 375   Definition PCF_Arrange {Γ}{Δ}{lev} : forall x y z, Arrange x y -> ND (PCFRule Γ Δ lev) [pcfjudg x z] [pcfjudg y z].
 376     admit.
 377     Defined.
 378
 379   Definition PCF_cut Γ Δ lev : forall a b c, ND (PCFRule Γ Δ lev) ([ pcfjudg a b ],,[ pcfjudg b c ]) [ pcfjudg a c ].
 380     intros.
 381     destruct b.
 382     destruct o.
 383     destruct c.
 384     destruct o.
 385
 386     (* when the cut is a single leaf and the RHS is a single leaf: *)
 387     eapply nd_comp.
 388       eapply nd_prod.
 389       apply nd_id.
 390       apply (PCF_Arrange [h] ([],,[h]) [h0]).
 391       apply RuCanL.
 392       eapply nd_comp; [ idtac | apply (PCF_Arrange ([],,a) a [h0]); apply RCanL ].
 393       apply nd_rule.
 394 (*
 395       set (@RLet Γ Δ [] (a@@@(ec::nil)) h0 h (ec::nil)) as q.
 396       exists q.
 397       apply (PCF_RLet _ [] a h0 h).
 398     apply (Prelude_error "cut rule invoked with [a|=[b]] [[b]|=[]]").
 399     apply (Prelude_error "cut rule invoked with [a|=[b]] [[b]|=[x,,y]]").
 400     apply (Prelude_error "cut rule invoked with [a|=[]]  [[]|=c]").
 401     apply (Prelude_error "cut rule invoked with [a|=[b,,c]] [[b,,c]|=z]").
 402 *)
 403     admit.
 404     admit.
 405     admit.
 406     admit.
 407     admit.
 408     Defined.
 409
 410   Instance PCF_cutrule Γ Δ lev : CutRule (PCF_sequents Γ Δ lev) :=
 411     { nd_cut := PCF_cut Γ Δ lev }.
 412     admit.
 413     admit.
 414     admit.
 415     Defined.
 416
 417   Definition PCF_left Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [pcfjudg b c] [pcfjudg (a,,b) (a,,c)].
 418     eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ].
 419     eapply nd_prod; [ apply nd_seq_reflexive | apply nd_id ].
 420     apply nd_rule.
 421     set (@PCF_RJoin Γ Δ lev a b a c) as q'.
 422     refine (existT _ _ _).
 423     apply q'.
 424     Defined.
 425
 426   Definition PCF_right Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [pcfjudg b c] [pcfjudg (b,,a) (c,,a)].
 427     eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ].
 428     eapply nd_prod; [ apply nd_id | apply nd_seq_reflexive ].
 429     apply nd_rule.
 430     set (@PCF_RJoin Γ Δ lev b a c a) as q'.
 431     refine (existT _ _ _).
 432     apply q'.
 433     Defined.
 434
 435   Instance PCF_sequent_join Γ Δ lev : @SequentExpansion _ _ _ _ _ (PCF_sequents Γ Δ lev) (PCF_cutrule Γ Δ lev) :=
 436   { se_expand_left  := PCF_left  Γ Δ lev
 437   ; se_expand_right := PCF_right Γ Δ lev }.
 438     admit.
 439     admit.
 440     admit.
 441     admit.
 442     Defined.
 443
 444   (* 5.1.3 *)
 445   Instance PCF Γ Δ lev : @ProgrammingLanguage _ _ pcfjudg (PCFRule Γ Δ lev) :=
 446   { pl_eqv                := OrgPCF Γ Δ lev
 447   ; pl_sc                 := PCF_sequents Γ Δ lev
 448   ; pl_subst              := PCF_cutrule Γ Δ lev
 449   ; pl_sequent_join       := PCF_sequent_join Γ Δ lev
 450   }.
 451     apply Build_TreeStructuralRules; intros; unfold eqv; unfold hom; simpl.
 452
 453     apply nd_rule. unfold PCFRule. simpl.
 454       exists (RArrange _ _ _ _ _ (RCossa _ _ _)).
 455       apply (PCF_RArrange lev ((a,,b),,c) (a,,(b,,c)) x).
 456
 457     apply nd_rule. unfold PCFRule. simpl.
 458       exists (RArrange _ _ _ _ _ (RAssoc _ _ _)).
 459       apply (PCF_RArrange lev (a,,(b,,c)) ((a,,b),,c) x).
 460
 461     apply nd_rule. unfold PCFRule. simpl.
 462       exists (RArrange _ _ _ _ _ (RCanL _)).
 463       apply (PCF_RArrange lev ([],,a) _ _).
 464
 465     apply nd_rule. unfold PCFRule. simpl.
 466       exists (RArrange _ _ _ _ _ (RCanR _)).
 467       apply (PCF_RArrange lev (a,,[]) _ _).
 468
 469     apply nd_rule. unfold PCFRule. simpl.
 470       exists (RArrange _ _ _ _ _ (RuCanL _)).
 471       apply (PCF_RArrange lev _ ([],,a) _).
 472
 473     apply nd_rule. unfold PCFRule. simpl.
 474       exists (RArrange _ _ _ _ _ (RuCanR _)).
 475       apply (PCF_RArrange lev _ (a,,[]) _).
 476       Defined.
 477
 478   Instance SystemFCa_sequents Γ Δ : @SequentCalculus _ OrgR _ (mkJudg Γ Δ).
 479     apply Build_SequentCalculus.
 480     intros.
 481     induction a.
 482     destruct a; simpl.
 483     apply nd_rule.
 484       destruct l.
 485       apply org_fc with (r:=RVar _ _ _ _).
 486       auto.
 487     apply nd_rule.
 488       apply org_fc with (r:=RVoid _ _ ).
 489       auto.
 490     eapply nd_comp.
 491       eapply nd_comp; [ apply nd_llecnac | idtac ].
 492       apply (nd_prod IHa1 IHa2).
 493       apply nd_rule.
 494         apply org_fc with (r:=RJoin _ _ _ _ _ _).
 495         auto.
 496         Defined.
 497
 498   Definition SystemFCa_cut Γ Δ : forall a b c, ND OrgR ([ Γ > Δ > a |- b ],,[ Γ > Δ > b |- c ]) [ Γ > Δ > a |- c ].
 499     intros.
 500     destruct b.
 501     destruct o.
 502     destruct c.
 503     destruct o.
 504
 505     (* when the cut is a single leaf and the RHS is a single leaf: *)
 506     eapply nd_comp.
 507       eapply nd_prod.
 508       apply nd_id.
 509       eapply nd_rule.
 510       apply org_fc with (r:=RArrange _ _ _ _ _ (RuCanL [l])).
 511       auto.
 512       eapply nd_comp; [ idtac | eapply nd_rule; apply org_fc with (r:=RArrange _ _ _ _ _ (RCanL _)) ].
 513       apply nd_rule.
 514       destruct l.
 515       destruct l0.
 516       assert (h0=h2). admit.
 517       subst.
 518       apply org_fc with (r:=@RLet Γ Δ [] a h1 h h2).
 519       auto.
 520       auto.
 521     apply (Prelude_error "systemfc cut rule invoked with [a|=[b]] [[b]|=[]]").
 522     apply (Prelude_error "systemfc cut rule invoked with [a|=[b]] [[b]|=[x,,y]]").
 523     apply (Prelude_error "systemfc rule invoked with [a|=[]]  [[]|=c]").
 524     apply (Prelude_error "systemfc rule invoked with [a|=[b,,c]] [[b,,c]|=z]").
 525     Defined.
 526
 527   Instance SystemFCa_cutrule Γ Δ : CutRule (SystemFCa_sequents Γ Δ) :=
 528     { nd_cut := SystemFCa_cut Γ Δ }.
 529     admit.
 530     admit.
 531     admit.
 532     Defined.
 533
 534   Definition SystemFCa_left Γ Δ a b c : ND OrgR [Γ > Δ > b |- c] [Γ > Δ > (a,,b) |- (a,,c)].
 535     eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ].
 536     eapply nd_prod; [ apply nd_seq_reflexive | apply nd_id ].
 537     apply nd_rule.
 538     apply org_fc with (r:=RJoin Γ Δ a b a c).
 539     auto.
 540     Defined.
 541
 542   Definition SystemFCa_right Γ Δ a b c : ND OrgR [Γ > Δ > b |- c] [Γ > Δ > (b,,a) |- (c,,a)].
 543     eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ].
 544     eapply nd_prod; [ apply nd_id | apply nd_seq_reflexive ].
 545     apply nd_rule.
 546     apply org_fc with (r:=RJoin Γ Δ b a c a).
 547     auto.
 548     Defined.
 549
 550   Instance SystemFCa_sequent_join Γ Δ : @SequentExpansion _ _ _ _ _ (SystemFCa_sequents Γ Δ) (SystemFCa_cutrule Γ Δ) :=
 551   { se_expand_left  := SystemFCa_left  Γ Δ
 552   ; se_expand_right := SystemFCa_right Γ Δ }.
 553     admit.
 554     admit.
 555     admit.
 556     admit.
 557     Defined.
 558
 559   (* 5.1.2 *)
 560   Instance SystemFCa Γ Δ : @ProgrammingLanguage _ _ (mkJudg Γ Δ) OrgR :=
 561   { pl_eqv                := OrgNDR
 562   ; pl_sc                 := SystemFCa_sequents     Γ Δ
 563   ; pl_subst              := SystemFCa_cutrule      Γ Δ
 564   ; pl_sequent_join       := SystemFCa_sequent_join Γ Δ
 565   }.
 566     apply Build_TreeStructuralRules; intros; unfold eqv; unfold hom; simpl.
 567     apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RCossa a b c))). apply Flat_RArrange.
 568     apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RAssoc a b c))). apply Flat_RArrange.
 569     apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanL  a    ))). apply Flat_RArrange.
 570     apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanR  a    ))). apply Flat_RArrange.
 571     apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanL a    ))). apply Flat_RArrange.
 572     apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanR a    ))). apply Flat_RArrange.
 573     Defined.
 574
 575 End HaskProofStratified.