}.
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 }.
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
| (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.
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 *)
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 =>
| 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.
+
Fixpoint ilist_to_list {T}{Z}{l:list T}(il:IList T (fun _ => Z) l) : list Z :=
match il with
| INil => nil
(* 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.
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".
projects / coq-hetmet.git / blobdiff