Multisets #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. These are implemented as the quotient of a list by permutations.
Notation #
We define the global infix notation ::ₘ
for multiset.cons
.
multiset α
is the quotient of list α
by list permutation. The result
is a type of finite sets with duplicates allowed.
Equations
- multiset α = quotient (list.is_setoid α)
Instances for multiset
- multiset.has_coe
- multiset.has_sizeof
- multiset.has_zero
- multiset.has_emptyc
- multiset.inhabited_multiset
- multiset.has_insert
- multiset.has_mem
- multiset.has_singleton
- multiset.is_lawful_singleton
- multiset.has_subset
- multiset.has_ssubset
- multiset.partial_order
- multiset.order_bot
- multiset.has_add
- multiset.has_le.le.covariant_class
- multiset.has_le.le.contravariant_class
- multiset.ordered_cancel_add_comm_monoid
- multiset.canonically_ordered_add_monoid
- multiset.is_well_founded_lt
- multiset.can_lift
- multiset.has_sub
- multiset.has_ordered_sub
- multiset.has_union
- multiset.has_inter
- multiset.lattice
- multiset.distrib_lattice
- multiset.can_lift_finset
- multiset.is_well_founded_ssubset
- multiset.infinite
- sym.has_coe
- multiset.has_repr
- multiset.encodable
- multiset.countable
- denumerable.multiset
Equations
- multiset.has_decidable_eq s₁ s₂ = quotient.rec_on_subsingleton₂ s₁ s₂ (λ (l₁ l₂ : list α), decidable_of_iff' (l₁ ≈ l₂) _)
defines a size for a multiset by referring to the size of the underlying list
Equations
- s.sizeof = quot.lift_on s sizeof multiset.sizeof._proof_1
Equations
- multiset.has_sizeof = {sizeof := multiset.sizeof _inst_1}
Empty multiset #
Equations
- multiset.has_zero = {zero := multiset.zero α}
Equations
- multiset.has_emptyc = {emptyc := 0}
Equations
Equations
Dependent recursor on multisets.
TODO: should be @[recursor 6], but then the definition of multiset.pi
fails with a stack
overflow in whnf
.
Equations
- multiset.rec C_0 C_cons C_cons_heq m = quotient.hrec_on m (list.rec C_0 (λ (a : α) (l : list α) (b : (λ (l : list α), C ⟦l⟧) l), C_cons a ⟦l⟧ b)) _
Companion to multiset.rec
with more convenient argument order.
Equations
- m.rec_on C_0 C_cons C_cons_heq = multiset.rec C_0 C_cons C_cons_heq m
a ∈ s
means that a
has nonzero multiplicity in s
.
Equations
- multiset.mem a s = quot.lift_on s (λ (l : list α), a ∈ l) _
Equations
- multiset.has_mem = {mem := multiset.mem α}
Equations
Singleton #
Equations
- multiset.has_singleton = {singleton := λ (a : α), a ::ₘ 0}
s ⊆ t
is the lift of the list subset relation. It means that any
element with nonzero multiplicity in s
has nonzero multiplicity in t
,
but it does not imply that the multiplicity of a
in s
is less or equal than in t
;
see s ≤ t
for this relation.
Equations
Produces a list of the elements in the multiset using choice.
Equations
- s.to_list = quotient.out' s
s ≤ t
means that s
is a sublist of t
(up to permutation).
Equivalently, s ≤ t
means that count a s ≤ count a t
for all a
.
Equations
- s.le t = quotient.lift_on₂ s t list.subperm multiset.le._proof_1
Equations
- multiset.partial_order = {le := multiset.le α, lt := preorder.lt._default multiset.le, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
Equations
- multiset.decidable_le = λ (s t : multiset α), quotient.rec_on_subsingleton₂ s t list.decidable_subperm
Alias of multiset.subset_of_le
.
Equations
- multiset.order_bot = {bot := 0, bot_le := _}
This is a rfl
and simp
version of bot_eq_zero
.
Additive monoid #
The sum of two multisets is the lift of the list append operation.
This adds the multiplicities of each element,
i.e. count a (s + t) = count a s + count a t
.
Equations
- multiset.has_add = {add := multiset.add α}
Equations
- multiset.ordered_cancel_add_comm_monoid = {add := has_add.add multiset.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul._default 0 has_add.add multiset.ordered_cancel_add_comm_monoid._proof_4 multiset.ordered_cancel_add_comm_monoid._proof_5, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := partial_order.le multiset.partial_order, lt := partial_order.lt multiset.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _}
Equations
- multiset.canonically_ordered_add_monoid = {add := ordered_cancel_add_comm_monoid.add multiset.ordered_cancel_add_comm_monoid, add_assoc := _, zero := ordered_cancel_add_comm_monoid.zero multiset.ordered_cancel_add_comm_monoid, zero_add := _, add_zero := _, nsmul := ordered_cancel_add_comm_monoid.nsmul multiset.ordered_cancel_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := ordered_cancel_add_comm_monoid.le multiset.ordered_cancel_add_comm_monoid, lt := ordered_cancel_add_comm_monoid.lt multiset.ordered_cancel_add_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, bot := order_bot.bot multiset.order_bot, bot_le := _, exists_add_of_le := _, le_self_add := _}
Cardinality #
The cardinality of a multiset is the sum of the multiplicities of all its elements, or simply the length of the underlying list.
Equations
- multiset.card = {to_fun := λ (s : multiset α), quot.lift_on s list.length multiset.card._proof_1, map_zero' := _, map_add' := _}
Induction principles #
Suppose that, given that p t
can be defined on all supersets of s
of cardinality less than
n
, one knows how to define p s
. Then one can inductively define p s
for all multisets s
of
cardinality less than n
, starting from multisets of card n
and iterating. This
can be used either to define data, or to prove properties.
Equations
- multiset.strong_downward_induction H s = H s (λ (t : multiset α) (ht : ⇑multiset.card t ≤ n) (h : s < t), multiset.strong_downward_induction H t ht)
Analogue of strong_downward_induction
with order of arguments swapped.
Equations
- multiset.strong_downward_induction_on = λ (s : multiset α) (H : Π (t₁ : multiset α), (Π {t₂ : multiset α}, ⇑multiset.card t₂ ≤ n → t₁ < t₂ → p t₂) → ⇑multiset.card t₁ ≤ n → p t₁), multiset.strong_downward_induction H s
Another way of expressing strong_induction_on
: the (<)
relation is well-founded.
replicate n a
is the multiset containing only a
with multiplicity n
.
Equations
- multiset.replicate n a = ↑(list.replicate n a)
multiset.replicate
as an add_monoid_hom
.
Equations
- multiset.replicate_add_monoid_hom a = {to_fun := λ (n : ℕ), multiset.replicate n a, map_zero' := _, map_add' := _}
Alias of the reverse direction of multiset.eq_replicate_card
.
Erasing one copy of an element #
erase s a
is the multiset that subtracts 1 from the
multiplicity of a
.
map f s
is the lift of the list map
operation. The multiplicity
of b
in map f s
is the number of a ∈ s
(counting multiplicity)
such that f a = b
.
Equations
- multiset.map f s = quot.lift_on s (λ (l : list α), ↑(list.map f l)) _
Instances for multiset.map
multiset.map
as an add_monoid_hom
.
Equations
- multiset.map_add_monoid_hom f = {to_fun := multiset.map f, map_zero' := _, map_add' := _}
foldl f H b s
is the lift of the list operation foldl f b l
,
which folds f
over the multiset. It is well defined when f
is right-commutative,
that is, f (f b a₁) a₂ = f (f b a₂) a₁
.
Equations
- multiset.foldl f H b s = quot.lift_on s (λ (l : list α), list.foldl f b l) _
foldr f H b s
is the lift of the list operation foldr f b l
,
which folds f
over the multiset. It is well defined when f
is left-commutative,
that is, f a₁ (f a₂ b) = f a₂ (f a₁ b)
.
Equations
- multiset.foldr f H b s = quot.lift_on s (λ (l : list α), list.foldr f b l) _
Map for partial functions #
Lift of the list pmap
operation. Map a partial function f
over a multiset
s
whose elements are all in the domain of f
.
Equations
- multiset.pmap f s = quot.rec_on s (λ (l : list α) (H : ∀ (a : α), a ∈ quot.mk setoid.r l → p a), ↑(list.pmap f l H)) _
"Attach" a proof that a ∈ s
to each element a
in s
to produce
a multiset on {x // x ∈ s}
.
Equations
- s.attach = multiset.pmap subtype.mk s _
If p
is a decidable predicate,
so is the predicate that all elements of a multiset satisfy p
.
Equations
- multiset.decidable_forall_multiset = quotient.rec_on_subsingleton m (λ (l : list α), decidable_of_iff (∀ (a : α), a ∈ l → p a) _)
Equations
- multiset.decidable_dforall_multiset = decidable_of_decidable_of_iff multiset.decidable_forall_multiset multiset.decidable_dforall_multiset._proof_3
decidable equality for functions whose domain is bounded by multisets
Equations
- multiset.decidable_eq_pi_multiset = λ (f g : Π (a : α), a ∈ m → β a), decidable_of_iff (∀ (a : α) (h : a ∈ m), f a h = g a h) _
If p
is a decidable predicate,
so is the existence of an element in a multiset satisfying p
.
Equations
- multiset.decidable_exists_multiset = quotient.rec_on_subsingleton m (λ (l : list α), decidable_of_iff (∃ (a : α) (H : a ∈ l), p a) _)
Equations
- multiset.decidable_dexists_multiset = decidable_of_decidable_of_iff multiset.decidable_exists_multiset multiset.decidable_dexists_multiset._proof_3
Subtraction #
s - t
is the multiset such that count a (s - t) = count a s - count a t
for all a
(note that it is truncated subtraction, so it is 0
if count a t ≥ count a s
).
Equations
- multiset.has_sub = {sub := multiset.sub (λ (a b : α), _inst_1 a b)}
This is a special case of tsub_zero
, which should be used instead of this.
This is needed to prove has_ordered_sub (multiset α)
.
This is a special case of tsub_le_iff_right
, which should be used instead of this.
This is needed to prove has_ordered_sub (multiset α)
.
Union #
s ∪ t
is the lattice join operation with respect to the
multiset ≤
. The multiplicity of a
in s ∪ t
is the maximum
of the multiplicities in s
and t
.
Equations
- multiset.has_union = {union := multiset.union (λ (a b : α), _inst_1 a b)}
Intersection #
s ∩ t
is the lattice meet operation with respect to the
multiset ≤
. The multiplicity of a
in s ∩ t
is the minimum
of the multiplicities in s
and t
.
Equations
- multiset.has_inter = {inter := multiset.inter (λ (a b : α), _inst_1 a b)}
Equations
- multiset.lattice = {sup := has_union.union multiset.has_union, le := partial_order.le multiset.partial_order, lt := partial_order.lt multiset.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inter.inter multiset.has_inter, inf_le_left := _, inf_le_right := _, le_inf := _}
filter p s
returns the elements in s
(with the same multiplicities)
which satisfy p
, and removes the rest.
Equations
- multiset.filter p s = quot.lift_on s (λ (l : list α), ↑(list.filter p l)) _
Simultaneously filter and map elements of a multiset #
filter_map f s
is a combination filter/map operation on s
.
The function f : α → option β
is applied to each element of s
;
if f a
is some b
then b
is added to the result, otherwise
a
is removed from the resulting multiset.
Equations
- multiset.filter_map f s = quot.lift_on s (λ (l : list α), ↑(list.filter_map f l)) _
countp #
countp p s
counts the number of elements of s
(with multiplicity) that
satisfy p
.
Equations
- multiset.countp p s = quot.lift_on s (list.countp p) _
countp p
, the number of elements of a multiset satisfying p
, promoted to an
add_monoid_hom
.
Equations
- multiset.countp_add_monoid_hom p = {to_fun := multiset.countp p (λ (a : α), _inst_1 a), map_zero' := _, map_add' := _}
Multiplicity of an element #
count a s
is the multiplicity of a
in s
.
Equations
- multiset.count a = multiset.countp (eq a)
count a
, the multiplicity of a
in a multiset, promoted to an add_monoid_hom
.
Equations
Equations
- multiset.distrib_lattice = {sup := lattice.sup multiset.lattice, le := lattice.le multiset.lattice, lt := lattice.lt multiset.lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf multiset.lattice, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _}
multiset.map f
preserves count
if f
is injective on the set of elements contained in
the multiset
multiset.map f
preserves count
if f
is injective
Associate to an embedding f
from α
to β
the order embedding that maps a multiset to its
image under f
.
Equations
Mapping a multiset through a predicate and counting the true
s yields the cardinality of the set
filtered by the predicate. Note that this uses the notion of a multiset of Prop
s - due to the
decidability requirements of count
, the decidability instance on the LHS is different from the
RHS. In particular, the decidability instance on the left leaks classical.dec_eq
.
See here
for more discussion.
- zero : ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Prop}, multiset.rel r 0 0
- cons : ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {a : α} {b : β} {as : multiset α} {bs : multiset β}, r a b → multiset.rel r as bs → multiset.rel r (a ::ₘ as) (b ::ₘ bs)
rel r s t
-- lift the relation r
between two elements to a relation between s
and t
,
s.t. there is a one-to-one mapping betweem elements in s
and t
following r
.
Disjoint multisets #
Given a proof hp
that there exists a unique a ∈ l
such that p a
, choose_x p l hp
returns
that a
together with proofs of a ∈ l
and p a
.
Equations
- multiset.choose_x p l = quotient.rec_on l (λ (l' : list α) (ex_unique : ∃! (a : α), a ∈ ⟦l'⟧ ∧ p a), list.choose_x p l' _) _
Given a proof hp
that there exists a unique a ∈ l
such that p a
, choose p l hp
returns
that a
.
Equations
- multiset.choose p l hp = ↑(multiset.choose_x p l hp)
The equivalence between lists and multisets of a subsingleton type.
Equations
- multiset.subsingleton_equiv α = {to_fun := coe coe_to_lift, inv_fun := quot.lift id _, left_inv := _, right_inv := _}