Multisets

Multisets are finite sets with duplicates allowed. They are implemented here as the quotient of lists by permutation. This gives them computational content.

This file contains the definition of Multiset and the basic predicates. Most operations have been split off into their own files. The goal is that we can define Finset with only importing Multiset.Defs.

Main definitions

• Multiset: the type of finite sets with duplicates allowed.

• Coe (List α) (Multiset α): turn a list into a multiset by forgetting the order.

• Multiset.pmap: map a partial function defined on a superset of the multiset's elements.

• Multiset.attach: add a proof of membership to the elements of the multiset.

• Multiset.card: number of elements of a multiset (counted with repetition).

• Membership α (Multiset α) instance: x ∈ s if x has multiplicity at least one in s.

• Subset (Multiset α) instance: s ⊆ t if every x ∈ s also enjoys x ∈ t.

• PartialOrder (Multiset α) instance: s ≤ t if all x have multiplicity in s less than their multiplicity in t.

• Multiset.Pairwise: Pairwise r s holds iff there exists a list of elements of s such that r holds pairwise.

• Multiset.Nodup: Nodup s holds if the multiplicity of any element is at most 1.

Notation (defined later)

• 0: The empty multiset.
• {a}: The multiset containing a single occurrence of a.
• a ::ₘ s: The multiset containing one more occurrence of a than s does.
• s + t: The multiset for which the number of occurrences of each a is the sum of the occurrences of a in s and t.
• s - t: The multiset for which the number of occurrences of each a is the difference of the occurrences of a in s and t.
• s ∪ t: The multiset for which the number of occurrences of each a is the max of the occurrences of a in s and t.
• s ∩ t: The multiset for which the number of occurrences of each a is the min of the occurrences of a in s and t.

def Multiset (α : Type u) : Type u

Multiset α is the quotient of List α by list permutation. The result is a type of finite sets with duplicates allowed.

Equations

• Multiset α = Quotient (List.isSetoid α)

def Multiset.ofList {α : Type u_1} : List α → Multiset α

The quotient map from List α to Multiset α.

Equations

• Multiset.ofList = Quot.mk ⇑(List.isSetoid α)

instance Multiset.instCoeList {α : Type u_1} : Coe (List α) (Multiset α)

Equations

• Multiset.instCoeList = { coe := Multiset.ofList }

@[simp]

theorem Multiset.quot_mk_to_coe {α : Type u_1} (l : List α) : ⟦l⟧ = ↑l

@[simp]

theorem Multiset.quot_mk_to_coe' {α : Type u_1} (l : List α) : Quot.mk (fun (x1 x2 : List α) => x1 ≈ x2) l = ↑l

@[simp]

theorem Multiset.quot_mk_to_coe'' {α : Type u_1} (l : List α) : Quot.mk (⇑(List.isSetoid α)) l = ↑l

@[simp]

theorem Multiset.lift_coe {α : Type u_3} {β : Type u_4} (x : List α) (f : List α → β) (h : ∀ (a b : List α), a ≈ b → f a = f b) : Quotient.lift f h ↑x = f x

@[simp]

theorem Multiset.coe_eq_coe {α : Type u_1} {l₁ l₂ : List α} : ↑l₁ = ↑l₂ ↔ l₁.Perm l₂

instance Multiset.instDecidableEquivListOfDecidableEq {α : Type u_1} [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ ≈ l₂)

Equations

• Multiset.instDecidableEquivListOfDecidableEq l₁ l₂ = inferInstanceAs (Decidable (l₁.Perm l₂))

instance Multiset.instDecidableRListOfDecidableEq {α : Type u_1} [DecidableEq α] (l₁ l₂ : List α) : Decidable ((List.isSetoid α) l₁ l₂)

Equations

• Multiset.instDecidableRListOfDecidableEq l₁ l₂ = inferInstanceAs (Decidable (l₁.Perm l₂))

instance Multiset.decidableEq {α : Type u_1} [DecidableEq α] : DecidableEq (Multiset α)

Equations

• x✝¹.decidableEq x✝ = Quotient.recOnSubsingleton₂ x✝¹ x✝ fun (x x_1 : List α) => decidable_of_iff' (x ≈ x_1) ⋯

def Multiset.Mem {α : Type u_1} (s : Multiset α) (a : α) : Prop

a ∈ s means that a has nonzero multiplicity in s.

Equations

• s.Mem a = Quot.liftOn s (fun (l : List α) => a ∈ l) ⋯

instance Multiset.instMembership {α : Type u_1} : Membership α (Multiset α)

Equations

• Multiset.instMembership = { mem := Multiset.Mem }

@[simp]

theorem Multiset.mem_coe {α : Type u_1} {a : α} {l : List α} : a ∈ ↑l ↔ a ∈ l

instance Multiset.decidableMem {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) : Decidable (a ∈ s)

Equations

• Multiset.decidableMem a s = Quot.recOnSubsingleton s fun (l : List α) => inferInstanceAs (Decidable (a ∈ l))

Multiset.Subset

def Multiset.Subset {α : Type u_1} (s t : Multiset α) : Prop

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

• s.Subset t = ∀ ⦃a : α⦄, a ∈ s → a ∈ t

instance Multiset.instHasSubset {α : Type u_1} : HasSubset (Multiset α)

Equations

• Multiset.instHasSubset = { Subset := Multiset.Subset }

instance Multiset.instHasSSubset {α : Type u_1} : HasSSubset (Multiset α)

Equations

• Multiset.instHasSSubset = { SSubset := fun (s t : Multiset α) => s ⊆ t ∧ ¬t ⊆ s }

instance Multiset.instIsNonstrictStrictOrder {α : Type u_1} : IsNonstrictStrictOrder (Multiset α) (fun (x1 x2 : Multiset α) => x1 ⊆ x2) fun (x1 x2 : Multiset α) => x1 ⊂ x2

@[simp]

theorem Multiset.coe_subset {α : Type u_1} {l₁ l₂ : List α} : ↑l₁ ⊆ ↑l₂ ↔ l₁ ⊆ l₂

@[simp]

theorem Multiset.Subset.refl {α : Type u_1} (s : Multiset α) : s ⊆ s

theorem Multiset.Subset.trans {α : Type u_1} {s t u : Multiset α} : s ⊆ t → t ⊆ u → s ⊆ u

theorem Multiset.subset_iff {α : Type u_1} {s t : Multiset α} : s ⊆ t ↔ ∀ ⦃x : α⦄, x ∈ s → x ∈ t

theorem Multiset.mem_of_subset {α : Type u_1} {s t : Multiset α} {a : α} (h : s ⊆ t) : a ∈ s → a ∈ t

Partial order on Multisets

def Multiset.Le {α : Type u_1} (s t : Multiset α) : Prop

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.liftOn₂ s t (fun (x1 x2 : List α) => x1.Subperm x2) ⋯

instance Multiset.instPartialOrder {α : Type u_1} : PartialOrder (Multiset α)

Equations

• Multiset.instPartialOrder = PartialOrder.mk ⋯

instance Multiset.decidableLE {α : Type u_1} [DecidableEq α] : DecidableRel fun (x1 x2 : Multiset α) => x1 ≤ x2

Equations

• s.decidableLE t = Quotient.recOnSubsingleton₂ s t List.decidableSubperm

theorem Multiset.subset_of_le {α : Type u_1} {s t : Multiset α} : s ≤ t → s ⊆ t

theorem Multiset.Le.subset {α : Type u_1} {s t : Multiset α} : s ≤ t → s ⊆ t

Alias of Multiset.subset_of_le.

theorem Multiset.mem_of_le {α : Type u_1} {s t : Multiset α} {a : α} (h : s ≤ t) : a ∈ s → a ∈ t

theorem Multiset.not_mem_mono {α : Type u_1} {s t : Multiset α} {a : α} (h : s ⊆ t) : ¬a ∈ t → ¬a ∈ s

@[simp]

theorem Multiset.coe_le {α : Type u_1} {l₁ l₂ : List α} : ↑l₁ ≤ ↑l₂ ↔ l₁.Subperm l₂

theorem Multiset.leInductionOn {α : Type u_1} {C : Multiset α → Multiset α → Prop} {s t : Multiset α} (h : s ≤ t) (H : ∀ {l₁ l₂ : List α}, l₁.Sublist l₂ → C ↑l₁ ↑l₂) : C s t

Cardinality

def Multiset.card {α : Type u_1} : Multiset α → ℕ

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 = Quot.lift List.length ⋯

@[simp]

theorem Multiset.coe_card {α : Type u_1} (l : List α) : (↑l).card = l.length

theorem Multiset.card_le_card {α : Type u_1} {s t : Multiset α} (h : s ≤ t) : s.card ≤ t.card

theorem Multiset.eq_of_le_of_card_le {α : Type u_1} {s t : Multiset α} (h : s ≤ t) : t.card ≤ s.card → s = t

theorem Multiset.card_lt_card {α : Type u_1} {s t : Multiset α} (h : s < t) : s.card < t.card

theorem Multiset.card_mono {α : Type u_1} : Monotone card

theorem Multiset.card_strictMono {α : Type u_1} : StrictMono card

instance Multiset.instWellFoundedLT {α : Type u_1} : WellFoundedLT (Multiset α)

Another way of expressing strongInductionOn: the (<) relation is well-founded.

@[simp]

theorem Multiset.coe_reverse {α : Type u_1} (l : List α) : ↑l.reverse = ↑l

Map for partial functions

def Multiset.pmap {α : Type u_1} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) (s : Multiset α) : (∀ (a : α), a ∈ s → p a) → Multiset β

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

• One or more equations did not get rendered due to their size.

@[simp]

theorem Multiset.coe_pmap {α : Type u_1} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) (l : List α) (H : ∀ (a : α), a ∈ l → p a) : pmap f (↑l) H = ↑(List.pmap f l H)

theorem Multiset.pmap_congr {α : Type u_1} {β : Type v} {p q : α → Prop} {f : (a : α) → p a → β} {g : (a : α) → q a → β} (s : Multiset α) {H₁ : ∀ (a : α), a ∈ s → p a} {H₂ : ∀ (a : α), a ∈ s → q a} : (∀ (a : α), a ∈ s → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂) → pmap f s H₁ = pmap g s H₂

@[simp]

theorem Multiset.mem_pmap {α : Type u_1} {β : Type v} {p : α → Prop} {f : (a : α) → p a → β} {s : Multiset α} {H : ∀ (a : α), a ∈ s → p a} {b : β} : b ∈ pmap f s H ↔ ∃ (a : α), ∃ (h : a ∈ s), f a ⋯ = b

@[simp]

theorem Multiset.card_pmap {α : Type u_1} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) (s : Multiset α) (H : ∀ (a : α), a ∈ s → p a) : (pmap f s H).card = s.card

def Multiset.attach {α : Type u_1} (s : Multiset α) : Multiset { x : α // x ∈ s }

"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 ⋯

@[simp]

theorem Multiset.coe_attach {α : Type u_1} (l : List α) : (↑l).attach = ↑l.attach

@[simp]

theorem Multiset.mem_attach {α : Type u_1} (s : Multiset α) (x : { x : α // x ∈ s }) : x ∈ s.attach

@[simp]

theorem Multiset.card_attach {α : Type u_1} {m : Multiset α} : m.attach.card = m.card

def Multiset.decidableForallMultiset {α : Type u_1} {m : Multiset α} {p : α → Prop} [(a : α) → Decidable (p a)] : Decidable (∀ (a : α), a ∈ m → p a)

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 : α), a ∈ l → p a) ⋯

instance Multiset.decidableDforallMultiset {α : Type u_1} {m : Multiset α} {p : (a : α) → a ∈ m → Prop} [_hp : (a : α) → (h : a ∈ m) → Decidable (p a h)] : Decidable (∀ (a : α) (h : a ∈ m), p a h)

Equations

• Multiset.decidableDforallMultiset = decidable_of_iff (∀ (a : { x : α // x ∈ m }), a ∈ m.attach → p ↑a ⋯) ⋯

instance Multiset.decidableEqPiMultiset {α : Type u_1} {m : Multiset α} {β : α → Type u_3} [(a : α) → DecidableEq (β a)] : DecidableEq ((a : α) → a ∈ m → β a)

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) ⋯

def Multiset.decidableExistsMultiset {α : Type u_1} {m : Multiset α} {p : α → Prop} [DecidablePred p] : Decidable (∃ (x : α), x ∈ m ∧ p x)

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 : α), a ∈ l ∧ p a) ⋯

instance Multiset.decidableDexistsMultiset {α : Type u_1} {m : Multiset α} {p : (a : α) → a ∈ m → Prop} [_hp : (a : α) → (h : a ∈ m) → Decidable (p a h)] : Decidable (∃ (a : α), ∃ (h : a ∈ m), p a h)

Equations

• Multiset.decidableDexistsMultiset = decidable_of_iff (∃ (x : { a : α // a ∈ m }), x ∈ m.attach ∧ p ↑x ⋯) ⋯

def Multiset.Pairwise {α : Type u_1} (r : α → α → Prop) (m : Multiset α) : Prop

Pairwise r m states that there exists a list of the elements s.t. r holds pairwise on this list.

Equations

• Multiset.Pairwise r m = ∃ (l : List α), m = ↑l ∧ List.Pairwise r l

theorem Multiset.pairwise_coe_iff {α : Type u_1} {r : α → α → Prop} {l : List α} : Pairwise r ↑l ↔ ∃ (l' : List α), l.Perm l' ∧ List.Pairwise r l'

theorem Multiset.pairwise_coe_iff_pairwise {α : Type u_1} {r : α → α → Prop} (hr : Symmetric r) {l : List α} : Pairwise r ↑l ↔ List.Pairwise r l

def Multiset.Nodup {α : Type u_1} (s : Multiset α) : Prop

Nodup s means that s has no duplicates, i.e. the multiplicity of any element is at most 1.

Equations

• s.Nodup = Quot.liftOn s List.Nodup ⋯

@[simp]

theorem Multiset.coe_nodup {α : Type u_1} {l : List α} : (↑l).Nodup ↔ l.Nodup

theorem Multiset.Nodup.ext {α : Type u_1} {s t : Multiset α} : s.Nodup → t.Nodup → (s = t ↔ ∀ (a : α), a ∈ s ↔ a ∈ t)

theorem Multiset.le_iff_subset {α : Type u_1} {s t : Multiset α} : s.Nodup → (s ≤ t ↔ s ⊆ t)

theorem Multiset.nodup_of_le {α : Type u_1} {s t : Multiset α} (h : s ≤ t) : t.Nodup → s.Nodup

instance Multiset.nodupDecidable {α : Type u_1} [DecidableEq α] (s : Multiset α) : Decidable s.Nodup

Equations

• s.nodupDecidable = Quotient.recOnSubsingleton s fun (l : List α) => l.nodupDecidable

def Multiset.sizeOf {α : Type u_1} [SizeOf α] (s : Multiset α) : ℕ

Defines a size for a multiset by referring to the size of the underlying list.

This has to be defined before the definition of Finset, otherwise its automatically generated SizeOf instance will be wrong.

Equations

• s.sizeOf = Quot.liftOn s sizeOf ⋯

instance Multiset.instSizeOf {α : Type u_1} [SizeOf α] : SizeOf (Multiset α)

Equations

• Multiset.instSizeOf = { sizeOf := Multiset.sizeOf }