move Arrange into NaturalDeductionContext

[coq-hetmet.git] / src / HaskProof.v

diff --git a/src/HaskProof.v b/src/HaskProof.v
index d92dd6b..c887b8a 100644 (file)
--- 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 :=
 
@@ -174,41 +158,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.