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

diff --git a/src/HaskProof.v b/src/HaskProof.v
index 0b0200b..d9c6a7e 100644
--- a/src/HaskProof.v
+++ b/src/HaskProof.v
@@ -45,6 +45,7 @@ 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    )
@@ -81,7 +82,7 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
 
 | 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]]
 
@@ -169,4 +170,41 @@ 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 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.