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 =>
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
(* 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