move Arrange into NaturalDeductionContext

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

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.