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
).
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'
.