replace UJudg with Arrange

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 2f0856f..ba0c241 100644 (file)
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -35,13 +35,11 @@ Require Import HaskWeakToCore.
 Require Import HaskProofToStrong.
 
 Require Import ProgrammingLanguage.
 Require Import HaskProofToStrong.
 
 Require Import ProgrammingLanguage.

-

 Require Import HaskProofCategory.
 Require Import HaskProofCategory.

-(*
-Require Import HaskStrongCategory.
-*)

 Require Import ReificationsIsomorphicToGeneralizedArrows.
 
 Require Import ReificationsIsomorphicToGeneralizedArrows.
 

+(*Require Import HaskStrongCategory.*)
+

 Open Scope string_scope.
 Extraction Language Haskell.
 
 Open Scope string_scope.
 Extraction Language Haskell.
 

@@ -228,6 +226,7 @@ Section core2proof.
       apply t.
       Defined.
 
       apply t.
       Defined.
 

+(*

     Definition env := ★::nil.
     Definition freshTV : HaskType env ★ := haskTyVarToType (FreshHaskTyVar _).
     Definition idproof0 : ND Rule [] [env > nil > [] |- [freshTV--->freshTV @@ nil]].
     Definition env := ★::nil.
     Definition freshTV : HaskType env ★ := haskTyVarToType (FreshHaskTyVar _).
     Definition idproof0 : ND Rule [] [env > nil > [] |- [freshTV--->freshTV @@ nil]].

@@ -235,13 +234,13 @@ Section core2proof.
       eapply nd_comp.
       eapply nd_rule.
       apply RVar.
       eapply nd_comp.
       eapply nd_rule.
       apply RVar.

-      eapply nd_rule.
-      eapply (RURule _ _ _ _ (RuCanL _ _)) .
+      eapply nd_rule
+      eapply (RArrange _ _ _ _ (RuCanL _ _)) .

       eapply nd_rule.
       eapply RLam.
       Defined.
 
       eapply nd_rule.
       eapply RLam.
       Defined.
 

-(*
+

     Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
     addErrorMessage ("input CoreSyn: " +++ toString ce)
     (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
     Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
     addErrorMessage ("input CoreSyn: " +++ toString ce)
     (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (

diff --git a/src/HaskProof.v b/src/HaskProof.v
index 7e3ef1c..4cc4605 100644 (file)
--- a/src/HaskProof.v
+++ b/src/HaskProof.v
@@ -32,23 +32,6 @@ Inductive Judg  :=
   Judg.
   Notation "Γ > Δ > a '|-' s" := (mkJudg Γ Δ a s) (at level 52, Δ at level 50, a at level 52, s at level 50).
 
   Judg.
   Notation "Γ > Δ > a '|-' s" := (mkJudg Γ Δ a s) (at level 52, Δ at level 50, a at level 52, s at level 50).
 

-(* A Uniform Judgment (UJudg) has its environment as a type index; we'll use these to distinguish proofs that have a single,
- * uniform context throughout the whole proof.  Such proofs are important because (1) we can do left and right context
- * expansion on them (see rules RLeft and RRight) and (2) they will form the fiber categories of our fibration later on *)
-Inductive UJudg (Γ:TypeEnv)(Δ:CoercionEnv Γ) :=
-  mkUJudg :
-  Tree ??(LeveledHaskType Γ ★) ->
-  Tree ??(LeveledHaskType Γ ★) ->
-  UJudg Γ Δ.
-  Notation "Γ >> Δ > a '|-' s" := (mkUJudg Γ Δ a s) (at level 52, Δ at level 50, a at level 52, s at level 50).
-  Definition ext_tree_left  {Γ}{Δ}  := (fun ctx (j:UJudg Γ Δ) => match j with mkUJudg t s => mkUJudg Γ Δ (ctx,,t) s end).
-  Definition ext_tree_right {Γ}{Δ}  := (fun ctx (j:UJudg Γ Δ) => match j with mkUJudg t s => mkUJudg Γ Δ (t,,ctx) s end).
-
-(* we can turn a UJudg into a Judg by simply internalizing the index *)
-Definition UJudg2judg {Γ}{Δ}(ej:@UJudg Γ Δ) : Judg :=
-  match ej with mkUJudg t s => Γ > Δ > t |- s end.
-  Coercion UJudg2judg : UJudg >-> Judg.
-

 (* information needed to define a case branch in a HaskProof *)
 Record ProofCaseBranch {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ ★}{avars}{sac:@StrongAltCon tc} :=
 { pcb_freevars       :  Tree ??(LeveledHaskType Γ ★)
 (* information needed to define a case branch in a HaskProof *)
 Record ProofCaseBranch {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ ★}{avars}{sac:@StrongAltCon tc} :=
 { pcb_freevars       :  Tree ??(LeveledHaskType Γ ★)

@@ -61,24 +44,25 @@ Record ProofCaseBranch {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ ★}{ava
 Implicit Arguments ProofCaseBranch [ ].
 
 (* Figure 3, production $\vdash_E$, Uniform rules *)
 Implicit Arguments ProofCaseBranch [ ].
 
 (* Figure 3, production $\vdash_E$, Uniform rules *)

-Inductive URule {Γ}{Δ} : Tree ??(UJudg Γ Δ) -> Tree ??(UJudg Γ Δ) -> Type :=
-| RCanL   : ∀ t a        ,                          URule  [Γ>>Δ>    [],,a   |- t         ]      [Γ>>Δ>       a   |- t           ]
-| RCanR   : ∀ t a        ,                          URule  [Γ>>Δ>    a,,[]   |- t         ]      [Γ>>Δ>       a   |- t           ]
-| RuCanL  : ∀ t a        ,                          URule  [Γ>>Δ>       a    |- t         ]      [Γ>>Δ>  [],,a    |- t           ]
-| RuCanR  : ∀ t a        ,                          URule  [Γ>>Δ>       a    |- t         ]      [Γ>>Δ>  a,,[]    |- t           ]
-| RAssoc  : ∀ t a b c    ,                          URule  [Γ>>Δ>a,,(b,,c)   |- t         ]      [Γ>>Δ>(a,,b),,c  |- t           ]
-| RCossa  : ∀ t a b c    ,                          URule  [Γ>>Δ>(a,,b),,c   |- t         ]      [Γ>>Δ> a,,(b,,c) |- t           ]
-| RLeft   : ∀ h c x      ,             URule h c -> URule (mapOptionTree (ext_tree_left  x) h) (mapOptionTree (ext_tree_left  x) c)
-| RRight  : ∀ h c x      ,             URule h c -> URule (mapOptionTree (ext_tree_right x) h) (mapOptionTree (ext_tree_right x) c)
-| RExch   : ∀ t a b      ,                          URule  [Γ>>Δ>   (b,,a)   |- t         ]      [Γ>>Δ>  (a,,b)   |- t           ]
-| RWeak   : ∀ t a        ,                          URule  [Γ>>Δ>       []   |- t         ]      [Γ>>Δ>       a   |- t           ]
-| RCont   : ∀ t a        ,                          URule  [Γ>>Δ>  (a,,a)    |- t         ]      [Γ>>Δ>       a   |- t           ].
-
+Inductive Arrange {T} : Tree ??T -> Tree ??T -> Type :=
+| RCanL   : forall a        ,                Arrange  (    [],,a   )      (       a   )
+| RCanR   : forall a        ,                Arrange  (    a,,[]   )      (       a   )
+| RuCanL  : forall a        ,                Arrange  (       a    )      (  [],,a    )
+| RuCanR  : forall a        ,                Arrange  (       a    )      (  a,,[]    )
+| RAssoc  : forall a b c    ,                Arrange  (a,,(b,,c)   )      ((a,,b),,c  )
+| RCossa  : forall a b c    ,                Arrange  ((a,,b),,c   )      ( a,,(b,,c) )
+| RExch   : forall a b      ,                Arrange  (   (b,,a)   )      (  (a,,b)   )
+| RWeak   : forall a        ,                Arrange  (       []   )      (       a   )
+| RCont   : forall a        ,                Arrange  (  (a,,a)    )      (       a   )
+| RLeft   : forall {h}{c} x , Arrange h c -> Arrange  (    x,,h    )      (       x,,c)
+| RRight  : forall {h}{c} x , Arrange h c -> Arrange  (    h,,x    )      (       c,,x)
+| RComp   : forall {a}{b}{c}, Arrange a b -> Arrange b c -> Arrange a c
+.

 
 (* Figure 3, production $\vdash_E$, all rules *)
 Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
 
 
 (* Figure 3, production $\vdash_E$, all rules *)
 Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
 

-| RURule  : ∀ Γ Δ h c,                  @URule Γ Δ h c -> Rule (mapOptionTree UJudg2judg h) (mapOptionTree UJudg2judg c)
+| RArrange  : ∀ Γ Δ Σ₁ Σ₂ Σ,         Arrange Σ₁ Σ₂ -> Rule [Γ > Δ > Σ₁     |- Σ              ]   [Γ > Δ > Σ₂    |- Σ              ]

 
 (* λ^α rules *)
 | RBrak : ∀ Γ Δ t v Σ l,                              Rule [Γ > Δ > Σ      |- [t  @@ (v::l) ]]   [Γ > Δ > Σ     |- [<[v|-t]>   @@l]]
 
 (* λ^α rules *)
 | RBrak : ∀ Γ Δ t v Σ l,                              Rule [Γ > Δ > Σ      |- [t  @@ (v::l) ]]   [Γ > Δ > Σ     |- [<[v|-t]>   @@l]]

@@ -93,8 +77,7 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
 | RGlobal : ∀ Γ Δ τ       l,   WeakExprVar ->         Rule [                                 ]   [Γ>Δ>     []   |- [τ          @@l]]
 | RLam    : forall Γ Δ Σ (tx:HaskType Γ ★) te l,      Rule [Γ>Δ> Σ,,[tx@@l]|- [te@@l]        ]   [Γ>Δ>    Σ     |- [tx--->te   @@l]]
 | RCast   : forall Γ Δ Σ (σ₁ σ₂:HaskType Γ ★) l,
 | RGlobal : ∀ Γ Δ τ       l,   WeakExprVar ->         Rule [                                 ]   [Γ>Δ>     []   |- [τ          @@l]]
 | RLam    : forall Γ Δ Σ (tx:HaskType Γ ★) te l,      Rule [Γ>Δ> Σ,,[tx@@l]|- [te@@l]        ]   [Γ>Δ>    Σ     |- [tx--->te   @@l]]
 | RCast   : forall Γ Δ Σ (σ₁ σ₂:HaskType Γ ★) l,

-HaskCoercion Γ Δ (σ₁∼∼∼σ₂) ->
- Rule [Γ>Δ> Σ         |- [σ₁@@l]         ]   [Γ>Δ>    Σ     |- [σ₂          @@l]]
+                   HaskCoercion Γ Δ (σ₁∼∼∼σ₂) ->      Rule [Γ>Δ> Σ         |- [σ₁@@l]        ]   [Γ>Δ>    Σ     |- [σ₂         @@l]]

 | RBindingGroup  : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ ,   Rule ([Γ > Δ > Σ₁ |- τ₁ ],,[Γ > Δ > Σ₂ |- τ₂ ])         [Γ>Δ>  Σ₁,,Σ₂  |- τ₁,,τ₂          ]
 | RApp           : ∀ Γ Δ Σ₁ Σ₂ tx te l,  Rule ([Γ>Δ> Σ₁       |- [tx--->te @@l]],,[Γ>Δ> Σ₂ |- [tx@@l]])  [Γ>Δ> Σ₁,,Σ₂ |- [te   @@l]]
 | RLet           : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₁,,[σ₂@@l] |- [σ₁@@l] ],,[Γ>Δ> Σ₂ |- [σ₂@@l]])     [Γ>Δ> Σ₁,,Σ₂ |- [σ₁   @@l]]
 | RBindingGroup  : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ ,   Rule ([Γ > Δ > Σ₁ |- τ₁ ],,[Γ > Δ > Σ₂ |- τ₂ ])         [Γ>Δ>  Σ₁,,Σ₂  |- τ₁,,τ₂          ]
 | RApp           : ∀ Γ Δ Σ₁ Σ₂ tx te l,  Rule ([Γ>Δ> Σ₁       |- [tx--->te @@l]],,[Γ>Δ> Σ₂ |- [tx@@l]])  [Γ>Δ> Σ₁,,Σ₂ |- [te   @@l]]
 | RLet           : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₁,,[σ₂@@l] |- [σ₁@@l] ],,[Γ>Δ> Σ₂ |- [σ₂@@l]])     [Γ>Δ> Σ₁,,Σ₂ |- [σ₁   @@l]]

@@ -116,12 +99,11 @@ HaskCoercion Γ Δ (σ₁∼∼∼σ₂) ->
                         [Γ > Δ >                                              Σ |- [ caseType tc avars @@ lev ] ])
                         [Γ > Δ > (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) alts),,Σ |- [ tbranches         @@ lev ] ]
 .
                         [Γ > Δ >                                              Σ |- [ caseType tc avars @@ lev ] ])
                         [Γ > Δ > (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) alts),,Σ |- [ tbranches         @@ lev ] ]
 .

-Coercion RURule : URule >-> Rule.

 
 
 (* A rule is considered "flat" if it is neither RBrak nor REsc *)
 Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop :=
 
 
 (* A rule is considered "flat" if it is neither RBrak nor REsc *)
 Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop :=

-| Flat_RURule           : ∀ Γ Δ  h c r            ,  Rule_Flat (RURule Γ Δ  h c r)
+| Flat_RArrange         : ∀ Γ Δ  h c r          a ,  Rule_Flat (RArrange Γ Δ h c r a)

 | Flat_RNote            : ∀ Γ Δ Σ τ l n            ,  Rule_Flat (RNote Γ Δ Σ τ l n)
 | Flat_RLit             : ∀ Γ Δ Σ τ               ,  Rule_Flat (RLit Γ Δ Σ τ  )
 | Flat_RVar             : ∀ Γ Δ  σ               l,  Rule_Flat (RVar Γ Δ  σ         l)
 | Flat_RNote            : ∀ Γ Δ Σ τ l n            ,  Rule_Flat (RNote Γ Δ Σ τ l n)
 | Flat_RLit             : ∀ Γ Δ Σ τ               ,  Rule_Flat (RLit Γ Δ Σ τ  )
 | Flat_RVar             : ∀ Γ Δ  σ               l,  Rule_Flat (RVar Γ Δ  σ         l)

@@ -138,53 +120,9 @@ Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop :=
 | Flat_RCase            : ∀ Σ Γ  T κlen κ θ l x  , Rule_Flat (RCase Σ Γ T κlen κ θ l x)
 | Flat_RLetRec          : ∀ Γ Δ Σ₁ τ₁ τ₂ lev,      Rule_Flat (RLetRec Γ Δ Σ₁ τ₁ τ₂ lev).
 
 | Flat_RCase            : ∀ Σ Γ  T κlen κ θ l x  , Rule_Flat (RCase Σ Γ T κlen κ θ l x)
 | Flat_RLetRec          : ∀ Γ Δ Σ₁ τ₁ τ₂ lev,      Rule_Flat (RLetRec Γ Δ Σ₁ τ₁ τ₂ lev).
 

-(* given a proof that uses only uniform rules, we can produce a general proof *)
-Definition UND_to_ND Γ Δ h c : ND (@URule Γ Δ) h c -> ND Rule (mapOptionTree UJudg2judg h) (mapOptionTree UJudg2judg c)
-  := @nd_map' _ (@URule Γ Δ ) _ Rule (@UJudg2judg Γ Δ ) (fun h c r => nd_rule (RURule _ _ h c r)) h c.
-
-Lemma no_urules_with_empty_conclusion : forall Γ Δ c h, @URule Γ Δ c h -> h=[] -> False.
-  intro.
-  intro.
-  induction 1; intros; inversion H.
-  simpl in *;  destruct c; try destruct o;  simpl in *; try destruct u;  inversion H;  simpl in *;  apply IHX;  auto;  inversion H1.
-  simpl in *;  destruct c; try destruct o;  simpl in *; try destruct u;  inversion H;  simpl in *;  apply IHX;  auto;  inversion H1.
-  Qed.
-

 Lemma no_rules_with_empty_conclusion : forall c h, @Rule c h -> h=[] -> False.
   intros.
   destruct X; try destruct c; try destruct o; simpl in *; try inversion H.
 Lemma no_rules_with_empty_conclusion : forall c h, @Rule c h -> h=[] -> False.
   intros.
   destruct X; try destruct c; try destruct o; simpl in *; try inversion H.

-  apply no_urules_with_empty_conclusion in u.
-  apply u.
-  auto.
-  Qed.
-
-Lemma no_urules_with_multiple_conclusions : forall Γ Δ c h,
-  @URule Γ Δ c h -> { h1:Tree ??(UJudg Γ Δ) & { h2:Tree ??(UJudg Γ Δ) & h=(h1,,h2) }} -> False.
-  intro.
-  intro.
-  induction 1; intros.
-  inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
-  inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
-  inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
-  inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
-  inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
-  inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
-
-  apply IHX.
-  destruct X0. destruct s. destruct c; try destruct o; try destruct u; simpl in *.
-    inversion e.
-    inversion e.
-    exists c1. exists c2. auto.
-
-  apply IHX.
-  destruct X0. destruct s. destruct c; try destruct o; try destruct u; simpl in *.
-    inversion e.
-    inversion e.
-    exists c1. exists c2. auto.
-
-  inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
-  inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
-  inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.

   Qed.
 
 Lemma no_rules_with_multiple_conclusions : forall c h,
   Qed.
 
 Lemma no_rules_with_multiple_conclusions : forall c h,

@@ -194,7 +132,6 @@ Lemma no_rules_with_multiple_conclusions : forall c h,
     try apply no_urules_with_empty_conclusion in u; try apply u.
     destruct X0; destruct s; inversion e.
     auto.
     try apply no_urules_with_empty_conclusion in u; try apply u.
     destruct X0; destruct s; inversion e.
     auto.

-    apply (no_urules_with_multiple_conclusions _ _ h (c1,,c2)) in u. inversion u. exists c1. exists c2. auto.

     destruct X0; destruct s; inversion e.
     destruct X0; destruct s; inversion e.
     destruct X0; destruct s; inversion e.
     destruct X0; destruct s; inversion e.
     destruct X0; destruct s; inversion e.
     destruct X0; destruct s; inversion e.

diff --git a/src/HaskProofCategory.v b/src/HaskProofCategory.v
index e74d580..18da307 100644 (file)
--- a/src/HaskProofCategory.v
+++ b/src/HaskProofCategory.v
@@ -44,15 +44,13 @@ Open Scope nd_scope.
 
 Section HaskProofCategory.
 
 
 Section HaskProofCategory.
 

-  Implicit Arguments RURule [[Γ][Δ][h][c]].
-

   Context (ndr_systemfc:@ND_Relation _ Rule).
 
   (* 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 {Γ}{Δ} : ∀ h c, Rule (mapOptionTree (@UJudg2judg Γ Δ) h) (mapOptionTree (@UJudg2judg Γ Δ) c) -> Type :=
   Context (ndr_systemfc:@ND_Relation _ Rule).
 
   (* 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 {Γ}{Δ} : ∀ h c, Rule (mapOptionTree (@UJudg2judg Γ Δ) h) (mapOptionTree (@UJudg2judg Γ Δ) c) -> Type :=

-  | PCF_RCanL            : ∀ t a              ,  Rule_PCF  [_>>_>_|-_] [_>>_>_|-_] (RURule (RCanL t a              ))
+  | PCF_RArrange         : ∀ x y              ,  Rule_PCF  [_>>_>_|-_] [_>>_>_|-_] (RURule (RCanL t a              ))

   | PCF_RCanR            : ∀ t a              ,  Rule_PCF  [_>>_>_|-_] [_>>_>_|-_] (RURule (RCanR t a              ))
   | PCF_RuCanL           : ∀ t a              ,  Rule_PCF  [_>>_>_|-_] [_>>_>_|-_] (RURule (RuCanL t a             ))
   | PCF_RuCanR           : ∀ t a              ,  Rule_PCF  [_>>_>_|-_] [_>>_>_|-_] (RURule (RuCanR t a             ))
   | PCF_RCanR            : ∀ t a              ,  Rule_PCF  [_>>_>_|-_] [_>>_>_|-_] (RURule (RCanR t a              ))
   | PCF_RuCanL           : ∀ t a              ,  Rule_PCF  [_>>_>_|-_] [_>>_>_|-_] (RURule (RuCanL t a             ))
   | PCF_RuCanR           : ∀ t a              ,  Rule_PCF  [_>>_>_|-_] [_>>_>_|-_] (RURule (RuCanR t a             ))

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index 39dd8ba..fb8c2fa 100644 (file)
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -157,24 +157,25 @@ Definition judgmentToRawLatexMath (j:Judg) : LatexMath :=
 Instance ToLatexMathJudgment : ToLatexMath Judg :=
   { toLatexMath := judgmentToRawLatexMath }.
 
 Instance ToLatexMathJudgment : ToLatexMath Judg :=
   { toLatexMath := judgmentToRawLatexMath }.
 

-Fixpoint nd_uruleToRawLatexMath {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : string :=
+Fixpoint nd_uruleToRawLatexMath {T}{h}{c}(r:@Arrange T h c) : string :=

   match r with
     | RLeft   _ _ _ r => nd_uruleToRawLatexMath r
     | RRight  _ _ _ r => nd_uruleToRawLatexMath r
   match r with
     | RLeft   _ _ _ r => nd_uruleToRawLatexMath r
     | RRight  _ _ _ r => nd_uruleToRawLatexMath r

-    | RCanL   _ _     => "CanL"
-    | RCanR   _ _     => "CanR"
-    | RuCanL  _ _     => "uCanL"
-    | RuCanR  _ _     => "uCanR"
-    | RAssoc  _ _ _ _ => "Assoc"
-    | RCossa  _ _ _ _ => "Cossa"
-    | RExch   _ _ _   => "Exch"
-    | RWeak   _ _     => "Weak"
-    | RCont   _ _     => "Cont"
+    | RCanL   _     => "CanL"
+    | RCanR   _     => "CanR"
+    | RuCanL  _     => "uCanL"
+    | RuCanR  _     => "uCanR"
+    | RAssoc  _ _ _ => "Assoc"
+    | RCossa  _ _ _ => "Cossa"
+    | RExch   _ _   => "Exch"
+    | RWeak   _     => "Weak"
+    | RCont   _     => "Cont"
+    | RComp   _ _ _ _ _  => "Comp"  (* FIXME: do a better job here *)

   end.
 
 Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string :=
   match r with
   end.
 
 Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string :=
   match r with

-    | RURule        _ _ _ _ r         => nd_uruleToRawLatexMath r
+    | RArrange      _ _ _ _ _ r       => nd_uruleToRawLatexMath r

     | RNote         _ _ _ _ _ _       => "Note"
     | RLit          _ _ _ _           => "Lit"
     | RVar          _ _ _ _           => "Var"
     | RNote         _ _ _ _ _ _       => "Note"
     | RLit          _ _ _ _           => "Lit"
     | RVar          _ _ _ _           => "Var"

@@ -195,25 +196,26 @@ Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string :=
     | REmptyGroup   _ _               => "REmptyGroup"
 end.
 
     | REmptyGroup   _ _               => "REmptyGroup"
 end.
 

-Fixpoint nd_hideURule {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : bool :=
+Fixpoint nd_hideURule {T}{h}{c}(r:@Arrange T h c) : bool :=

   match r with
   match r with

-    | RLeft   _ _ _ r               => nd_hideURule r
-    | RRight  _ _ _ r               => nd_hideURule r
-    | RCanL   _ _                   => true
-    | RCanR   _ _                   => true
-    | RuCanL  _ _                   => true
-    | RuCanR  _ _                   => true
-    | RAssoc  _ _ _ _               => true
-    | RCossa  _ _ _ _               => true
-    | RExch   _    (T_Leaf None) b  => true
-    | RExch   _ a  (T_Leaf None)    => true
-    | RWeak   _    (T_Leaf None)    => true
-    | RCont   _    (T_Leaf None)    => true
-    | _                             => false
+    | RLeft   _ _ _ r             => nd_hideURule r
+    | RRight  _ _ _ r             => nd_hideURule r
+    | RCanL   _                   => true
+    | RCanR   _                   => true
+    | RuCanL  _                   => true
+    | RuCanR  _                   => true
+    | RAssoc  _ _ _               => true
+    | RCossa  _ _ _               => true
+    | RExch      (T_Leaf None) b  => true
+    | RExch   a  (T_Leaf None)    => true
+    | RWeak      (T_Leaf None)    => true
+    | RCont      (T_Leaf None)    => true
+    | RComp   _ _ _ _ _           => false   (* FIXME: do better *)
+    | _                           => false

   end.
 Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool :=
   match r with
   end.
 Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool :=
   match r with

-    | RURule        _ _ _ _ r   => nd_hideURule r
+    | RArrange      _ _ _ _ _ r => nd_hideURule r

     | REmptyGroup   _ _         => true
     | RBindingGroup _ _ _ _ _ _ => true
     | _                         => false
     | REmptyGroup   _ _         => true
     | RBindingGroup _ _ _ _ _ _ => true
     | _                         => false

diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v
index 3dee0fe..0218ddd 100644 (file)
--- a/src/HaskProofToStrong.v
+++ b/src/HaskProofToStrong.v
@@ -228,172 +228,125 @@ Section HaskProofToStrong.
       inversion pf2.
     Defined.
 
       inversion pf2.
     Defined.
 

-  Definition urule2expr  : forall Γ Δ h j (r:@URule Γ Δ h j) (ξ:VV -> LeveledHaskType Γ ★),
-    ITree _ (ujudg2exprType ξ) h -> ITree _ (ujudg2exprType ξ) j.
-
-      refine (fix urule2expr Γ Δ h j (r:@URule Γ Δ h j) ξ {struct r} : 
-        ITree _ (ujudg2exprType ξ) h -> ITree _ (ujudg2exprType ξ) j :=
-        match r as R in URule H C return ITree _ (ujudg2exprType ξ) H -> ITree _ (ujudg2exprType ξ) C with
-          | RLeft   h c ctx r => let case_RLeft  := tt in (fun e => _) (urule2expr _ _ _ _ r)
-          | RRight  h c ctx r => let case_RRight := tt in (fun e => _) (urule2expr _ _ _ _ r)
-          | RCanL   t a       => let case_RCanL  := tt in _
-          | RCanR   t a       => let case_RCanR  := tt in _
-          | RuCanL  t a       => let case_RuCanL := tt in _
-          | RuCanR  t a       => let case_RuCanR := tt in _
-          | RAssoc  t a b c   => let case_RAssoc := tt in _
-          | RCossa  t a b c   => let case_RCossa := tt in _
-          | RExch   t a b     => let case_RExch  := tt in _
-          | RWeak   t a       => let case_RWeak  := tt in _
-          | RCont   t a       => let case_RCont  := tt in _
+  Definition urule2expr  : forall Γ Δ h j t (r:@Arrange _ h j) (ξ:VV -> LeveledHaskType Γ ★),
+    ujudg2exprType ξ (Γ >> Δ > h |- t) ->
+    ujudg2exprType ξ (Γ >> Δ > j |- t)
+    .
+    intros Γ Δ.
+      refine (fix urule2expr h j t (r:@Arrange _ h j) ξ {struct r} : 
+        ujudg2exprType ξ (Γ >> Δ > h |- t) ->
+        ujudg2exprType ξ (Γ >> Δ > j |- t) :=
+        match r as R in Arrange H C return ujudg2exprType ξ (Γ >> Δ > H |- t) ->
+        ujudg2exprType ξ (Γ >> Δ > C |- t) with
+          | RLeft   h c ctx r => let case_RLeft  := tt in (fun e => _) (urule2expr _ _ _ r)
+          | RRight  h c ctx r => let case_RRight := tt in (fun e => _) (urule2expr _ _ _ r)
+          | RCanL   a       => let case_RCanL  := tt in _
+          | RCanR   a       => let case_RCanR  := tt in _
+          | RuCanL  a       => let case_RuCanL := tt in _
+          | RuCanR  a       => let case_RuCanR := tt in _
+          | RAssoc  a b c   => let case_RAssoc := tt in _
+          | RCossa  a b c   => let case_RCossa := tt in _
+          | RExch   a b     => let case_RExch  := tt in _
+          | RWeak   a       => let case_RWeak  := tt in _
+          | RCont   a       => let case_RCont  := tt in _
+          | RComp   a b c f g => let case_RComp  := tt in (fun e1 e2 => _) (urule2expr _ _ _ f) (urule2expr _ _ _ g)

           end); clear urule2expr; intros.
 
       destruct case_RCanL.
           end); clear urule2expr; intros.
 
       destruct case_RCanL.

-        apply ILeaf; simpl; intros.
-        inversion X.
-        simpl in X0.
-        apply (X0 ([],,vars)).
+        simpl; intros.
+        simpl in X.
+        apply (X ([],,vars)).

         simpl; rewrite <- H; auto.
 
       destruct case_RCanR.
         simpl; rewrite <- H; auto.
 
       destruct case_RCanR.

-        apply ILeaf; simpl; intros.
-        inversion X.
-        simpl in X0.
-        apply (X0 (vars,,[])).
+        simpl; intros.
+        simpl in X.
+        apply (X (vars,,[])).

         simpl; rewrite <- H; auto.
 
       destruct case_RuCanL.
         simpl; rewrite <- H; auto.
 
       destruct case_RuCanL.

-        apply ILeaf; simpl; intros.
+        simpl; intros.

         destruct vars; try destruct o; inversion H.
         destruct vars; try destruct o; inversion H.

-        inversion X.
-        simpl in X0.
-        apply (X0 vars2); auto.
+        simpl in X.
+        apply (X vars2); auto.

 
       destruct case_RuCanR.
 
       destruct case_RuCanR.

-        apply ILeaf; simpl; intros.
+        simpl; intros.

         destruct vars; try destruct o; inversion H.
         destruct vars; try destruct o; inversion H.

-        inversion X.
-        simpl in X0.
-        apply (X0 vars1); auto.
+        simpl in X.
+        apply (X vars1); auto.

 
       destruct case_RAssoc.
 
       destruct case_RAssoc.

-        apply ILeaf; simpl; intros.
-        inversion X.
-        simpl in X0.
+        simpl; intros.
+        simpl in X.

         destruct vars; try destruct o; inversion H.
         destruct vars1; try destruct o; inversion H.
         destruct vars; try destruct o; inversion H.
         destruct vars1; try destruct o; inversion H.

-        apply (X0 (vars1_1,,(vars1_2,,vars2))).
+        apply (X (vars1_1,,(vars1_2,,vars2))).

         subst; auto.
 
       destruct case_RCossa.
         subst; auto.
 
       destruct case_RCossa.

-        apply ILeaf; simpl; intros.
-        inversion X.
-        simpl in X0.
+        simpl; intros.
+        simpl in X.

         destruct vars; try destruct o; inversion H.
         destruct vars2; try destruct o; inversion H.
         destruct vars; try destruct o; inversion H.
         destruct vars2; try destruct o; inversion H.

-        apply (X0 ((vars1,,vars2_1),,vars2_2)).
+        apply (X ((vars1,,vars2_1),,vars2_2)).

         subst; auto.
 
         subst; auto.
 

+      destruct case_RExch.
+        simpl; intros.
+        simpl in X.
+        destruct vars; try destruct o; inversion H.
+        apply (X (vars2,,vars1)).
+        inversion H; subst; auto.
+        
+      destruct case_RWeak.
+        simpl; intros.
+        simpl in X.
+        apply (X []).
+        auto.
+        
+      destruct case_RCont.
+        simpl; intros.
+        simpl in X.
+        apply (X (vars,,vars)).
+        simpl.
+        rewrite <- H.
+        auto.
+

       destruct case_RLeft.
       destruct case_RLeft.

-        destruct c; [ idtac | apply no_urules_with_multiple_conclusions in r0; inversion r0; exists c1; exists c2; auto ].
-        destruct o; [ idtac | apply INone ].
-        destruct u; simpl in *.
-        apply ILeaf; simpl; intros.
+        intro vars; intro H.

         destruct vars; try destruct o; inversion H.
         destruct vars; try destruct o; inversion H.

-        set (fun q => ileaf (e ξ q)) as r'.
-        simpl in r'.
-        apply r' with (vars:=vars2).
-        clear r' e.
-        clear r0.
-        induction h0.
-          destruct a.
-          destruct u.
+        apply (fun q => e ξ q vars2 H2).
+        clear r0 e H2.

           simpl in X.
           simpl in X.

-          apply ileaf in X. 
-          apply ILeaf.

           simpl.
           simpl.

-          simpl in X.

           intros.
           apply X with (vars:=vars1,,vars).
           intros.
           apply X with (vars:=vars1,,vars).

-          simpl.

           rewrite H0.
           rewrite H1.
           rewrite H0.
           rewrite H1.

+          simpl.

           reflexivity.
           reflexivity.

-          apply INone.
-          apply IBranch.
-          apply IHh0_1. inversion X; auto.
-          apply IHh0_2. inversion X; auto.
-          auto.
-        
+

       destruct case_RRight.
       destruct case_RRight.

-        destruct c; [ idtac | apply no_urules_with_multiple_conclusions in r0; inversion r0; exists c1; exists c2; auto ].
-        destruct o; [ idtac | apply INone ].
-        destruct u; simpl in *.
-        apply ILeaf; simpl; intros.
+        intro vars; intro H.

         destruct vars; try destruct o; inversion H.
         destruct vars; try destruct o; inversion H.

-        set (fun q => ileaf (e ξ q)) as r'.
-        simpl in r'.
-        apply r' with (vars:=vars1).
-        clear r' e.
-        clear r0.
-        induction h0.
-          destruct a.
-          destruct u.
+        apply (fun q => e ξ q vars1 H1).
+        clear r0 e H2.

           simpl in X.
           simpl in X.

-          apply ileaf in X. 
-          apply ILeaf.

           simpl.
           simpl.

-          simpl in X.

           intros.
           apply X with (vars:=vars,,vars2).
           intros.
           apply X with (vars:=vars,,vars2).

-          simpl.

           rewrite H0.
           rewrite H0.

-          rewrite H2.
+          inversion H.
+          simpl.

           reflexivity.
           reflexivity.

-          apply INone.
-          apply IBranch.
-          apply IHh0_1. inversion X; auto.
-          apply IHh0_2. inversion X; auto.
-          auto.

 
 

-      destruct case_RExch.
-        apply ILeaf; simpl; intros.
-        inversion X.
-        simpl in X0.
-        destruct vars; try destruct o; inversion H.
-        apply (X0 (vars2,,vars1)).
-        inversion H; subst; auto.
-        
-      destruct case_RWeak.
-        apply ILeaf; simpl; intros.
-        inversion X.
-        simpl in X0.
-        apply (X0 []).
-        auto.
-        
-      destruct case_RCont.
-        apply ILeaf; simpl; intros.
-        inversion X.
-        simpl in X0.
-        apply (X0 (vars,,vars)).
-        simpl.
-        rewrite <- H.
-        auto.
+      destruct case_RComp.
+        apply e2.
+        apply e1.
+        apply X.

         Defined.
 
         Defined.
 

-  Definition bridge Γ Δ (c:Tree ??(UJudg Γ Δ)) ξ :
-    ITree Judg judg2exprType (mapOptionTree UJudg2judg c) -> ITree (UJudg Γ Δ) (ujudg2exprType ξ) c.
-    intro it.
-    induction c.
-    destruct a.
-      destruct u; simpl in *.
-      apply ileaf in it.
-      apply ILeaf.
-      simpl in *.
-      intros; apply it with (vars:=vars); auto.
-    apply INone.
-    apply IBranch; [ apply IHc1 | apply IHc2 ]; inversion it; auto.
-    Defined.
-

   Definition letrec_helper Γ Δ l (varstypes:Tree ??(VV * HaskType Γ ★)) ξ' :
     ITree (LeveledHaskType Γ ★)
          (fun t : LeveledHaskType Γ ★ => Expr Γ Δ ξ' t)
   Definition letrec_helper Γ Δ l (varstypes:Tree ??(VV * HaskType Γ ★)) ξ' :
     ITree (LeveledHaskType Γ ★)
          (fun t : LeveledHaskType Γ ★ => Expr Γ Δ ξ' t)

@@ -553,7 +506,7 @@ Section HaskProofToStrong.
     intros h j r.
 
       refine (match r as R in Rule H C return ITree _ judg2exprType H -> ITree _ judg2exprType C with
     intros h j r.
 
       refine (match r as R in Rule H C return ITree _ judg2exprType H -> ITree _ judg2exprType C with

-      | RURule a b c d e              => let case_RURule := tt        in _
+      | RArrange a b c d e  r         => let case_RURule := tt        in _

       | RNote   Γ Δ Σ τ l n           => let case_RNote := tt         in _
       | RLit    Γ Δ l     _           => let case_RLit := tt          in _
       | RVar    Γ Δ σ         p       => let case_RVar := tt          in _
       | RNote   Γ Δ Σ τ l n           => let case_RNote := tt         in _
       | RLit    Γ Δ l     _           => let case_RLit := tt          in _
       | RVar    Γ Δ σ         p       => let case_RVar := tt          in _

@@ -574,19 +527,17 @@ Section HaskProofToStrong.
       | RLetRec Γ Δ lri x y t         => let case_RLetRec := tt       in _
       end); intro X_; try apply ileaf in X_; simpl in X_.
 
       | RLetRec Γ Δ lri x y t         => let case_RLetRec := tt       in _
       end); intro X_; try apply ileaf in X_; simpl in X_.
 

-  destruct case_RURule.
-    destruct d; try destruct o.
-      apply ILeaf; destruct u; simpl; intros.
-      set (@urule2expr a b _ _ e ξ) as q.
-      set (fun z => ileaf (q z)) as q'.
+    destruct case_RURule.
+      apply ILeaf. simpl. intros.
+      set (@urule2expr a b _ _ e r0 ξ) as q.
+      set (fun z => q z) as q'.

       simpl in q'.
       apply q' with (vars:=vars).
       clear q' q.
       simpl in q'.
       apply q' with (vars:=vars).
       clear q' q.

-      apply bridge.
-      apply X_.
+      intros.
+      apply X_ with (vars:=vars0).
+      auto.

       auto.
       auto.

-      apply no_urules_with_empty_conclusion in e; inversion e; auto.
-      apply no_urules_with_multiple_conclusions in e; inversion e; auto; exists d1; exists d2; auto.

 
   destruct case_RBrak.
     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 
   destruct case_RBrak.
     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.

diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v
index 79e16cd..b0c5b11 100644 (file)
--- a/src/HaskStrongToProof.v
+++ b/src/HaskStrongToProof.v
@@ -16,51 +16,24 @@ Require Import HaskProof.
 
 Section HaskStrongToProof.
 
 
 Section HaskStrongToProof.
 

-(* Whereas RLeft/RRight perform left and right context expansion on a single uniform rule, these functions perform
- * expansion on an entire uniform proof *)
-Definition ext_left  {Γ}{Δ}(ctx:Tree ??(LeveledHaskType Γ ★))
-  := @nd_map' _ _ _ _ (ext_tree_left ctx)  (fun h c r => nd_rule (@RLeft Γ Δ h c ctx r)).
-Definition ext_right {Γ}{Δ}(ctx:Tree ??(LeveledHaskType Γ ★))
-  := @nd_map' _ _ _ _ (ext_tree_right ctx) (fun h c r => nd_rule (@RRight Γ Δ h c ctx r)).
-
-Definition pivotContext {Γ}{Δ} a b c τ :
-  @ND _ (@URule Γ Δ)
-    [ Γ >> Δ > (a,,b),,c |- τ]
-    [ Γ >> Δ > (a,,c),,b |- τ].
-  set (ext_left a _ _ (nd_rule (@RExch Γ Δ τ c b))) as q.
-  simpl in *.
-  eapply nd_comp ; [ eapply nd_rule; apply RCossa | idtac ]. 
-  eapply nd_comp ; [ idtac | eapply nd_rule; apply RAssoc ].
-  apply q.
+Definition pivotContext {T} a b c : @Arrange T ((a,,b),,c) ((a,,c),,b) :=
+  RComp (RComp (RCossa _ _ _) (RLeft a (RExch c b))) (RAssoc _ _ _).
+
+Definition copyAndPivotContext {T} a b c : @Arrange T ((a,,b),,(c,,b)) ((a,,c),,b).
+  eapply RComp; [ idtac | apply (RLeft (a,,c) (RCont b)) ].
+  eapply RComp; [ idtac | apply RCossa ]. 
+  eapply RComp; [ idtac | apply (RRight b (pivotContext a b c)) ].
+  apply RAssoc.

   Defined.
   Defined.

-
-Definition copyAndPivotContext {Γ}{Δ} a b c τ :
-  @ND _ (@URule Γ Δ)
-    [ Γ >> Δ > (a,,b),,(c,,b) |- τ]
-    [ Γ >> Δ > (a,,c),,b |- τ].
-    set (ext_left (a,,c) _ _ (nd_rule (@RCont Γ Δ τ b))) as q.
-    simpl in *.
-    eapply nd_comp; [ idtac | apply q ].
-    clear q.
-    eapply nd_comp ; [ idtac | eapply nd_rule; apply RCossa ].
-    set (ext_right b _ _ (@pivotContext _ Δ a b c τ)) as q.
-    simpl in *.
-    eapply nd_comp ; [ idtac | apply q ]. 
-    clear q.
-    apply nd_rule.
-    apply RAssoc.
-    Defined.
-
-

   
 Context {VV:Type}{eqd_vv:EqDecidable VV}.
 
   
 Context {VV:Type}{eqd_vv:EqDecidable VV}.
 

-  (* maintenance of Xi *)
-  Fixpoint dropVar (lv:list VV)(v:VV) : ??VV :=
-    match lv with
-      | nil     => Some v
-      | v'::lv' => if eqd_dec v v' then None else dropVar lv' v
-    end.
+(* maintenance of Xi *)
+Fixpoint dropVar (lv:list VV)(v:VV) : ??VV :=
+  match lv with
+    | nil     => Some v
+    | v'::lv' => if eqd_dec v v' then None else dropVar lv' v
+  end.

 
 Fixpoint mapOptionTree' {a b:Type}(f:a->??b)(t:@Tree ??a) : @Tree ??b :=
   match t with 
 
 Fixpoint mapOptionTree' {a b:Type}(f:a->??b)(t:@Tree ??a) : @Tree ??b :=
   match t with 

@@ -422,23 +395,22 @@ Lemma stripping_nothing_is_inert
     reflexivity.
     Qed.
 
     reflexivity.
     Qed.
 

-Definition arrangeContext 
+Definition arrangeContext

      (Γ:TypeEnv)(Δ:CoercionEnv Γ)
      v      (* variable to be pivoted, if found *)
      ctx    (* initial context *)
      (Γ:TypeEnv)(Δ:CoercionEnv Γ)
      v      (* variable to be pivoted, if found *)
      ctx    (* initial context *)

-     τ      (* type of succedent *)

      (ξ:VV -> LeveledHaskType Γ ★)
      :
  
     (* a proof concluding in a context where that variable does not appear *)
      (ξ:VV -> LeveledHaskType Γ ★)
      :
  
     (* a proof concluding in a context where that variable does not appear *)

-    sum (ND (@URule Γ Δ)
-          [Γ >> Δ > mapOptionTree ξ                        ctx                        |- τ]
-          [Γ >> Δ > mapOptionTree ξ (stripOutVars (v::nil) ctx),,[]                   |- τ])
+     sum (Arrange
+          (mapOptionTree ξ                        ctx                        )
+          (mapOptionTree ξ (stripOutVars (v::nil) ctx),,[]                   ))

    
     (* or a proof concluding in a context where that variable appears exactly once in the left branch *)
    
     (* or a proof concluding in a context where that variable appears exactly once in the left branch *)

-        (ND (@URule Γ Δ)
-          [Γ >> Δ > mapOptionTree ξ                         ctx                       |- τ]
-          [Γ >> Δ > mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v])                |- τ]).
+        (Arrange
+          (mapOptionTree ξ                         ctx                       )
+          (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v])                )).

 
   induction ctx.
   
 
   induction ctx.
   

@@ -455,18 +427,15 @@ Definition arrangeContext
             (* where the leaf is v *)
             apply inr.
               subst.
             (* where the leaf is v *)
             apply inr.
               subst.

-              apply nd_rule.

               apply RuCanL.
 
             (* where the leaf is NOT v *)
             apply inl.
               apply RuCanL.
 
             (* where the leaf is NOT v *)
             apply inl.

-              apply nd_rule.

               apply RuCanR.
   
         (* empty leaf *)
         destruct case_None.
           apply inl; simpl in *.
               apply RuCanR.
   
         (* empty leaf *)
         destruct case_None.
           apply inl; simpl in *.

-          apply nd_rule.

           apply RuCanR.
   
       (* branch *)
           apply RuCanR.
   
       (* branch *)

@@ -486,87 +455,77 @@ Definition arrangeContext
 
     destruct case_Neither.
       apply inl.
 
     destruct case_Neither.
       apply inl.

-      eapply nd_comp; [idtac | eapply nd_rule; apply RuCanR ].
-        exact (nd_comp
+      eapply RComp; [idtac | apply RuCanR ].
+        exact (RComp

           (* order will not matter because these are central as morphisms *)
           (* order will not matter because these are central as morphisms *)

-          (ext_right _ _ _ (nd_comp lpf (nd_rule (@RCanR _ _ _ _))))
-          (ext_left  _ _ _ (nd_comp rpf (nd_rule (@RCanR _ _ _ _))))).
+          (RRight _ (RComp lpf (RCanR _)))
+          (RLeft  _ (RComp rpf (RCanR _)))).

 
 
     destruct case_Right.
       apply inr.
       fold (stripOutVars (v::nil)).
 
 
     destruct case_Right.
       apply inr.
       fold (stripOutVars (v::nil)).

-      set (ext_right (mapOptionTree ξ ctx2) _ _ (nd_comp lpf (nd_rule (@RCanR _ _ _ _)))) as q.
+      set (RRight (mapOptionTree ξ ctx2)  (RComp lpf ((RCanR _)))) as q.

       simpl in *.
       simpl in *.

-      eapply nd_comp.
+      eapply RComp.

       apply q.
       clear q.
       clear lpf.
       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
       apply q.
       clear q.
       clear lpf.
       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.

-      eapply nd_comp; [ idtac | eapply nd_rule; apply RAssoc ].
-      set (ext_left (mapOptionTree ξ (stripOutVars (v :: nil) ctx1)) [Γ >> Δ>mapOptionTree ξ ctx2 |- τ]
-                                                            [Γ >> Δ> (mapOptionTree ξ (stripOutVars (v :: nil) ctx2),,[ξ v])  |- τ]) as qq.
-      apply qq.
-      clear qq.
+      eapply RComp; [ idtac | apply RAssoc ].
+      apply RLeft.

       apply rpf.
 
     destruct case_Left.
       apply inr.
       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
       fold (stripOutVars (v::nil)).
       apply rpf.
 
     destruct case_Left.
       apply inr.
       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
       fold (stripOutVars (v::nil)).

-      eapply nd_comp; [ idtac | eapply pivotContext ].
-      set (nd_comp rpf (nd_rule (@RCanR _ _ _ _ ) ) ) as rpf'.
-      set (ext_left ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) _ _ rpf') as qq.
+      eapply RComp; [ idtac | eapply pivotContext ].
+      set (RComp rpf (RCanR _ )) as rpf'.
+      set (RLeft ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) rpf') as qq.

       simpl in *.
       simpl in *.

-      eapply nd_comp; [ idtac | apply qq ].
+      eapply RComp; [ idtac | apply qq ].

       clear qq rpf' rpf.
       clear qq rpf' rpf.

-      set (ext_right (mapOptionTree ξ ctx2) [Γ >>Δ> mapOptionTree ξ ctx1 |- τ] [Γ >>Δ> (mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v]) |- τ]) as q.
-      apply q.
-      clear q.
+      apply (RRight (mapOptionTree ξ ctx2)).

       apply lpf.
 
     destruct case_Both.
       apply inr.
       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
       fold (stripOutVars (v::nil)).
       apply lpf.
 
     destruct case_Both.
       apply inr.
       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
       fold (stripOutVars (v::nil)).

-      eapply nd_comp; [ idtac | eapply copyAndPivotContext ].
-        exact (nd_comp
-          (* order will not matter because these are central as morphisms *)
-          (ext_right _ _ _ lpf)
-          (ext_left  _ _ _ rpf)).
+      eapply RComp; [ idtac | eapply copyAndPivotContext ].
+        (* order will not matter because these are central as morphisms *)
+        exact (RComp (RRight _ lpf) (RLeft _ rpf)).

 
     Defined.
 
 (* same as before, but use RWeak if necessary *)
 
     Defined.
 
 (* same as before, but use RWeak if necessary *)

-Definition arrangeContextAndWeaken v ctx Γ Δ τ ξ : 
-       ND (@URule Γ Δ)
-          [Γ >> Δ>mapOptionTree ξ                        ctx                |- τ]
-          [Γ >> Δ>mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v])        |- τ].
-  set (arrangeContext Γ Δ v ctx τ ξ) as q.
+Definition arrangeContextAndWeaken  
+     (Γ:TypeEnv)(Δ:CoercionEnv Γ)
+     v      (* variable to be pivoted, if found *)
+     ctx    (* initial context *)
+     (ξ:VV -> LeveledHaskType Γ ★) :
+       Arrange
+          (mapOptionTree ξ                        ctx                )
+          (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v])        ).
+  set (arrangeContext Γ Δ v ctx ξ) as q.

   destruct q; auto.
   destruct q; auto.

-  eapply nd_comp; [ apply n | idtac ].
-  clear n.
-  refine (ext_left _ _ _ (nd_rule (RWeak _ _))).
+  eapply RComp; [ apply a | idtac ].
+  refine (RLeft _ (RWeak _)).

   Defined.
 
   Defined.
 

-Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree t lev :
-      mapOptionTree (update_ξ ξ lev ((v,t)::nil)) (stripOutVars (v :: nil) tree)
-    = mapOptionTree ξ (stripOutVars (v :: nil) tree).
-  set (@updating_stripped_tree_is_inert' Γ lev ξ ((v,t)::nil)) as p.
-  rewrite p.
-  simpl.
-  reflexivity.
-  Qed.
-

 Lemma cheat : forall {T}(a b:list T), distinct (app a b) -> distinct (app b a).
   admit.
   Qed.
 
 Lemma cheat : forall {T}(a b:list T), distinct (app a b) -> distinct (app b a).
   admit.
   Qed.
 

-Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z, 
+Definition arrangeContextAndWeaken''
+     (Γ:TypeEnv)(Δ:CoercionEnv Γ)
+     v      (* variable to be pivoted, if found *)
+     (ξ:VV -> LeveledHaskType Γ ★) : forall ctx,

   distinct (leaves v) ->
   distinct (leaves v) ->

-  ND (@URule Γ Δ)
-    [Γ >> Δ>(mapOptionTree ξ ctx)                                       |-  z]
-    [Γ >> Δ>(mapOptionTree ξ (stripOutVars (leaves v) ctx)),,(mapOptionTree ξ v) |-  z].
+  Arrange
+    ((mapOptionTree ξ ctx)                                       )
+    ((mapOptionTree ξ (stripOutVars (leaves v) ctx)),,(mapOptionTree ξ v)).

 
   induction v; intros.
     destruct a.
 
   induction v; intros.
     destruct a.

@@ -575,11 +534,11 @@ Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z,
     fold (mapOptionTree ξ) in *.
     intros.
     apply arrangeContextAndWeaken.
     fold (mapOptionTree ξ) in *.
     intros.
     apply arrangeContextAndWeaken.

+    apply Δ.

 
   unfold mapOptionTree; simpl in *.
     intros.
     rewrite (@stripping_nothing_is_inert Γ); auto.
 
   unfold mapOptionTree; simpl in *.
     intros.
     rewrite (@stripping_nothing_is_inert Γ); auto.

-    apply nd_rule.

     apply RuCanR.
     intros.
     unfold mapOptionTree in *.
     apply RuCanR.
     intros.
     unfold mapOptionTree in *.

@@ -587,7 +546,7 @@ Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z,
     fold (mapOptionTree ξ) in *.
     set (mapOptionTree ξ) as X in *.
 
     fold (mapOptionTree ξ) in *.
     set (mapOptionTree ξ) as X in *.
 

-    set (IHv2 ((stripOutVars (leaves v1) ctx),, v1) z) as IHv2'.
+    set (IHv2 ((stripOutVars (leaves v1) ctx),, v1)) as IHv2'.

     unfold stripOutVars in IHv2'.
     simpl in IHv2'.
     fold (stripOutVars (leaves v2)) in IHv2'.
     unfold stripOutVars in IHv2'.
     simpl in IHv2'.
     fold (stripOutVars (leaves v2)) in IHv2'.

@@ -599,19 +558,27 @@ Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z,
     fold X in IHv2'.
     set (distinct_app _ _ _ H) as H'.
     destruct H' as [H1 H2].
     fold X in IHv2'.
     set (distinct_app _ _ _ H) as H'.
     destruct H' as [H1 H2].

-    set (nd_comp (IHv1 _ _ H1) (IHv2' H2)) as qq.
-    eapply nd_comp.
+    set (RComp (IHv1 _ H1) (IHv2' H2)) as qq.
+    eapply RComp.

       apply qq.
       clear qq IHv2' IHv2 IHv1.
       rewrite strip_twice_lemma.
 
       rewrite (strip_distinct' v1 (leaves v2)).
       apply qq.
       clear qq IHv2' IHv2 IHv1.
       rewrite strip_twice_lemma.
 
       rewrite (strip_distinct' v1 (leaves v2)).

-        apply nd_rule.

         apply RCossa.
         apply cheat.
         auto.
     Defined.
 
         apply RCossa.
         apply cheat.
         auto.
     Defined.
 

+Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree t lev :
+      mapOptionTree (update_ξ ξ lev ((v,t)::nil)) (stripOutVars (v :: nil) tree)
+    = mapOptionTree ξ (stripOutVars (v :: nil) tree).
+  set (@updating_stripped_tree_is_inert' Γ lev ξ ((v,t)::nil)) as p.
+  rewrite p.
+  simpl.
+  reflexivity.
+  Qed.
+

 (* IDEA: use multi-conclusion proofs instead *)
 Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type := 
   | lrsp_nil  : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _)
 (* IDEA: use multi-conclusion proofs instead *)
 Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type := 
   | lrsp_nil  : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _)

@@ -665,23 +632,25 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree  :
   eapply nd_comp; [ idtac | eapply nd_rule; apply z ].
   clear z.
 
   eapply nd_comp; [ idtac | eapply nd_rule; apply z ].
   clear z.
 

-  set (@arrangeContextAndWeaken''  Γ Δ ξ' pctx (expr2antecedent body,,eLetRecContext branches)) as q'.
+  set (@arrangeContextAndWeaken''  Γ Δ  pctx ξ' (expr2antecedent body,,eLetRecContext branches)) as q'.

   unfold passback in *; clear passback.
   unfold pctx in *; clear pctx.
   unfold passback in *; clear passback.
   unfold pctx in *; clear pctx.

-  eapply UND_to_ND in q'.
+  rewrite <- mapleaves in disti.
+  set (q' disti) as q''.

 
   unfold ξ' in *.
   set (@updating_stripped_tree_is_inert' Γ lev ξ (leaves tree)) as zz.
   rewrite <- mapleaves in zz.
 
   unfold ξ' in *.
   set (@updating_stripped_tree_is_inert' Γ lev ξ (leaves tree)) as zz.
   rewrite <- mapleaves in zz.

-  rewrite zz in q'.
+  rewrite zz in q''.

   clear zz.
   clear ξ'.
   Opaque stripOutVars.
   simpl.
   clear zz.
   clear ξ'.
   Opaque stripOutVars.
   simpl.

-  rewrite <- mapOptionTree_compose in q'.
+  rewrite <- mapOptionTree_compose in q''.

   rewrite <- ξlemma.
   rewrite <- ξlemma.

-  eapply nd_comp; [ idtac | apply q' ].
+  eapply nd_comp; [ idtac | eapply nd_rule; apply (RArrange _ _ _ _ _ q'') ].

   clear q'.
   clear q'.

+  clear q''.

   simpl.
 
   set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.
   simpl.
 
   set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.

@@ -690,10 +659,6 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree  :
     apply nd_prod; auto.
     rewrite ξlemma.
     apply q.
     apply nd_prod; auto.
     rewrite ξlemma.
     apply q.

-    clear q'.
-
-  rewrite <- mapleaves in disti.
-    apply disti.

     Defined.
 
 Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} :
     Defined.
 
 Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} :

@@ -843,15 +808,14 @@ Definition expr2proof  :
       unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
       eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ].
       set (update_ξ ξ lev ((v,t1)::nil)) as ξ'.
       unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
       eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ].
       set (update_ξ ξ lev ((v,t1)::nil)) as ξ'.

-      set (arrangeContextAndWeaken v (expr2antecedent e) Γ Δ [t2 @@ lev] ξ') as pfx.
-        apply UND_to_ND in pfx.
-        unfold mapOptionTree in pfx; simpl in pfx; fold (mapOptionTree ξ) in pfx.
+      set (arrangeContextAndWeaken Γ Δ v (expr2antecedent e) ξ') as pfx.
+        eapply RArrange in pfx.
+        unfold mapOptionTree in pfx; simpl in pfx.

         unfold ξ' in pfx.
         unfold ξ' in pfx.

-        fold (mapOptionTree (update_ξ ξ lev ((v,t1)::nil))) in pfx.

         rewrite updating_stripped_tree_is_inert in pfx.
         unfold update_ξ in pfx.
         destruct (eqd_dec v v).
         rewrite updating_stripped_tree_is_inert in pfx.
         unfold update_ξ in pfx.
         destruct (eqd_dec v v).

-        eapply nd_comp; [ idtac | apply pfx ].
+        eapply nd_comp; [ idtac | apply (nd_rule pfx) ].

         clear pfx.
         apply e'.
         assert False.
         clear pfx.
         apply e'.
         assert False.

@@ -869,7 +833,7 @@ Definition expr2proof  :
       fold (@mapOptionTree VV).
       fold (mapOptionTree ξ).
       set (update_ξ ξ v ((lev,tv)::nil)) as ξ'.
       fold (@mapOptionTree VV).
       fold (mapOptionTree ξ).
       set (update_ξ ξ v ((lev,tv)::nil)) as ξ'.

-      set (arrangeContextAndWeaken lev (expr2antecedent ebody) Γ Δ [t@@v] ξ') as n.
+      set (arrangeContextAndWeaken Γ Δ lev (expr2antecedent ebody) ξ') as n.

       unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n.
       unfold ξ' in n.
       rewrite updating_stripped_tree_is_inert in n.
       unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n.
       unfold ξ' in n.
       rewrite updating_stripped_tree_is_inert in n.

@@ -877,8 +841,8 @@ Definition expr2proof  :
       destruct (eqd_dec lev lev).
       unfold ξ'.
       unfold update_ξ.
       destruct (eqd_dec lev lev).
       unfold ξ'.
       unfold update_ξ.

-      apply UND_to_ND in n.
-      apply n.
+      eapply RArrange in n.
+      apply (nd_rule n).

       assert False. apply n0; auto. inversion H.
 
     destruct case_EEsc.
       assert False. apply n0; auto. inversion H.
 
     destruct case_EEsc.

@@ -925,11 +889,9 @@ Definition expr2proof  :
       clear o x alts alts' e.
       eapply nd_comp; [ apply e' | idtac ].
       clear e'.
       clear o x alts alts' e.
       eapply nd_comp; [ apply e' | idtac ].
       clear e'.

-      set (fun q r x1 x2 y1 y2 => @UND_to_ND q r [q >> r > x1 |- y1] [q >> r > x2 |- y2]).
-      simpl in n.
-      apply n.
-      clear n.
-
+      apply nd_rule.
+      apply RArrange.
+      simpl.

       rewrite mapleaves'.
       simpl.
       rewrite <- mapOptionTree_compose.
       rewrite mapleaves'.
       simpl.
       rewrite <- mapOptionTree_compose.

@@ -951,6 +913,7 @@ Definition expr2proof  :
       replace (stripOutVars (vec2list (scbwv_exprvars scbx))) with
         (stripOutVars (leaves (unleaves (vec2list (scbwv_exprvars scbx))))).
       apply q.
       replace (stripOutVars (vec2list (scbwv_exprvars scbx))) with
         (stripOutVars (leaves (unleaves (vec2list (scbwv_exprvars scbx))))).
       apply q.

+      apply (sac_Δ sac Γ atypes (weakCK'' Δ)).

       rewrite leaves_unleaves.
       apply (scbwv_exprvars_distinct scbx).
       rewrite leaves_unleaves.
       rewrite leaves_unleaves.
       apply (scbwv_exprvars_distinct scbx).
       rewrite leaves_unleaves.