X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FGeneral.v;h=ee5cb1690a13480f641daa7d808a7f20fd2925db;hp=6cb18becc1f882df7b938e6e015c6a2ee2083e79;hb=423b0bd3972c5bcbbd757cb715e13b5b9104a9a6;hpb=97552c1a6dfb32098d4491951929ab1d4aca96a0

diff --git a/src/General.v b/src/General.v
index 6cb18be..ee5cb16 100644
--- a/src/General.v
+++ b/src/General.v
@@ -20,6 +20,24 @@ Class EqDecidable (T:Type) :=
 }.
 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 }.
@@ -88,6 +106,18 @@ 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
+    | 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),
@@ -444,6 +474,112 @@ Instance EqDecidableList {T:Type}(eqd:EqDecidable T) : EqDecidable (list T).
   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                                                        *)
 
@@ -739,6 +875,10 @@ Lemma extensionality_composes : forall t1 t2 t3 (f f':t1->t2) (g g':t2->t3),
 
 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.
@@ -826,6 +966,16 @@ Lemma list2vecOrFail {T}(l:list T)(n:nat)(error_message:nat->nat->string) : ???(
     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".
@@ -906,14 +1056,64 @@ Lemma unleaves_injective : forall T (t1 t2:list T), unleaves t1 = unleaves t2 ->
   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.
-  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.
 
 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