Library Coq.Sets.Multiset
Require
Import
Permut
.
Section
multiset_defs
.
Variable
A
:
Type
.
Variable
eqA
:
A
->
A
->
Prop
.
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
).
Require
Plus
.
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
).
End
multiset_defs
.
Hint
Unfold
meq
multiplicity
:
v62
datatypes
.
Hint
Resolve
munion_empty_right
munion_comm
munion_ass
meq_left
meq_right
munion_empty_left
:
v62
datatypes
.
Hint
Immediate
meq_sym
:
v62
datatypes
.