(* 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 )
| RJoin : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ , Rule ([Γ > Δ > Σ₁ |- τ₁ ],,[Γ > Δ > Σ₂ |- τ₂ ]) [Γ>Δ> Σ₁,,Σ₂ |- τ₁,,τ₂ ]
-| RApp : ∀ Γ Δ Σ₁ Σ₂ tx te l, Rule ([Γ>Δ> Σ₁ |- [tx--->te @@l]],,[Γ>Δ> Σ₂ |- [tx@@l]]) [Γ>Δ> Σ₁,,Σ₂ |- [te @@l]]
+| RApp : ∀ Γ Δ Σ₁ Σ₂ tx te l, Rule ([Γ>Δ> Σ₁ |- [tx@@l]],,[Γ>Δ> Σ₂ |- [tx--->te @@l]]) [Γ>Δ> Σ₁,,Σ₂ |- [te @@l]]
| RLet : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₂ |- [σ₂@@l]],,[Γ>Δ> Σ₁,,[σ₂@@l] |- [σ₁@@l] ]) [Γ>Δ> Σ₁,,Σ₂ |- [σ₁ @@l]]
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.