diff options
Diffstat (limited to 'theories/Lists/ListDec.v')
-rw-r--r-- | theories/Lists/ListDec.v | 103 |
1 files changed, 103 insertions, 0 deletions
diff --git a/theories/Lists/ListDec.v b/theories/Lists/ListDec.v new file mode 100644 index 00000000..8bd2daaf --- /dev/null +++ b/theories/Lists/ListDec.v @@ -0,0 +1,103 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Decidability results about lists *) + +Require Import List Decidable. +Set Implicit Arguments. + +Definition decidable_eq A := forall x y:A, decidable (x=y). + +Section Dec_in_Prop. +Variables (A:Type)(dec:decidable_eq A). + +Lemma In_decidable x (l:list A) : decidable (In x l). +Proof using A dec. + induction l as [|a l IH]. + - now right. + - destruct (dec a x). + + left. now left. + + destruct IH; simpl; [left|right]; tauto. +Qed. + +Lemma incl_decidable (l l':list A) : decidable (incl l l'). +Proof using A dec. + induction l as [|a l IH]. + - left. inversion 1. + - destruct (In_decidable a l') as [IN|IN]. + + destruct IH as [IC|IC]. + * left. destruct 1; subst; auto. + * right. contradict IC. intros x H. apply IC; now right. + + right. contradict IN. apply IN; now left. +Qed. + +Lemma NoDup_decidable (l:list A) : decidable (NoDup l). +Proof using A dec. + induction l as [|a l IH]. + - left; now constructor. + - destruct (In_decidable a l). + + right. inversion_clear 1. tauto. + + destruct IH. + * left. now constructor. + * right. inversion_clear 1. tauto. +Qed. + +End Dec_in_Prop. + +Section Dec_in_Type. +Variables (A:Type)(dec : forall x y:A, {x=y}+{x<>y}). + +Definition In_dec := List.In_dec dec. (* Already in List.v *) + +Lemma incl_dec (l l':list A) : {incl l l'}+{~incl l l'}. +Proof using A dec. + induction l as [|a l IH]. + - left. inversion 1. + - destruct (In_dec a l') as [IN|IN]. + + destruct IH as [IC|IC]. + * left. destruct 1; subst; auto. + * right. contradict IC. intros x H. apply IC; now right. + + right. contradict IN. apply IN; now left. +Qed. + +Lemma NoDup_dec (l:list A) : {NoDup l}+{~NoDup l}. +Proof using A dec. + induction l as [|a l IH]. + - left; now constructor. + - destruct (In_dec a l). + + right. inversion_clear 1. tauto. + + destruct IH. + * left. now constructor. + * right. inversion_clear 1. tauto. +Qed. + +End Dec_in_Type. + +(** An extra result: thanks to decidability, a list can be purged + from redundancies. *) + +Lemma uniquify_map A B (d:decidable_eq B)(f:A->B)(l:list A) : + exists l', NoDup (map f l') /\ incl (map f l) (map f l'). +Proof. + induction l. + - exists nil. simpl. split; [now constructor | red; trivial]. + - destruct IHl as (l' & N & I). + destruct (In_decidable d (f a) (map f l')). + + exists l'; simpl; split; trivial. + intros x [Hx|Hx]. now subst. now apply I. + + exists (a::l'); simpl; split. + * now constructor. + * intros x [Hx|Hx]. subst; now left. right; now apply I. +Qed. + +Lemma uniquify A (d:decidable_eq A)(l:list A) : + exists l', NoDup l' /\ incl l l'. +Proof. + destruct (uniquify_map d id l) as (l',H). + exists l'. now rewrite !map_id in H. +Qed. |