X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FGeneral.v;h=541dc6f1200ad8bcb54ea45713a3897af76f7d9c;hp=e1e57910bb30a4ea3160927b3767bb1df800cf28;hb=18a60d7a8ae87aa64c73f9ac03c785b12f8bd25a;hpb=30cc675d57492799644506f3632625f371a3e89a

diff --git a/src/General.v b/src/General.v
index e1e5791..541dc6f 100644
--- a/src/General.v
+++ b/src/General.v
@@ -20,10 +20,37 @@ Class EqDecidable (T:Type) :=
 }.
 Coercion eqd_type : EqDecidable >-> Sortclass.
 
+Instance EqDecidableOption (T:Type)(EQDT:EqDecidable T) : EqDecidable ??T.
+  apply Build_EqDecidable.
+  intros.
+  destruct v1;
+  destruct v2.
+  destruct (eqd_dec t t0).
+  subst.
+  left; auto.
+  right.
+  unfold not; intros.
+  inversion H.
+  subst.
+  apply n.
+  auto.
+  right; unfold not; intro; inversion H.
+  right; unfold not; intro; inversion H.
+  left; auto.
+  Defined.
 
 Class ToString (T:Type) := { toString : T -> string }.
 Instance StringToString : ToString string := { toString := fun x => x }.
-Notation "a +++ b" := (append (toString a) (toString b)) (at level 100).
+
+Class Concatenable {T:Type} :=
+ { concatenate : T -> T -> T }.
+ Implicit Arguments Concatenable [ ].
+Open Scope string_scope.
+Open Scope type_scope.
+Close Scope list_scope.
+Notation "a +++ b" := (@concatenate _ _ a b) (at level 99).
+Instance ConcatenableString : Concatenable string := { concatenate := append }.
+
 
 (*******************************************************************************)
 (* Trees                                                                       *)
@@ -41,6 +68,13 @@ Notation "[ q ]"    := (@T_Leaf (option _) (Some q))            : tree_scope.
 Notation "[ ]"      := (@T_Leaf (option _) None)                : tree_scope.
 Notation "[]"       := (@T_Leaf (option _) None)                : tree_scope.
 
+Fixpoint InT {A} (a:A) (t:Tree ??A) {struct t} : Prop :=
+  match t with
+    | T_Leaf None     => False
+    | T_Leaf (Some x) => x = a
+    | T_Branch b1 b2  => InT a b1 \/ InT a b2
+  end.
+
 Open Scope tree_scope.
 
 Fixpoint mapTree {a b:Type}(f:a->b)(t:@Tree a) : @Tree b :=
@@ -52,7 +86,7 @@ Fixpoint mapOptionTree {a b:Type}(f:a->b)(t:@Tree ??a) : @Tree ??b :=
   match t with 
     | T_Leaf None     => T_Leaf None
     | T_Leaf (Some x) => T_Leaf (Some (f x))
-    | T_Branch l r => T_Branch (mapOptionTree f l) (mapOptionTree f r)
+    | T_Branch l r    => T_Branch (mapOptionTree f l) (mapOptionTree f r)
   end.
 Fixpoint mapTreeAndFlatten {a b:Type}(f:a->@Tree b)(t:@Tree a) : @Tree b :=
   match t with 
@@ -72,6 +106,18 @@ Fixpoint treeReduce {T:Type}{R:Type}(mapLeaf:T->R)(mergeBranches:R->R->R) (t:Tre
   end.
 Definition treeDecomposition {D T:Type} (mapLeaf:T->D) (mergeBranches:D->D->D) :=
   forall d:D, { tt:Tree T & d = treeReduce mapLeaf mergeBranches tt }.
+Lemma mapOptionTree_distributes
+  : forall T R (a b:Tree ??T) (f:T->R),
+    mapOptionTree f (a,,b) = (mapOptionTree f a),,(mapOptionTree f b).
+  reflexivity.
+  Qed.
+
+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),
@@ -129,11 +175,18 @@ Lemma mapOptionTree_compose : forall A B C (f:A->B)(g:B->C)(l:Tree ??A),
     reflexivity.
     Qed.
 
-Open Scope string_scope.
+Lemma mapOptionTree_extensional {A}{B}(f g:A->B) : (forall a, f a = g a) -> (forall t, mapOptionTree f t = mapOptionTree g t).
+  intros.
+  induction t.
+  destruct a; auto.
+  simpl; rewrite H; auto.
+  simpl; rewrite IHt1; rewrite IHt2; auto.
+  Qed.
+
 Fixpoint treeToString {T}{TT:ToString T}(t:Tree ??T) : string :=
 match t with
   | T_Leaf None => "[]"
-  | T_Leaf (Some s) => "["+++s+++"]"
+  | T_Leaf (Some s) => "["+++toString s+++"]"
   | T_Branch b1 b2 => treeToString b1 +++ ",," +++ treeToString b2
 end.
 Instance TreeToString {T}{TT:ToString T} : ToString (Tree ??T) := { toString := treeToString }.
@@ -165,6 +218,104 @@ Fixpoint mapProp {A:Type} (f:A->Prop) (l:list A) : Prop :=
     | (a::al) => f a /\ mapProp f al
   end.
 
+
+(* delete the n^th element of a list *)
+Definition list_del : forall {T:Type} (l:list T) (n:nat)(pf:lt n (length l)), list T.
+  refine (fix list_del {T:Type} (l:list T) (n:nat) : lt n (length l) -> list T :=
+    match l as L return lt n (length L) -> list T with
+      | nil  => _
+      | a::b => match n with
+                  | O    => fun _ => b
+                  | S n' => fun pf => (fun list_del' => _) (list_del _ b n')
+                end
+    end).
+    intro pf.
+    simpl in pf.
+    assert False.
+    inversion pf.
+    inversion H.
+
+    simpl in *.
+    apply list_del'.
+    omega.
+    Defined.
+
+Definition list_get : forall {T:Type} (l:list T) (n:nat), lt n (length l) -> T.
+  refine (fix list_get {T:Type} (l:list T) (n:nat) : lt n (length l) -> T :=
+    match l as L return lt n (length L) -> T with
+      | nil => _
+      | a::b => match n with
+                  | O    => fun _ => a
+                  | S n' => fun pf => (fun list_get' => _) (list_get _ b n')
+                end
+    end).
+  intro pf.
+  assert False.
+  inversion pf.
+  inversion H.
+
+  simpl in *.
+  apply list_get'.
+  omega.
+  Defined.
+
+Fixpoint list_ins (n:nat) {T:Type} (t:T) (l:list T) : list T :=
+  match n with
+    | O    => t::l
+    | S n' => match l with
+                | nil  => t::nil
+                | a::b => a::(list_ins n' t b)
+              end
+  end.
+
+Lemma list_ins_nil : forall T n x, @list_ins n T x nil = x::nil.
+  intros.
+  destruct n; auto.
+  Qed.
+
+Fixpoint list_take {T:Type}(l:list T)(n:nat) :=
+  match n with
+    | O    => nil
+    | S n' => match l with
+                | nil  => nil
+                | a::b => a::(list_take b n')
+              end
+  end.
+
+Fixpoint list_drop {T:Type}(l:list T)(n:nat) :=
+  match n with
+    | O    => l
+    | S n' => match l with
+                | nil  => nil
+                | a::b => list_drop b n'
+              end
+  end.
+
+Lemma list_ins_app T n κ : forall Γ, @list_ins n T κ Γ = app (list_take Γ n) (κ::(list_drop Γ n)).
+  induction n.
+  simpl.
+  intros.
+  destruct Γ; auto.
+  intro Γ.
+  destruct Γ.
+  reflexivity.
+  simpl.
+  rewrite <- IHn.
+  reflexivity.
+  Qed.
+
+Lemma list_take_drop T l : forall n, app (@list_take T l n) (list_drop l n) = l.
+  induction l; auto.
+  simpl.
+  destruct n; auto.
+  simpl.
+  destruct n.
+  reflexivity.
+  simpl.
+  rewrite IHl.
+  reflexivity.
+  Qed.
+
 Lemma map_id : forall A (l:list A), (map (fun x:A => x) l) = l.
   induction l.
   auto.
@@ -223,6 +374,17 @@ Lemma mapOptionTree_comp a b c (f:a->b) (g:b->c) q : (mapOptionTree g (mapOption
     reflexivity.
   Qed.
 
+Lemma leaves_unleaves {T}(t:list T) : leaves (unleaves t) = t.
+  induction t; auto.
+  simpl.
+  rewrite IHt; auto.
+  Qed.
+
+Lemma mapleaves' {T:Type}(t:list T){Q}{f:T->Q} : unleaves (map f t) = mapOptionTree f (unleaves t).
+  induction t; simpl in *; auto.
+  rewrite IHt; auto.
+  Qed.
+
 (* handy facts: map preserves the length of a list *)
 Lemma map_on_nil : forall A B (s1:list A) (f:A->B), nil = map f s1 -> s1=nil.
   intros.
@@ -301,6 +463,16 @@ Fixpoint unleaves'' {A:Type}(l:list ??A) : Tree ??A :=
     | (a::b) => (unleaves'' b),,(T_Leaf a)
   end.
 
+Lemma mapleaves {T:Type}(t:Tree ??T){Q}{f:T->Q} : leaves (mapOptionTree f t) = map f (leaves t).
+  induction t.
+  destruct a; auto.
+  simpl.
+  rewrite IHt1.
+  rewrite IHt2.
+  rewrite map_app.
+  auto.
+  Qed.
+
 Fixpoint filter {T:Type}(l:list ??T) : list T :=
   match l with
     | nil => nil
@@ -312,6 +484,55 @@ Inductive distinct {T:Type} : list T -> Prop :=
 | distinct_nil  : distinct nil
 | distinct_cons : forall a ax, (@In _ a ax -> False) -> distinct ax -> distinct (a::ax).
 
+Inductive distinctT {T:Type} : Tree ??T -> Prop :=
+| distinctT_nil  : distinctT []
+| distinctT_leaf : forall t, distinctT [t]
+| distinctT_cons : forall t1 t2, (forall v, InT v t1 -> InT v t2 -> False) -> distinctT (t1,,t2).
+
+Lemma in_decidable {VV:Type}{eqdVV:EqDecidable VV} : forall (v:VV)(lv:list VV), sumbool (In v lv) (not (In v lv)).
+  intros.
+  induction lv.
+  right.
+  unfold not.
+  intros.
+  inversion H.
+  destruct IHlv.
+  left.
+  simpl.
+  auto.
+  set (eqd_dec v a) as dec.
+  destruct dec.
+  subst.
+  left; simpl; auto.
+  right.
+  unfold not; intros.
+  destruct H.
+  subst.
+  apply n0; auto.
+  apply n.
+  apply H.
+  Defined.
+
+Lemma distinct_decidable {VV:Type}{eqdVV:EqDecidable VV} : forall (lv:list VV), sumbool (distinct lv) (not (distinct lv)).
+  intros.
+  induction lv.
+  left; apply distinct_nil.
+  destruct IHlv.
+  set (in_decidable a lv) as dec.
+  destruct dec.
+  right; unfold not; intros.
+  inversion H.
+  subst.
+  apply H2; auto.
+  left.
+  apply distinct_cons; auto.
+  right.
+  unfold not; intros.
+  inversion H.
+  subst.
+  apply n; auto.
+  Defined.
+
 Lemma map_preserves_length {A}{B}(f:A->B)(l:list A) : (length l) = (length (map f l)).
   induction l; auto.
   simpl.
@@ -351,6 +572,112 @@ Instance EqDecidableList {T:Type}(eqd:EqDecidable T) : EqDecidable (list T).
   apply eqd_dec.
   Defined.
 
+Fixpoint listToString {T:Type}{tst:ToString T}(l:list T) : string :=
+  match l with
+    | nil  => "nil"
+    | a::b => (toString a) +++ "::" +++ listToString b
+  end.
+
+Instance ListToString {T:Type}{tst:ToString T} : ToString (list T) :=
+  { toString := @listToString _ _ }.
+
+
+(*******************************************************************************)
+(* 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.
+
+Definition takeT' {T}{Σ:Tree ??T}(tf:TreeFlags Σ) : Tree ??T :=
+  match takeT tf with
+    | None   => []
+    | Some x => x
+  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.
+
+(* decidable quality on a tree of elements which have decidable equality *)
+Definition tree_eq_dec : forall {T:Type}(l1 l2:Tree T)(dec:forall t1 t2:T, sumbool (eq t1 t2) (not (eq t1 t2))),
+  sumbool (eq l1 l2) (not (eq l1 l2)).
+  intro T.
+  intro l1.
+  induction l1; intros.
+    destruct l2.
+    destruct (dec a t).
+    subst.
+    left; auto.
+    right; unfold not; intro; apply n; inversion H; auto.
+  right.
+    unfold not; intro.
+    inversion H.
+
+  destruct l2.
+    right; unfold not; intro; inversion H.
+    destruct (IHl1_1 l2_1 dec);
+    destruct (IHl1_2 l2_2 dec); subst.
+    left; auto.
+    right.
+      unfold not; intro.
+      inversion H; subst.
+      apply n; auto.
+    right.
+      unfold not; intro.
+      inversion H; subst.
+      apply n; auto.
+    right.
+      unfold not; intro.
+      inversion H; subst.
+      apply n; auto.
+      Defined.
+
+Instance EqDecidableTree {T:Type}(eqd:EqDecidable T) : EqDecidable (Tree T).
+  apply Build_EqDecidable.
+  intros.
+  apply tree_eq_dec.
+  apply eqd_dec.
+  Defined.
+
 (*******************************************************************************)
 (* Length-Indexed Lists                                                        *)
 
@@ -574,6 +901,30 @@ Lemma ilist_chop' {T}{F}{l1 l2:list T}(v:IList T F (app l1 l2)) : IList T F l2.
   inversion v; subst; auto.
   Defined.
 
+Lemma ilist_app {T}{F}{l1:list T}(v1:IList T F l1) : forall {l2:list T}(v2:IList T F l2), IList T F (app l1 l2).
+  induction l1; auto.
+  intros.
+  inversion v1.
+  subst.
+  simpl.
+  apply ICons.
+  apply X.
+  apply IHl1; auto.
+  Defined.
+
+Definition ilist_ins {T}{F}{l:list T} z (fz:F z) : forall n (il:IList T F l), IList T F (list_ins n z l).
+  induction l; simpl.
+  intros.
+  destruct n; simpl.
+  apply ICons; [ apply fz | apply INil ].
+  apply ICons; [ apply fz | apply INil ].
+  intros.
+  destruct n; simpl.
+  apply ICons; auto.
+  inversion il; subst.
+  apply ICons; auto.
+  Defined.
+
 Fixpoint ilist_to_list {T}{Z}{l:list T}(il:IList T (fun _ => Z) l) : list Z :=
   match il with
   | INil   => nil
@@ -589,7 +940,22 @@ Implicit Arguments INil    [ I F ].
 Implicit Arguments ILeaf   [ I F ].
 Implicit Arguments IBranch [ I F ].
 
+Definition itmap {I}{F}{G}{il:Tree ??I}(f:forall i:I, F i -> G i) : ITree I F il -> ITree I G il.
+  induction il; intros; auto.
+  destruct a.
+  apply ILeaf.
+  apply f.
+  inversion X; auto.
+  apply INone.
+  apply IBranch; inversion X; auto.
+  Defined.
 
+Fixpoint itree_to_tree {T}{Z}{l:Tree ??T}(il:ITree T (fun _ => Z) l) : Tree ??Z :=
+  match il with
+  | INone     => []
+  | ILeaf _ a => [a]
+  | IBranch _ _ b1 b2 => (itree_to_tree b1),,(itree_to_tree b2)
+  end.
 
 
 (*******************************************************************************)
@@ -624,10 +990,6 @@ Lemma extensionality_composes : forall t1 t2 t3 (f f':t1->t2) (g g':t2->t3),
 
 
 
-CoInductive Fresh A T :=
-{ next  : forall a:A, (T a * Fresh A T)
-; split : Fresh A T * Fresh A T
-}.
 
 
 
@@ -635,6 +997,10 @@ CoInductive Fresh A 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.
+Definition band (b1 b2:bool) : bool := if b1 then b2 else false.
+Definition bor  (b1 b2:bool) : bool := if b1 then true else b2.
 
 (* string stuff *)
 Variable eol : string.
@@ -662,7 +1028,6 @@ Definition orErrorBind {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) :=
   end.
 Notation "a >>= b" := (@orErrorBind _ a _ b) (at level 20).
 
-Open Scope string_scope.
 Definition orErrorBindWithMessage {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) err_msg :=
   match oe with
     | Error s => Error (err_msg +++ eol +++ "  " +++ s)
@@ -672,7 +1037,7 @@ Definition orErrorBindWithMessage {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrErr
 Notation "a >>=[ S ] b" := (@orErrorBindWithMessage _ a _ b S) (at level 20).
 
 Definition addErrorMessage s {T} (x:OrError T) :=
-  x >>=[ s ] (fun y => OK y).
+  x >>=[ eol +++ eol +++ s ] (fun y => OK y).
 
 Inductive Indexed {T:Type}(f:T -> Type) : ???T -> Type :=
 | Indexed_Error : forall error_message:string, Indexed f (Error error_message)
@@ -723,8 +1088,206 @@ Lemma list2vecOrFail {T}(l:list T)(n:nat)(error_message:nat->nat->string) : ???(
     apply (Error (error_message (length l) n)).
     Defined.
 
+(* this makes a type function application, ensuring not to oversaturate it (though if it was undersaturated we can't fix that) *)
+Fixpoint split_list {T}(l:list T)(n:nat) : ???(list T * list T) :=
+  match n with
+    | O    => OK (nil , l)
+    | S n' => match l with
+                | nil  => Error "take_list failed"
+                | h::t => split_list t n' >>= fun t' => let (t1,t2) := t' in OK ((h::t1),t2)
+              end
+    end.
+
+(* Uniques *)
+Variable UniqSupply      : Type.                   Extract Inlined Constant UniqSupply     => "UniqSupply.UniqSupply".
+Variable Unique          : Type.                   Extract Inlined Constant Unique         => "Unique.Unique".
+Variable uniqFromSupply  : UniqSupply -> Unique.   Extract Inlined Constant uniqFromSupply => "UniqSupply.uniqFromSupply".
+Variable splitUniqSupply : UniqSupply -> UniqSupply * UniqSupply.
+    Extract Inlined Constant splitUniqSupply => "UniqSupply.splitUniqSupply".
+Variable unique_eq       : forall u1 u2:Unique, sumbool (u1=u2) (u1≠u2).
+    Extract Inlined Constant unique_eq => "(==)".
+Variable unique_toString : Unique -> string.
+    Extract Inlined Constant unique_toString => "show".
+Instance EqDecidableUnique : EqDecidable Unique :=
+  { eqd_dec := unique_eq }.
+Instance EqDecidableToString : ToString Unique :=
+  { toString := unique_toString }.
+
+Inductive UniqM {T:Type} : Type :=
+ | uniqM    : (UniqSupply -> ???(UniqSupply * T)) -> UniqM.
+ Implicit Arguments UniqM [ ].
+
+Instance UniqMonad : Monad UniqM :=
+{ returnM := fun T (x:T) => uniqM (fun u => OK (u,x))
+; bindM   := fun a b (x:UniqM a) (f:a->UniqM b) =>
+  uniqM (fun u =>
+    match x with
+      | uniqM fa =>
+        match fa u with
+          | Error s   => Error s
+          | OK (u',va) => match f va with
+                           | uniqM fb => fb u'
+                         end
+        end
+    end)
+}.
+
+Definition getU : UniqM Unique :=
+  uniqM (fun us => let (us1,us2) := splitUniqSupply us in OK (us1,(uniqFromSupply us2))).
+
+Notation "'bind' x = e ; f" := (@bindM _ _ _ _ e (fun x => f)) (x ident, at level 60, right associativity).
+Notation "'return' x" := (returnM x) (at level 100).
+Notation "'failM'  x" := (uniqM (fun _ => Error x)) (at level 100).
+
 
 
 
 
+
+Record FreshMonad {T:Type} :=
+{ FMT       :  Type -> Type
+; FMT_Monad :> Monad FMT
+; FMT_fresh :  forall tl:list T, FMT { t:T & @In _ t tl -> False }
+}.
+Implicit Arguments FreshMonad [ ].
+Coercion FMT       : FreshMonad >-> Funclass.
+
+
+
 Variable Prelude_error : forall {A}, string -> A.   Extract Inlined Constant Prelude_error => "Prelude.error".
+
+
+
+
+Ltac eqd_dec_refl X :=
+  destruct (eqd_dec X X) as [eqd_dec1 | eqd_dec2];
+    [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ].
+
+Lemma unleaves_injective : forall T (t1 t2:list T), unleaves t1 = unleaves t2 -> t1 = t2.
+  intros T.
+  induction t1; intros.
+  destruct t2.
+  auto.
+  inversion H.
+  destruct t2.
+  inversion H.
+  simpl in H.
+  inversion H.
+  set (IHt1 _ H2) as q.
+  rewrite q.
+  reflexivity.
+  Qed.
+
+(* adapted from Adam Chlipala's posting to the coq-club list (thanks!) *)
+Definition openVec A n (v: vec A (S n)) : exists a, exists v0, v = a:::v0 :=
+  match v in vec _ N return match N return vec A N -> Prop with
+                              | O => fun _ => True
+                              | S n => fun v => exists a, exists v0, v = a:::v0
+                            end v with
+    | vec_nil => I
+    | a:::v0 => ex_intro _ a (ex_intro _ v0 (refl_equal _))
+  end.
+
+Definition nilVec A (v: vec A O) : v = vec_nil :=
+  match v in vec _ N return match N return vec A N -> Prop with
+                              | O   => fun v => v = vec_nil
+                              | S n => fun v => True
+                            end v with
+    | vec_nil => refl_equal _
+    | a:::v0  => I
+  end.
+
+Lemma fst_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@fst _ _) (vec_zip v1 v2) = v1.
+  intros.
+  induction n.
+  set (nilVec _ v1) as v1'.
+  set (nilVec _ v2) as v2'.
+  subst.
+  simpl.
+  reflexivity.
+  set (openVec _ _ v1) as v1'.
+  set (openVec _ _ v2) as v2'.
+  destruct v1'.
+  destruct v2'.
+  destruct H.
+  destruct H0.
+  subst.
+  simpl.
+  rewrite IHn.
+  reflexivity.
+  Qed.
+
+Lemma snd_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@snd _ _) (vec_zip v1 v2) = v2.
+  intros.
+  induction n.
+  set (nilVec _ v1) as v1'.
+  set (nilVec _ v2) as v2'.
+  subst.
+  simpl.
+  reflexivity.
+  set (openVec _ _ v1) as v1'.
+  set (openVec _ _ v2) as v2'.
+  destruct v1'.
+  destruct v2'.
+  destruct H.
+  destruct H0.
+  subst.
+  simpl.
+  rewrite IHn.
+  reflexivity.
+  Qed.
+
+Fixpoint mapM {M}{mon:Monad M}{T}(ml:list (M T)) : M (list T) :=
+  match ml with
+    | nil  => return nil
+    | a::b => bind a' = a ; bind b' = mapM b ; return a'::b'
+  end.
+
+Fixpoint list_to_ilist {T}{F}(f:forall t:T, F t) (l:list T) : IList T F l :=
+  match l as L return IList T F L with
+  | nil  => INil
+  | a::b => ICons a b (f a) (list_to_ilist f b)
+  end.
+
+Fixpoint treeM {T}{M}{MT:Monad M}(t:Tree ??(M T)) : M (Tree ??T) :=
+  match t with
+    | T_Leaf None     => return []
+    | T_Leaf (Some x) => bind x' = x ; return [x']
+    | T_Branch b1 b2  => bind b1' = treeM b1 ; bind b2' = treeM b2 ; return (b1',,b2')
+  end.
+
+
+(* escapifies any characters which might cause trouble for LaTeX *)
+Variable sanitizeForLatex    : string      -> string.
+   Extract Inlined Constant sanitizeForLatex      => "sanitizeForLatex".
+Inductive Latex     : Type := rawLatex     : string -> Latex.
+Inductive LatexMath : Type := rawLatexMath : string -> LatexMath.
+
+Class ToLatex (T:Type) := { toLatex : T -> Latex }.
+Instance ConcatenableLatex : Concatenable Latex :=
+  { concatenate := fun l1 l2 => match l1 with rawLatex l1' => match l2 with rawLatex l2' => rawLatex (l1'+++l2') end end }.
+Instance LatexToString : ToString Latex := { toString := fun x => match x with rawLatex s => s end }.
+
+Class ToLatexMath (T:Type) := { toLatexMath : T -> LatexMath }.
+Instance ConcatenableLatexMath : Concatenable LatexMath :=
+  { concatenate := fun l1 l2 =>
+    match l1 with rawLatexMath l1' =>
+      match l2 with rawLatexMath l2' => rawLatexMath (l1'+++l2')
+      end end }.
+Instance LatexMathToString : ToString LatexMath := { toString := fun x => match x with rawLatexMath s => s end }.
+
+Instance ToLatexLatexMath : ToLatex LatexMath := { toLatex     := fun l => rawLatex     ("$"+++toString l+++"$") }.
+Instance ToLatexMathLatex : ToLatexMath Latex := { toLatexMath := fun l => rawLatexMath ("\text{"+++toString l+++"}") }.
+
+Instance StringToLatex     : ToLatex string := { toLatex := fun x => rawLatex (sanitizeForLatex x) }.
+Instance StringToLatexMath : ToLatexMath  string := { toLatexMath := fun x => toLatexMath (toLatex x) }.
+Instance LatexToLatex          : ToLatex     Latex      := { toLatex := fun x => x }.
+Instance LatexMathToLatexMath  : ToLatexMath LatexMath  := { toLatexMath := fun x => x }.
+
+Fixpoint treeToLatexMath {V}{ToLatexV:ToLatexMath V}(t:Tree ??V) : LatexMath :=
+  match t with
+    | T_Leaf None     => rawLatexMath "\langle\rangle"
+    | T_Leaf (Some x) => (rawLatexMath "\langle")+++toLatexMath x+++(rawLatexMath "\rangle")
+    | T_Branch b1 b2  => (rawLatexMath "\langle")+++treeToLatexMath b1+++(rawLatexMath " , ")
+      +++treeToLatexMath b2+++(rawLatexMath "\rangle")
+  end.