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