From: Adam Megacz <megacz@cs.berkeley.edu>
Date: Sun, 20 Mar 2011 06:05:18 +0000 (-0700)
Subject: add distinct_decidable, in_decidable to General.v
X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=2f9327bdfddb3908dc279c02db25ad527b37e17a;hp=17ed8145b371ce578db7fdd67aced8dd2013e623

add distinct_decidable, in_decidable to General.v
---

diff --git a/src/General.v b/src/General.v
index 2d8a35c..b0266f4 100644
--- a/src/General.v
+++ b/src/General.v
@@ -322,6 +322,50 @@ 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).
 
+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.
+  right.
+  unfold not.
+  intros.
+  inversion H.
+  destruct IHlv.
+  left.
+  simpl.
+  auto.
+  set (eqd_dec v a) as dec.
+  destruct dec.
+  subst.
+  left; simpl; auto.
+  right.
+  unfold not; intros.
+  destruct H.
+  subst.
+  apply n0; auto.
+  apply n.
+  apply H.
+  Defined.
+
+Lemma distinct_decidable {VV:Type}{eqdVV:EqDecidable VV} : forall (lv:list VV), sumbool (distinct lv) (not (distinct lv)).
+  intros.
+  induction lv.
+  left; apply distinct_nil.
+  destruct IHlv.
+  set (in_decidable a lv) as dec.
+  destruct dec.
+  right; unfold not; intros.
+  inversion H.
+  subst.
+  apply H2; auto.
+  left.
+  apply distinct_cons; auto.
+  right.
+  unfold not; intros.
+  inversion H.
+  subst.
+  apply n; auto.
+  Defined.
+
 Lemma map_preserves_length {A}{B}(f:A->B)(l:list A) : (length l) = (length (map f l)).
   induction l; auto.
   simpl.