Library Coq.Sets.Multiset
Require
Import
Permut
Setoid
.
Require
Plus
.
Set Implicit Arguments
.
Section
multiset_defs
.
Variable
A
:
Type
.
Variable
eqA
:
A
->
A
->
Prop
.
Hypothesis
eqA_equiv
:
Equivalence
eqA
.
Hypothesis
Aeq_dec
:
forall
x
y
:
A
,
{
eqA
x
y
}
+
{
~
eqA
x
y
}
.
Inductive
multiset
:
Type
:=
Bag
:
(
A
->
nat
)
->
multiset
.
Definition
EmptyBag
:=
Bag
(
fun
a
:
A
=> 0).
Definition
SingletonBag
(
a
:
A
) :=
Bag
(
fun
a'
:
A
=>
match
Aeq_dec
a
a'
with
|
left
_
=> 1
|
right
_
=> 0
end
).
Definition
multiplicity
(
m
:
multiset
) (
a
:
A
) :
nat
:=
let
(
f
) :=
m
in
f
a
.
multiset equality
Definition
meq
(
m1
m2
:
multiset
) :=
forall
a
:
A
,
multiplicity
m1
a
=
multiplicity
m2
a
.
Lemma
meq_refl
:
forall
x
:
multiset
,
meq
x
x
.
Lemma
meq_trans
:
forall
x
y
z
:
multiset
,
meq
x
y
->
meq
y
z
->
meq
x
z
.
Lemma
meq_sym
:
forall
x
y
:
multiset
,
meq
x
y
->
meq
y
x
.
multiset union
Definition
munion
(
m1
m2
:
multiset
) :=
Bag
(
fun
a
:
A
=>
multiplicity
m1
a
+
multiplicity
m2
a
).
Lemma
munion_empty_left
:
forall
x
:
multiset
,
meq
x
(
munion
EmptyBag
x
).
Lemma
munion_empty_right
:
forall
x
:
multiset
,
meq
x
(
munion
x
EmptyBag
).
Lemma
munion_comm
:
forall
x
y
:
multiset
,
meq
(
munion
x
y
) (
munion
y
x
).
Lemma
munion_ass
:
forall
x
y
z
:
multiset
,
meq
(
munion
(
munion
x
y
)
z
) (
munion
x
(
munion
y
z
)).
Lemma
meq_left
:
forall
x
y
z
:
multiset
,
meq
x
y
->
meq
(
munion
x
z
) (
munion
y
z
).
Lemma
meq_right
:
forall
x
y
z
:
multiset
,
meq
x
y
->
meq
(
munion
z
x
) (
munion
z
y
).
Here we should make multiset an abstract datatype, by hiding
Bag
,
munion
,
multiplicity
; all further properties are proved abstractly
Lemma
munion_rotate
:
forall
x
y
z
:
multiset
,
meq
(
munion
x
(
munion
y
z
)) (
munion
z
(
munion
x
y
)).
Lemma
meq_congr
:
forall
x
y
z
t
:
multiset
,
meq
x
y
->
meq
z
t
->
meq
(
munion
x
z
) (
munion
y
t
).
Lemma
munion_perm_left
:
forall
x
y
z
:
multiset
,
meq
(
munion
x
(
munion
y
z
)) (
munion
y
(
munion
x
z
)).
Lemma
multiset_twist1
:
forall
x
y
z
t
:
multiset
,
meq
(
munion
x
(
munion
(
munion
y
z
)
t
)) (
munion
(
munion
y
(
munion
x
t
))
z
).
Lemma
multiset_twist2
:
forall
x
y
z
t
:
multiset
,
meq
(
munion
x
(
munion
(
munion
y
z
)
t
)) (
munion
(
munion
y
(
munion
x
z
))
t
).
specific for treesort
Lemma
treesort_twist1
:
forall
x
y
z
t
u
:
multiset
,
meq
u
(
munion
y
z
)
->
meq
(
munion
x
(
munion
u
t
)) (
munion
(
munion
y
(
munion
x
t
))
z
).
Lemma
treesort_twist2
:
forall
x
y
z
t
u
:
multiset
,
meq
u
(
munion
y
z
)
->
meq
(
munion
x
(
munion
u
t
)) (
munion
(
munion
y
(
munion
x
z
))
t
).
SingletonBag
Lemma
meq_singleton
:
forall
a
a'
,
eqA
a
a'
->
meq
(
SingletonBag
a
) (
SingletonBag
a'
).
End
multiset_defs
.
Unset Implicit Arguments
.
Hint Unfold
meq
multiplicity
:
datatypes
.
Hint Resolve
munion_empty_right
munion_comm
munion_ass
meq_left
meq_right
munion_empty_left
:
datatypes
.
Hint Immediate
meq_sym
:
datatypes
.