X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FGeneral.v;h=d017894f651da7db29cc03dcd2c587861b3e857b;hp=685619ff1e646ebf75eb4bff45c744fe2994d62b;hb=3351499d7cb3d32c8df441426309ec6a1ef2a035;hpb=8f00501ac48984925832279f7d67302c09a570ec

diff --git a/src/General.v b/src/General.v
index 685619f..d017894 100644
--- a/src/General.v
+++ b/src/General.v
@@ -23,7 +23,16 @@ Coercion eqd_type : EqDecidable >-> Sortclass.
 
 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 +50,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 +68,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 
@@ -137,11 +153,10 @@ Lemma mapOptionTree_extensional {A}{B}(f g:A->B) : (forall a, f a = g a) -> (for
   simpl; rewrite IHt1; rewrite IHt2; auto.
   Qed.
 
-Open Scope string_scope.
 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 }.
@@ -341,6 +356,11 @@ 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.
@@ -712,10 +732,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
-}.
 
 
 
@@ -750,7 +766,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)
@@ -868,3 +883,139 @@ 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.