X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FGeneral.v;h=53e37537cd009ec46e96bdca00f01cb0463a39c7;hp=ae27b9f99cc725f7b68a5a2cf719e83421825146;hb=4edce334b28e694c711dfb8e331d737bd0310fe2;hpb=a3592b805c570883fd63a5c75d6e16ea83f2e849

diff --git a/src/General.v b/src/General.v
index ae27b9f..53e3753 100644
--- a/src/General.v
+++ b/src/General.v
@@ -106,6 +106,11 @@ Fixpoint treeReduce {T:Type}{R:Type}(mapLeaf:T->R)(mergeBranches:R->R->R) (t:Tre
   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
@@ -213,6 +218,104 @@ Fixpoint mapProp {A:Type} (f:A->Prop) (l:list A) : Prop :=
     | (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.
@@ -520,6 +623,12 @@ Fixpoint takeT {T}{Σ:Tree T}(tf:TreeFlags Σ) : ??(Tree T) :=
       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 =>
@@ -792,6 +901,17 @@ Lemma ilist_chop' {T}{F}{l1 l2:list T}(v:IList T F (app l1 l2)) : IList T F l2.
   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
@@ -904,7 +1024,7 @@ Definition orErrorBindWithMessage {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrErr
 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)