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 *)
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 :=
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
reflexivity.
Qed.
+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) => "["+++toString s+++"]"
+ | T_Branch b1 b2 => treeToString b1 +++ ",," +++ treeToString b2
+end.
+Instance TreeToString {T}{TT:ToString T} : ToString (Tree ??T) := { toString := treeToString }.
(*******************************************************************************)
(* Lists *)
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.
| (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
| 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.
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.
(*******************************************************************************)
-CoInductive Fresh A T :=
-{ next : forall a:A, (T a * Fresh A T)
-; split : Fresh A T * Fresh A T
-}.
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)
apply (Error (error_message (length l) n)).
Defined.
+(* 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.
projects / coq-hetmet.git / blobdiff