X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FGeneral.v;h=96ac1baf758f6721787292c58d588c4e66f8a3c9;hb=32436fdf380f7f2efc7a70896268509e7b3e0d6f;hp=055a39a4086c39cf57fe32123559a84fc77f1f68;hpb=96ea5272fe6ec62022351f69289eedd330322eb4;p=coq-hetmet.git

diff --git a/src/General.v b/src/General.v
index 055a39a..96ac1ba 100644
--- a/src/General.v
+++ b/src/General.v
@@ -41,6 +41,13 @@ Notation "[ q ]"    := (@T_Leaf (option _) (Some q))            : tree_scope.
 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 :=
@@ -341,6 +348,11 @@ Inductive distinct {T:Type} : list T -> Prop :=
 | 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.
@@ -385,6 +397,10 @@ Lemma distinct_decidable {VV:Type}{eqdVV:EqDecidable VV} : forall (lv:list VV),
   apply n; auto.
   Defined.
 
+Lemma distinctT_decidable {VV:Type}{eqdVV:EqDecidable VV} : forall (lv:Tree ??VV), sumbool (distinctT lv) (not (distinctT lv)).
+  admit.
+  Defined.
+
 Lemma map_preserves_length {A}{B}(f:A->B)(l:list A) : (length l) = (length (map f l)).
   induction l; auto.
   simpl.
@@ -876,17 +892,24 @@ Ltac eqd_dec_refl X :=
   destruct (eqd_dec X X) as [eqd_dec1 | eqd_dec2];
     [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ].
 
-Lemma vec2list_injective : forall T n (v1 v2:vec T n), vec2list v1 = vec2list v2 -> v1 = v2.
-  admit.
-  Defined.
-
 Lemma unleaves_injective : forall T (t1 t2:list T), unleaves t1 = unleaves t2 -> t1 = t2.
-  admit.
+  intros T.
+  induction t1; intros.
+  destruct t2.
+  auto.
+  inversion H.
+  destruct t2.
+  inversion H.
+  simpl in H.
+  inversion H.
+  set (IHt1 _ H2) as q.
+  rewrite q.
+  reflexivity.
   Qed.
 
 Lemma fst_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@fst _ _) (vec_zip v1 v2) = v1.
   admit.
-  Qed.
+  Defined.
 
 Lemma snd_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@snd _ _) (vec_zip v1 v2) = v2.
   admit.