X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProof.v;h=f98800db63e803f955082fe9bd24a30f6193c871;hp=d92dd6bb5612a6e1a90510de4667574f07ca1e90;hb=3282a2b78028238987a5a49e59d8e8d495aea0e1;hpb=57e387249da84dac0f1c5a9411e3900831ce2d81

diff --git a/src/HaskProof.v b/src/HaskProof.v
index d92dd6b..f98800d 100644
--- a/src/HaskProof.v
+++ b/src/HaskProof.v
@@ -10,6 +10,7 @@ Generalizable All Variables.
 Require Import Preamble.
 Require Import General.
 Require Import NaturalDeduction.
+Require Import NaturalDeductionContext.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
@@ -44,23 +45,6 @@ Record ProofCaseBranch {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ ★}{ava
 }.
 Implicit Arguments ProofCaseBranch [ ].
 
-(* Figure 3, production $\vdash_E$, Uniform rules *)
-Inductive Arrange {T} : Tree ??T -> Tree ??T -> Type :=
-| RId     : forall a        ,                Arrange           a                  a
-| 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 :=
 
@@ -81,13 +65,12 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
 | RCast   : forall Γ Δ Σ (σ₁ σ₂:HaskType Γ ★) l,
                    HaskCoercion Γ Δ (σ₁∼∼∼σ₂) ->      Rule [Γ>Δ> Σ         |- [σ₁]         @l]   [Γ>Δ>    Σ     |- [σ₂         ] @l]
 
-| RJoin  : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ l,   Rule ([Γ > Δ > Σ₁ |- τ₁ @l],,[Γ > Δ > Σ₂ |- τ₂ @l])         [Γ>Δ>  Σ₁,,Σ₂  |- τ₁,,τ₂       @l ]
-
-(* order is important here; we want to be able to skolemize without introducing new RExch'es *)
+(* order is important here; we want to be able to skolemize without introducing new AExch'es *)
 | RApp           : ∀ Γ Δ Σ₁ Σ₂ tx te l,  Rule ([Γ>Δ> Σ₁ |- [tx--->te]@l],,[Γ>Δ> Σ₂ |- [tx]@l])  [Γ>Δ> Σ₁,,Σ₂ |- [te]@l]
 
-| RLet           : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₁ |- [σ₁]@l],,[Γ>Δ> [σ₁@@l],,Σ₂ |- [σ₂]@l ])     [Γ>Δ> Σ₁,,Σ₂ |- [σ₂   ]@l]
-| RWhere         : ∀ Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₁,,([σ₁@@l],,Σ₃) |- [σ₂]@l ],,[Γ>Δ> Σ₂ |- [σ₁]@l])     [Γ>Δ> Σ₁,,(Σ₂,,Σ₃) |- [σ₂ ]@l]
+| RCut           : ∀ Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l, Rule ([Γ>Δ> Σ₁ |- Σ₁₂ @l],,[Γ>Δ> Σ,,((Σ₁₂@@@l),,Σ₂) |- Σ₃@l ]) [Γ>Δ> Σ,,(Σ₁,,Σ₂) |- Σ₃@l]
+| RLeft          : ∀ Γ Δ Σ₁ Σ₂  Σ     l,  Rule  [Γ>Δ> Σ₁ |- Σ₂  @l]                                 [Γ>Δ> (Σ@@@l),,Σ₁ |- Σ,,Σ₂@l]
+| RRight         : ∀ Γ Δ Σ₁ Σ₂  Σ     l,  Rule  [Γ>Δ> Σ₁ |- Σ₂  @l]                                 [Γ>Δ> Σ₁,,(Σ@@@l) |- Σ₂,,Σ@l]
 
 | RVoid    : ∀ Γ Δ l,               Rule [] [Γ > Δ > [] |- [] @l ]
 
@@ -102,7 +85,7 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
    Rule [Γ > ((σ₁∼∼∼σ₂)::Δ)            > Σ |- [σ ]@l]
         [Γ > Δ >                         Σ |- [σ₁∼∼σ₂⇒ σ ]@l]
 
-| RLetRec        : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > Σ₁,,(τ₂@@@lev) |- (τ₂,,[τ₁]) @lev ] [Γ > Δ > Σ₁ |- [τ₁] @lev]
+| RLetRec        : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > (τ₂@@@lev),,Σ₁ |- (τ₂,,[τ₁]) @lev ] [Γ > Δ > Σ₁ |- [τ₁] @lev]
 | RCase          : forall Γ Δ lev tc Σ avars tbranches
   (alts:Tree ??{ sac : @StrongAltCon tc & @ProofCaseBranch tc Γ Δ lev tbranches avars sac }),
                    Rule
@@ -111,6 +94,34 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
                         [Γ > Δ > (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) alts),,Σ |- [ tbranches ] @ lev]
 .
 
+Definition RCut'  : ∀ Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l,
+  ND Rule ([Γ>Δ> Σ₁ |- Σ₁₂ @l],,[Γ>Δ> (Σ₁₂@@@l),,Σ₂ |- Σ₃@l ]) [Γ>Δ> Σ₁,,Σ₂ |- Σ₃@l].
+  intros.
+  eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
+  eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
+  apply nd_prod.
+  apply nd_id.
+  apply nd_rule.
+  apply RArrange.
+  apply AuCanL.
+  Defined.
+
+Definition RLet : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l,
+  ND Rule ([Γ>Δ> Σ₁ |- [σ₁]@l],,[Γ>Δ> [σ₁@@l],,Σ₂ |- [σ₂]@l ])     [Γ>Δ> Σ₁,,Σ₂ |- [σ₂   ]@l].
+  intros.
+  eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
+  eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
+  apply nd_prod.
+  apply nd_id.
+  eapply nd_rule; eapply RArrange; eapply AuCanL.
+  Defined.
+
+Definition RWhere : ∀ Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ l,
+  ND Rule ([Γ>Δ> Σ₁,,([σ₁@@l],,Σ₃) |- [σ₂]@l ],,[Γ>Δ> Σ₂ |- [σ₁]@l])     [Γ>Δ> Σ₁,,(Σ₂,,Σ₃) |- [σ₂ ]@l].
+  intros.
+  eapply nd_comp; [ apply nd_exch | idtac ].
+  eapply nd_rule; eapply RCut.
+  Defined.
 
 (* A rule is considered "flat" if it is neither RBrak nor REsc *)
 (* TODO: change this to (if RBrak/REsc -> False) *)
@@ -126,8 +137,6 @@ Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop :=
 | Flat_RAppCo           : ∀ Γ Δ  Σ σ₁ σ₂ σ γ q l,  Rule_Flat (RAppCo Γ Δ  Σ  σ₁ σ₂ σ γ  q l)
 | Flat_RAbsCo           : ∀ Γ   Σ κ σ  σ₁ σ₂ q1 q2   , Rule_Flat (RAbsCo Γ   Σ κ σ  σ₁ σ₂  q1 q2   )
 | Flat_RApp             : ∀ Γ Δ  Σ tx te   p     l,  Rule_Flat (RApp Γ Δ  Σ tx te   p l)
-| Flat_RLet             : ∀ Γ Δ  Σ σ₁ σ₂   p     l,  Rule_Flat (RLet Γ Δ  Σ σ₁ σ₂   p l)
-| Flat_RJoin    : ∀ q a b c d e l,  Rule_Flat (RJoin q a b c d e l)
 | Flat_RVoid      : ∀ q a                  l,  Rule_Flat (RVoid q a l)
 | Flat_RCase            : ∀ Σ Γ  T κlen κ θ l x  , Rule_Flat (RCase Σ Γ T κlen κ θ l x)
 | Flat_RLetRec          : ∀ Γ Δ Σ₁ τ₁ τ₂ lev,      Rule_Flat (RLetRec Γ Δ Σ₁ τ₁ τ₂ lev).
@@ -174,41 +183,3 @@ Lemma systemfc_all_rules_one_conclusion : forall h c1 c2 (r:Rule h (c1,,c2)), Fa
   auto.
   Qed.
 
-(* "Arrange" objects are parametric in the type of the leaves of the tree *)
-Definition arrangeMap :
-  forall {T} (Σ₁ Σ₂:Tree ??T) {R} (f:T -> R),
-    Arrange Σ₁ Σ₂ ->
-    Arrange (mapOptionTree f Σ₁) (mapOptionTree f Σ₂).
-  intros.
-  induction X; simpl.
-  apply RId.
-  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 IHX1 | apply IHX2 ].
-  Defined.
-
-(* a frequently-used Arrange *)
-Definition arrangeSwapMiddle {T} (a b c d:Tree ??T) :
-  Arrange ((a,,b),,(c,,d)) ((a,,c),,(b,,d)).
-  eapply RComp.
-  apply RCossa.
-  eapply RComp.
-  eapply RLeft.
-  eapply RComp.
-  eapply RAssoc.
-  eapply RRight.
-  apply RExch.
-  eapply RComp.
-  eapply RLeft.
-  eapply RCossa.
-  eapply RAssoc.
-  Defined.