Library Coq.FSets.FSetBridge
Finite sets library
This module implements bridges (as functors) from dependent to/from non-dependent set signature.
Require
Export
FSetInterface
.
Set Implicit Arguments
.
From non-dependent signature
S
to dependent signature
Sdep
.
Module
DepOfNodep
(
Import
M
:
S
) <:
Sdep
with
Module
E
:=
M.E
.
Definition
empty
:
{
s
:
t
|
Empty
s
}
.
Definition
is_empty
:
forall
s
:
t
,
{
Empty
s
}
+
{
~
Empty
s
}
.
Definition
mem
:
forall
(
x
:
elt
) (
s
:
t
),
{
In
x
s
}
+
{
~
In
x
s
}
.
Definition
Add
(
x
:
elt
) (
s
s´
:
t
) :=
forall
y
:
elt
,
In
y
s´
<->
E.eq
x
y
\/
In
y
s
.
Definition
add
:
forall
(
x
:
elt
) (
s
:
t
),
{
s´
:
t
|
Add
x
s
s´
}
.
Definition
singleton
:
forall
x
:
elt
,
{
s
:
t
|
forall
y
:
elt
,
In
y
s
<->
E.eq
x
y
}
.
Definition
remove
:
forall
(
x
:
elt
) (
s
:
t
),
{
s´
:
t
|
forall
y
:
elt
,
In
y
s´
<->
~
E.eq
x
y
/\
In
y
s
}
.
Definition
union
:
forall
s
s´
:
t
,
{
s´´
:
t
|
forall
x
:
elt
,
In
x
s´´
<->
In
x
s
\/
In
x
s´
}
.
Definition
inter
:
forall
s
s´
:
t
,
{
s´´
:
t
|
forall
x
:
elt
,
In
x
s´´
<->
In
x
s
/\
In
x
s´
}
.
Definition
diff
:
forall
s
s´
:
t
,
{
s´´
:
t
|
forall
x
:
elt
,
In
x
s´´
<->
In
x
s
/\
~
In
x
s´
}
.
Definition
equal
:
forall
s
s´
:
t
,
{
Equal
s
s´
}
+
{
~
Equal
s
s´
}
.
Definition
subset
:
forall
s
s´
:
t
,
{
Subset
s
s´
}
+
{
~
Subset
s
s´
}
.
Definition
elements
:
forall
s
:
t
,
{
l
:
list
elt
|
sort
E.lt
l
/\
(
forall
x
:
elt
,
In
x
s
<->
InA
E.eq
x
l
)
}
.
Definition
fold
:
forall
(
A
:
Type
) (
f
:
elt
->
A
->
A
) (
s
:
t
) (
i
:
A
),
{
r
:
A
|
let
(
l
,
_
) :=
elements
s
in
r
=
fold_left
(
fun
a
e
=>
f
e
a
)
l
i
}
.
Definition
cardinal
:
forall
s
:
t
,
{
r
:
nat
|
let
(
l
,
_
) :=
elements
s
in
r
=
length
l
}
.
Definition
fdec
(
P
:
elt
->
Prop
) (
Pdec
:
forall
x
:
elt
,
{
P
x
}
+
{
~
P
x
}
)
(
x
:
elt
) :=
if
Pdec
x
then
true
else
false
.
Lemma
compat_P_aux
:
forall
(
P
:
elt
->
Prop
) (
Pdec
:
forall
x
:
elt
,
{
P
x
}
+
{
~
P
x
}
),
compat_P
E.eq
P
->
compat_bool
E.eq
(
fdec
Pdec
).
Hint Resolve
compat_P_aux
.
Definition
filter
:
forall
(
P
:
elt
->
Prop
) (
Pdec
:
forall
x
:
elt
,
{
P
x
}
+
{
~
P
x
}
) (
s
:
t
),
{
s´
:
t
|
compat_P
E.eq
P
->
forall
x
:
elt
,
In
x
s´
<->
In
x
s
/\
P
x
}
.
Definition
for_all
:
forall
(
P
:
elt
->
Prop
) (
Pdec
:
forall
x
:
elt
,
{
P
x
}
+
{
~
P
x
}
) (
s
:
t
),
{
compat_P
E.eq
P
->
For_all
P
s
}
+
{
compat_P
E.eq
P
->
~
For_all
P
s
}
.
Definition
exists_
:
forall
(
P
:
elt
->
Prop
) (
Pdec
:
forall
x
:
elt
,
{
P
x
}
+
{
~
P
x
}
) (
s
:
t
),
{
compat_P
E.eq
P
->
Exists
P
s
}
+
{
compat_P
E.eq
P
->
~
Exists
P
s
}
.
Definition
partition
:
forall
(
P
:
elt
->
Prop
) (
Pdec
:
forall
x
:
elt
,
{
P
x
}
+
{
~
P
x
}
) (
s
:
t
),
{
partition
:
t
*
t
|
let
(
s1
,
s2
) :=
partition
in
compat_P
E.eq
P
->
For_all
P
s1
/\
For_all
(
fun
x
=>
~
P
x
)
s2
/\
(
forall
x
:
elt
,
In
x
s
<->
In
x
s1
\/
In
x
s2
)
}
.
Definition
choose_aux
:
forall
s
:
t
,
{
x
:
elt
|
M.choose
s
=
Some
x
}
+
{
M.choose
s
=
None
}
.
Definition
choose
:
forall
s
:
t
,
{
x
:
elt
|
In
x
s
}
+
{
Empty
s
}
.
Lemma
choose_ok1
:
forall
s
x
,
M.choose
s
=
Some
x
<->
exists
H
:
In
x
s
,
choose
s
=
inleft
_
(
exist
(
fun
x
=>
In
x
s
)
x
H
).
Lemma
choose_ok2
:
forall
s
,
M.choose
s
=
None
<->
exists
H
:
Empty
s
,
choose
s
=
inright
_
H
.
Lemma
choose_equal
:
forall
s
s´
,
Equal
s
s´
->
match
choose
s
,
choose
s´
with
|
inleft
(
exist
x
_
),
inleft
(
exist
x´
_
) =>
E.eq
x
x´
|
inright
_
,
inright
_
=>
True
|
_
,
_
=>
False
end
.
Definition
min_elt
:
forall
s
:
t
,
{
x
:
elt
|
In
x
s
/\
For_all
(
fun
y
=>
~
E.lt
y
x
)
s
}
+
{
Empty
s
}
.
Definition
max_elt
:
forall
s
:
t
,
{
x
:
elt
|
In
x
s
/\
For_all
(
fun
y
=>
~
E.lt
x
y
)
s
}
+
{
Empty
s
}
.
Definition
elt
:=
elt
.
Definition
t
:=
t
.
Definition
In
:=
In
.
Definition
Equal
s
s´
:=
forall
a
:
elt
,
In
a
s
<->
In
a
s´
.
Definition
Subset
s
s´
:=
forall
a
:
elt
,
In
a
s
->
In
a
s´
.
Definition
Empty
s
:=
forall
a
:
elt
,
~
In
a
s
.
Definition
For_all
(
P
:
elt
->
Prop
) (
s
:
t
) :=
forall
x
:
elt
,
In
x
s
->
P
x
.
Definition
Exists
(
P
:
elt
->
Prop
) (
s
:
t
) :=
exists
x
:
elt
,
In
x
s
/\
P
x
.
Definition
eq_In
:=
In_1
.
Definition
eq
:=
Equal
.
Definition
lt
:=
lt
.
Definition
eq_refl
:=
eq_refl
.
Definition
eq_sym
:=
eq_sym
.
Definition
eq_trans
:=
eq_trans
.
Definition
lt_trans
:=
lt_trans
.
Definition
lt_not_eq
:=
lt_not_eq
.
Definition
compare
:=
compare
.
Module
E
:=
E
.
End
DepOfNodep
.
From dependent signature
Sdep
to non-dependent signature
S
.
Module
NodepOfDep
(
M
:
Sdep
) <:
S
with
Module
E
:=
M.E
.
Import
M
.
Module
ME
:=
OrderedTypeFacts
E
.
Definition
empty
:
t
:=
let
(
s
,
_
) :=
empty
in
s
.
Lemma
empty_1
:
Empty
empty
.
Definition
is_empty
(
s
:
t
) :
bool
:=
if
is_empty
s
then
true
else
false
.
Lemma
is_empty_1
:
forall
s
:
t
,
Empty
s
->
is_empty
s
=
true
.
Lemma
is_empty_2
:
forall
s
:
t
,
is_empty
s
=
true
->
Empty
s
.
Definition
mem
(
x
:
elt
) (
s
:
t
) :
bool
:=
if
mem
x
s
then
true
else
false
.
Lemma
mem_1
:
forall
(
s
:
t
) (
x
:
elt
),
In
x
s
->
mem
x
s
=
true
.
Lemma
mem_2
:
forall
(
s
:
t
) (
x
:
elt
),
mem
x
s
=
true
->
In
x
s
.
Definition
eq_dec
:=
equal
.
Definition
equal
(
s
s´
:
t
) :
bool
:=
if
equal
s
s´
then
true
else
false
.
Lemma
equal_1
:
forall
s
s´
:
t
,
Equal
s
s´
->
equal
s
s´
=
true
.
Lemma
equal_2
:
forall
s
s´
:
t
,
equal
s
s´
=
true
->
Equal
s
s´
.
Definition
subset
(
s
s´
:
t
) :
bool
:=
if
subset
s
s´
then
true
else
false
.
Lemma
subset_1
:
forall
s
s´
:
t
,
Subset
s
s´
->
subset
s
s´
=
true
.
Lemma
subset_2
:
forall
s
s´
:
t
,
subset
s
s´
=
true
->
Subset
s
s´
.
Definition
choose
(
s
:
t
) :
option
elt
:=
match
choose
s
with
|
inleft
(
exist
x
_
) =>
Some
x
|
inright
_
=>
None
end
.
Lemma
choose_1
:
forall
(
s
:
t
) (
x
:
elt
),
choose
s
=
Some
x
->
In
x
s
.
Lemma
choose_2
:
forall
s
:
t
,
choose
s
=
None
->
Empty
s
.
Lemma
choose_3
:
forall
s
s´
x
x´
,
choose
s
=
Some
x
->
choose
s´
=
Some
x´
->
Equal
s
s´
->
E.eq
x
x´
.
Definition
elements
(
s
:
t
) :
list
elt
:=
let
(
l
,
_
) :=
elements
s
in
l
.
Lemma
elements_1
:
forall
(
s
:
t
) (
x
:
elt
),
In
x
s
->
InA
E.eq
x
(
elements
s
).
Lemma
elements_2
:
forall
(
s
:
t
) (
x
:
elt
),
InA
E.eq
x
(
elements
s
) ->
In
x
s
.
Lemma
elements_3
:
forall
s
:
t
,
sort
E.lt
(
elements
s
).
Hint Resolve
elements_3
.
Lemma
elements_3w
:
forall
s
:
t
,
NoDupA
E.eq
(
elements
s
).
Definition
min_elt
(
s
:
t
) :
option
elt
:=
match
min_elt
s
with
|
inleft
(
exist
x
_
) =>
Some
x
|
inright
_
=>
None
end
.
Lemma
min_elt_1
:
forall
(
s
:
t
) (
x
:
elt
),
min_elt
s
=
Some
x
->
In
x
s
.
Lemma
min_elt_2
:
forall
(
s
:
t
) (
x
y
:
elt
),
min_elt
s
=
Some
x
->
In
y
s
->
~
E.lt
y
x
.
Lemma
min_elt_3
:
forall
s
:
t
,
min_elt
s
=
None
->
Empty
s
.
Definition
max_elt
(
s
:
t
) :
option
elt
:=
match
max_elt
s
with
|
inleft
(
exist
x
_
) =>
Some
x
|
inright
_
=>
None
end
.
Lemma
max_elt_1
:
forall
(
s
:
t
) (
x
:
elt
),
max_elt
s
=
Some
x
->
In
x
s
.
Lemma
max_elt_2
:
forall
(
s
:
t
) (
x
y
:
elt
),
max_elt
s
=
Some
x
->
In
y
s
->
~
E.lt
x
y
.
Lemma
max_elt_3
:
forall
s
:
t
,
max_elt
s
=
None
->
Empty
s
.
Definition
add
(
x
:
elt
) (
s
:
t
) :
t
:=
let
(
s´
,
_
) :=
add
x
s
in
s´
.
Lemma
add_1
:
forall
(
s
:
t
) (
x
y
:
elt
),
E.eq
x
y
->
In
y
(
add
x
s
).
Lemma
add_2
:
forall
(
s
:
t
) (
x
y
:
elt
),
In
y
s
->
In
y
(
add
x
s
).
Lemma
add_3
:
forall
(
s
:
t
) (
x
y
:
elt
),
~
E.eq
x
y
->
In
y
(
add
x
s
) ->
In
y
s
.
Definition
remove
(
x
:
elt
) (
s
:
t
) :
t
:=
let
(
s´
,
_
) :=
remove
x
s
in
s´
.
Lemma
remove_1
:
forall
(
s
:
t
) (
x
y
:
elt
),
E.eq
x
y
->
~
In
y
(
remove
x
s
).
Lemma
remove_2
:
forall
(
s
:
t
) (
x
y
:
elt
),
~
E.eq
x
y
->
In
y
s
->
In
y
(
remove
x
s
).
Lemma
remove_3
:
forall
(
s
:
t
) (
x
y
:
elt
),
In
y
(
remove
x
s
) ->
In
y
s
.
Definition
singleton
(
x
:
elt
) :
t
:=
let
(
s
,
_
) :=
singleton
x
in
s
.
Lemma
singleton_1
:
forall
x
y
:
elt
,
In
y
(
singleton
x
) ->
E.eq
x
y
.
Lemma
singleton_2
:
forall
x
y
:
elt
,
E.eq
x
y
->
In
y
(
singleton
x
).
Definition
union
(
s
s´
:
t
) :
t
:=
let
(
s´´
,
_
) :=
union
s
s´
in
s´´
.
Lemma
union_1
:
forall
(
s
s´
:
t
) (
x
:
elt
),
In
x
(
union
s
s´
) ->
In
x
s
\/
In
x
s´
.
Lemma
union_2
:
forall
(
s
s´
:
t
) (
x
:
elt
),
In
x
s
->
In
x
(
union
s
s´
).
Lemma
union_3
:
forall
(
s
s´
:
t
) (
x
:
elt
),
In
x
s´
->
In
x
(
union
s
s´
).
Definition
inter
(
s
s´
:
t
) :
t
:=
let
(
s´´
,
_
) :=
inter
s
s´
in
s´´
.
Lemma
inter_1
:
forall
(
s
s´
:
t
) (
x
:
elt
),
In
x
(
inter
s
s´
) ->
In
x
s
.
Lemma
inter_2
:
forall
(
s
s´
:
t
) (
x
:
elt
),
In
x
(
inter
s
s´
) ->
In
x
s´
.
Lemma
inter_3
:
forall
(
s
s´
:
t
) (
x
:
elt
),
In
x
s
->
In
x
s´
->
In
x
(
inter
s
s´
).
Definition
diff
(
s
s´
:
t
) :
t
:=
let
(
s´´
,
_
) :=
diff
s
s´
in
s´´
.
Lemma
diff_1
:
forall
(
s
s´
:
t
) (
x
:
elt
),
In
x
(
diff
s
s´
) ->
In
x
s
.
Lemma
diff_2
:
forall
(
s
s´
:
t
) (
x
:
elt
),
In
x
(
diff
s
s´
) ->
~
In
x
s´
.
Lemma
diff_3
:
forall
(
s
s´
:
t
) (
x
:
elt
),
In
x
s
->
~
In
x
s´
->
In
x
(
diff
s
s´
).
Definition
cardinal
(
s
:
t
) :
nat
:=
let
(
f
,
_
) :=
cardinal
s
in
f
.
Lemma
cardinal_1
:
forall
s
,
cardinal
s
=
length
(
elements
s
).
Definition
fold
(
B
:
Type
) (
f
:
elt
->
B
->
B
) (
i
:
t
)
(
s
:
B
) :
B
:=
let
(
fold
,
_
) :=
fold
f
i
s
in
fold
.
Lemma
fold_1
:
forall
(
s
:
t
) (
A
:
Type
) (
i
:
A
) (
f
:
elt
->
A
->
A
),
fold
f
s
i
=
fold_left
(
fun
a
e
=>
f
e
a
) (
elements
s
)
i
.
Definition
f_dec
:
forall
(
f
:
elt
->
bool
) (
x
:
elt
),
{
f
x
=
true
}
+
{
f
x
<>
true
}
.
Lemma
compat_P_aux
:
forall
f
:
elt
->
bool
,
compat_bool
E.eq
f
->
compat_P
E.eq
(
fun
x
=>
f
x
=
true
).
Hint Resolve
compat_P_aux
.
Definition
filter
(
f
:
elt
->
bool
) (
s
:
t
) :
t
:=
let
(
s´
,
_
) :=
filter
(
P
:=
fun
x
=>
f
x
=
true
) (
f_dec
f
)
s
in
s´
.
Lemma
filter_1
:
forall
(
s
:
t
) (
x
:
elt
) (
f
:
elt
->
bool
),
compat_bool
E.eq
f
->
In
x
(
filter
f
s
) ->
In
x
s
.
Lemma
filter_2
:
forall
(
s
:
t
) (
x
:
elt
) (
f
:
elt
->
bool
),
compat_bool
E.eq
f
->
In
x
(
filter
f
s
) ->
f
x
=
true
.
Lemma
filter_3
:
forall
(
s
:
t
) (
x
:
elt
) (
f
:
elt
->
bool
),
compat_bool
E.eq
f
->
In
x
s
->
f
x
=
true
->
In
x
(
filter
f
s
).
Definition
for_all
(
f
:
elt
->
bool
) (
s
:
t
) :
bool
:=
if
for_all
(
P
:=
fun
x
=>
f
x
=
true
) (
f_dec
f
)
s
then
true
else
false
.
Lemma
for_all_1
:
forall
(
s
:
t
) (
f
:
elt
->
bool
),
compat_bool
E.eq
f
->
For_all
(
fun
x
=>
f
x
=
true
)
s
->
for_all
f
s
=
true
.
Lemma
for_all_2
:
forall
(
s
:
t
) (
f
:
elt
->
bool
),
compat_bool
E.eq
f
->
for_all
f
s
=
true
->
For_all
(
fun
x
=>
f
x
=
true
)
s
.
Definition
exists_
(
f
:
elt
->
bool
) (
s
:
t
) :
bool
:=
if
exists_
(
P
:=
fun
x
=>
f
x
=
true
) (
f_dec
f
)
s
then
true
else
false
.
Lemma
exists_1
:
forall
(
s
:
t
) (
f
:
elt
->
bool
),
compat_bool
E.eq
f
->
Exists
(
fun
x
=>
f
x
=
true
)
s
->
exists_
f
s
=
true
.
Lemma
exists_2
:
forall
(
s
:
t
) (
f
:
elt
->
bool
),
compat_bool
E.eq
f
->
exists_
f
s
=
true
->
Exists
(
fun
x
=>
f
x
=
true
)
s
.
Definition
partition
(
f
:
elt
->
bool
) (
s
:
t
) :
t
*
t
:=
let
(
p
,
_
) :=
partition
(
P
:=
fun
x
=>
f
x
=
true
) (
f_dec
f
)
s
in
p
.
Lemma
partition_1
:
forall
(
s
:
t
) (
f
:
elt
->
bool
),
compat_bool
E.eq
f
->
Equal
(
fst
(
partition
f
s
)) (
filter
f
s
).
Lemma
partition_2
:
forall
(
s
:
t
) (
f
:
elt
->
bool
),
compat_bool
E.eq
f
->
Equal
(
snd
(
partition
f
s
)) (
filter
(
fun
x
=>
negb
(
f
x
))
s
).
Definition
elt
:=
elt
.
Definition
t
:=
t
.
Definition
In
:=
In
.
Definition
Equal
s
s´
:=
forall
a
:
elt
,
In
a
s
<->
In
a
s´
.
Definition
Subset
s
s´
:=
forall
a
:
elt
,
In
a
s
->
In
a
s´
.
Definition
Add
(
x
:
elt
) (
s
s´
:
t
) :=
forall
y
:
elt
,
In
y
s´
<->
E.eq
y
x
\/
In
y
s
.
Definition
Empty
s
:=
forall
a
:
elt
,
~
In
a
s
.
Definition
For_all
(
P
:
elt
->
Prop
) (
s
:
t
) :=
forall
x
:
elt
,
In
x
s
->
P
x
.
Definition
Exists
(
P
:
elt
->
Prop
) (
s
:
t
) :=
exists
x
:
elt
,
In
x
s
/\
P
x
.
Definition
In_1
:=
eq_In
.
Definition
eq
:=
Equal
.
Definition
lt
:=
lt
.
Definition
eq_refl
:=
eq_refl
.
Definition
eq_sym
:=
eq_sym
.
Definition
eq_trans
:=
eq_trans
.
Definition
lt_trans
:=
lt_trans
.
Definition
lt_not_eq
:=
lt_not_eq
.
Definition
compare
:=
compare
.
Module
E
:=
E
.
End
NodepOfDep
.