Multisets #
These are implemented as the quotient of a list by permutations.
Notation #
We define the global infix notation ::ₘ
for Multiset.cons
.
The quotient map from List α
to Multiset α
.
Equations
- Multiset.ofList = Quot.mk ⇑(List.isSetoid α)
Instances For
Equations
- Multiset.instDecidableEquivListOfDecidableEq l₁ l₂ = inferInstanceAs (Decidable (l₁.Perm l₂))
Equations
- x✝.decidableEq x = Quotient.recOnSubsingleton₂ x✝ x fun (x x_1 : List α) => decidable_of_iff' (x ≈ x_1) ⋯
defines a size for a multiset by referring to the size of the underlying list
Equations
- s.sizeOf = Quot.liftOn s sizeOf ⋯
Instances For
Empty multiset #
Equations
- Multiset.instEmptyCollection = { emptyCollection := 0 }
cons a s
is the multiset which contains s
plus one more instance of a
.
Equations
- Multiset.«term_::ₘ_» = Lean.ParserDescr.trailingNode `Multiset.term_::ₘ_ 67 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ::ₘ ") (Lean.ParserDescr.cat `term 67))
Instances For
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.hrecOn m (List.rec C_0 fun (a : α) (l : List α) (b : C ⟦l⟧) => C_cons a ⟦l⟧ b) ⋯
Instances For
Companion to Multiset.rec
with more convenient argument order.
Equations
- m.recOn C_0 C_cons C_cons_heq = Multiset.rec C_0 C_cons C_cons_heq m
Instances For
a ∈ s
means that a
has nonzero multiplicity in s
.
Equations
- s.Mem a = Quot.liftOn s (fun (l : List α) => a ∈ l) ⋯
Instances For
Equations
- Multiset.instMembership = { mem := Multiset.Mem }
Equations
- Multiset.decidableMem a s = Quot.recOnSubsingleton s fun (l : List α) => inferInstanceAs (Decidable (a ∈ l))
Singleton #
Equations
- ⋯ = ⋯
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.
Instances For
Equations
- ⋯ = ⋯
Produces a list of the elements in the multiset using choice.
Equations
- s.toList = Quotient.out' s
Instances For
Equations
- Multiset.instPartialOrder = PartialOrder.mk ⋯
Equations
- s.decidableLE t = Quotient.recOnSubsingleton₂ s t List.decidableSubperm
Alias of Multiset.subset_of_le
.
Equations
- Multiset.instOrderBot = OrderBot.mk ⋯
This is a rfl
and simp
version of bot_eq_zero
.
Additive monoid #
Equations
- Multiset.instAddCommMonoid = AddCancelCommMonoid.mk ⋯
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 = { toFun := fun (s : Multiset α) => Quot.liftOn s List.length ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
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.strongDownwardInduction H s = H s fun {t : Multiset α} (ht : Multiset.card t ≤ n) (_h : s < t) => Multiset.strongDownwardInduction H t ht
Instances For
Analogue of strongDownwardInduction
with order of arguments swapped.
Equations
- s.strongDownwardInductionOn H = Multiset.strongDownwardInduction H s
Instances For
Another way of expressing strongInductionOn
: the (<)
relation is well-founded.
Equations
- ⋯ = ⋯
replicate n a
is the multiset containing only a
with multiplicity n
.
Equations
- Multiset.replicate n a = ↑(List.replicate n a)
Instances For
Multiset.replicate
as an AddMonoidHom
.
Equations
- Multiset.replicateAddMonoidHom a = { toFun := fun (n : ℕ) => Multiset.replicate n a, map_zero' := ⋯, map_add' := ⋯ }
Instances For
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
.
Equations
- s.erase a = Quot.liftOn s (fun (l : List α) => ↑(l.erase a)) ⋯
Instances For
Equations
- ⋯ = ⋯
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.liftOn s (fun (l : List α) => ↑(List.map f l)) ⋯
Instances For
Multiset.map
as an AddMonoidHom
.
Equations
- Multiset.mapAddMonoidHom f = { toFun := Multiset.map f, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Multiset.fold
#
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 b s = Quot.liftOn s (fun (l : List α) => List.foldl f b l) ⋯
Instances For
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 b s = Quot.liftOn s (fun (l : List α) => List.foldr f b l) ⋯
Instances For
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.recOn (motive := fun (x : Multiset α) => (∀ a ∈ x, p a) → Multiset β) s (fun (l : List α) (H : ∀ a ∈ Quot.mk (⇑(List.isSetoid α)) l, p a) => ↑(List.pmap f l H)) ⋯
Instances For
"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 ⋯
Instances For
If p
is a decidable predicate,
so is the predicate that all elements of a multiset satisfy p
.
Equations
- Multiset.decidableForallMultiset = Quotient.recOnSubsingleton m fun (l : List α) => decidable_of_iff (∀ a ∈ l, p a) ⋯
Instances For
decidable equality for functions whose domain is bounded by multisets
Equations
- Multiset.decidableEqPiMultiset f g = 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.decidableExistsMultiset = Quotient.recOnSubsingleton m fun (l : List α) => decidable_of_iff (∃ a ∈ l, p a) ⋯
Instances For
Subtraction #
Equations
- Multiset.instSub = { sub := Multiset.sub }
This is a special case of tsub_zero
, which should be used instead of this.
This is needed to prove OrderedSub (Multiset α)
.
This is a special case of tsub_le_iff_right
, which should be used instead of this.
This is needed to prove OrderedSub (Multiset α)
.
Equations
- ⋯ = ⋯
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
.
Instances For
Equations
- Multiset.instUnion = { union := Multiset.union }
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
- s.inter t = Quotient.liftOn₂ s t (fun (l₁ l₂ : List α) => ↑(l₁.bagInter l₂)) ⋯
Instances For
Equations
- Multiset.instInter = { inter := Multiset.inter }
Equations
- Multiset.instLattice = Lattice.mk ⋯ ⋯ ⋯
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.liftOn s (fun (l : List α) => ↑(List.filter (fun (b : α) => decide (p b)) l)) ⋯
Instances For
Alias of Multiset.filter_map
.
Simultaneously filter and map elements of a multiset #
filterMap 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.filterMap f s = Quot.liftOn s (fun (l : List α) => ↑(List.filterMap f l)) ⋯
Instances For
countP #
countP p s
counts the number of elements of s
(with multiplicity) that
satisfy p
.
Equations
- Multiset.countP p s = Quot.liftOn s (List.countP fun (b : α) => decide (p b)) ⋯
Instances For
countP p
, the number of elements of a multiset satisfying p
, promoted to an
AddMonoidHom
.
Equations
- Multiset.countPAddMonoidHom p = { toFun := Multiset.countP p, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Multiplicity of an element #
count a s
is the multiplicity of a
in s
.
Equations
- Multiset.count a = Multiset.countP fun (x : α) => a = x
Instances For
count a
, the multiplicity of a
in a multiset, promoted to an AddMonoidHom
.
Equations
- Multiset.countAddMonoidHom a = Multiset.countPAddMonoidHom fun (x : α) => a = x
Instances For
Equations
- Multiset.instDistribLattice = DistribLattice.mk ⋯
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
Instances For
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.decEq
.
See here
for more discussion.
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 between elements in s
and t
following r
.
- zero: ∀ {α : Type u_1} {β : Type v} {r : α → β → Prop}, Multiset.Rel r 0 0
- cons: ∀ {α : Type u_1} {β : Type v} {r : α → β → Prop} {a : α} {b : β} {as : Multiset α} {bs : Multiset β}, r a b → Multiset.Rel r as bs → Multiset.Rel r (a ::ₘ as) (b ::ₘ bs)