move Arrange into NaturalDeductionContext

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 4da66c7..d500e79 100644 (file)
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -13,6 +13,7 @@ Require Import Preamble.
 Require Import General.
 
 Require Import NaturalDeduction.
 Require Import General.
 
 Require Import NaturalDeduction.

+Require Import NaturalDeductionContext.

 
 Require Import HaskKinds.
 Require Import HaskLiterals.
 
 Require Import HaskKinds.
 Require Import HaskLiterals.

diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v
index 9b3a163..cc9c9aa 100644 (file)
--- a/src/HaskFlattener.v
+++ b/src/HaskFlattener.v
@@ -9,6 +9,7 @@ Generalizable All Variables.
 Require Import Preamble.
 Require Import General.
 Require Import NaturalDeduction.
 Require Import Preamble.
 Require Import General.
 Require Import NaturalDeduction.

+Require Import NaturalDeductionContext.

 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 

@@ -45,52 +46,6 @@ Set Printing Width 130.
  *)
 Section HaskFlattener.
 
  *)
 Section HaskFlattener.
 

-  Definition getlev {Γ}{κ}(lht:LeveledHaskType Γ κ) : HaskLevel Γ :=
-    match lht with t @@ l => l end.
-
-  Definition arrange :
-    forall {T} (Σ:Tree ??T) (f:T -> bool),
-      Arrange Σ (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))).
-    intros.
-    induction Σ.
-      simpl.
-      destruct a.
-      simpl.
-      destruct (f t); simpl.
-      apply RuCanL.
-      apply RuCanR.
-      simpl.
-      apply RuCanL.
-      simpl in *.
-      eapply RComp; [ idtac | apply arrangeSwapMiddle ].
-      eapply RComp.
-      eapply RLeft.
-      apply IHΣ2.
-      eapply RRight.
-      apply IHΣ1.
-      Defined.
-
-  Definition arrange' :
-    forall {T} (Σ:Tree ??T) (f:T -> bool),
-      Arrange (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))) Σ.
-    intros.
-    induction Σ.
-      simpl.
-      destruct a.
-      simpl.
-      destruct (f t); simpl.
-      apply RCanL.
-      apply RCanR.
-      simpl.
-      apply RCanL.
-      simpl in *.
-      eapply RComp; [ apply arrangeSwapMiddle | idtac ].
-      eapply RComp.
-      eapply RLeft.
-      apply IHΣ2.
-      eapply RRight.
-      apply IHΣ1.
-      Defined.

 
   Ltac eqd_dec_refl' :=
     match goal with
 
   Ltac eqd_dec_refl' :=
     match goal with

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 Preamble.
 Require Import General.
 Require Import NaturalDeduction.

+Require Import NaturalDeductionContext.

 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
 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 [ ].
 
 }.
 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 :=
 
 (* 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.
 
   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.

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index 4319a1c..9d88e79 100644 (file)
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -6,6 +6,7 @@ Generalizable All Variables.
 Require Import Preamble.
 Require Import General.
 Require Import NaturalDeduction.
 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.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.

diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v
index 97ef42b..e70322e 100644 (file)
--- a/src/HaskProofToStrong.v
+++ b/src/HaskProofToStrong.v
@@ -6,6 +6,7 @@ Generalizable All Variables.
 Require Import Preamble.
 Require Import General.
 Require Import NaturalDeduction.
 Require Import Preamble.
 Require Import General.
 Require Import NaturalDeduction.

+Require Import NaturalDeductionContext.

 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import Coq.Init.Specif.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import Coq.Init.Specif.

diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v
index bb4dc92..76e1bdb 100644 (file)
--- a/src/HaskSkolemizer.v
+++ b/src/HaskSkolemizer.v
@@ -9,6 +9,7 @@ Generalizable All Variables.
 Require Import Preamble.
 Require Import General.
 Require Import NaturalDeduction.
 Require Import Preamble.
 Require Import General.
 Require Import NaturalDeduction.

+Require Import NaturalDeductionContext.

 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 

diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v
index 8a49c81..8aa4005 100644 (file)
--- a/src/HaskStrongToProof.v
+++ b/src/HaskStrongToProof.v
@@ -6,6 +6,7 @@ Generalizable All Variables.
 Require Import Preamble.
 Require Import General.
 Require Import NaturalDeduction.
 Require Import Preamble.
 Require Import General.
 Require Import NaturalDeduction.

+Require Import NaturalDeductionContext.

 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import Coq.Init.Specif.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import Coq.Init.Specif.

@@ -15,20 +16,7 @@ Require Import HaskStrong.
 Require Import HaskProof.
 
 Section HaskStrongToProof.
 Require Import HaskProof.
 
 Section HaskStrongToProof.

-
-Definition pivotContext {T} a b c : @Arrange T ((a,,b),,c) ((a,,c),,b) :=
-  RComp (RComp (RCossa _ _ _) (RLeft a (RExch c b))) (RAssoc _ _ _).
-
-Definition pivotContext' {T} a b c : @Arrange T (a,,(b,,c)) (b,,(a,,c)) :=
-  RComp (RComp (RAssoc _ _ _) (RRight c (RExch b a))) (RCossa _ _ _).
-
-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.
-  
+ 

 Context {VV:Type}{eqd_vv:EqDecidable VV}.
 
 (* maintenance of Xi *)
 Context {VV:Type}{eqd_vv:EqDecidable VV}.
 
 (* maintenance of Xi *)

diff --git a/src/NaturalDeductionContext.v b/src/NaturalDeductionContext.v
new file mode 100644 (file)
index 0000000..4e9a802
--- /dev/null
+++ b/src/NaturalDeductionContext.v
@@ -0,0 +1,128 @@
+(*********************************************************************************************************************************)
+(* NaturalDeductionContext:                                                                                                      *)
+(*                                                                                                                               *)
+(*   Manipulations of a context in natural deduction proofs.                                                                     *)
+(*                                                                                                                               *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import NaturalDeduction.
+
+Section NaturalDeductionContext.
+
+  (* 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
+  .
+  
+  (* "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.
+
+  Definition arrange :
+    forall {T} (Σ:Tree ??T) (f:T -> bool),
+      Arrange Σ (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))).
+    intros.
+    induction Σ.
+      simpl.
+      destruct a.
+      simpl.
+      destruct (f t); simpl.
+      apply RuCanL.
+      apply RuCanR.
+      simpl.
+      apply RuCanL.
+      simpl in *.
+      eapply RComp; [ idtac | apply arrangeSwapMiddle ].
+      eapply RComp.
+      eapply RLeft.
+      apply IHΣ2.
+      eapply RRight.
+      apply IHΣ1.
+      Defined.
+
+  Definition arrange' :
+    forall {T} (Σ:Tree ??T) (f:T -> bool),
+      Arrange (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))) Σ.
+    intros.
+    induction Σ.
+      simpl.
+      destruct a.
+      simpl.
+      destruct (f t); simpl.
+      apply RCanL.
+      apply RCanR.
+      simpl.
+      apply RCanL.
+      simpl in *.
+      eapply RComp; [ apply arrangeSwapMiddle | idtac ].
+      eapply RComp.
+      eapply RLeft.
+      apply IHΣ2.
+      eapply RRight.
+      apply IHΣ1.
+      Defined.
+
+  Definition pivotContext {T} a b c : @Arrange T ((a,,b),,c) ((a,,c),,b) :=
+    RComp (RComp (RCossa _ _ _) (RLeft a (RExch c b))) (RAssoc _ _ _).
+  
+  Definition pivotContext' {T} a b c : @Arrange T (a,,(b,,c)) (b,,(a,,c)) :=
+    RComp (RComp (RAssoc _ _ _) (RRight c (RExch b a))) (RCossa _ _ _).
+  
+  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.
+
+End NaturalDeductionContext.