Library Coq.Lists.ListSet
A Library for finite sets, implemented as lists
List is loaded, but not exported. This allow to "hide" the definitions, functions and theorems of List and to see only the ones of ListSet
Require
Import
List
.
Set Implicit Arguments
.
Section
first_definitions
.
Variable
A
:
Type
.
Hypothesis
Aeq_dec
:
forall
x
y
:
A
,
{
x
=
y
}
+
{
x
<>
y
}
.
Definition
set
:=
list
A
.
Definition
empty_set
:
set
:=
nil
.
Fixpoint
set_add
(
a
:
A
) (
x
:
set
) :
set
:=
match
x
with
|
nil
=>
a
::
nil
|
a1
::
x1
=>
match
Aeq_dec
a
a1
with
|
left
_
=>
a1
::
x1
|
right
_
=>
a1
::
set_add
a
x1
end
end
.
Fixpoint
set_mem
(
a
:
A
) (
x
:
set
) :
bool
:=
match
x
with
|
nil
=>
false
|
a1
::
x1
=>
match
Aeq_dec
a
a1
with
|
left
_
=>
true
|
right
_
=>
set_mem
a
x1
end
end
.
If
a
belongs to
x
, removes
a
from
x
. If not, does nothing
Fixpoint
set_remove
(
a
:
A
) (
x
:
set
) :
set
:=
match
x
with
|
nil
=>
empty_set
|
a1
::
x1
=>
match
Aeq_dec
a
a1
with
|
left
_
=>
x1
|
right
_
=>
a1
::
set_remove
a
x1
end
end
.
Fixpoint
set_inter
(
x
:
set
) :
set
->
set
:=
match
x
with
|
nil
=>
fun
y
=>
nil
|
a1
::
x1
=>
fun
y
=>
if
set_mem
a1
y
then
a1
::
set_inter
x1
y
else
set_inter
x1
y
end
.
Fixpoint
set_union
(
x
y
:
set
) :
set
:=
match
y
with
|
nil
=>
x
|
a1
::
y1
=>
set_add
a1
(
set_union
x
y1
)
end
.
returns the set of all els of
x
that does not belong to
y
Fixpoint
set_diff
(
x
y
:
set
) :
set
:=
match
x
with
|
nil
=>
nil
|
a1
::
x1
=>
if
set_mem
a1
y
then
set_diff
x1
y
else
set_add
a1
(
set_diff
x1
y
)
end
.
Definition
set_In
:
A
->
set
->
Prop
:=
In
(
A
:=
A
).
Lemma
set_In_dec
:
forall
(
a
:
A
) (
x
:
set
),
{
set_In
a
x
}
+
{
~
set_In
a
x
}
.
Lemma
set_mem_ind
:
forall
(
B
:
Type
) (
P
:
B
->
Prop
) (
y
z
:
B
) (
a
:
A
) (
x
:
set
),
(
set_In
a
x
->
P
y
) ->
P
z
->
P
(
if
set_mem
a
x
then
y
else
z
).
Lemma
set_mem_ind2
:
forall
(
B
:
Type
) (
P
:
B
->
Prop
) (
y
z
:
B
) (
a
:
A
) (
x
:
set
),
(
set_In
a
x
->
P
y
) ->
(
~
set_In
a
x
->
P
z
) ->
P
(
if
set_mem
a
x
then
y
else
z
).
Lemma
set_mem_correct1
:
forall
(
a
:
A
) (
x
:
set
),
set_mem
a
x
=
true
->
set_In
a
x
.
Lemma
set_mem_correct2
:
forall
(
a
:
A
) (
x
:
set
),
set_In
a
x
->
set_mem
a
x
=
true
.
Lemma
set_mem_complete1
:
forall
(
a
:
A
) (
x
:
set
),
set_mem
a
x
=
false
->
~
set_In
a
x
.
Lemma
set_mem_complete2
:
forall
(
a
:
A
) (
x
:
set
),
~
set_In
a
x
->
set_mem
a
x
=
false
.
Lemma
set_add_intro1
:
forall
(
a
b
:
A
) (
x
:
set
),
set_In
a
x
->
set_In
a
(
set_add
b
x
).
Lemma
set_add_intro2
:
forall
(
a
b
:
A
) (
x
:
set
),
a
=
b
->
set_In
a
(
set_add
b
x
).
Hint Resolve
set_add_intro1
set_add_intro2
.
Lemma
set_add_intro
:
forall
(
a
b
:
A
) (
x
:
set
),
a
=
b
\/
set_In
a
x
->
set_In
a
(
set_add
b
x
).
Lemma
set_add_elim
:
forall
(
a
b
:
A
) (
x
:
set
),
set_In
a
(
set_add
b
x
) ->
a
=
b
\/
set_In
a
x
.
Lemma
set_add_elim2
:
forall
(
a
b
:
A
) (
x
:
set
),
set_In
a
(
set_add
b
x
) ->
a
<>
b
->
set_In
a
x
.
Hint Resolve
set_add_intro
set_add_elim
set_add_elim2
.
Lemma
set_add_not_empty
:
forall
(
a
:
A
) (
x
:
set
),
set_add
a
x
<>
empty_set
.
Lemma
set_union_intro1
:
forall
(
a
:
A
) (
x
y
:
set
),
set_In
a
x
->
set_In
a
(
set_union
x
y
).
Lemma
set_union_intro2
:
forall
(
a
:
A
) (
x
y
:
set
),
set_In
a
y
->
set_In
a
(
set_union
x
y
).
Hint Resolve
set_union_intro2
set_union_intro1
.
Lemma
set_union_intro
:
forall
(
a
:
A
) (
x
y
:
set
),
set_In
a
x
\/
set_In
a
y
->
set_In
a
(
set_union
x
y
).
Lemma
set_union_elim
:
forall
(
a
:
A
) (
x
y
:
set
),
set_In
a
(
set_union
x
y
) ->
set_In
a
x
\/
set_In
a
y
.
Lemma
set_union_emptyL
:
forall
(
a
:
A
) (
x
:
set
),
set_In
a
(
set_union
empty_set
x
) ->
set_In
a
x
.
Lemma
set_union_emptyR
:
forall
(
a
:
A
) (
x
:
set
),
set_In
a
(
set_union
x
empty_set
) ->
set_In
a
x
.
Lemma
set_inter_intro
:
forall
(
a
:
A
) (
x
y
:
set
),
set_In
a
x
->
set_In
a
y
->
set_In
a
(
set_inter
x
y
).
Lemma
set_inter_elim1
:
forall
(
a
:
A
) (
x
y
:
set
),
set_In
a
(
set_inter
x
y
) ->
set_In
a
x
.
Lemma
set_inter_elim2
:
forall
(
a
:
A
) (
x
y
:
set
),
set_In
a
(
set_inter
x
y
) ->
set_In
a
y
.
Hint Resolve
set_inter_elim1
set_inter_elim2
.
Lemma
set_inter_elim
:
forall
(
a
:
A
) (
x
y
:
set
),
set_In
a
(
set_inter
x
y
) ->
set_In
a
x
/\
set_In
a
y
.
Lemma
set_diff_intro
:
forall
(
a
:
A
) (
x
y
:
set
),
set_In
a
x
->
~
set_In
a
y
->
set_In
a
(
set_diff
x
y
).
Lemma
set_diff_elim1
:
forall
(
a
:
A
) (
x
y
:
set
),
set_In
a
(
set_diff
x
y
) ->
set_In
a
x
.
Lemma
set_diff_elim2
:
forall
(
a
:
A
) (
x
y
:
set
),
set_In
a
(
set_diff
x
y
) ->
~
set_In
a
y
.
Lemma
set_diff_trivial
:
forall
(
a
:
A
) (
x
:
set
),
~
set_In
a
(
set_diff
x
x
).
Hint Resolve
set_diff_intro
set_diff_trivial
.
End
first_definitions
.
Section
other_definitions
.
Definition
set_prod
:
forall
{
A
B
:
Type
},
set
A
->
set
B
->
set
(
A
*
B
) :=
list_prod
.
B
^
A
, set of applications from
A
to
B
Definition
set_power
:
forall
{
A
B
:
Type
},
set
A
->
set
B
->
set
(
set
(
A
*
B
)) :=
list_power
.
Definition
set_fold_left
{
A
B
:
Type
} : (
B
->
A
->
B
) ->
set
A
->
B
->
B
:=
fold_left
(
A
:=
B
) (
B
:=
A
).
Definition
set_fold_right
{
A
B
:
Type
} (
f
:
A
->
B
->
B
) (
x
:
set
A
)
(
b
:
B
) :
B
:=
fold_right
f
b
x
.
Definition
set_map
{
A
B
:
Type
} (
Aeq_dec
:
forall
x
y
:
B
,
{
x
=
y
}
+
{
x
<>
y
}
)
(
f
:
A
->
B
) (
x
:
set
A
) :
set
B
:=
set_fold_right
(
fun
a
=>
set_add
Aeq_dec
(
f
a
))
x
(
empty_set
B
).
End
other_definitions
.
Unset Implicit Arguments
.