--- /dev/null
+(*********************************************************************************************************************************)
+(* 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.