Library Coq.Sets.Uniset
Sets as characteristic functions
Require
Import
Bool
.
Set Implicit Arguments
.
Section
defs
.
Variable
A
:
Set
.
Variable
eqA
:
A
->
A
->
Prop
.
Hypothesis
eqA_dec
:
forall
x
y
:
A
,
{
eqA
x
y
}
+
{
~
eqA
x
y
}
.
Inductive
uniset
:
Set
:=
Charac
: (
A
->
bool
) ->
uniset
.
Definition
charac
(
s
:
uniset
) (
a
:
A
) :
bool
:=
let
(
f
) :=
s
in
f
a
.
Definition
Emptyset
:=
Charac
(
fun
a
:
A
=>
false
).
Definition
Fullset
:=
Charac
(
fun
a
:
A
=>
true
).
Definition
Singleton
(
a
:
A
) :=
Charac
(
fun
a'
:
A
=>
match
eqA_dec
a
a'
with
|
left
h
=>
true
|
right
h
=>
false
end
).
Definition
In
(
s
:
uniset
) (
a
:
A
) :
Prop
:=
charac
s
a
=
true
.
Hint Unfold
In
.
uniset inclusion
Definition
incl
(
s1
s2
:
uniset
) :=
forall
a
:
A
,
leb
(
charac
s1
a
) (
charac
s2
a
).
Hint Unfold
incl
.
uniset equality
Definition
seq
(
s1
s2
:
uniset
) :=
forall
a
:
A
,
charac
s1
a
=
charac
s2
a
.
Hint Unfold
seq
.
Lemma
leb_refl
:
forall
b
:
bool
,
leb
b
b
.
Hint Resolve
leb_refl
.
Lemma
incl_left
:
forall
s1
s2
:
uniset
,
seq
s1
s2
->
incl
s1
s2
.
Lemma
incl_right
:
forall
s1
s2
:
uniset
,
seq
s1
s2
->
incl
s2
s1
.
Lemma
seq_refl
:
forall
x
:
uniset
,
seq
x
x
.
Hint Resolve
seq_refl
.
Lemma
seq_trans
:
forall
x
y
z
:
uniset
,
seq
x
y
->
seq
y
z
->
seq
x
z
.
Lemma
seq_sym
:
forall
x
y
:
uniset
,
seq
x
y
->
seq
y
x
.
uniset union
Definition
union
(
m1
m2
:
uniset
) :=
Charac
(
fun
a
:
A
=>
orb
(
charac
m1
a
) (
charac
m2
a
)).
Lemma
union_empty_left
:
forall
x
:
uniset
,
seq
x
(
union
Emptyset
x
).
Hint Resolve
union_empty_left
.
Lemma
union_empty_right
:
forall
x
:
uniset
,
seq
x
(
union
x
Emptyset
).
Hint Resolve
union_empty_right
.
Lemma
union_comm
:
forall
x
y
:
uniset
,
seq
(
union
x
y
) (
union
y
x
).
Hint Resolve
union_comm
.
Lemma
union_ass
:
forall
x
y
z
:
uniset
,
seq
(
union
(
union
x
y
)
z
) (
union
x
(
union
y
z
)).
Hint Resolve
union_ass
.
Lemma
seq_left
:
forall
x
y
z
:
uniset
,
seq
x
y
->
seq
(
union
x
z
) (
union
y
z
).
Hint Resolve
seq_left
.
Lemma
seq_right
:
forall
x
y
z
:
uniset
,
seq
x
y
->
seq
(
union
z
x
) (
union
z
y
).
Hint Resolve
seq_right
.
All the proofs that follow duplicate
Multiset_of_A
Here we should make uniset an abstract datatype, by hiding
Charac
,
union
,
charac
; all further properties are proved abstractly
Require
Import
Permut
.
Lemma
union_rotate
:
forall
x
y
z
:
uniset
,
seq
(
union
x
(
union
y
z
)) (
union
z
(
union
x
y
)).
Lemma
seq_congr
:
forall
x
y
z
t
:
uniset
,
seq
x
y
->
seq
z
t
->
seq
(
union
x
z
) (
union
y
t
).
Lemma
union_perm_left
:
forall
x
y
z
:
uniset
,
seq
(
union
x
(
union
y
z
)) (
union
y
(
union
x
z
)).
Lemma
uniset_twist1
:
forall
x
y
z
t
:
uniset
,
seq
(
union
x
(
union
(
union
y
z
)
t
)) (
union
(
union
y
(
union
x
t
))
z
).
Lemma
uniset_twist2
:
forall
x
y
z
t
:
uniset
,
seq
(
union
x
(
union
(
union
y
z
)
t
)) (
union
(
union
y
(
union
x
z
))
t
).
specific for treesort
Lemma
treesort_twist1
:
forall
x
y
z
t
u
:
uniset
,
seq
u
(
union
y
z
) ->
seq
(
union
x
(
union
u
t
)) (
union
(
union
y
(
union
x
t
))
z
).
Lemma
treesort_twist2
:
forall
x
y
z
t
u
:
uniset
,
seq
u
(
union
y
z
) ->
seq
(
union
x
(
union
u
t
)) (
union
(
union
y
(
union
x
z
))
t
).
End
defs
.
Unset Implicit Arguments
.