X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProof.v;h=d28db62e90b3354fa1cd6ea200829c4387b16f9d;hp=0b0200bc9dc52f9fdaf623c87641d113ac8ec5e6;hb=86533ec8492c5736e8cc2bdd55b88fc013c21f89;hpb=1c1cdb9014f409248ca96b677503719916b2b477

diff --git a/src/HaskProof.v b/src/HaskProof.v
index 0b0200b..d28db62 100644
--- a/src/HaskProof.v
+++ b/src/HaskProof.v
@@ -169,4 +169,40 @@ 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 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.