separate HaskProofStratified into PCF.v, HaskProgrammingLanguage.v, and HaskFlattener...

diff --git a/src/All.v b/src/All.v
index d4956dd..9443bbb 100644 (file)
--- a/src/All.v
+++ b/src/All.v
@@ -1,4 +1,7 @@
 Require Import ExtractionMain.
 Require Import ExtractionMain.

+Require Import HaskProgrammingLanguage.
+Require Import PCF.
+Require Import HaskFlattener.

 Require Import ProgrammingLanguageArrow.
 Require Import ProgrammingLanguageReification.
 Require Import ProgrammingLanguageFlattening.
 Require Import ProgrammingLanguageArrow.
 Require Import ProgrammingLanguageReification.
 Require Import ProgrammingLanguageFlattening.

diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v
index 35ab0d5..65e0637 100644 (file)
--- a/src/HaskFlattener.v
+++ b/src/HaskFlattener.v
@@ -56,64 +56,693 @@ Open Scope nd_scope.
  *)
 Section HaskFlattener.
 
  *)
 Section HaskFlattener.
 

-  Context {Γ:TypeEnv}.
-  Context {Δ:CoercionEnv Γ}.
-  Context {ec:HaskTyVar Γ ★}.
+  (* this actually has nothing to do with categories; it shows that proofs [|-A]//[|-B] are one-to-one with []//[A|-B] *)
+  (* TODO Lemma hom_functor_full*)
+
+  (* lemma: if a proof from no hypotheses contains no Brak's or Esc's, then the context contains no variables at level!=0 *)
+
+  (* In a tree of types, replace any type at level "lev" with None *)
+  Definition drop_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
+    mapTree (fun t => match t with
+                        | Some (ttype @@ tlev) => if eqd_dec tlev lev then None else t
+                        | _ => t
+                      end) tt.
+  (* The opposite: replace any type which is NOT at level "lev" with None *)
+  Definition take_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★) :=
+    mapTree (fun t => match t with
+                        | Some (ttype @@ tlev) => if eqd_dec tlev lev then Some ttype else None
+                        | _                    => None
+                      end) tt.
+
+  (* In a tree of types, replace any type at depth "lev" or greater None *)
+  Definition drop_depth {Γ}(n:nat)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
+    mapTree (fun t => match t with
+                        | Some (ttype @@ tlev) => if eqd_dec (length tlev) n then None else t
+                        | _ => t
+                      end) tt.
+
+  (* delete from the tree any type which is NOT at level "lev" *)
+
+  Fixpoint take_lev' {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : ??(Tree ??(HaskType Γ ★)) :=
+    match tt with
+      | T_Leaf   None  => Some (T_Leaf None)    (* FIXME: unsure of this; it ends up on both sides *)
+      | T_Branch b1 b2 =>
+        let b1' := take_lev' lev b1 in
+          let b2' := take_lev' lev b2 in
+            match b1' with
+              | None => b2'
+              | Some b1'' => match b2' with
+                               | None => Some b1''
+                               | Some b2'' => Some (b1'',,b2'')
+                             end
+            end
+      | T_Leaf   (Some (ttype@@tlev))  =>
+                if eqd_dec tlev lev
+                  then Some [ttype]
+                  else None
+    end.
+
+  Context (ga' : forall TV, TV ★ -> Tree ??(RawHaskType TV ★) -> Tree ??(RawHaskType TV ★) -> RawHaskType TV ★).
+
+  Definition ga : forall Γ, HaskTyVar Γ ★ -> Tree ??(HaskType Γ ★) -> Tree ??(HaskType Γ ★) -> HaskType Γ ★
+    := fun Γ ec ant suc =>
+      fun TV ite =>
+        ga'
+        TV
+        (ec TV ite)
+        (mapOptionTree (fun x => x TV ite) ant)
+        (mapOptionTree (fun x => x TV ite) suc).
+
+  Implicit Arguments ga [ [Γ] ].
+  Notation "a ~~~~> b" := (@ga _ _ a b) (at level 20).
+
+  Context (unit_type : forall TV, RawHaskType TV ★).
+
+  (*
+   *  The story:
+   *    - code types <[t]>@c                                                become garrows  c () t 
+   *    - free variables of type t at a level lev deeper than the succedent become garrows  c () t
+   *    - free variables at the level of the succedent become 
+   *)
+  Fixpoint flatten_rawtype {TV}{κ}(depth:nat)(exp: RawHaskType TV κ) : RawHaskType TV κ :=
+    match exp with
+    | TVar    _  x        => TVar x
+    | TAll     _ y        => TAll   _  (fun v => flatten_rawtype depth (y v))
+    | TApp   _ _ x y      => TApp      (flatten_rawtype depth x) (flatten_rawtype depth y)
+    | TCon       tc       => TCon      tc
+    | TCoerc _ t1 t2 t    => TCoerc    (flatten_rawtype depth t1) (flatten_rawtype depth t2) (flatten_rawtype depth t)
+    | TArrow              => TArrow
+    | TCode      v e      => match depth with
+                               | O => match v return RawHaskType TV ★ with
+                                        | TVar ★ ec => ga' TV ec [] [flatten_rawtype depth e]
+                                        | _         => unit_type TV
+                                      end
+                               | (S depth') => TCode v (flatten_rawtype depth' e)
+                             end
+    | TyFunApp     tfc lt => TyFunApp tfc (flatten_rawtype_list _ depth lt)
+    end
+    with flatten_rawtype_list {TV}(lk:list Kind)(depth:nat)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
+    match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
+    | TyFunApp_nil               => TyFunApp_nil
+    | TyFunApp_cons  κ kl t rest => TyFunApp_cons _ _ (flatten_rawtype depth t) (flatten_rawtype_list _ depth rest)
+    end.
+
+  Inductive AllT {T:Type}{P:T->Prop} : Tree ??T -> Prop :=
+    | allt_none   :                  AllT []
+    | allt_some   : forall t, P t -> AllT [t]
+    | allt_branch : forall b1 b2, AllT b1 -> AllT b2 -> AllT (b1,,b2)
+    .
+  Implicit Arguments AllT [[T]].
+
+  Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ => Γ end.
+
+  Definition getSuc (j:Judg) : Tree ??(LeveledHaskType (getΓ j) ★) :=
+    match j as J return Tree ??(LeveledHaskType (getΓ J) ★) with
+      Γ > _ > _ |- s => s
+        end.
+
+  Definition getlev {Γ}{κ}(lht:LeveledHaskType Γ κ) :=
+    match lht with t@@l => l end.
+
+  (* This tries to assign a single level to the entire succedent of a judgment.  If the succedent has types from different
+   * levels (should not happen) it just picks one; if the succedent has no non-None leaves (also should not happen) it
+   * picks nil *)
+  Fixpoint getjlev {Γ}(tt:Tree ??(LeveledHaskType Γ ★)) : HaskLevel Γ :=
+    match tt with
+      | T_Leaf None              => nil
+      | T_Leaf (Some (_ @@ lev)) => lev
+      | T_Branch b1 b2 =>
+        match getjlev b1 with
+          | nil => getjlev b2
+          | lev => lev
+        end
+    end.
+
+  (* an XJudg is a Judg for which the SUCCEDENT types all come from the same level, and that level is no deeper than "n" *)
+  (* even the empty succedent [] has a level... *)
+  Definition QJudg (n:nat)(j:Judg) := le (length (getjlev (getSuc j))) n.
+
+(*  Definition qjudg2judg {n}(qj:QJudg n) : Judg := projT1 qj.*)
+
+  Inductive QRule : nat -> Tree ??Judg -> Tree ??Judg -> Type :=
+    mkQRule : forall n h c,
+      Rule h c ->
+      ITree _ (QJudg n) h ->
+      ITree _ (QJudg n) c ->
+      QRule n h c.
+
+  Definition QND n := ND (QRule n).
+
+  (*
+   * Any type   "t"   at a level with length "n"   becomes (g () t)
+   * Any type "<[t]>" at a level with length "n-1" becomes (g () t)
+   *)
+
+  Definition flatten_type {Γ}(n:nat)(ht:HaskType Γ ★) : HaskType Γ ★ :=
+    fun TV ite =>
+      flatten_rawtype n (ht TV ite).
+
+  Definition minus' n m :=
+    match m with
+      | 0 => n
+      | _ => n - m
+    end.
+
+  (* to do: integrate this more cleanly with qjudg *)
+  Definition flatten_leveled_type {Γ}(n:nat)(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
+    match ht with
+      htt @@ htlev =>
+      flatten_type (minus' n (length htlev)) htt @@ htlev
+    end.
+
+  Definition flatten_qjudg_ok (n:nat)(j:Judg) : Judg :=
+    match j with
+      Γ > Δ > ant |- suc =>
+        let ant' := mapOptionTree (flatten_leveled_type n) ant in
+          let suc' := mapOptionTree (flatten_leveled_type n) suc
+            in  (Γ > Δ > ant' |- suc')
+    end.
+
+  Definition take_lev'' {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★) :=
+    match (take_lev' lev tt) with
+      | None => []
+      | Some x => x
+    end.
+
+  Definition flatten_qjudg : forall (n:nat), Judg -> Judg.
+    refine (fun {n}{j} =>
+      match j as J return Judg with
+        Γ > Δ > ant |- suc =>
+          match getjlev suc with
+            | nil        => flatten_qjudg_ok n j
+            | (ec::lev') => if eqd_dec (length lev') n
+                            then let ant_host    := drop_depth (S n) ant in
+                                   let ant_guest := take_lev (ec::lev') ant in  (* FIXME: I want take_lev''!!!!! *)
+                                     (Γ > Δ > ant_host |- [ga ec ant_guest (mapOptionTree unlev suc) @@ lev'])
+                            else flatten_qjudg_ok n j
+          end
+      end).
+    Defined.
+
+  Axiom literal_types_unchanged : forall n Γ l, flatten_type n (literalType l) = literalType(Γ:=Γ) l.
+
+  Lemma drop_depth_lemma : forall Γ (lev:HaskLevel Γ) x, drop_depth (length lev) [x @@  lev] = [].
+    admit.
+    Defined.
+
+  Lemma drop_depth_lemma_s : forall Γ (lev:HaskLevel Γ) ec x, drop_depth (S (length lev)) [x @@  (ec :: lev)] = [].
+    admit.
+    Defined.
+
+  Ltac drop_simplify :=
+    match goal with
+      | [ |- context[@drop_depth ?G (length ?L) [ ?X @@ ?L ] ] ] =>
+        rewrite (drop_depth_lemma G L X)
+      | [ |- context[@drop_depth ?G (S (length ?L)) [ ?X @@ (?E :: ?L) ] ] ] =>
+        rewrite (drop_depth_lemma_s G L E X)
+      | [ |- context[@drop_depth ?G ?N (?A,,?B)] ] =>
+      change (@drop_depth G N (A,,B)) with ((@drop_depth G N A),,(@drop_depth G N B))
+      | [ |- context[@drop_depth ?G ?N (T_Leaf None)] ] =>
+      change (@drop_depth G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
+    end.
+
+  Lemma take_lemma : forall Γ (lev:HaskLevel Γ) x, take_lev lev [x @@  lev] = [x].
+    admit.
+    Defined.
+
+  Ltac take_simplify :=
+    match goal with
+      | [ |- context[@take_lev ?G ?L [ ?X @@ ?L ] ] ] =>
+        rewrite (take_lemma G L X)
+      | [ |- context[@take_lev ?G ?N (?A,,?B)] ] =>
+      change (@take_lev G N (A,,B)) with ((@take_lev G N A),,(@take_lev G N B))
+      | [ |- context[@take_lev ?G ?N (T_Leaf None)] ] =>
+      change (@take_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
+    end.
+
+  Class garrow :=
+  { ga_id        : ∀ Γ Δ ec lev a    , ND Rule [] [Γ > Δ >                                           [] |- [@ga Γ ec a a @@ lev] ]
+  ; ga_comp      : ∀ Γ Δ ec lev a b c, ND Rule [] [Γ > Δ > [@ga Γ ec a b @@ lev],,[@ga Γ ec b c @@ lev] |- [@ga Γ ec a c @@ lev] ] 
+  ; ga_cancelr   : ∀ Γ Δ ec lev a    , ND Rule [] [Γ > Δ >                                           [] |- [@ga Γ ec (a,,[]) a @@ lev] ]
+  ; ga_cancell   : ∀ Γ Δ ec lev a    , ND Rule [] [Γ > Δ >                                           [] |- [@ga Γ ec ([],,a) a @@ lev] ]
+  ; ga_uncancelr : ∀ Γ Δ ec lev a    , ND Rule [] [Γ > Δ >                                           [] |- [@ga Γ ec a (a,,[]) @@ lev] ]
+  ; ga_uncancell : ∀ Γ Δ ec lev a    , ND Rule [] [Γ > Δ >                                           [] |- [@ga Γ ec a ([],,a) @@ lev] ]
+  ; ga_assoc     : ∀ Γ Δ ec lev a b c, ND Rule [] [Γ > Δ >                                           [] |- [@ga Γ ec ((a,,b),,c) (a,,(b,,c)) @@ lev] ]
+  ; ga_unassoc   : ∀ Γ Δ ec lev a b c, ND Rule [] [Γ > Δ >                                           [] |- [@ga Γ ec (a,,(b,,c)) ((a,,b),,c) @@ lev] ]
+  ; ga_swap      : ∀ Γ Δ ec lev a b  , ND Rule [] [Γ > Δ >                                           [] |- [@ga Γ ec (a,,b) (b,,a) @@ lev] ]
+  ; ga_drop      : ∀ Γ Δ ec lev a    , ND Rule [] [Γ > Δ >                                           [] |- [@ga Γ ec a [] @@ lev] ]
+  ; ga_copy      : ∀ Γ Δ ec lev a    , ND Rule [] [Γ > Δ >                                           [] |- [@ga Γ ec a (a,,a) @@ lev] ]
+  ; ga_first     : ∀ Γ Δ ec lev a b x, ND Rule [] [Γ > Δ >                        [@ga Γ ec a b @@ lev] |- [@ga Γ ec (a,,x) (b,,x) @@ lev] ]
+  ; ga_second    : ∀ Γ Δ ec lev a b x, ND Rule [] [Γ > Δ >                        [@ga Γ ec a b @@ lev] |- [@ga Γ ec (x,,a) (x,,b) @@ lev] ]
+  ; ga_lit       : ∀ Γ Δ ec lev lit  , ND Rule [] [Γ > Δ >                                           [] |- [@ga Γ ec [] [literalType lit] @@ lev] ]
+  ; ga_curry     : ∀ Γ Δ ec lev a b c, ND Rule [] [Γ > Δ >               [@ga Γ ec (a,,[b]) [c] @@ lev] |- [@ga Γ ec a [b ---> c] @@ lev] ]
+  ; ga_apply     : ∀ Γ Δ ec lev a a' b c, ND Rule [] [Γ > Δ >
+    [@ga Γ ec a [b ---> c] @@ lev],,[@ga Γ ec a' [b] @@ lev]
+    |-
+    [@ga Γ ec (a,,a') [c] @@ lev] ]
+  }.
+
+  Context (gar:garrow).
+
+  Definition boost : forall Γ Δ ant x y,
+     ND Rule []                   [ Γ > Δ > x   |- y ] ->
+     ND Rule [ Γ > Δ > ant |- x ] [ Γ > Δ > ant |- y ].
+     admit.
+     Defined.
+  Definition postcompose : ∀ Γ Δ ec lev a b c,
+     ND Rule [] [ Γ > Δ > []                    |- [@ga Γ ec a b @@ lev] ] ->
+     ND Rule [] [ Γ > Δ > [@ga Γ ec b c @@ lev] |- [@ga Γ ec a c @@ lev] ].
+     admit.
+     Defined.
+  Definition precompose : ∀ Γ Δ lev a b c x,
+     ND Rule [] [ Γ > Δ > a |- x,,[b @@ lev] ] ->
+     ND Rule [] [ Γ > Δ > [b @@ lev] |- [c @@ lev] ] ->
+     ND Rule [] [ Γ > Δ > a,,x |- [c @@ lev] ].
+     admit.
+     Defined.
+
+  Set Printing Width 130.
+
+  Definition garrowfy_arrangement' :
+    forall Γ (Δ:CoercionEnv Γ)
+      (ec:HaskTyVar Γ ★) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
+      ND Rule [] [Γ > Δ > [] |- [@ga _ ec (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ lev] ].
+
+      intros Γ Δ ec lev.
+      refine (fix garrowfy ant1 ant2 (r:Arrange ant1 ant2):
+           ND Rule [] [Γ > Δ > [] |- [@ga _ ec (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ lev]] :=
+        match r as R in Arrange A B return
+          ND Rule [] [Γ > Δ > [] |- [@ga _ ec (take_lev (ec :: lev) B) (take_lev (ec :: lev) A) @@ lev]]
+          with
+          | RCanL  a             => let case_RCanL := tt  in ga_uncancell _ _ _ _ _
+          | RCanR  a             => let case_RCanR := tt  in ga_uncancelr _ _ _ _ _
+          | RuCanL a             => let case_RuCanL := tt in ga_cancell _ _ _ _ _
+          | RuCanR a             => let case_RuCanR := tt in ga_cancelr _ _ _ _ _
+          | RAssoc a b c         => let case_RAssoc := tt in ga_assoc _ _ _ _ _ _ _
+          | RCossa a b c         => let case_RCossa := tt in ga_unassoc _ _ _ _ _ _ _
+          | RExch  a b           => let case_RExch := tt  in ga_swap  _ _ _ _ _ _
+          | RWeak  a             => let case_RWeak := tt  in ga_drop  _ _ _ _ _ 
+          | RCont  a             => let case_RCont := tt  in ga_copy  _ _ _ _ _ 
+          | RLeft  a b c r'      => let case_RLeft := tt  in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
+          | RRight a b c r'      => let case_RRight := tt in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_first  _ _ _ _ _ _ _)
+          | RComp  a b c r1 r2   => let case_RComp := tt  in (fun r1' r2' => _) (garrowfy _ _ r1) (garrowfy _ _ r2)
+        end); clear garrowfy; repeat take_simplify; repeat drop_simplify; intros.
+
+        destruct case_RComp.
+          (*
+          set (ga_comp Γ Δ ec lev (``c) (``b) (``a)) as q.
+          eapply precompose.
+          Focus 2.
+          apply q.
+          refine ( _ ;; boost _ _ _ _ _ (ga_comp _ _ _ _ _ _ _)).
+          apply precompose.
+          Focus 2.
+          eapply ga_comp.
+          *)
+          admit.
+          Defined.
+
+  Definition garrowfy_arrangement :
+    forall Γ (Δ:CoercionEnv Γ) n
+      (ec:HaskTyVar Γ ★) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
+      (*ec :: lev = getjlev succ ->*)
+      (* H0 : left (Datatypes.length lev ≠ n) e = Peano_dec.eq_nat_dec (Datatypes.length lev) n *)
+      ND Rule
+      [Γ > Δ > drop_depth n ant1 |- [@ga _ ec (take_lev (ec :: lev) ant1) (mapOptionTree unlev succ) @@ lev]]
+      [Γ > Δ > drop_depth n ant2 |- [@ga _ ec (take_lev (ec :: lev) ant2) (mapOptionTree unlev succ) @@ lev]].
+      intros.
+      refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (garrowfy_arrangement' Γ Δ ec lev ant1 ant2 r)))).
+      apply nd_rule.
+      apply RArrange.
+      refine ((fix garrowfy ant1 ant2 (r:Arrange ant1 ant2) :=
+        match r as R in Arrange A B return Arrange (drop_depth _ A) (drop_depth _ B) with
+          | RCanL  a             => let case_RCanL := tt  in RCanL _
+          | RCanR  a             => let case_RCanR := tt  in RCanR _
+          | RuCanL a             => let case_RuCanL := tt in RuCanL _
+          | RuCanR a             => let case_RuCanR := tt in RuCanR _
+          | RAssoc a b c         => let case_RAssoc := tt in RAssoc _ _ _
+          | RCossa a b c         => let case_RCossa := tt in RCossa _ _ _
+          | RExch  a b           => let case_RExch := tt  in RExch _ _
+          | RWeak  a             => let case_RWeak := tt  in RWeak _
+          | RCont  a             => let case_RCont := tt  in RCont _
+          | RLeft  a b c r'      => let case_RLeft := tt  in RLeft  _ (garrowfy _ _ r')
+          | RRight a b c r'      => let case_RRight := tt in RRight _ (garrowfy _ _ r')
+          | RComp  a b c r1 r2   => let case_RComp := tt  in RComp    (garrowfy _ _ r1) (garrowfy _ _ r2)
+        end) ant1 ant2 r); clear garrowfy; repeat take_simplify; repeat drop_simplify; intros.
+        Defined.

 
 

-  Lemma unlev_lemma : forall (x:Tree ??(HaskType Γ ★)) lev, x = mapOptionTree unlev (x @@@ lev).
+  Definition flatten_arrangement :
+    forall n Γ Δ ant1 ant2 succ (r:Arrange ant1 ant2),
+      ND Rule (mapOptionTree (flatten_qjudg n) [Γ > Δ > ant1 |- succ])
+      (mapOptionTree (flatten_qjudg n) [Γ > Δ > ant2 |- succ]).

     intros.
     intros.

-    rewrite <- mapOptionTree_compose.
-    simpl.
-    induction x.
-    destruct a; simpl; auto.

     simpl.
     simpl.

-    rewrite IHx1 at 1.
-    rewrite IHx2 at 1.
-    reflexivity.
-    Qed.
+    set (getjlev succ) as succ_lev.
+    assert (succ_lev=getjlev succ).
+      reflexivity.
+
+    destruct succ_lev.
+      apply nd_rule.
+      apply RArrange.
+      induction r; simpl.
+        apply RCanL.
+        apply RCanR.
+        apply RuCanL.
+        apply RuCanR.
+        apply RAssoc.
+        apply RCossa.
+        apply RExch.
+        apply RWeak.
+        apply RCont.
+        apply RLeft; auto.
+        apply RRight; auto.
+        eapply RComp; [ apply IHr1 | apply IHr2 ].
+
+    set (Peano_dec.eq_nat_dec (Datatypes.length succ_lev) n) as lev_is_n.
+      assert (lev_is_n=Peano_dec.eq_nat_dec (Datatypes.length succ_lev) n).
+        reflexivity.
+      destruct lev_is_n.
+        rewrite <- e.
+        apply garrowfy_arrangement.
+        apply r.
+        auto.
+      apply nd_rule.
+      apply RArrange.
+      induction r; simpl.
+        apply RCanL.
+        apply RCanR.
+        apply RuCanL.
+        apply RuCanR.
+        apply RAssoc.
+        apply RCossa.
+        apply RExch.
+        apply RWeak.
+        apply RCont.
+        apply RLeft; auto.
+        apply RRight; auto.
+        eapply RComp; [ apply IHr1 | apply IHr2 ].
+        Defined.
+
+  Lemma flatten_coercion : forall n Γ Δ σ τ (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)),
+    HaskCoercion Γ Δ (flatten_type n σ ∼∼∼ flatten_type n τ).
+    admit.
+    Defined.
+
+  Ltac eqd_dec_refl' :=
+    match goal with
+      | [ |- context[@eqd_dec ?T ?V ?X ?X] ] =>
+        destruct (@eqd_dec T V X X) as [eqd_dec1 | eqd_dec2];
+          [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ]
+  end.
+
+
+(*
+  Lemma foog : forall Γ Δ,
+    ND Rule
+    ( [ Γ > Δ > Σ₁ |- a ],,[ Γ > Δ > Σ₂ |- b ] )
+      [ Γ > Δ > Σ₁,,Σ₂ |- a,,b ]
+*)
+
+  Notation "`  x" := (take_lev _ x) (at level 20).
+  Notation "`` x" := (mapOptionTree unlev x) (at level 20).
+  Notation "``` x" := (drop_depth _ x) (at level 20).
+
+  Definition flatten :
+    forall n {h}{c},
+      QND (S n) h c ->
+      ND Rule (mapOptionTree (flatten_qjudg n) h) (mapOptionTree (flatten_qjudg n) c).
+    intros.
+    eapply nd_map'; [ idtac | apply X ].
+    clear h c X.
+    intros.
+    simpl in *.
+
+    inversion X.
+    subst.
+    refine (match X0 as R in Rule H C with
+      | RArrange Γ Δ a b x d           => let case_RArrange := tt      in _
+      | RNote    Γ Δ Σ τ l n           => let case_RNote := tt         in _
+      | RLit     Γ Δ l     _           => let case_RLit := tt          in _
+      | RVar     Γ Δ σ           lev   => let case_RVar := tt          in _
+      | RGlobal  Γ Δ σ l wev           => let case_RGlobal := tt       in _
+      | RLam     Γ Δ Σ tx te     lev   => let case_RLam := tt          in _
+      | RCast    Γ Δ Σ σ τ lev γ       => let case_RCast := tt         in _
+      | RAbsT    Γ Δ Σ κ σ lev         => let case_RAbsT := tt         in _
+      | RAppT    Γ Δ Σ κ σ τ     lev   => let case_RAppT := tt         in _
+      | RAppCo   Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt        in _
+      | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _
+      | RApp     Γ Δ Σ₁ Σ₂ tx te lev   => let case_RApp := tt          in _
+      | RLet     Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev   => let case_RLet := tt          in _
+      | RJoin    Γ p lri m x q         => let case_RJoin := tt in _
+      | RVoid    _ _                   => let case_RVoid := tt   in _
+      | RBrak    Σ a b c n m           => let case_RBrak := tt         in _
+      | REsc     Σ a b c n m           => let case_REsc := tt          in _
+      | RCase    Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
+      | RLetRec  Γ Δ lri x y t         => let case_RLetRec := tt       in _
+      end); clear X X0 X1 X2 h c.
+
+    destruct case_RArrange.
+      apply (flatten_arrangement n Γ Δ a b x d).
+
+    destruct case_RBrak.
+      admit.
+
+    destruct case_REsc.
+      admit.
+      
+    destruct case_RNote.
+      simpl.
+      destruct l; simpl.
+        apply nd_rule; apply RNote; auto.
+        destruct (Peano_dec.eq_nat_dec (Datatypes.length l) n).
+        apply nd_rule; apply RNote; auto.
+        apply nd_rule; apply RNote; auto.

 
 

-  Context (ga_rep      : Tree ??(HaskType Γ ★) -> HaskType Γ ★ ).
-  Context (ga_type     : HaskType Γ ★ -> HaskType Γ ★ -> HaskType Γ ★).
+    destruct case_RLit.
+      simpl.
+      destruct l0; simpl.
+        rewrite literal_types_unchanged.
+          apply nd_rule; apply RLit.
+        destruct (Peano_dec.eq_nat_dec (Datatypes.length l0) n); unfold mapTree; unfold mapOptionTree; simpl.
+        unfold take_lev; simpl.
+        unfold drop_depth; simpl.
+        apply ga_lit.
+        rewrite literal_types_unchanged.
+        apply nd_rule.
+        apply RLit.

 
 

-  (*Notation "a ~~~~> b" := (ND Rule [] [ Γ > Δ > a |- b ]) (at level 20).*)
-  Notation "a ~~~~> b" := (ND (OrgR Γ Δ) [] [ (a , b) ]) (at level 20).
+    destruct case_RVar.
+      simpl.
+      destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RVar | idtac ].
+      destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RVar ]; simpl.
+      rewrite <- e.
+      clear e n.
+      repeat drop_simplify.
+      repeat take_simplify.
+      apply ga_id.
+
+    destruct case_RGlobal.
+      simpl.
+      destruct l as [|ec lev]; simpl; [ apply nd_rule; apply RGlobal; auto | idtac ].
+      destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RGlobal; auto ]; simpl.
+      apply (Prelude_error "found RGlobal at depth >0").

 
 

-  Lemma magic : forall a b c,
-    ([]                   ~~~~> [ga_type a b @@ nil]) ->
-    ([ga_type b c @@ nil] ~~~~> [ga_type a c @@ nil]).
+    destruct case_RLam.
+      simpl.
+      destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
+      destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RLam; auto ]; simpl.
+      rewrite <- e.
+      clear e n.
+      repeat drop_simplify.
+      repeat take_simplify.
+      eapply nd_comp.
+        eapply nd_rule.
+        eapply RArrange.
+        apply RCanR.
+      apply boost.
+      apply ga_curry.
+        
+    destruct case_RCast.
+      simpl.
+      destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
+      apply flatten_coercion; auto.
+      destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RCast; auto ]; simpl.
+      apply (Prelude_error "RCast at level >0").
+      apply flatten_coercion; auto.
+
+    destruct case_RJoin.
+      simpl.
+      destruct (getjlev x); destruct (getjlev q).
+      apply nd_rule.
+      apply RJoin.
+      apply (Prelude_error "RJoin at depth >0").
+      apply (Prelude_error "RJoin at depth >0").
+      apply (Prelude_error "RJoin at depth >0").
+
+    destruct case_RApp.
+      simpl.
+
+      destruct lev as [|ec lev]. simpl. apply nd_rule.
+        replace (flatten_type n (tx ---> te)) with ((flatten_type n tx) ---> (flatten_type n te)).
+        apply RApp.
+        unfold flatten_type.
+        simpl.
+        reflexivity.
+
+        destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n).
+          eapply nd_comp.
+          eapply nd_rule.
+          apply RJoin.
+          repeat drop_simplify.
+          repeat take_simplify.
+          apply boost.
+          apply ga_apply.
+
+          replace (flatten_type (minus' n (length (ec::lev))) (tx ---> te))
+            with ((flatten_type (minus' n (length (ec::lev))) tx) ---> (flatten_type (minus' n (length (ec::lev))) te)).
+          apply nd_rule.
+          apply RApp.
+          unfold flatten_type.
+          simpl.
+          reflexivity.
+
+    destruct case_RLet.
+      simpl.
+      destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
+      destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RLet; auto ]; simpl.
+      repeat drop_simplify.
+      repeat take_simplify.
+      admit.  (* FIXME *)
+
+    destruct case_RVoid.
+      simpl.
+      apply nd_rule.
+      apply RVoid.
+        
+    destruct case_RAppT.
+      simpl. destruct lev; simpl.
+      admit.
+      admit.
+
+    destruct case_RAbsT.
+      simpl. destruct lev; simpl.
+      admit.
+      admit.
+
+    destruct case_RAppCo.
+      simpl. destruct lev; simpl.
+      admit.
+      admit.
+
+    destruct case_RAbsCo.
+      simpl. destruct lev; simpl.
+      admit.
+      admit.
+
+    destruct case_RLetRec.
+      simpl.
+      admit.
+
+    destruct case_RCase.
+      simpl.
+      admit.
+      Defined.
+
+    Lemma flatten_qjudg_qjudg : forall {n}{j} (q:QJudg (S n) j), QJudg n (flatten_qjudg n j).
+      admit.
+      (*
+      intros.
+      destruct q.
+      destruct a.
+      unfold flatten_qjudg.
+      destruct j.
+      destruct (eqd_dec (Datatypes.length x) (S n)).
+      destruct x.
+      inversion e.
+      exists x; split.
+        simpl in e.
+        inversion e.
+        auto.
+        simpl in *.
+        apply allt_some.
+        simpl.
+        auto.
+      unfold QJudg.
+      exists x.
+      split; auto.
+        clear a.
+        Set Printing Implicit.
+        simpl.
+        set (length x) as x'.
+        assert (x'=length x).
+          reflexivity.
+          simpl in *.
+          rewrite <- H.
+          Unset Printing Implicit.
+          idtac.
+          omega.
+    simpl in *.
+      induction t0.
+      destruct a0; simpl in *.
+      apply allt_some.
+      inversion a.
+      subst.
+      destruct l0.
+      simpl.
+      auto.
+      apply allt_none.
+      simpl in *.
+      inversion a; subst.
+      apply allt_branch.
+        apply IHt0_1; auto.
+        apply IHt0_2; auto.
+        *)
+        Defined.
+
+
+  (*
+  Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
+    { fmor := FlatteningFunctor_fmor }.
+    Admitted.
+
+  Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
+    refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
+    Admitted.
+
+  Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
+    refine {| plsmme_pl := PCF n Γ Δ |}.

     admit.
     admit.

-    Qed.
-
-  Context (ga_lit      : ∀ lit, [] ~~~~> [ga_type (ga_rep   []   )      (ga_rep [literalType lit])@@ nil]).
-  Context (ga_id       : ∀ σ,   [] ~~~~> [ga_type (ga_rep   σ    )      (ga_rep σ                )@@ nil]).
-  Context (ga_cancell  : ∀ c  , [] ~~~~> [ga_type (ga_rep ([],,c))      (ga_rep c                )@@ nil]).
-  Context (ga_cancelr  : ∀ c  , [] ~~~~> [ga_type (ga_rep (c,,[]))      (ga_rep c                )@@ nil]).
-  Context (ga_uncancell: ∀ c  , [] ~~~~> [ga_type (ga_rep  c     )      (ga_rep ([],,c)          )@@ nil]).
-  Context (ga_uncancelr: ∀ c  , [] ~~~~> [ga_type (ga_rep  c     )      (ga_rep (c,,[])          )@@ nil]).
-  Context (ga_assoc    : ∀ a b c,[] ~~~~> [ga_type (ga_rep ((a,,b),,c))  (ga_rep (a,,(b,,c))      )@@ nil]).
-  Context (ga_unassoc  : ∀ a b c,[] ~~~~> [ga_type (ga_rep ( a,,(b,,c))) (ga_rep ((a,,b),,c))      @@ nil]).
-  Context (ga_swap     : ∀ a b, [] ~~~~> [ga_type (ga_rep (a,,b) )      (ga_rep (b,,a)           )@@ nil]).
-  Context (ga_copy     : ∀ a  , [] ~~~~> [ga_type (ga_rep  a     )      (ga_rep (a,,a)           )@@ nil]).
-  Context (ga_drop     : ∀ a  , [] ~~~~> [ga_type (ga_rep  a     )      (ga_rep []               )@@ nil]).
-  Context (ga_first    : ∀ a b c,
-    [ga_type (ga_rep a) (ga_rep b) @@nil] ~~~~> [ga_type (ga_rep (a,,c)) (ga_rep (b,,c)) @@nil]).
-  Context (ga_second   : ∀ a b c,
-    [ga_type (ga_rep a) (ga_rep b) @@nil] ~~~~> [ga_type (ga_rep (c,,a)) (ga_rep (c,,b)) @@nil]).
-  Context (ga_comp     : ∀ a b c,
-    ([ga_type (ga_rep a) (ga_rep b) @@nil],,[ga_type (ga_rep b) (ga_rep c) @@nil])
-    ~~~~>
-    [ga_type (ga_rep a) (ga_rep c) @@nil]).
-
-  Definition guestJudgmentAsGArrowType (lt:PCFJudg Γ ec) : HaskType Γ ★ :=
-    match lt with
-      (x,y) => (ga_type (ga_rep x) (ga_rep y)) 
-    end.
+    Defined.
+
+  Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
+    refine {| plsmme_pl := SystemFCa n Γ Δ |}.
+    admit.
+    Defined.
+
+  Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
+    admit.
+    Defined.
+
+  (* 5.1.4 *)
+  Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
+    admit.
+    Defined.
+  *)
+  (*  ... and the retraction exists *)
+
+End HaskFlattener.
+

 
 

-  Definition obact (X:Tree ??(PCFJudg Γ ec)) : Tree ??(LeveledHaskType Γ ★) :=
-    mapOptionTree guestJudgmentAsGArrowType X @@@ nil.

 
 

-  Hint Constructors Rule_Flat.
-  Context {ndr:@ND_Relation _ Rule}.
+
+
+
+
+
+
+(*
+
+  Old flattening code; ignore this - just to remind me how I used to do it

 
   (*
    * Here it is, what you've all been waiting for!  When reading this,
 
   (*
    * Here it is, what you've all been waiting for!  When reading this,

@@ -124,7 +753,7 @@ Section HaskFlattener.
   Definition FlatteningFunctor_fmor
     : forall h c,
       (ND (PCFRule Γ Δ ec) h c) ->
   Definition FlatteningFunctor_fmor
     : forall h c,
       (ND (PCFRule Γ Δ ec) h c) ->

-      ((obact h)~~~~>(obact c)).
+      ((obact h)====>(obact c)).

 
     set (@nil (HaskTyVar Γ ★)) as lev.
 
 
     set (@nil (HaskTyVar Γ ★)) as lev.
 

@@ -367,36 +996,4 @@ Section HaskFlattener.
         (* this assumes we want effects to occur in syntactically-left-to-right order *)
         admit.
         Defined.
         (* this assumes we want effects to occur in syntactically-left-to-right order *)
         admit.
         Defined.

-
-(*
-  Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
-    { fmor := FlatteningFunctor_fmor }.
-    Admitted.
-
-  Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
-    refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
-    Admitted.
-
-  Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
-    refine {| plsmme_pl := PCF n Γ Δ |}.
-    admit.
-    Defined.
-
-  Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
-    refine {| plsmme_pl := SystemFCa n Γ Δ |}.
-    admit.
-    Defined.
-
-  Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
-    admit.
-    Defined.
-
-  (* 5.1.4 *)
-  Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
-    admit.
-    Defined.
-*)
-  (*  ... and the retraction exists *)
-
-End HaskFlattener.
-
+*)
\ No newline at end of file

diff --git a/src/HaskProgrammingLanguage.v b/src/HaskProgrammingLanguage.v
index 0d612d6..9801168 100644 (file)
--- a/src/HaskProgrammingLanguage.v
+++ b/src/HaskProgrammingLanguage.v
@@ -39,48 +39,26 @@ Require Import HaskProof.
 Require Import HaskStrongToProof.
 Require Import HaskProofToStrong.
 Require Import ProgrammingLanguage.
 Require Import HaskStrongToProof.
 Require Import HaskProofToStrong.
 Require Import ProgrammingLanguage.

-Require Import PCF.

 
 Open Scope nd_scope.
 
 
 Open Scope nd_scope.
 

+(* The judgments any specific Γ,Δ form a category with proofs as morphisms *)

 Section HaskProgrammingLanguage.
 
   Context (ndr_systemfc:@ND_Relation _ Rule).
 Section HaskProgrammingLanguage.
 
   Context (ndr_systemfc:@ND_Relation _ Rule).

-  Context Γ (Δ:CoercionEnv Γ).
-
-  (* An organized deduction has been reorganized into contiguous blocks whose
-   * hypotheses (if any) and conclusion have the same Γ and Δ and a fixed nesting depth.  The boolean
-   * indicates if non-PCF rules have been used *)
-  Inductive OrgR : Tree ??(@FCJudg Γ) -> Tree ??(@FCJudg Γ) -> Type :=

 
 

-  | org_fc        : forall (h c:Tree ??(FCJudg Γ))
-    (r:Rule (mapOptionTree (fcjudg2judg Γ Δ) h) (mapOptionTree (fcjudg2judg Γ Δ) c)),
-    Rule_Flat r ->
-    OrgR h c
+  Context Γ (Δ:CoercionEnv Γ).

 
 

-  | org_pcf      : forall ec h c,
-    ND (PCFRule Γ Δ ec)  h c  ->
-    OrgR                (mapOptionTree (pcfjudg2fcjudg Γ ec) h)  (mapOptionTree (pcfjudg2fcjudg Γ ec) c).
+  
+  Definition JudgΓΔ := prod (Tree ??(LeveledHaskType Γ ★)) (Tree ??(LeveledHaskType Γ ★)).

 
 

-  (* any proof in organized form can be "dis-organized" *)
-  (*
-  Definition unOrgR : forall Γ Δ h c, OrgR Γ Δ h c -> ND Rule h c.
-    intros.
-    induction X.
-      apply nd_rule.
-      apply r.
-    eapply nd_comp.
-      (*
-      apply (mkEsc h).
-      eapply nd_comp; [ idtac |  apply (mkBrak c) ].
-      apply pcfToND.
-      apply n.
-      *)
-      Admitted.
-  Definition unOrgND Γ Δ h c :  ND (OrgR Γ Δ) h c -> ND Rule h c := nd_map (unOrgR Γ Δ).
-  *)
+  Definition RuleΓΔ : Tree ??JudgΓΔ -> Tree ??JudgΓΔ -> Type :=
+    fun h c =>
+      Rule
+      (mapOptionTree (fun j => Γ > Δ > fst j |- snd j) h)
+      (mapOptionTree (fun j => Γ > Δ > fst j |- snd j) c).

 
 

-  Definition SystemFCa_cut : forall a b c, ND OrgR ([(a,b)],,[(b,c)]) [(a,c)].
+  Definition SystemFCa_cut : forall a b c, ND RuleΓΔ ([(a,b)],,[(b,c)]) [(a,c)].

     intros.
     destruct b.
     destruct o.
     intros.
     destruct b.
     destruct o.

@@ -114,7 +92,7 @@ Section HaskProgrammingLanguage.
     apply (Prelude_error "systemfc rule invoked with [a|=[b,,c]] [[b,,c]|=z]").
     Defined.
 
     apply (Prelude_error "systemfc rule invoked with [a|=[b,,c]] [[b,,c]|=z]").
     Defined.
 

-  Instance SystemFCa_sequents : @SequentND _ OrgR _ _ :=
+  Instance SystemFCa_sequents : @SequentND _ RuleΓΔ _ _ :=

   { snd_cut := SystemFCa_cut }.
     apply Build_SequentND.
     intros.
   { snd_cut := SystemFCa_cut }.
     apply Build_SequentND.
     intros.

@@ -142,7 +120,7 @@ Section HaskProgrammingLanguage.
       admit.
       Defined.
 
       admit.
       Defined.
 

-  Definition SystemFCa_left a b c : ND OrgR [(b,c)] [((a,,b),(a,,c))].
+  Definition SystemFCa_left a b c : ND RuleΓΔ [(b,c)] [((a,,b),(a,,c))].

     admit.
     (*
     eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ].
     admit.
     (*
     eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ].

@@ -153,7 +131,7 @@ Section HaskProgrammingLanguage.
     *)
     Defined.
 
     *)
     Defined.
 

-  Definition SystemFCa_right a b c : ND OrgR [(b,c)] [((b,,a),(c,,a))].
+  Definition SystemFCa_right a b c : ND RuleΓΔ [(b,c)] [((b,,a),(c,,a))].

     admit.
     (*
     eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ].
     admit.
     (*
     eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ].

@@ -195,7 +173,7 @@ Section HaskProgrammingLanguage.
       admit.
       Defined.
 
       admit.
       Defined.
 

-  Instance OrgFC : @ND_Relation _ OrgR.
+  Instance OrgFC : @ND_Relation _ RuleΓΔ.

     Admitted.
 
   Instance OrgFC_SequentND_Relation : SequentND_Relation SystemFCa_sequent_join OrgFC.
     Admitted.
 
   Instance OrgFC_SequentND_Relation : SequentND_Relation SystemFCa_sequent_join OrgFC.

diff --git a/src/HaskProofFlattener.v b/src/HaskProofFlattener.v
deleted file mode 100644 (file)
index 2797716..0000000
--- a/src/HaskProofFlattener.v
+++ /dev/null
@@ -1,396 +0,0 @@
-(*********************************************************************************************************************************)
-(* HaskProofFlattener:                                                                                                           *)
-(*                                                                                                                               *)
-(*    The Flattening Functor.                                                                                                    *)
-(*                                                                                                                               *)
-(*********************************************************************************************************************************)
-
-Generalizable All Variables.
-Require Import Preamble.
-Require Import General.
-Require Import NaturalDeduction.
-Require Import Coq.Strings.String.
-Require Import Coq.Lists.List.
-
-Require Import HaskKinds.
-Require Import HaskCoreTypes.
-Require Import HaskLiteralsAndTyCons.
-Require Import HaskStrongTypes.
-Require Import HaskProof.
-Require Import NaturalDeduction.
-Require Import NaturalDeductionCategory.
-
-Require Import Algebras_ch4.
-Require Import Categories_ch1_3.
-Require Import Functors_ch1_4.
-Require Import Isomorphisms_ch1_5.
-Require Import ProductCategories_ch1_6_1.
-Require Import OppositeCategories_ch1_6_2.
-Require Import Enrichment_ch2_8.
-Require Import Subcategories_ch7_1.
-Require Import NaturalTransformations_ch7_4.
-Require Import NaturalIsomorphisms_ch7_5.
-Require Import BinoidalCategories.
-Require Import PreMonoidalCategories.
-Require Import MonoidalCategories_ch7_8.
-Require Import Coherence_ch7_8.
-
-Require Import HaskStrongTypes.
-Require Import HaskStrong.
-Require Import HaskProof.
-Require Import HaskStrongToProof.
-Require Import HaskProofToStrong.
-Require Import ProgrammingLanguage.
-Require Import HaskProofStratified.
-
-Open Scope nd_scope.
-
-(*
- *  The flattening transformation.  Currently only TWO-level languages are
- *  supported, and the level-1 sublanguage is rather limited.
- *
- *  This file abuses terminology pretty badly.  For purposes of this file,
- *  "PCF" means "the level-1 sublanguage" and "FC" (aka System FC) means 
- *  the whole language (level-0 language including bracketed level-1 terms)
- *)
-Section HaskProofFlattener.
-
-  Context {Γ:TypeEnv}.
-  Context {Δ:CoercionEnv Γ}.
-  Context {ec:HaskTyVar Γ ★}.
-
-  Lemma unlev_lemma : forall (x:Tree ??(HaskType Γ ★)) lev, x = mapOptionTree unlev (x @@@ lev).
-    intros.
-    rewrite <- mapOptionTree_compose.
-    simpl.
-    induction x.
-    destruct a; simpl; auto.
-    simpl.
-    rewrite IHx1 at 1.
-    rewrite IHx2 at 1.
-    reflexivity.
-    Qed.
-
-  Context (ga_rep      : Tree ??(HaskType Γ ★) -> HaskType Γ ★ ).
-  Context (ga_type     : HaskType Γ ★ -> HaskType Γ ★ -> HaskType Γ ★).
-
-  Lemma magic : forall a b c,
-    ([]                   ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type a b @@ nil]) ->
-    ([ga_type b c @@ nil] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type a c @@ nil]).
-    admit.
-    Qed.
-
-  Context (ga_lit       : forall lit,     [] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep   []   )      (ga_rep [literalType lit])@@ nil]).
-  Context (ga_id        : forall σ,       [] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep   σ    )      (ga_rep σ                )@@ nil]).
-  Context (ga_cancell   : forall c  ,     [] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep ([],,c))      (ga_rep c                )@@ nil]).
-  Context (ga_cancelr   : forall c  ,     [] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep (c,,[]))      (ga_rep c                )@@ nil]).
-  Context (ga_uncancell : forall c  ,     [] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep  c     )      (ga_rep ([],,c)          )@@ nil]).
-  Context (ga_uncancelr : forall c  ,     [] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep  c     )      (ga_rep (c,,[])          )@@ nil]).
-  Context (ga_assoc     : forall a b c,   [] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep ((a,,b),,c))  (ga_rep (a,,(b,,c))      )@@ nil]).
-  Context (ga_unassoc   : forall a b c,   [] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep ( a,,(b,,c))) (ga_rep ((a,,b),,c))      @@ nil]).
-  Context (ga_swap      : forall a b,     [] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep (a,,b) )      (ga_rep (b,,a)           )@@ nil]).
-  Context (ga_copy      : forall a  ,     [] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep  a     )      (ga_rep (a,,a)           )@@ nil]).
-  Context (ga_drop      : forall a  ,     [] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep  a     )      (ga_rep []               )@@ nil]).
-  Context (ga_first     : forall a b c,   [ga_type (ga_rep a) (ga_rep b) @@nil] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep (a,,c)) (ga_rep (b,,c)) @@nil]).
-  Context (ga_second    : forall a b c,   [ga_type (ga_rep a) (ga_rep b) @@nil] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep (c,,a)) (ga_rep (c,,b)) @@nil]).
-  Context (ga_comp      : forall a b c,
-    [ga_type (ga_rep a) (ga_rep b) @@nil],,[ga_type (ga_rep b) (ga_rep c) @@nil]
-    ~~{TypesL (SystemFCa Γ Δ)}~~>
-    [ga_type (ga_rep a) (ga_rep c) @@nil]).
-
-  Definition guestJudgmentAsGArrowType (lt:PCFJudg Γ ec) : HaskType Γ ★ :=
-    match lt with
-      (x,y) => (ga_type (ga_rep x) (ga_rep y)) 
-    end.
-
-  Definition obact (X:Tree ??(PCFJudg Γ ec)) : Tree ??(LeveledHaskType Γ ★) :=
-    mapOptionTree guestJudgmentAsGArrowType X @@@ nil.
-
-  Hint Constructors Rule_Flat.
-  Context {ndr:@ND_Relation _ Rule}.
-
-  (*
-   * Here it is, what you've all been waiting for!  When reading this,
-   * it might help to have the definition for "Inductive ND" (see
-   * NaturalDeduction.v) handy as a cross-reference.
-   *)
-  Hint Constructors Rule_Flat.
-  Definition FlatteningFunctor_fmor
-    : forall h c,
-      (h~~{JudgmentsL (PCF Γ Δ ec)}~~>c) ->
-      ((obact h)~~{TypesL (SystemFCa Γ Δ)}~~>(obact c)).
-
-    set (@nil (HaskTyVar Γ ★)) as lev.
-
-    unfold hom; unfold ob; unfold ehom; simpl; unfold pmon_I; unfold obact; intros.
-
-    induction X; simpl.
-
-    (* the proof from no hypotheses of no conclusions (nd_id0) becomes RVoid *)
-    apply nd_rule; apply (org_fc _ _ [] [(_,_)] (RVoid _ _)). apply Flat_RVoid.
-
-    (* the proof from hypothesis X of conclusion X (nd_id1) becomes RVar *)
-    apply nd_rule; apply (org_fc _ _ [] [(_,_)] (RVar _ _ _ _)). apply Flat_RVar.
-
-    (* the proof from hypothesis X of no conclusions (nd_weak) becomes RWeak;;RVoid *)
-    eapply nd_comp;
-      [ idtac
-      | eapply nd_rule
-      ; eapply (org_fc  _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RWeak _)))
-      ; auto ].
-      eapply nd_rule.
-      eapply (org_fc _ _ [] [(_,_)] (RVoid _ _)); auto. apply Flat_RVoid.
-      apply Flat_RArrange.
-
-    (* the proof from hypothesis X of two identical conclusions X,,X (nd_copy) becomes RVar;;RJoin;;RCont *)
-    eapply nd_comp; [ idtac | eapply nd_rule; eapply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCont _))) ].
-      eapply nd_comp; [ apply nd_llecnac | idtac ].
-      set (snd_initial(SequentND:=pl_snd(ProgrammingLanguage:=SystemFCa Γ Δ))
-        (mapOptionTree (guestJudgmentAsGArrowType) h @@@ lev)) as q.
-      eapply nd_comp.
-      eapply nd_prod.
-      apply q.
-      apply q.
-      apply nd_rule. 
-      eapply (org_fc _ _ ([(_,_)],,[(_,_)]) [(_,_)] (RJoin _ _ _ _ _ _ )).
-      destruct h; simpl.
-      destruct o.
-      simpl.
-      apply Flat_RJoin.
-      apply Flat_RJoin.
-      apply Flat_RJoin.
-      apply Flat_RArrange.
-
-    (* nd_prod becomes nd_llecnac;;nd_prod;;RJoin *)
-    eapply nd_comp.
-      apply (nd_llecnac ;; nd_prod IHX1 IHX2).
-      apply nd_rule.
-      eapply (org_fc _ _ ([(_,_)],,[(_,_)]) [(_,_)] (RJoin _ _ _ _ _ _ )).
-      apply (Flat_RJoin Γ Δ (mapOptionTree guestJudgmentAsGArrowType h1 @@@ nil)
-       (mapOptionTree guestJudgmentAsGArrowType h2 @@@ nil)
-       (mapOptionTree guestJudgmentAsGArrowType c1 @@@ nil)
-       (mapOptionTree guestJudgmentAsGArrowType c2 @@@ nil)).
-
-    (* nd_comp becomes pl_subst (aka nd_cut) *)
-    eapply nd_comp.
-      apply (nd_llecnac ;; nd_prod IHX1 IHX2).
-      clear IHX1 IHX2 X1 X2.
-      apply (@snd_cut _ _ _ _ (pl_snd(ProgrammingLanguage:=SystemFCa Γ Δ))). 
-
-    (* nd_cancell becomes RVar;;RuCanL *)
-    eapply nd_comp;
-      [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RuCanL _))) ].
-      apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
-      apply Flat_RArrange.
-
-    (* nd_cancelr becomes RVar;;RuCanR *)
-    eapply nd_comp;
-      [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RuCanR _))) ].
-      apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
-      apply Flat_RArrange.
-
-    (* nd_llecnac becomes RVar;;RCanL *)
-    eapply nd_comp;
-      [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCanL _))) ].
-      apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
-      apply Flat_RArrange.
-
-    (* nd_rlecnac becomes RVar;;RCanR *)
-    eapply nd_comp;
-      [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCanR _))) ].
-      apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
-      apply Flat_RArrange.
-
-    (* nd_assoc becomes RVar;;RAssoc *)
-    eapply nd_comp;
-      [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RAssoc _ _ _))) ].
-      apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
-      apply Flat_RArrange.
-
-    (* nd_cossa becomes RVar;;RCossa *)
-    eapply nd_comp;
-      [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCossa _ _ _))) ].
-      apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
-      apply Flat_RArrange.
-
-      destruct r as [r rp].
-      rename h into h'.
-      rename c into c'.
-      rename r into r'.
-
-      refine (match rp as R in @Rule_PCF _ _ _ H C _
-                return
-                ND (OrgR Γ Δ) []
-                [sequent (mapOptionTree guestJudgmentAsGArrowType H @@@ nil)
-                  (mapOptionTree guestJudgmentAsGArrowType C @@@ nil)]
-                with
-                | PCF_RArrange         h c r q          => let case_RURule        := tt in _
-                | PCF_RLit             lit              => let case_RLit          := tt in _
-                | PCF_RNote            Σ τ   n          => let case_RNote         := tt in _
-                | PCF_RVar             σ                => let case_RVar          := tt in _
-                | PCF_RLam             Σ tx te          => let case_RLam          := tt in _
-                | PCF_RApp             Σ tx te   p      => let case_RApp          := tt in _
-                | PCF_RLet             Σ σ₁ σ₂   p      => let case_RLet          := tt in _
-                | PCF_RJoin    b c d e          => let case_RJoin := tt in _
-                | PCF_RVoid                       => let case_RVoid   := tt in _
-              (*| PCF_RCase            T κlen κ θ l x   => let case_RCase         := tt in _*)
-              (*| PCF_RLetRec          Σ₁ τ₁ τ₂ lev     => let case_RLetRec       := tt in _*)
-              end); simpl in *.
-      clear rp h' c' r'.
-
-      rewrite (unlev_lemma h (ec::nil)).
-      rewrite (unlev_lemma c (ec::nil)).
-      destruct case_RURule.
-        refine (match q as Q in Arrange H C
-                return
-                H=(h @@@ (ec :: nil)) ->
-                C=(c @@@ (ec :: nil)) ->
-                ND (OrgR Γ Δ) []
-                [sequent
-                  [ga_type (ga_rep (mapOptionTree unlev H)) (ga_rep r) @@ nil ]
-                  [ga_type (ga_rep (mapOptionTree unlev C)) (ga_rep r) @@ nil ] ]
-                  with
-          | RLeft   a b c r => let case_RLeft  := tt in _
-          | RRight  a b c r => let case_RRight := tt in _
-          | RCanL     b     => let case_RCanL  := tt in _
-          | RCanR     b     => let case_RCanR  := tt in _
-          | RuCanL    b     => let case_RuCanL := tt in _
-          | RuCanR    b     => let case_RuCanR := tt in _
-          | RAssoc    b c d => let case_RAssoc := tt in _
-          | RCossa    b c d => let case_RCossa := tt in _
-          | RExch     b c   => let case_RExch  := tt in _
-          | RWeak     b     => let case_RWeak  := tt in _
-          | RCont     b     => let case_RCont  := tt in _
-          | RComp a b c f g => let case_RComp  := tt in _
-        end (refl_equal _) (refl_equal _));
-        intros; simpl in *;
-        subst;
-        try rewrite <- unlev_lemma in *.
-
-      destruct case_RCanL.
-        apply magic.
-        apply ga_uncancell.
-        
-      destruct case_RCanR.
-        apply magic.
-        apply ga_uncancelr.
-
-      destruct case_RuCanL.
-        apply magic.
-        apply ga_cancell.
-
-      destruct case_RuCanR.
-        apply magic.
-        apply ga_cancelr.
-
-      destruct case_RAssoc.
-        apply magic.
-        apply ga_assoc.
-        
-      destruct case_RCossa.
-        apply magic.
-        apply ga_unassoc.
-
-      destruct case_RExch.
-        apply magic.
-        apply ga_swap.
-        
-      destruct case_RWeak.
-        apply magic.
-        apply ga_drop.
-        
-      destruct case_RCont.
-        apply magic.
-        apply ga_copy.
-        
-      destruct case_RLeft.
-        apply magic.
-        (*apply ga_second.*)
-        admit.
-        
-      destruct case_RRight.
-        apply magic.
-        (*apply ga_first.*)
-        admit.
-
-      destruct case_RComp.
-        apply magic.
-        (*apply ga_comp.*)
-        admit.
-
-      destruct case_RLit.
-        apply ga_lit.
-
-      (* hey cool, I figured out how to pass CoreNote's through... *)
-      destruct case_RNote.
-        eapply nd_comp.
-        eapply nd_rule.
-        eapply (org_fc _ _ [] [(_,_)] (RVar _ _ _ _)) . auto.
-        apply Flat_RVar.
-        apply nd_rule.
-        apply (org_fc _ _ [(_,_)] [(_,_)] (RNote _ _ _ _ _ n)). auto.
-        apply Flat_RNote.
-        
-      destruct case_RVar.
-        apply ga_id.
-
-      (*
-       *   class GArrow g (**) u => GArrowApply g (**) u (~>) where
-       *     ga_applyl    :: g (x**(x~>y)   ) y
-       *     ga_applyr    :: g (   (x~>y)**x) y
-       *   
-       *   class GArrow g (**) u => GArrowCurry g (**) u (~>) where
-       *     ga_curryl    :: g (x**y) z  ->  g x (y~>z)
-       *     ga_curryr    :: g (x**y) z  ->  g y (x~>z)
-       *)
-      destruct case_RLam.
-        (* GArrowCurry.ga_curry *)
-        admit.
-
-      destruct case_RApp.
-        (* GArrowApply.ga_apply *)
-        admit.
-
-      destruct case_RLet.
-        admit.
-
-      destruct case_RVoid.
-        apply ga_id.
-
-      destruct case_RJoin.
-        (* this assumes we want effects to occur in syntactically-left-to-right order *)
-        admit.
-        Defined.
-
-(*
-  Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
-    { fmor := FlatteningFunctor_fmor }.
-    Admitted.
-
-  Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
-    refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
-    Admitted.
-
-  Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
-    refine {| plsmme_pl := PCF n Γ Δ |}.
-    admit.
-    Defined.
-
-  Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
-    refine {| plsmme_pl := SystemFCa n Γ Δ |}.
-    admit.
-    Defined.
-
-  Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
-    admit.
-    Defined.
-
-  (* 5.1.4 *)
-  Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
-    admit.
-    Defined.
-*)
-  (*  ... and the retraction exists *)
-
-End HaskProofFlattener.
-

diff --git a/src/HaskProofStratified.v b/src/HaskProofStratified.v
deleted file mode 100644 (file)
index 177bd6d..0000000
--- a/src/HaskProofStratified.v
+++ /dev/null
@@ -1,588 +0,0 @@
-(*********************************************************************************************************************************)
-(* HaskProofStratified:                                                                                                          *)
-(*                                                                                                                               *)
-(*    An alternate representation for HaskProof which ensures that deductions on a given level are grouped into contiguous       *)
-(*    blocks.  This representation lacks the attractive compositionality properties of HaskProof, but makes it easier to         *)
-(*    perform the flattening process.                                                                                            *)
-(*                                                                                                                               *)
-(*********************************************************************************************************************************)
-
-Generalizable All Variables.
-Require Import Preamble.
-Require Import General.
-Require Import NaturalDeduction.
-Require Import Coq.Strings.String.
-Require Import Coq.Lists.List.
-
-Require Import HaskKinds.
-Require Import HaskCoreTypes.
-Require Import HaskLiteralsAndTyCons.
-Require Import HaskStrongTypes.
-Require Import HaskProof.
-Require Import NaturalDeduction.
-Require Import NaturalDeductionCategory.
-
-Require Import Algebras_ch4.
-Require Import Categories_ch1_3.
-Require Import Functors_ch1_4.
-Require Import Isomorphisms_ch1_5.
-Require Import ProductCategories_ch1_6_1.
-Require Import OppositeCategories_ch1_6_2.
-Require Import Enrichment_ch2_8.
-Require Import Subcategories_ch7_1.
-Require Import NaturalTransformations_ch7_4.
-Require Import NaturalIsomorphisms_ch7_5.
-Require Import MonoidalCategories_ch7_8.
-Require Import Coherence_ch7_8.
-
-Require Import HaskStrongTypes.
-Require Import HaskStrong.
-Require Import HaskProof.
-Require Import HaskStrongToProof.
-Require Import HaskProofToStrong.
-Require Import ProgrammingLanguage.
-
-Open Scope nd_scope.
-
-
-(*
- *  The flattening transformation.  Currently only TWO-level languages are
- *  supported, and the level-1 sublanguage is rather limited.
-*
- *  This file abuses terminology pretty badly.  For purposes of this file,
- *  "PCF" means "the level-1 sublanguage" and "FC" (aka System FC) means 
- *  the whole language (level-0 language including bracketed level-1 terms)
- *)
-Section HaskProofStratified.
-
-  Section PCF.
-
-  Context (ndr_systemfc:@ND_Relation _ Rule).
-
-  Context Γ (Δ:CoercionEnv Γ).
-  Definition PCFJudg (ec:HaskTyVar Γ ★) :=
-    @prod (Tree ??(HaskType Γ ★)) (Tree ??(HaskType Γ ★)).
-  Definition pcfjudg (ec:HaskTyVar Γ ★) :=
-    @pair (Tree ??(HaskType Γ ★)) (Tree ??(HaskType Γ ★)).
-
-  (* given an PCFJudg at depth (ec::depth) we can turn it into an PCFJudg
-   * from depth (depth) by wrapping brackets around everything in the
-   * succedent and repopulating *)
-  Definition brakify {ec} (j:PCFJudg ec) : Judg :=
-    match j with
-      (Σ,τ) => Γ > Δ > (Σ@@@(ec::nil)) |- (mapOptionTree (fun t => HaskBrak ec t) τ @@@ nil)
-      end.
-
-  Definition pcf_vars {Γ}(ec:HaskTyVar Γ ★)(t:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★)
-    := mapOptionTreeAndFlatten (fun lt =>
-      match lt with t @@ l => match l with
-                                | ec'::nil => if eqd_dec ec ec' then [t] else []
-                                | _ => []
-                              end
-      end) t.
-
-  Inductive MatchingJudgments {ec} : Tree ??(PCFJudg ec) -> Tree ??Judg -> Type :=
-    | match_nil    : MatchingJudgments [] []
-    | match_branch : forall a b c d, MatchingJudgments a b -> MatchingJudgments c d -> MatchingJudgments (a,,c) (b,,d)
-    | match_leaf   : 
-      forall Σ τ lev,
-        MatchingJudgments
-          [((pcf_vars ec Σ)         ,                              τ        )]
-          [Γ > Δ >              Σ  |- (mapOptionTree (HaskBrak ec) τ @@@ lev)].
-
-  Definition fc_vars {Γ}(ec:HaskTyVar Γ ★)(t:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★)
-    := mapOptionTreeAndFlatten (fun lt =>
-      match lt with t @@ l => match l with
-                                | ec'::nil => if eqd_dec ec ec' then [] else [t]
-                                | _ => []
-                              end
-      end) t.
-
-  Definition pcfjudg2judg ec (cj:PCFJudg ec) :=
-    match cj with (Σ,τ) => Γ > Δ > (Σ @@@ (ec::nil)) |- (τ @@@ (ec::nil)) end.
-
-  (* Rules allowed in PCF; i.e. rules we know how to turn into GArrows     *)
-  (* Rule_PCF consists of the rules allowed in flat PCF: everything except *)
-  (* AppT, AbsT, AppC, AbsC, Cast, Global, and some Case statements        *)
-  Inductive Rule_PCF (ec:HaskTyVar Γ ★)
-    : forall (h c:Tree ??(PCFJudg ec)), Rule (mapOptionTree (pcfjudg2judg ec) h) (mapOptionTree (pcfjudg2judg ec) c) -> Type :=
-  | PCF_RArrange    : ∀ x y t     a,  Rule_PCF ec [(_, _)] [(_, _)] (RArrange Γ Δ (x@@@(ec::nil)) (y@@@(ec::nil)) (t@@@(ec::nil)) a)
-  | PCF_RLit        : ∀ lit        ,  Rule_PCF ec [           ] [ ([],[_]) ] (RLit   Γ Δ  lit (ec::nil))
-  | PCF_RNote       : ∀ Σ τ   n    ,  Rule_PCF ec [(_,[_])] [(_,[_])] (RNote  Γ Δ  (Σ@@@(ec::nil)) τ         (ec::nil) n)
-  | PCF_RVar        : ∀ σ          ,  Rule_PCF ec [           ] [([_],[_])] (RVar   Γ Δ    σ         (ec::nil)  )
-  | PCF_RLam        : ∀ Σ tx te    ,  Rule_PCF ec [((_,,[_]),[_])] [(_,[_])] (RLam   Γ Δ  (Σ@@@(ec::nil)) tx te  (ec::nil)  )
-
-  | PCF_RApp             : ∀ Σ Σ' tx te ,
-    Rule_PCF ec ([(_,[_])],,[(_,[_])]) [((_,,_),[_])]
-    (RApp Γ Δ (Σ@@@(ec::nil))(Σ'@@@(ec::nil)) tx te (ec::nil))
-
-  | PCF_RLet             : ∀ Σ Σ' σ₂   p,
-    Rule_PCF ec ([(_,[_])],,[((_,,[_]),[_])]) [((_,,_),[_])]
-    (RLet Γ Δ (Σ@@@(ec::nil)) (Σ'@@@(ec::nil)) σ₂ p (ec::nil))
-
-  | PCF_RVoid      :                 Rule_PCF ec [           ] [([],[])] (RVoid   Γ Δ  )
-(*| PCF_RLetRec          : ∀ Σ₁ τ₁ τ₂   ,  Rule_PCF (ec::nil) _ _ (RLetRec Γ Δ Σ₁ τ₁ τ₂ (ec::nil) )*)
-  | PCF_RJoin    : ∀ Σ₁ Σ₂ τ₁ τ₂,  Rule_PCF ec ([(_,_)],,[(_,_)]) [((_,,_),(_,,_))]
-    (RJoin Γ Δ (Σ₁@@@(ec::nil)) (Σ₂@@@(ec::nil)) (τ₁@@@(ec::nil)) (τ₂@@@(ec::nil))).
-  (* need int/boolean case *)
-  Implicit Arguments Rule_PCF [ ].
-
-  Definition PCFRule lev h c := { r:_ & @Rule_PCF lev h c r }.
-  End PCF.
-
-  Definition FCJudg Γ (Δ:CoercionEnv Γ) :=
-    @prod (Tree ??(LeveledHaskType Γ ★)) (Tree ??(LeveledHaskType Γ ★)).
-  Definition fcjudg2judg {Γ}{Δ}(fc:FCJudg Γ Δ) :=
-    match fc with
-      (x,y) => Γ > Δ > x |- y
-        end.
-  Coercion fcjudg2judg : FCJudg >-> Judg.
-
-  Definition pcfjudg2fcjudg {Γ}{Δ} ec (fc:PCFJudg Γ ec) : FCJudg Γ Δ :=
-    match fc with
-      (x,y) => (x @@@ (ec::nil),y @@@ (ec::nil))
-        end.
-
-  (* An organized deduction has been reorganized into contiguous blocks whose
-   * hypotheses (if any) and conclusion have the same Γ and Δ and a fixed nesting depth.  The boolean
-   * indicates if non-PCF rules have been used *)
-  Inductive OrgR Γ Δ : Tree ??(FCJudg Γ Δ) -> Tree ??(FCJudg Γ Δ) -> Type :=
-
-  | org_fc        : forall (h c:Tree ??(FCJudg Γ Δ))
-    (r:Rule (mapOptionTree fcjudg2judg h) (mapOptionTree fcjudg2judg c)),
-    Rule_Flat r ->
-    OrgR _ _ h c
-
-  | org_pcf      : forall ec h c,
-    ND (PCFRule Γ Δ ec)  h c  ->
-    OrgR        Γ Δ     (mapOptionTree (pcfjudg2fcjudg ec) h)  (mapOptionTree (pcfjudg2fcjudg ec) c).
-
-  Definition mkEsc Γ Δ ec (h:Tree ??(PCFJudg Γ ec))
-    : ND Rule
-    (mapOptionTree (brakify Γ Δ) h)
-    (mapOptionTree (pcfjudg2judg Γ Δ ec) h).
-    apply nd_replicate; intros.
-    destruct o; simpl in *.
-    induction t0.
-    destruct a; simpl.
-    apply nd_rule.
-    apply REsc.
-    apply nd_id.
-    apply (Prelude_error "mkEsc got multi-leaf succedent").
-    Defined.
-
-  Definition mkBrak Γ Δ ec (h:Tree ??(PCFJudg Γ ec))
-    : ND Rule
-    (mapOptionTree (pcfjudg2judg Γ Δ ec) h)
-    (mapOptionTree (brakify Γ Δ) h).
-    apply nd_replicate; intros.
-    destruct o; simpl in *.
-    induction t0.
-    destruct a; simpl.
-    apply nd_rule.
-    apply RBrak.
-    apply nd_id.
-    apply (Prelude_error "mkBrak got multi-leaf succedent").
-    Defined.
-
-    (*
-  Definition Partition {Γ} ec (Σ:Tree ??(LeveledHaskType Γ ★)) :=
-    { vars:(_ * _) | 
-      fc_vars  ec Σ = fst vars /\
-      pcf_vars ec Σ = snd vars }.
-      *)
-
-  Definition pcfToND Γ Δ : forall ec h c,
-    ND (PCFRule Γ Δ ec) h c -> ND Rule (mapOptionTree (pcfjudg2judg Γ Δ ec) h) (mapOptionTree (pcfjudg2judg Γ Δ ec) c).
-    intros.
-    eapply (fun q => nd_map' _ q X).
-    intros.
-    destruct X0.
-    apply nd_rule.
-    apply x.
-    Defined.
-    
-  Instance OrgPCF Γ Δ lev : @ND_Relation _ (PCFRule Γ Δ lev) :=
-    { ndr_eqv := fun a b f g => (pcfToND  _ _ _ _ _ f) === (pcfToND _ _ _ _ _ g) }.
-    Admitted.
-
-  (*
-   * An intermediate representation necessitated by Coq's termination
-   * conditions.  This is basically a tree where each node is a
-   * subproof which is either entirely level-1 or entirely level-0
-   *)
-  Inductive Alternating : Tree ??Judg -> Type :=
-
-    | alt_nil    : Alternating []
-
-    | alt_branch : forall a b,
-      Alternating a -> Alternating b -> Alternating (a,,b)
-
-    | alt_fc     : forall h c,
-      Alternating h ->
-      ND Rule h c ->
-      Alternating c
-
-    | alt_pcf    : forall Γ Δ ec h c h' c',
-      MatchingJudgments Γ Δ  h  h' ->
-      MatchingJudgments Γ Δ  c  c' ->
-      Alternating h' ->
-      ND (PCFRule Γ Δ ec) h c ->
-      Alternating c'.
-
-  Require Import Coq.Logic.Eqdep.
-(*
-  Lemma magic a b c d ec e :
-    ClosedSIND(Rule:=Rule) [a > b > c |- [d @@  (ec :: e)]] ->
-    ClosedSIND(Rule:=Rule) [a > b > pcf_vars ec c @@@ (ec :: nil) |- [d @@  (ec :: nil)]].
-    admit.
-    Defined.
-
-  Definition orgify : forall Γ Δ Σ τ (pf:ClosedSIND(Rule:=Rule) [Γ > Δ > Σ |- τ]), Alternating [Γ > Δ > Σ |- τ].
-
-    refine (
-      fix  orgify_fc' Γ Δ Σ τ (pf:ClosedSIND [Γ > Δ > Σ |- τ]) {struct pf} : Alternating [Γ > Δ > Σ |- τ] :=
-        let case_main := tt in _
-      with orgify_fc c (pf:ClosedSIND c) {struct pf} : Alternating c :=
-      (match c as C return C=c -> Alternating C with
-        | T_Leaf None                    => fun _ => alt_nil
-        | T_Leaf (Some (Γ > Δ > Σ |- τ)) => let case_leaf := tt in fun eqpf => _
-        | T_Branch b1 b2                 => let case_branch := tt in fun eqpf => _
-      end (refl_equal _))
-      with orgify_pcf   Γ Δ ec pcfj j (m:MatchingJudgments Γ Δ pcfj j)
-        (pf:ClosedSIND (mapOptionTree (pcfjudg2judg Γ Δ ec) pcfj)) {struct pf} : Alternating j :=
-        let case_pcf := tt in _
-      for orgify_fc').
-
-      destruct case_main.
-      inversion pf; subst.
-      set (alt_fc _ _ (orgify_fc _ X) (nd_rule X0)) as backup.
-      refine (match X0 as R in Rule H C return
-                match C with
-                  | T_Leaf (Some (Γ > Δ > Σ |- τ)) =>
-                    h=H -> Alternating [Γ > Δ > Σ |- τ] -> Alternating [Γ > Δ > Σ |- τ]
-                  | _                              => True
-                end
-                 with
-                | RBrak   Σ a b c n m           => let case_RBrak := tt         in fun pf' backup => _
-                | REsc    Σ a b c n m           => let case_REsc := tt          in fun pf' backup => _
-                | _ => fun pf' x => x
-              end (refl_equal _) backup).
-      clear backup0 backup.
-
-      destruct case_RBrak.
-        rename c into ec.
-        set (@match_leaf Σ0 a ec n [b] m) as q.
-        set (orgify_pcf Σ0 a ec _ _ q) as q'.
-        apply q'.
-        simpl.
-        rewrite pf' in X.
-        apply magic in X.
-        apply X.
-
-      destruct case_REsc.
-        apply (Prelude_error "encountered Esc in wrong side of mkalt").
-
-    destruct case_leaf.
-      apply orgify_fc'.
-      rewrite eqpf.
-      apply pf.
-
-    destruct case_branch.
-      rewrite <- eqpf in pf.
-      inversion pf; subst.
-      apply no_rules_with_multiple_conclusions in X0.
-      inversion X0.
-      exists b1. exists b2.
-      auto.
-      apply (alt_branch _ _ (orgify_fc _ X) (orgify_fc _ X0)).
-
-    destruct case_pcf.
-    Admitted.
-
-  Definition pcfify Γ Δ ec : forall Σ τ,
-    ClosedSIND(Rule:=Rule) [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)]
-      -> ND (PCFRule Γ Δ ec) [] [(Σ,τ)].
-
-    refine ((
-      fix pcfify Σ τ (pn:@ClosedSIND _ Rule [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)]) {struct pn}
-      : ND (PCFRule Γ Δ ec) [] [(Σ,τ)] :=
-     (match pn in @ClosedSIND _ _ J return J=[Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)] -> _ with
-      | cnd_weak             => let case_nil    := tt in _
-      | cnd_rule h c cnd' r  => let case_rule   := tt in _
-      | cnd_branch _ _ c1 c2 => let case_branch := tt in _
-      end (refl_equal _)))).
-      intros.
-      inversion H.
-      intros.
-      destruct c; try destruct o; inversion H.
-      destruct j.
-      Admitted.
-*)
-  (* any proof in organized form can be "dis-organized" *)
-  (*
-  Definition unOrgR : forall Γ Δ h c, OrgR Γ Δ h c -> ND Rule h c.
-    intros.
-    induction X.
-      apply nd_rule.
-      apply r.
-    eapply nd_comp.
-      (*
-      apply (mkEsc h).
-      eapply nd_comp; [ idtac |  apply (mkBrak c) ].
-      apply pcfToND.
-      apply n.
-      *)
-      Admitted.
-  Definition unOrgND Γ Δ h c :  ND (OrgR Γ Δ) h c -> ND Rule h c := nd_map (unOrgR Γ Δ).
-  *)
-    
-  Hint Constructors Rule_Flat.
-
-  Definition PCF_Arrange {Γ}{Δ}{lev} : forall x y z, Arrange x y -> ND (PCFRule Γ Δ lev) [(x,z)] [(y,z)].
-    admit.
-    Defined.
-
-  Definition PCF_cut Γ Δ lev : forall a b c, ND (PCFRule Γ Δ lev) ([(a,b)],,[(b,c)]) [(a,c)].
-    intros.
-    destruct b.
-    destruct o.
-    destruct c.
-    destruct o.
-
-    (* when the cut is a single leaf and the RHS is a single leaf: *)
-    eapply nd_comp.
-      eapply nd_prod.
-      apply nd_id.
-      apply (PCF_Arrange [h] ([],,[h]) [h0]).
-      apply RuCanL.
-      eapply nd_comp; [ idtac | apply (PCF_Arrange ([],,a) a [h0]); apply RCanL ].
-      apply nd_rule.
-      (*
-      set (@RLet Γ Δ [] (a@@@(ec::nil)) h0 h (ec::nil)) as q.
-      exists q.
-      apply (PCF_RLet _ [] a h0 h).
-    apply (Prelude_error "cut rule invoked with [a|=[b]] [[b]|=[]]").
-    apply (Prelude_error "cut rule invoked with [a|=[b]] [[b]|=[x,,y]]").
-    apply (Prelude_error "cut rule invoked with [a|=[]]  [[]|=c]").
-    apply (Prelude_error "cut rule invoked with [a|=[b,,c]] [[b,,c]|=z]").
-    *)
-    Admitted.
-
-  Instance PCF_sequents Γ Δ lev ec : @SequentND _ (PCFRule Γ Δ lev) _ (pcfjudg Γ ec) :=
-    { snd_cut := PCF_cut Γ Δ lev }.
-    apply Build_SequentND.
-    intros.
-    induction a.
-    destruct a; simpl.
-    apply nd_rule.
-      exists (RVar _ _ _ _).
-      apply PCF_RVar.
-    apply nd_rule.
-      exists (RVoid _ _ ).
-      apply PCF_RVoid.
-    eapply nd_comp.
-      eapply nd_comp; [ apply nd_llecnac | idtac ].
-      apply (nd_prod IHa1 IHa2).
-      apply nd_rule.
-        exists (RJoin _ _ _ _ _ _). 
-        apply PCF_RJoin.
-      admit.
-        Defined.
-
-  Definition PCF_left Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [(b,c)] [((a,,b),(a,,c))].
-    eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ].
-    eapply nd_prod; [ apply snd_initial | apply nd_id ].
-    apply nd_rule.
-    set (@PCF_RJoin Γ Δ lev a b a c) as q'.
-    refine (existT _ _ _).
-    apply q'.
-    Admitted.
-
-  Definition PCF_right Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [(b,c)] [((b,,a),(c,,a))].
-    eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ].
-    eapply nd_prod; [ apply nd_id | apply snd_initial ].
-    apply nd_rule.
-    set (@PCF_RJoin Γ Δ lev b a c a) as q'.
-    refine (existT _ _ _).
-    apply q'.
-    Admitted.
-
-  Instance PCF_sequent_join Γ Δ lev : @ContextND _ (PCFRule Γ Δ lev) _ (pcfjudg Γ lev) _ :=
-  { cnd_expand_left  := fun a b c => PCF_left  Γ Δ lev c a b
-  ; cnd_expand_right := fun a b c => PCF_right Γ Δ lev c a b }.
-
-    intros; apply nd_rule. unfold PCFRule. simpl.
-      exists (RArrange _ _ _ _ _ (RCossa _ _ _)).
-      apply (PCF_RArrange _ _ lev ((a,,b),,c) (a,,(b,,c)) x).
-
-    intros; apply nd_rule. unfold PCFRule. simpl.
-      exists (RArrange _ _ _ _ _ (RAssoc _ _ _)).
-      apply (PCF_RArrange _ _ lev (a,,(b,,c)) ((a,,b),,c) x).
-
-    intros; apply nd_rule. unfold PCFRule. simpl.
-      exists (RArrange _ _ _ _ _ (RCanL _)).
-      apply (PCF_RArrange _ _ lev ([],,a) _ _).
-
-    intros; apply nd_rule. unfold PCFRule. simpl.
-      exists (RArrange _ _ _ _ _ (RCanR _)).
-      apply (PCF_RArrange _ _ lev (a,,[]) _ _).
-
-    intros; apply nd_rule. unfold PCFRule. simpl.
-      exists (RArrange _ _ _ _ _ (RuCanL _)).
-      apply (PCF_RArrange _ _ lev _ ([],,a) _).
-
-    intros; apply nd_rule. unfold PCFRule. simpl.
-      exists (RArrange _ _ _ _ _ (RuCanR _)).
-      apply (PCF_RArrange _ _ lev _ (a,,[]) _).
-      Defined.
-
-  Instance OrgPCF_SequentND_Relation Γ Δ lev : SequentND_Relation (PCF_sequent_join Γ Δ lev) (OrgPCF Γ Δ lev).
-    admit.
-    Defined.
-
-  Definition OrgPCF_ContextND_Relation Γ Δ lev
-    : @ContextND_Relation _ _ _ _ _ (PCF_sequent_join Γ Δ lev) (OrgPCF Γ Δ lev) (OrgPCF_SequentND_Relation Γ Δ lev).
-    admit.
-    Defined.
-
-  (* 5.1.3 *)
-  Instance PCF Γ Δ lev : ProgrammingLanguage :=
-  { pl_cnd     := PCF_sequent_join Γ Δ lev
-  ; pl_eqv     := OrgPCF_ContextND_Relation Γ Δ lev
-  }.
-
-  Definition SystemFCa_cut Γ Δ : forall a b c, ND (OrgR Γ Δ) ([(a,b)],,[(b,c)]) [(a,c)].
-    intros.
-    destruct b.
-    destruct o.
-    destruct c.
-    destruct o.
-
-    (* when the cut is a single leaf and the RHS is a single leaf: *)
-    (*
-    eapply nd_comp.
-      eapply nd_prod.
-      apply nd_id.
-      eapply nd_rule.
-      set (@org_fc) as ofc.
-      set (RArrange Γ Δ _ _ _ (RuCanL [l0])) as rule.
-      apply org_fc with (r:=RArrange _ _ _ _ _ (RuCanL [_])).
-      auto.
-      eapply nd_comp; [ idtac | eapply nd_rule; apply org_fc with (r:=RArrange _ _ _ _ _ (RCanL _)) ].
-      apply nd_rule.
-      destruct l.
-      destruct l0.
-      assert (h0=h2). admit.
-      subst.
-      apply org_fc with (r:=@RLet Γ Δ [] a h1 h h2). 
-      auto.
-      auto.
-      *)
-    admit.
-    apply (Prelude_error "systemfc cut rule invoked with [a|=[b]] [[b]|=[]]").
-    apply (Prelude_error "systemfc cut rule invoked with [a|=[b]] [[b]|=[x,,y]]").
-    apply (Prelude_error "systemfc rule invoked with [a|=[]]  [[]|=c]").
-    apply (Prelude_error "systemfc rule invoked with [a|=[b,,c]] [[b,,c]|=z]").
-    Defined.
-
-  Instance SystemFCa_sequents Γ Δ : @SequentND _ (OrgR Γ Δ) _ _ :=
-  { snd_cut := SystemFCa_cut Γ Δ }.
-    apply Build_SequentND.
-    intros.
-    induction a.
-    destruct a; simpl.
-    (*
-    apply nd_rule.
-      destruct l.
-      apply org_fc with (r:=RVar _ _ _ _).
-      auto.
-    apply nd_rule.
-      apply org_fc with (r:=RVoid _ _ ).
-      auto.
-    eapply nd_comp.
-      eapply nd_comp; [ apply nd_llecnac | idtac ].
-      apply (nd_prod IHa1 IHa2).
-      apply nd_rule.
-        apply org_fc with (r:=RJoin _ _ _ _ _ _). 
-        auto.
-      admit.
-      *)
-      admit.
-      admit.
-      admit.
-      admit.
-      Defined.
-
-  Definition SystemFCa_left Γ Δ a b c : ND (OrgR Γ Δ) [(b,c)] [((a,,b),(a,,c))].
-    admit.
-    (*
-    eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ].
-    eapply nd_prod; [ apply snd_initial | apply nd_id ].
-    apply nd_rule.
-    apply org_fc with (r:=RJoin Γ Δ a b a c).
-    auto.
-    *)
-    Defined.
-
-  Definition SystemFCa_right Γ Δ a b c : ND (OrgR Γ Δ) [(b,c)] [((b,,a),(c,,a))].
-    admit.
-    (*
-    eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ].
-    eapply nd_prod; [ apply nd_id | apply snd_initial ].
-    apply nd_rule.
-    apply org_fc with (r:=RJoin Γ Δ b a c a).
-    auto.
-    *)
-    Defined.
-
-  Instance SystemFCa_sequent_join Γ Δ : @ContextND _ _ _ _ (SystemFCa_sequents Γ Δ) :=
-  { cnd_expand_left  := fun a b c => SystemFCa_left Γ Δ c a b
-  ; cnd_expand_right := fun a b c => SystemFCa_right Γ Δ c a b }.
-    (*
-    intros; apply nd_rule. simpl.
-      apply (org_fc _ _ _ _ ((RArrange _ _ _ _ _ (RCossa _ _ _)))).
-      auto.
-
-    intros; apply nd_rule. simpl.
-      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RAssoc _ _ _))); auto.
-
-    intros; apply nd_rule. simpl.
-      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RCanL _))); auto.
-
-    intros; apply nd_rule. simpl.
-      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RCanR _))); auto.
-
-    intros; apply nd_rule. simpl.
-      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RuCanL _))); auto.
-
-    intros; apply nd_rule. simpl.
-      apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RuCanR _))); auto.
-      *)
-      admit.
-      admit.
-      admit.
-      admit.
-      admit.
-      admit.
-      Defined.
-
-  Instance OrgFC Γ Δ : @ND_Relation _ (OrgR Γ Δ).
-    Admitted.
-
-  Instance OrgFC_SequentND_Relation Γ Δ : SequentND_Relation (SystemFCa_sequent_join Γ Δ) (OrgFC Γ Δ).
-    admit.
-    Defined.
-
-  Definition OrgFC_ContextND_Relation Γ Δ
-    : @ContextND_Relation _ _ _ _ _ (SystemFCa_sequent_join Γ Δ) (OrgFC Γ Δ) (OrgFC_SequentND_Relation Γ Δ).
-    admit.
-    Defined.
-
-  (* 5.1.2 *)
-  Instance SystemFCa Γ Δ : @ProgrammingLanguage (LeveledHaskType Γ ★) _ :=
-  { pl_eqv                := OrgFC_ContextND_Relation Γ Δ
-  ; pl_snd                := SystemFCa_sequents Γ Δ
-  }.
-
-End HaskProofStratified.

diff --git a/src/PCF.v b/src/PCF.v
index 16dceef..00ffd77 100644 (file)
--- a/src/PCF.v
+++ b/src/PCF.v
@@ -90,30 +90,9 @@ Section PCF.
           [((pcf_vars ec Σ)         ,                              τ        )]
           [Γ > Δ >              Σ  |- (mapOptionTree (HaskBrak ec) τ @@@ lev)].
 
           [((pcf_vars ec Σ)         ,                              τ        )]
           [Γ > Δ >              Σ  |- (mapOptionTree (HaskBrak ec) τ @@@ lev)].
 

-  Definition fc_vars {Γ}(ec:HaskTyVar Γ ★)(t:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★)
-    := mapOptionTreeAndFlatten (fun lt =>
-      match lt with t @@ l => match l with
-                                | ec'::nil => if eqd_dec ec ec' then [] else [t]
-                                | _ => []
-                              end
-      end) t.
-
-  Definition FCJudg :=
-    @prod (Tree ??(LeveledHaskType Γ ★)) (Tree ??(LeveledHaskType Γ ★)).
-  Definition fcjudg2judg (fc:FCJudg) :=
-    match fc with
-      (x,y) => Γ > Δ > x |- y
-        end.
-  Coercion fcjudg2judg : FCJudg >-> Judg.
-

   Definition pcfjudg2judg ec (cj:PCFJudg ec) :=
     match cj with (Σ,τ) => Γ > Δ > (Σ @@@ (ec::nil)) |- (τ @@@ (ec::nil)) end.
 
   Definition pcfjudg2judg ec (cj:PCFJudg ec) :=
     match cj with (Σ,τ) => Γ > Δ > (Σ @@@ (ec::nil)) |- (τ @@@ (ec::nil)) end.
 

-  Definition pcfjudg2fcjudg ec (fc:PCFJudg ec) : FCJudg :=
-    match fc with
-      (x,y) => (x @@@ (ec::nil),y @@@ (ec::nil))
-        end.
-

   (* Rules allowed in PCF; i.e. rules we know how to turn into GArrows     *)
   (* Rule_PCF consists of the rules allowed in flat PCF: everything except *)
   (* AppT, AbsT, AppC, AbsC, Cast, Global, and some Case statements        *)
   (* Rules allowed in PCF; i.e. rules we know how to turn into GArrows     *)
   (* Rule_PCF consists of the rules allowed in flat PCF: everything except *)
   (* AppT, AbsT, AppC, AbsC, Cast, Global, and some Case statements        *)

@@ -171,13 +150,6 @@ Section PCF.
     apply (Prelude_error "mkBrak got multi-leaf succedent").
     Defined.
 
     apply (Prelude_error "mkBrak got multi-leaf succedent").
     Defined.
 

-    (*
-  Definition Partition {Γ} ec (Σ:Tree ??(LeveledHaskType Γ ★)) :=
-    { vars:(_ * _) | 
-      fc_vars  ec Σ = fst vars /\
-      pcf_vars ec Σ = snd vars }.
-      *)
-

   Definition pcfToND Γ Δ : forall ec h c,
     ND (PCFRule Γ Δ ec) h c -> ND Rule (mapOptionTree (pcfjudg2judg Γ Δ ec) h) (mapOptionTree (pcfjudg2judg Γ Δ ec) c).
     intros.
   Definition pcfToND Γ Δ : forall ec h c,
     ND (PCFRule Γ Δ ec) h c -> ND Rule (mapOptionTree (pcfjudg2judg Γ Δ ec) h) (mapOptionTree (pcfjudg2judg Γ Δ ec) c).
     intros.

@@ -192,120 +164,6 @@ Section PCF.
     { ndr_eqv := fun a b f g => (pcfToND  _ _ _ _ _ f) === (pcfToND _ _ _ _ _ g) }.
     Admitted.
 
     { ndr_eqv := fun a b f g => (pcfToND  _ _ _ _ _ f) === (pcfToND _ _ _ _ _ g) }.
     Admitted.
 

-  (*
-   * An intermediate representation necessitated by Coq's termination
-   * conditions.  This is basically a tree where each node is a
-   * subproof which is either entirely level-1 or entirely level-0
-   *)
-  Inductive Alternating : Tree ??Judg -> Type :=
-
-    | alt_nil    : Alternating []
-
-    | alt_branch : forall a b,
-      Alternating a -> Alternating b -> Alternating (a,,b)
-
-    | alt_fc     : forall h c,
-      Alternating h ->
-      ND Rule h c ->
-      Alternating c
-
-    | alt_pcf    : forall Γ Δ ec h c h' c',
-      MatchingJudgments Γ Δ  h  h' ->
-      MatchingJudgments Γ Δ  c  c' ->
-      Alternating h' ->
-      ND (PCFRule Γ Δ ec) h c ->
-      Alternating c'.
-
-  Require Import Coq.Logic.Eqdep.
-(*
-  Lemma magic a b c d ec e :
-    ClosedSIND(Rule:=Rule) [a > b > c |- [d @@  (ec :: e)]] ->
-    ClosedSIND(Rule:=Rule) [a > b > pcf_vars ec c @@@ (ec :: nil) |- [d @@  (ec :: nil)]].
-    admit.
-    Defined.
-
-  Definition orgify : forall Γ Δ Σ τ (pf:ClosedSIND(Rule:=Rule) [Γ > Δ > Σ |- τ]), Alternating [Γ > Δ > Σ |- τ].
-
-    refine (
-      fix  orgify_fc' Γ Δ Σ τ (pf:ClosedSIND [Γ > Δ > Σ |- τ]) {struct pf} : Alternating [Γ > Δ > Σ |- τ] :=
-        let case_main := tt in _
-      with orgify_fc c (pf:ClosedSIND c) {struct pf} : Alternating c :=
-      (match c as C return C=c -> Alternating C with
-        | T_Leaf None                    => fun _ => alt_nil
-        | T_Leaf (Some (Γ > Δ > Σ |- τ)) => let case_leaf := tt in fun eqpf => _
-        | T_Branch b1 b2                 => let case_branch := tt in fun eqpf => _
-      end (refl_equal _))
-      with orgify_pcf   Γ Δ ec pcfj j (m:MatchingJudgments Γ Δ pcfj j)
-        (pf:ClosedSIND (mapOptionTree (pcfjudg2judg Γ Δ ec) pcfj)) {struct pf} : Alternating j :=
-        let case_pcf := tt in _
-      for orgify_fc').
-
-      destruct case_main.
-      inversion pf; subst.
-      set (alt_fc _ _ (orgify_fc _ X) (nd_rule X0)) as backup.
-      refine (match X0 as R in Rule H C return
-                match C with
-                  | T_Leaf (Some (Γ > Δ > Σ |- τ)) =>
-                    h=H -> Alternating [Γ > Δ > Σ |- τ] -> Alternating [Γ > Δ > Σ |- τ]
-                  | _                              => True
-                end
-                 with
-                | RBrak   Σ a b c n m           => let case_RBrak := tt         in fun pf' backup => _
-                | REsc    Σ a b c n m           => let case_REsc := tt          in fun pf' backup => _
-                | _ => fun pf' x => x
-              end (refl_equal _) backup).
-      clear backup0 backup.
-
-      destruct case_RBrak.
-        rename c into ec.
-        set (@match_leaf Σ0 a ec n [b] m) as q.
-        set (orgify_pcf Σ0 a ec _ _ q) as q'.
-        apply q'.
-        simpl.
-        rewrite pf' in X.
-        apply magic in X.
-        apply X.
-
-      destruct case_REsc.
-        apply (Prelude_error "encountered Esc in wrong side of mkalt").
-
-    destruct case_leaf.
-      apply orgify_fc'.
-      rewrite eqpf.
-      apply pf.
-
-    destruct case_branch.
-      rewrite <- eqpf in pf.
-      inversion pf; subst.
-      apply no_rules_with_multiple_conclusions in X0.
-      inversion X0.
-      exists b1. exists b2.
-      auto.
-      apply (alt_branch _ _ (orgify_fc _ X) (orgify_fc _ X0)).
-
-    destruct case_pcf.
-    Admitted.
-
-  Definition pcfify Γ Δ ec : forall Σ τ,
-    ClosedSIND(Rule:=Rule) [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)]
-      -> ND (PCFRule Γ Δ ec) [] [(Σ,τ)].
-
-    refine ((
-      fix pcfify Σ τ (pn:@ClosedSIND _ Rule [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)]) {struct pn}
-      : ND (PCFRule Γ Δ ec) [] [(Σ,τ)] :=
-     (match pn in @ClosedSIND _ _ J return J=[Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)] -> _ with
-      | cnd_weak             => let case_nil    := tt in _
-      | cnd_rule h c cnd' r  => let case_rule   := tt in _
-      | cnd_branch _ _ c1 c2 => let case_branch := tt in _
-      end (refl_equal _)))).
-      intros.
-      inversion H.
-      intros.
-      destruct c; try destruct o; inversion H.
-      destruct j.
-      Admitted.
-*)
-    

   Hint Constructors Rule_Flat.
 
   Definition PCF_Arrange {Γ}{Δ}{lev} : forall x y z, Arrange x y -> ND (PCFRule Γ Δ lev) [(x,z)] [(y,z)].
   Hint Constructors Rule_Flat.
 
   Definition PCF_Arrange {Γ}{Δ}{lev} : forall x y z, Arrange x y -> ND (PCFRule Γ Δ lev) [(x,z)] [(y,z)].