}.
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 *)
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 :=
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),
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 }.
| (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.
| 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.
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 *)
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
-CoInductive Fresh A T :=
-{ next : forall a:A, (T a * Fresh A T)
-; split : Fresh A T * 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.
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)
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)
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".
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.
- admit.
+ 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.
- admit.
- Defined.
+ 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