The Coq Proof Assistant

# Library Coq.Lists.ListDec

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).
Lemma incl_decidable (l l':list A) : decidable (incl l l').
Lemma NoDup_decidable (l:list A) : decidable (NoDup l).
Lemma not_NoDup (l: list A):
~ NoDup l -> exists a l1 l2 l3, l = l1++a::l2++a::l3.
Lemma NoDup_list_decidable (l:list A) : NoDup l -> forall x y:A, In x l -> In y l -> decidable (x=y).
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.
Lemma incl_dec (l l':list A) : {incl l l'}+{~incl l l'}.
Lemma NoDup_dec (l:list A) : {NoDup l}+{~NoDup l}.
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').
Lemma uniquify A (d:decidable_eq A)(l:list A) :
exists l', NoDup l' /\ incl l l'.