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       Defined.
 202
 203   (*
 204    * An intermediate representation necessitated by Coq's termination
 205    * conditions.  This is basically a tree where each node is a
 206    * subproof which is either entirely level-1 or entirely level-0
 207    *)
 208   Inductive Alternating : Tree ??Judg -> Type :=
 209
 210     | alt_nil    : Alternating []
 211
 212     | alt_branch : forall a b,
 213       Alternating a -> Alternating b -> Alternating (a,,b)
 214
 215     | alt_fc     : forall h c,
 216       Alternating h ->
 217       ND Rule h c ->
 218       Alternating c
 219
 220     | alt_pcf    : forall Γ Δ ec h c h' c',
 221       MatchingJudgments    h  h' ->
 222       MatchingJudgments    c  c' ->
 223       Alternating h' ->
 224       ND (PCFRule Γ Δ ec) h c ->
 225       Alternating c'.
 226
 227   Require Import Coq.Logic.Eqdep.
 228
 229   Lemma magic a b c d ec e :
 230     ClosedSIND(Rule:=Rule) [a > b > c |- [d @@  (ec :: e)]] ->
 231     ClosedSIND(Rule:=Rule) [a > b > pcf_vars ec c @@@ (ec :: nil) |- [d @@  (ec :: nil)]].
 232   admit.
 233   Defined.
 234
 235   Definition orgify : forall Γ Δ Σ τ (pf:ClosedSIND(Rule:=Rule) [Γ > Δ > Σ |- τ]), Alternating [Γ > Δ > Σ |- τ].
 236
 237     refine (
 238       fix  orgify_fc' Γ Δ Σ τ (pf:ClosedSIND [Γ > Δ > Σ |- τ]) {struct pf} : Alternating [Γ > Δ > Σ |- τ] :=
 239         let case_main := tt in _
 240       with orgify_fc c (pf:ClosedSIND c) {struct pf} : Alternating c :=
 241       (match c as C return C=c -> Alternating C with
 242         | T_Leaf None                    => fun _ => alt_nil
 243         | T_Leaf (Some (Γ > Δ > Σ |- τ)) => let case_leaf := tt in fun eqpf => _
 244         | T_Branch b1 b2                 => let case_branch := tt in fun eqpf => _
 245       end (refl_equal _))
 246       with orgify_pcf   Γ Δ ec pcfj j (m:MatchingJudgments pcfj j)
 247         (pf:ClosedSIND (mapOptionTree (pcfjudg2judg ec) pcfj)) {struct pf} : Alternating j :=
 248         let case_pcf := tt in _
 249       for orgify_fc').
 250
 251       destruct case_main.
 252       inversion pf; subst.
 253       set (alt_fc _ _ (orgify_fc _ X) (nd_rule X0)) as backup.
 254       refine (match X0 as R in Rule H C return
 255                 match C with
 256                   | T_Leaf (Some (Γ > Δ > Σ |- τ)) =>
 257                     h=H -> Alternating [Γ > Δ > Σ |- τ] -> Alternating [Γ > Δ > Σ |- τ]
 258                   | _                              => True
 259                 end
 260                  with
 261                 | RBrak   Σ a b c n m           => let case_RBrak := tt         in fun pf' backup => _
 262                 | REsc    Σ a b c n m           => let case_REsc := tt          in fun pf' backup => _
 263                 | _ => fun pf' x => x
 264               end (refl_equal _) backup).
 265       clear backup0 backup.
 266
 267       destruct case_RBrak.
 268         rename c into ec.
 269         set (@match_leaf Σ0 a ec n [b] m) as q.
 270         set (orgify_pcf Σ0 a ec _ _ q) as q'.
 271         apply q'.
 272         simpl.
 273         rewrite pf' in X.
 274         apply magic in X.
 275         apply X.
 276
 277       destruct case_REsc.
 278         apply (Prelude_error "encountered Esc in wrong side of mkalt").
 279
 280     destruct case_leaf.
 281       apply orgify_fc'.
 282       rewrite eqpf.
 283       apply pf.
 284
 285     destruct case_branch.
 286       rewrite <- eqpf in pf.
 287       inversion pf; subst.
 288       apply no_rules_with_multiple_conclusions in X0.
 289       inversion X0.
 290       exists b1. exists b2.
 291       auto.
 292       apply (alt_branch _ _ (orgify_fc _ X) (orgify_fc _ X0)).
 293
 294     destruct case_pcf.
 295     Admitted.
 296
 297   Definition pcfify Γ Δ ec : forall Σ τ,
 298     ClosedSIND(Rule:=Rule) [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)]
 299       -> ND (PCFRule Γ Δ ec) [] [pcfjudg Σ τ].
 300
 301     refine ((
 302       fix pcfify Σ τ (pn:@ClosedSIND _ Rule [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)]) {struct pn}
 303       : ND (PCFRule Γ Δ ec) [] [pcfjudg Σ τ] :=
 304      (match pn in @ClosedSIND _ _ J return J=[Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)] -> _ with
 305       | cnd_weak             => let case_nil    := tt in _
 306       | cnd_rule h c cnd' r  => let case_rule   := tt in _
 307       | cnd_branch _ _ c1 c2 => let case_branch := tt in _
 308       end (refl_equal _)))).
 309       intros.
 310       inversion H.
 311       intros.
 312       destruct c; try destruct o; inversion H.
 313       destruct j.
 314       Admitted.
 315
 316   (* any proof in organized form can be "dis-organized" *)
 317   Definition unOrgR : forall h c, OrgR h c -> ND Rule h c.
 318     intros.
 319
 320     induction X.
 321       apply nd_rule.
 322       apply r.
 323
 324     eapply nd_comp.
 325       (*
 326       apply (mkEsc h).
 327       eapply nd_comp; [ idtac |  apply (mkBrak c) ].
 328       apply pcfToND.
 329       apply n.
 330       *)
 331       Admitted.
 332
 333   Definition unOrgND h c :  ND OrgR h c -> ND Rule h c := nd_map unOrgR.
 334
 335   Instance OrgNDR : @ND_Relation _ OrgR :=
 336     { ndr_eqv := fun a b f g => (unOrgND _ _ f) === (unOrgND _ _ g) }.
 337       admit.
 338       admit.
 339       admit.
 340       admit.
 341       admit.
 342       admit.
 343       admit.
 344       admit.
 345       admit.
 346       admit.
 347       admit.
 348       Defined.
 349
 350   Hint Constructors Rule_Flat.
 351
 352   Definition PCF_Arrange {Γ}{Δ}{lev} : forall x y z, Arrange x y -> ND (PCFRule Γ Δ lev) [pcfjudg x z] [pcfjudg y z].
 353     admit.
 354     Defined.
 355
 356   Definition PCF_cut Γ Δ lev : forall a b c, ND (PCFRule Γ Δ lev) ([ pcfjudg a b ],,[ pcfjudg b c ]) [ pcfjudg a c ].
 357     intros.
 358     destruct b.
 359     destruct o.
 360     destruct c.
 361     destruct o.
 362
 363     (* when the cut is a single leaf and the RHS is a single leaf: *)
 364     eapply nd_comp.
 365       eapply nd_prod.
 366       apply nd_id.
 367       apply (PCF_Arrange [h] ([],,[h]) [h0]).
 368       apply RuCanL.
 369       eapply nd_comp; [ idtac | apply (PCF_Arrange ([],,a) a [h0]); apply RCanL ].
 370       apply nd_rule.
 371 (*
 372       set (@RLet Γ Δ [] (a@@@(ec::nil)) h0 h (ec::nil)) as q.
 373       exists q.
 374       apply (PCF_RLet _ [] a h0 h).
 375     apply (Prelude_error "cut rule invoked with [a|=[b]] [[b]|=[]]").
 376     apply (Prelude_error "cut rule invoked with [a|=[b]] [[b]|=[x,,y]]").
 377     apply (Prelude_error "cut rule invoked with [a|=[]]  [[]|=c]").
 378     apply (Prelude_error "cut rule invoked with [a|=[b,,c]] [[b,,c]|=z]").
 379 *)
 380     admit.
 381     admit.
 382     admit.
 383     admit.
 384     admit.
 385     Defined.
 386
 387   Instance PCF_sequents Γ Δ lev : @SequentND _ (PCFRule Γ Δ lev) _ pcfjudg :=
 388     { snd_cut := PCF_cut Γ Δ lev }.
 389     apply Build_SequentND.
 390     intros.
 391     induction a.
 392     destruct a; simpl.
 393     apply nd_rule.
 394       exists (RVar _ _ _ _).
 395       apply PCF_RVar.
 396     apply nd_rule.
 397       exists (RVoid _ _ ).
 398       apply PCF_RVoid.
 399     eapply nd_comp.
 400       eapply nd_comp; [ apply nd_llecnac | idtac ].
 401       apply (nd_prod IHa1 IHa2).
 402       apply nd_rule.
 403         exists (RJoin _ _ _ _ _ _).
 404         apply PCF_RJoin.
 405       admit.
 406         Defined.
 407
 408   Definition PCF_left Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [pcfjudg b c] [pcfjudg (a,,b) (a,,c)].
 409     eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ].
 410     eapply nd_prod; [ apply snd_initial | apply nd_id ].
 411     apply nd_rule.
 412     set (@PCF_RJoin Γ Δ lev a b a c) as q'.
 413     refine (existT _ _ _).
 414     apply q'.
 415     Defined.
 416
 417   Definition PCF_right Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [pcfjudg b c] [pcfjudg (b,,a) (c,,a)].
 418     eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ].
 419     eapply nd_prod; [ apply nd_id | apply snd_initial ].
 420     apply nd_rule.
 421     set (@PCF_RJoin Γ Δ lev b a c a) as q'.
 422     refine (existT _ _ _).
 423     apply q'.
 424     Defined.
 425
 426   Instance PCF_sequent_join Γ Δ lev : @ContextND _ (PCFRule Γ Δ lev) _ pcfjudg _ :=
 427   { cnd_expand_left  := fun a b c => PCF_left  Γ Δ lev c a b
 428   ; cnd_expand_right := fun a b c => PCF_right Γ Δ lev c a b }.
 429     admit.
 430     admit.
 431     admit.
 432     admit.
 433     admit.
 434     admit.
 435     Defined.
 436
 437   Instance OrgPCF_SequentND_Relation Γ Δ lev : SequentND_Relation (PCF_sequent_join Γ Δ lev) OrgND.
 438     admit.
 439     Defined.
 440
 441   Instance OrgPCF_ContextND_Relation Γ Δ lev : ContextND_Relation (PCF_sequent_join Γ Δ lev).
 442     admit.
 443     Defined.
 444
 445   (* 5.1.3 *)
 446   Instance PCF Γ Δ lev : @ProgrammingLanguage _ _ pcfjudg (PCFRule Γ Δ lev) :=
 447   { pl_eqv                := OrgPCF_ContextND_Relation Γ Δ lev
 448   ; pl_snd                := PCF_sequents Γ Δ lev
 449   }.
 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
 479   Definition SystemFCa_cut Γ Δ : forall a b c, ND OrgR ([ Γ > Δ > a |- b ],,[ Γ > Δ > b |- c ]) [ Γ > Δ > a |- c ].
 480     intros.
 481     destruct b.
 482     destruct o.
 483     destruct c.
 484     destruct o.
 485
 486     (* when the cut is a single leaf and the RHS is a single leaf: *)
 487     eapply nd_comp.
 488       eapply nd_prod.
 489       apply nd_id.
 490       eapply nd_rule.
 491       apply org_fc with (r:=RArrange _ _ _ _ _ (RuCanL [l])).
 492       auto.
 493       eapply nd_comp; [ idtac | eapply nd_rule; apply org_fc with (r:=RArrange _ _ _ _ _ (RCanL _)) ].
 494       apply nd_rule.
 495       destruct l.
 496       destruct l0.
 497       assert (h0=h2). admit.
 498       subst.
 499       apply org_fc with (r:=@RLet Γ Δ [] a h1 h h2).
 500       auto.
 501       auto.
 502     apply (Prelude_error "systemfc cut rule invoked with [a|=[b]] [[b]|=[]]").
 503     apply (Prelude_error "systemfc cut rule invoked with [a|=[b]] [[b]|=[x,,y]]").
 504     apply (Prelude_error "systemfc rule invoked with [a|=[]]  [[]|=c]").
 505     apply (Prelude_error "systemfc rule invoked with [a|=[b,,c]] [[b,,c]|=z]").
 506     Defined.
 507
 508   Instance SystemFCa_sequents Γ Δ : @SequentND _ OrgR _ (mkJudg Γ Δ) :=
 509   { snd_cut := SystemFCa_cut Γ Δ }.
 510     apply Build_SequentND.
 511     intros.
 512     induction a.
 513     destruct a; simpl.
 514     apply nd_rule.
 515       destruct l.
 516       apply org_fc with (r:=RVar _ _ _ _).
 517       auto.
 518     apply nd_rule.
 519       apply org_fc with (r:=RVoid _ _ ).
 520       auto.
 521     eapply nd_comp.
 522       eapply nd_comp; [ apply nd_llecnac | idtac ].
 523       apply (nd_prod IHa1 IHa2).
 524       apply nd_rule.
 525         apply org_fc with (r:=RJoin _ _ _ _ _ _).
 526         auto.
 527       admit.
 528         Defined.
 529
 530   Definition SystemFCa_left Γ Δ a b c : ND OrgR [Γ > Δ > b |- c] [Γ > Δ > (a,,b) |- (a,,c)].
 531     eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ].
 532     eapply nd_prod; [ apply snd_initial | apply nd_id ].
 533     apply nd_rule.
 534     apply org_fc with (r:=RJoin Γ Δ a b a c).
 535     auto.
 536     Defined.
 537
 538   Definition SystemFCa_right Γ Δ a b c : ND OrgR [Γ > Δ > b |- c] [Γ > Δ > (b,,a) |- (c,,a)].
 539     eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ].
 540     eapply nd_prod; [ apply nd_id | apply snd_initial ].
 541     apply nd_rule.
 542     apply org_fc with (r:=RJoin Γ Δ b a c a).
 543     auto.
 544     Defined.
 545
 546 (*
 547   Instance SystemFCa_sequent_join Γ Δ : @SequentExpansion _ _ _ _ _ (SystemFCa_sequents Γ Δ) (SystemFCa_cutrule Γ Δ) :=
 548   { se_expand_left  := SystemFCa_left  Γ Δ
 549   ; se_expand_right := SystemFCa_right Γ Δ }.
 550     admit.
 551     admit.
 552     admit.
 553     admit.
 554     Defined.
 555 *)
 556   (* 5.1.2 *)
 557   Instance SystemFCa Γ Δ : @ProgrammingLanguage _ _ (mkJudg Γ Δ) OrgR.
 558 (*
 559   { pl_eqv                := OrgNDR
 560   ; pl_sn                 := SystemFCa_sequents     Γ Δ
 561   ; pl_subst              := SystemFCa_cutrule      Γ Δ
 562   ; pl_sequent_join       := SystemFCa_sequent_join Γ Δ
 563   }.
 564     apply Build_TreeStructuralRules; intros; unfold eqv; unfold hom; simpl.
 565     apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RCossa a b c))). apply Flat_RArrange.
 566     apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RAssoc a b c))). apply Flat_RArrange.
 567     apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanL  a    ))). apply Flat_RArrange.
 568     apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanR  a    ))). apply Flat_RArrange.
 569     apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanL a    ))). apply Flat_RArrange.
 570     apply nd_rule. apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanR a    ))). apply Flat_RArrange.
 571 *)
 572 admit.
 573     Defined.
 574
 575 End HaskProofStratified.