From 32436fdf380f7f2efc7a70896268509e7b3e0d6f Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 21 Mar 2011 15:14:15 -0700 Subject: [PATCH] add distinctT, InT to General --- src/General.v | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/src/General.v b/src/General.v index 2a1a398..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. -- 1.7.10.4