move general-purpose routines from HaskFlattener to HaskProof/General

diff --git a/src/General.v b/src/General.v
index d017894..cf9d28d 100644 (file)
--- a/src/General.v
+++ b/src/General.v
@@ -89,6 +89,13 @@ Fixpoint treeReduce {T:Type}{R:Type}(mapLeaf:T->R)(mergeBranches:R->R->R) (t:Tre
 Definition treeDecomposition {D T:Type} (mapLeaf:T->D) (mergeBranches:D->D->D) :=
   forall d:D, { tt:Tree T & d = treeReduce mapLeaf mergeBranches tt }.
 
 Definition treeDecomposition {D T:Type} (mapLeaf:T->D) (mergeBranches:D->D->D) :=
   forall d:D, { tt:Tree T & d = treeReduce mapLeaf mergeBranches tt }.
 

+Fixpoint reduceTree {T}(unit:T)(merge:T -> T -> T)(tt:Tree ??T) : T :=
+  match tt with
+    | T_Leaf None     => unit
+    | T_Leaf (Some x) => x
+    | T_Branch b1 b2  => merge (reduceTree unit merge b1) (reduceTree unit merge b2)
+  end.
+

 Lemma tree_dec_eq :
    forall {Q}(t1 t2:Tree ??Q),
      (forall q1 q2:Q, sumbool (q1=q2) (not (q1=q2))) ->
 Lemma tree_dec_eq :
    forall {Q}(t1 t2:Tree ??Q),
      (forall q1 q2:Q, sumbool (q1=q2) (not (q1=q2))) ->

@@ -445,6 +452,55 @@ Instance EqDecidableList {T:Type}(eqd:EqDecidable T) : EqDecidable (list T).
   Defined.
 
 (*******************************************************************************)
   Defined.
 
 (*******************************************************************************)

+(* Tree Flags                                                                  *)
+
+(* TreeFlags is effectively a tree of booleans whose shape matches that of another tree *)
+Inductive TreeFlags {T:Type} : Tree T -> Type :=
+| tf_leaf_true  : forall x, TreeFlags (T_Leaf x)
+| tf_leaf_false : forall x, TreeFlags (T_Leaf x)
+| tf_branch     : forall b1 b2, TreeFlags b1 -> TreeFlags b2 -> TreeFlags (b1,,b2).
+
+(* If flags are calculated using a local condition, this will build the flags *)
+Fixpoint mkFlags {T}(f:T -> bool)(t:Tree T) : TreeFlags t :=
+  match t as T return TreeFlags T with
+    | T_Leaf x => if f x then tf_leaf_true x else tf_leaf_false x
+    | T_Branch b1 b2 => tf_branch _ _ (mkFlags f b1) (mkFlags f b2)
+  end.
+
+(* takeT and dropT are not exact inverses! *)
+
+(* drop replaces each leaf where the flag is set with a [] *)
+Fixpoint dropT {T}{Σ:Tree ??T}(tf:TreeFlags Σ) : Tree ??T :=
+  match tf with
+    | tf_leaf_true  x         => []
+    | tf_leaf_false x         => Σ
+    | tf_branch b1 b2 tb1 tb2 => (dropT tb1),,(dropT tb2)
+  end.
+
+(* takeT returns only those leaves for which the flag is set; all others are omitted entirely from the tree *)
+Fixpoint takeT {T}{Σ:Tree T}(tf:TreeFlags Σ) : ??(Tree T) :=
+  match tf with
+    | tf_leaf_true  x         => Some Σ
+    | tf_leaf_false x         => None
+    | tf_branch b1 b2 tb1 tb2 =>
+      match takeT tb1 with
+        | None     => takeT tb2
+        | Some b1' => match takeT tb2 with
+                        | None     => Some b1'
+                        | Some b2' => Some (b1',,b2')
+                      end
+      end
+  end.
+
+(* lift a function T->bool to a function (option T)->bool by yielding (None |-> b) *)
+Definition liftBoolFunc {T}(b:bool)(f:T -> bool) : ??T -> bool :=
+  fun t =>
+    match t with
+      | None   => b
+      | Some x => f x
+    end.
+
+(*******************************************************************************)

 (* Length-Indexed Lists                                                        *)
 
 Inductive vec (A:Type) : nat -> Type :=
 (* Length-Indexed Lists                                                        *)
 
 Inductive vec (A:Type) : nat -> Type :=

@@ -739,6 +795,8 @@ Lemma extensionality_composes : forall t1 t2 t3 (f f':t1->t2) (g g':t2->t3),
 
 Definition map2 {A}{B}(f:A->B)(t:A*A) : (B*B) := ((f (fst t)), (f (snd t))).
 
 
 Definition map2 {A}{B}(f:A->B)(t:A*A) : (B*B) := ((f (fst t)), (f (snd t))).
 

+(* boolean "not" *)
+Definition bnot (b:bool) : bool := if b then false else true.

 
 (* string stuff *)
 Variable eol : string.
 
 (* string stuff *)
 Variable eol : string.

diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v
index ae99605..6386c19 100644 (file)
--- a/src/HaskFlattener.v
+++ b/src/HaskFlattener.v
@@ -31,6 +31,7 @@ Require Import HaskProofToStrong.
 Require Import HaskWeakToStrong.
 
 Open Scope nd_scope.
 Require Import HaskWeakToStrong.
 
 Open Scope nd_scope.

+Set Printing Width 130.

 
 (*
  *  The flattening transformation.  Currently only TWO-level languages are
 
 (*
  *  The flattening transformation.  Currently only TWO-level languages are

@@ -42,97 +43,9 @@ Open Scope nd_scope.
  *)
 Section HaskFlattener.
 
  *)
 Section HaskFlattener.
 

-  Inductive TreeFlags {T:Type} : Tree T -> Type :=
-  | tf_leaf_true  : forall x, TreeFlags (T_Leaf x)
-  | tf_leaf_false : forall x, TreeFlags (T_Leaf x)
-  | tf_branch     : forall b1 b2, TreeFlags b1 -> TreeFlags b2 -> TreeFlags (b1,,b2).
-
-  Fixpoint mkFlags {T}(f:T -> bool)(t:Tree T) : TreeFlags t :=
-    match t as T return TreeFlags T with
-      | T_Leaf x => if f x then tf_leaf_true x else tf_leaf_false x
-      | T_Branch b1 b2 => tf_branch _ _ (mkFlags f b1) (mkFlags f b2)
-    end.
-
-  (* take and drop are not exact inverses *)
-
-  (* drop replaces each leaf where the flag is set with a [] *)
-  Fixpoint drop {T}{Σ:Tree ??T}(tf:TreeFlags Σ) : Tree ??T :=
-    match tf with
-      | tf_leaf_true  x         => []
-      | tf_leaf_false x         => Σ
-      | tf_branch b1 b2 tb1 tb2 => (drop tb1),,(drop tb2)
-    end.
-
-  (* take returns only those leaves for which the flag is set; all others are omitted entirely from the tree *)
-  Fixpoint take {T}{Σ:Tree T}(tf:TreeFlags Σ) : ??(Tree T) :=
-    match tf with
-      | tf_leaf_true  x         => Some Σ
-      | tf_leaf_false x         => None
-      | tf_branch b1 b2 tb1 tb2 =>
-        match take tb1 with
-          | None     => take tb2
-          | Some b1' => match take tb2 with
-                          | None     => Some b1'
-                          | Some b2' => Some (b1',,b2')
-                        end
-        end
-    end.
-
-  Definition maybeTree {T}(t:??(Tree ??T)) : Tree ??T :=
-    match t with
-      | None => []
-      | Some x => x
-    end.
-
-  Definition setNone {T}(b:bool)(f:T -> bool) : ??T -> bool :=
-    fun t =>
-      match t with
-        | None => b
-        | Some x => f x
-      end.
-
-  (* "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.
-
-  Definition bnot (b:bool) : bool := if b then false else true.
-
-  Definition swapMiddle {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),
   Definition arrange :
     forall {T} (Σ:Tree ??T) (f:T -> bool),

-      Arrange Σ (drop (mkFlags (setNone false f) Σ),,( (drop (mkFlags (setNone false (bnot ○ f)) Σ)))).
+      Arrange Σ (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))).

     intros.
     induction Σ.
       simpl.
     intros.
     induction Σ.
       simpl.

@@ -144,7 +57,7 @@ Section HaskFlattener.
       simpl.
       apply RuCanL.
       simpl in *.
       simpl.
       apply RuCanL.
       simpl in *.

-      eapply RComp; [ idtac | apply swapMiddle ].
+      eapply RComp; [ idtac | apply arrangeSwapMiddle ].

       eapply RComp.
       eapply RLeft.
       apply IHΣ2.
       eapply RComp.
       eapply RLeft.
       apply IHΣ2.

@@ -154,7 +67,7 @@ Section HaskFlattener.
 
   Definition arrange' :
     forall {T} (Σ:Tree ??T) (f:T -> bool),
 
   Definition arrange' :
     forall {T} (Σ:Tree ??T) (f:T -> bool),

-      Arrange (drop (mkFlags (setNone false f) Σ),,( (drop (mkFlags (setNone false (bnot ○ f)) Σ)))) Σ.
+      Arrange (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))) Σ.

     intros.
     induction Σ.
       simpl.
     intros.
     induction Σ.
       simpl.

@@ -166,7 +79,7 @@ Section HaskFlattener.
       simpl.
       apply RCanL.
       simpl in *.
       simpl.
       apply RCanL.
       simpl in *.

-      eapply RComp; [ apply swapMiddle | idtac ].
+      eapply RComp; [ apply arrangeSwapMiddle | idtac ].

       eapply RComp.
       eapply RLeft.
       apply IHΣ2.
       eapply RComp.
       eapply RLeft.
       apply IHΣ2.

@@ -174,15 +87,6 @@ Section HaskFlattener.
       apply IHΣ1.
       Defined.
 
       apply IHΣ1.
       Defined.
 

-  Definition minus' n m :=
-    match m with
-      | 0 => n
-      | _ => match n with
-               | 0 => 0
-               | _ => n - m
-             end
-    end.
-

   Ltac eqd_dec_refl' :=
     match goal with
       | [ |- context[@eqd_dec ?T ?V ?X ?X] ] =>
   Ltac eqd_dec_refl' :=
     match goal with
       | [ |- context[@eqd_dec ?T ?V ?X ?X] ] =>

@@ -190,15 +94,6 @@ Section HaskFlattener.
           [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ]
   end.
 
           [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ]
   end.
 

-  Fixpoint reduceTree {T}(unit:T)(merge:T -> T -> T)(tt:Tree ??T) : T :=
-    match tt with
-      | T_Leaf None     => unit
-      | T_Leaf (Some x) => x
-      | T_Branch b1 b2  => merge (reduceTree unit merge b1) (reduceTree unit merge b2)
-    end.
-
-  Set Printing Width 130.
-

   Context (hetmet_flatten : WeakExprVar).
   Context (hetmet_unflatten : WeakExprVar).
   Context (hetmet_id      : WeakExprVar).
   Context (hetmet_flatten : WeakExprVar).
   Context (hetmet_unflatten : WeakExprVar).
   Context (hetmet_id      : WeakExprVar).

@@ -284,25 +179,31 @@ Section HaskFlattener.
 
   (* In a tree of types, replace any type at depth "lev" or greater None *)
   Definition mkDropFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
 
   (* In a tree of types, replace any type at depth "lev" or greater None *)
   Definition mkDropFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=

-    mkFlags (setNone false (levelMatch lev)) tt.
+    mkFlags (liftBoolFunc false (levelMatch lev)) tt.

 
   Definition drop_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
 
   Definition drop_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=

-    drop (mkDropFlags lev tt).
+    dropT (mkDropFlags lev tt).

 
   (* The opposite: replace any type which is NOT at level "lev" with None *)
   Definition mkTakeFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
 
   (* The opposite: replace any type which is NOT at level "lev" with None *)
   Definition mkTakeFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=

-    mkFlags (setNone true (bnot ○ levelMatch lev)) tt.
+    mkFlags (liftBoolFunc true (bnot ○ levelMatch lev)) tt.

 
   Definition take_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★) :=
 
   Definition take_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★) :=

-    mapOptionTree (fun x => garrowfy_code_types (unlev x)) (drop (mkTakeFlags lev tt)).
+    mapOptionTree (fun x => garrowfy_code_types (unlev x)) (dropT (mkTakeFlags lev tt)).

 (*
     mapOptionTree (fun x => garrowfy_code_types (unlev x))
 (*
     mapOptionTree (fun x => garrowfy_code_types (unlev x))

-    (maybeTree (take tt (mkFlags (
+    (maybeTree (takeT tt (mkFlags (

       fun t => match t with
                  | Some (ttype @@ tlev) => if eqd_dec tlev lev then true else false
                  | _                    => true
                end
     ) tt))).
       fun t => match t with
                  | Some (ttype @@ tlev) => if eqd_dec tlev lev then true else false
                  | _                    => true
                end
     ) tt))).

+
+  Definition maybeTree {T}(t:??(Tree ??T)) : Tree ??T :=
+    match t with
+      | None   => []
+      | Some x => x
+    end.

 *)
 
   Lemma drop_lev_lemma : forall Γ (lev:HaskLevel Γ) x, drop_lev lev [x @@  lev] = [].
 *)
 
   Lemma drop_lev_lemma : forall Γ (lev:HaskLevel Γ) x, drop_lev lev [x @@  lev] = [].

@@ -361,11 +262,33 @@ Section HaskFlattener.
       change (@take_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
     end.
 
       change (@take_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
     end.
 

+  (* AXIOMS *)
+

   Axiom literal_types_unchanged : forall Γ l, garrowfy_code_types (literalType l) = literalType(Γ:=Γ) l.
 
   Axiom flatten_coercion : forall Γ Δ κ (σ τ:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)),
     HaskCoercion Γ Δ (garrowfy_code_types σ ∼∼∼ garrowfy_code_types τ).
 
   Axiom literal_types_unchanged : forall Γ l, garrowfy_code_types (literalType l) = literalType(Γ:=Γ) l.
 
   Axiom flatten_coercion : forall Γ Δ κ (σ τ:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)),
     HaskCoercion Γ Δ (garrowfy_code_types σ ∼∼∼ garrowfy_code_types τ).
 

+  Axiom garrowfy_commutes_with_substT :
+    forall  κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★) (τ:HaskType Γ κ),
+    garrowfy_code_types  (substT σ τ) = substT (fun TV ite v => garrowfy_raw_codetypes  (σ TV ite v))
+      (garrowfy_code_types  τ).
+
+  Axiom garrowfy_commutes_with_HaskTAll :
+    forall  κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
+    garrowfy_code_types  (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => garrowfy_raw_codetypes (σ TV ite v)).
+
+  Axiom garrowfy_commutes_with_HaskTApp :
+    forall  κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
+    garrowfy_code_types  (HaskTApp (weakF σ) (FreshHaskTyVar κ)) =
+    HaskTApp (weakF (fun TV ite v => garrowfy_raw_codetypes  (σ TV ite v))) (FreshHaskTyVar κ).
+
+  Axiom garrowfy_commutes_with_weakLT : forall (Γ:TypeEnv) κ  t,
+    garrowfy_leveled_code_types  (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (garrowfy_leveled_code_types  t).
+
+  Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v,
+    garrowfy_code_types (g v) = g v.
+

   (* This tries to assign a single level to the entire succedent of a judgment.  If the succedent has types from different
    * levels (should not happen) it just picks one; if the succedent has no non-None leaves (also should not happen) it
    * picks nil *)
   (* This tries to assign a single level to the entire succedent of a judgment.  If the succedent has types from different
    * levels (should not happen) it just picks one; if the succedent has no non-None leaves (also should not happen) it
    * picks nil *)

@@ -510,11 +433,12 @@ Section HaskFlattener.
     apply q.
     Defined.
 
     apply q.
     Defined.
 

-(*
+  (* useful for cutting down on the pretty-printed noise
+  

   Notation "`  x" := (take_lev _ x) (at level 20).
   Notation "`` x" := (mapOptionTree unlev x) (at level 20).
   Notation "``` x" := (drop_lev _ x) (at level 20).
   Notation "`  x" := (take_lev _ x) (at level 20).
   Notation "`` x" := (mapOptionTree unlev x) (at level 20).
   Notation "``` x" := (drop_lev _ x) (at level 20).

-*)
+  *)

   Definition garrowfy_arrangement' :
     forall Γ (Δ:CoercionEnv Γ)
       (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
   Definition garrowfy_arrangement' :
     forall Γ (Δ:CoercionEnv Γ)
       (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),

@@ -533,7 +457,7 @@ Section HaskFlattener.
           | RAssoc a b c         => let case_RAssoc := tt in ga_assoc _ _ _ _ _ _ _
           | RCossa a b c         => let case_RCossa := tt in ga_unassoc _ _ _ _ _ _ _
           | RExch  a b           => let case_RExch := tt  in ga_swap  _ _ _ _ _ _
           | RAssoc a b c         => let case_RAssoc := tt in ga_assoc _ _ _ _ _ _ _
           | RCossa a b c         => let case_RCossa := tt in ga_unassoc _ _ _ _ _ _ _
           | RExch  a b           => let case_RExch := tt  in ga_swap  _ _ _ _ _ _

-          | RWeak  a             => let case_RWeak := tt  in ga_drop  _ _ _ _ _ 
+          | RWeak  a             => let case_RWeak := tt  in ga_drop _ _ _ _ _ 

           | RCont  a             => let case_RCont := tt  in ga_copy  _ _ _ _ _ 
           | RLeft  a b c r'      => let case_RLeft := tt  in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
           | RRight a b c r'      => let case_RRight := tt in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_first  _ _ _ _ _ _ _)
           | RCont  a             => let case_RCont := tt  in ga_copy  _ _ _ _ _ 
           | RLeft  a b c r'      => let case_RLeft := tt  in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
           | RRight a b c r'      => let case_RRight := tt in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_first  _ _ _ _ _ _ _)

@@ -747,26 +671,6 @@ Section HaskFlattener.
     reflexivity.
     Qed.
 
     reflexivity.
     Qed.
 

-  Axiom garrowfy_commutes_with_substT :
-    forall  κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★) (τ:HaskType Γ κ),
-    garrowfy_code_types  (substT σ τ) = substT (fun TV ite v => garrowfy_raw_codetypes  (σ TV ite v))
-      (garrowfy_code_types  τ).
-
-  Axiom garrowfy_commutes_with_HaskTAll :
-    forall  κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
-    garrowfy_code_types  (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => garrowfy_raw_codetypes (σ TV ite v)).
-
-  Axiom garrowfy_commutes_with_HaskTApp :
-    forall  κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
-    garrowfy_code_types  (HaskTApp (weakF σ) (FreshHaskTyVar κ)) =
-    HaskTApp (weakF (fun TV ite v => garrowfy_raw_codetypes  (σ TV ite v))) (FreshHaskTyVar κ).
-
-  Axiom garrowfy_commutes_with_weakLT : forall (Γ:TypeEnv) κ  t,
-    garrowfy_leveled_code_types  (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (garrowfy_leveled_code_types  t).
-
-  Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v,
-    garrowfy_code_types (g v) = g v.
-

   Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
     sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
     intro T.
   Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
     sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
     intro T.

diff --git a/src/HaskProof.v b/src/HaskProof.v
index 0b0200b..d28db62 100644 (file)
--- 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.
 
   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.