From c78dd97a0ad6c37e6a5ac5fff666178bc3cb41e0 Mon Sep 17 00:00:00 2001 From: Sébastien Hinderer Date: Fri, 12 Dec 2014 18:01:41 +0100 Subject: Implement the nodup function on lists and prove associated results. --- theories/Lists/List.v | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) (limited to 'theories/Lists') 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. -- cgit v1.2.3