Implement the nodup function on lists and prove associated results.

1 files changed, 34 insertions, 0 deletions

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 74d453b15..da851aae0 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -1777,8 +1777,42 @@ Section ReDun.
     + now constructor.
   Qed.
 
+  (** Effective computation of a list without duplicates *)
+
   Hypothesis decA: forall x y : A, {x = y} + {x <> y}.
 
+  Fixpoint nodup (l : list A) : list A :=
+    match l with
+      | [] => []
+      | x::xs => if in_dec decA x xs then nodup xs else x::(nodup xs)
+    end.
+
+  Lemma nodup_In l x : In x (nodup l) <-> In x l.
+  Proof.
+    induction l as [|a l' Hrec]; simpl.
+    - reflexivity.
+    - destruct (in_dec decA a l'); simpl; rewrite Hrec.
+      * intuition; now subst.
+      * reflexivity.
+  Qed.
+
+  Lemma NoDup_nodup l: NoDup (nodup l).
+  Proof.
+    induction l as [|a l' Hrec]; simpl.
+    - constructor.
+    - destruct (in_dec decA a l'); simpl.
+      * assumption.
+      * constructor; [ now rewrite nodup_In | assumption].
+  Qed.
+
+  Lemma nodup_inv k l a : nodup k = a :: l -> ~ In a l.
+  Proof.
+    intros H.
+    assert (H' : NoDup (a::l)).
+    { rewrite <- H. apply NoDup_nodup. }
+    now inversion_clear H'.
+  Qed.
+
   Theorem NoDup_count_occ l:
     NoDup l <-> (forall x:A, count_occ decA l x <= 1).
   Proof.