Mathlib.Data.Multiset.Basic

Multiset.toList definition

(s : Multiset α)

Full source

/-- Produces a list of the elements in the multiset using choice. -/
noncomputable def toList (s : Multiset α) :=
  s.out

List representation of a multiset

Informal description

Given a multiset $s$ over a type $\alpha$, the function returns a list containing all elements of $s$ (with multiplicities), where the order of elements is determined by the choice function.

Multiset.coe_toList theorem

(s : Multiset α) : (s.toList : Multiset α) = s

Full source

@[simp, norm_cast]
theorem coe_toList (s : Multiset α) : (s.toList : Multiset α) = s :=
  s.out_eq'

Coercion of Multiset to List and Back Preserves Equality

Informal description

For any multiset $s$ over a type $\alpha$, the multiset obtained by coercing the list representation of $s$ (via `toList`) back to a multiset is equal to $s$ itself. That is, $\text{toList}(s) = s$ where the left side is interpreted as a multiset.

Multiset.toList_eq_nil theorem

{s : Multiset α} : s.toList = [] ↔ s = 0

Full source

@[simp]
theorem toList_eq_nil {s : Multiset α} : s.toList = [] ↔ s = 0 := by
  rw [← coe_eq_zero, coe_toList]

Empty List Representation of Multiset Equivalence

Informal description

For any multiset $s$ over a type $\alpha$, the list representation of $s$ is empty if and only if $s$ is the empty multiset. That is, $\text{toList}(s) = [] \leftrightarrow s = 0$.

Multiset.empty_toList theorem

{s : Multiset α} : s.toList.isEmpty ↔ s = 0

Full source

theorem empty_toList {s : Multiset α} : s.toList.isEmpty ↔ s = 0 := by simp

Empty List Representation of Multiset Equivalence

Informal description

For any multiset $s$ over a type $\alpha$, the list representation of $s$ is empty if and only if $s$ is the empty multiset (i.e., $s = 0$).

Multiset.toList_zero theorem

: (Multiset.toList 0 : List α) = []

Full source

@[simp]
theorem toList_zero : (Multiset.toList 0 : List α) = [] :=
  toList_eq_nil.mpr rfl

Empty Multiset Maps to Empty List

Informal description

The list representation of the empty multiset $0$ over a type $\alpha$ is the empty list $[]$.

Multiset.mem_toList theorem

{a : α} {s : Multiset α} : a ∈ s.toList ↔ a ∈ s

Full source

@[simp]
theorem mem_toList {a : α} {s : Multiset α} : a ∈ s.toLista ∈ s.toList ↔ a ∈ s := by
  rw [← mem_coe, coe_toList]

Membership Preservation in Multiset to List Conversion

Informal description

For any element $a$ of type $\alpha$ and any multiset $s$ over $\alpha$, the element $a$ belongs to the list representation of $s$ if and only if $a$ belongs to the multiset $s$. That is, $a \in \text{toList}(s) \leftrightarrow a \in s$.

Multiset.toList_eq_singleton_iff theorem

{a : α} {m : Multiset α} : m.toList = [a] ↔ m = { a }

Full source

@[simp]
theorem toList_eq_singleton_iff {a : α} {m : Multiset α} : m.toList = [a] ↔ m = {a} := by
  rw [← perm_singleton, ← coe_eq_coe, coe_toList, coe_singleton]

Multiset-to-List Singleton Equivalence

Informal description

For any element $a$ of type $\alpha$ and any multiset $m$ over $\alpha$, the list representation of $m$ is equal to the singleton list $[a]$ if and only if $m$ is equal to the singleton multiset $\{a\}$. That is, $\text{toList}(m) = [a] \leftrightarrow m = \{a\}$.

Multiset.toList_singleton theorem

(a : α) : ({ a } : Multiset α).toList = [a]

Full source

@[simp]
theorem toList_singleton (a : α) : ({a} : Multiset α).toList = [a] :=
  Multiset.toList_eq_singleton_iff.2 rfl

Singleton Multiset to List Conversion: $\text{toList}(\{a\}) = [a]$

Informal description

For any element $a$ of type $\alpha$, the list representation of the singleton multiset $\{a\}$ is equal to the singleton list $[a]$.

Multiset.length_toList theorem

(s : Multiset α) : s.toList.length = card s

Full source

@[simp]
theorem length_toList (s : Multiset α) : s.toList.length = card s := by
  rw [← coe_card, coe_toList]

Length of Multiset-to-List Conversion Equals Cardinality

Informal description

For any multiset $s$ over a type $\alpha$, the length of the list obtained by converting $s$ to a list (via `toList`) is equal to the cardinality of $s$. That is, $|\text{toList}(s)| = \text{card}(s)$.

Multiset.strongInductionOn definition

{p : Multiset α → Sort*} (s : Multiset α) (ih : ∀ s, (∀ t < s, p t) → p s) : p s

Full source

/-- The strong induction principle for multisets. -/
@[elab_as_elim]
def strongInductionOn {p : Multiset α → Sort*} (s : Multiset α) (ih : ∀ s, (∀ t < s, p t) → p s) :
    p s :=
    (ih s) fun t _h =>
      strongInductionOn t ih
termination_by card s
decreasing_by exact card_lt_card _h

Strong induction principle for multisets

Informal description

The strong induction principle for multisets states that for any property $ p $ on multisets of type $ \alpha $ and any multiset $ s $, if for every multiset $ s' $, the property $ p(s') $ holds whenever $ p(t) $ holds for all $ t < s' $, then $ p(s) $ holds. In other words, to prove $ p(s) $ for all multisets $ s $, it suffices to show that $ p(s) $ holds under the inductive hypothesis that $ p(t) $ holds for all $ t < s $.

Multiset.strongInductionOn_eq theorem

 {p : Multiset α → Sort*} (s : Multiset α) (H) : @strongInductionOn _ p s H = H s fun t _h => @strongInductionOn _ p t H

Full source

theorem strongInductionOn_eq {p : Multiset α → Sort*} (s : Multiset α) (H) :
    @strongInductionOn _ p s H = H s fun t _h => @strongInductionOn _ p t H := by
  rw [strongInductionOn]

Recursive Unfolding of Strong Induction for Multisets

Informal description

For any property $p$ on multisets of type $\alpha$ and any multiset $s$, the application of the strong induction principle `strongInductionOn` to $s$ with hypothesis $H$ is equal to $H$ applied to $s$ and the function that recursively applies `strongInductionOn` to all multisets $t$ less than $s$.

Multiset.case_strongInductionOn theorem

{p : Multiset α → Prop} (s : Multiset α) (h₀ : p 0) (h₁ : ∀ a s, (∀ t ≤ s, p t) → p (a ::ₘ s)) : p s

Full source

@[elab_as_elim]
theorem case_strongInductionOn {p : Multiset α → Prop} (s : Multiset α) (h₀ : p 0)
    (h₁ : ∀ a s, (∀ t ≤ s, p t) → p (a ::ₘ s)) : p s :=
  Multiset.strongInductionOn s fun s =>
    Multiset.induction_on s (fun _ => h₀) fun _a _s _ ih =>
      (h₁ _ _) fun _t h => ih _ <| lt_of_le_of_lt h <| lt_cons_self _ _

Case-based Strong Induction Principle for Multisets

Informal description

For any predicate $p$ on multisets of type $\alpha$ and any multiset $s$, if $p$ holds for the empty multiset (base case), and for any element $a$ and multiset $s'$, $p(a \cup s')$ holds whenever $p(t)$ holds for all multisets $t \leq s'$ (inductive step), then $p(s)$ holds for all multisets $s$.

Multiset.strongDownwardInduction definition

 {p : Multiset α → Sort*} {n : ℕ} (H : ∀ t₁, (∀ {t₂ : Multiset α}, card t₂ ≤ n → t₁ < t₂ → p t₂) → card t₁ ≤ n → p t₁)
  (s : Multiset α) : card s ≤ n → p s

Full source

/-- 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. -/
def strongDownwardInduction {p : Multiset α → Sort*} {n : ℕ}
    (H : ∀ t₁, (∀ {t₂ : Multiset α}, card t₂ ≤ n → t₁ < t₂ → p t₂) → card t₁ ≤ n → p t₁)
    (s : Multiset α) :
    card s ≤ n → p s :=
  H s fun {t} ht _h =>
    strongDownwardInduction H t ht
termination_by n - card s
decreasing_by simp_wf; have := (card_lt_card _h); omega

Strong downward induction for multisets

Informal description

Given a predicate $p$ on multisets of type $\alpha$ and a natural number $n$, the function `strongDownwardInduction` takes a proof $H$ that for any multiset $t_1$, if $p$ holds for all multisets $t_2$ with cardinality at most $n$ and $t_1 < t_2$, then $p$ holds for $t_1$ provided its cardinality is at most $n$. Then for any multiset $s$ with cardinality at most $n$, the function returns a proof that $p$ holds for $s$.

Multiset.strongDownwardInduction_eq theorem

 {p : Multiset α → Sort*} {n : ℕ} (H : ∀ t₁, (∀ {t₂ : Multiset α}, card t₂ ≤ n → t₁ < t₂ → p t₂) → card t₁ ≤ n → p t₁)
  (s : Multiset α) : strongDownwardInduction H s = H s fun ht _hst => strongDownwardInduction H _ ht

Full source

theorem strongDownwardInduction_eq {p : Multiset α → Sort*} {n : ℕ}
    (H : ∀ t₁, (∀ {t₂ : Multiset α}, card t₂ ≤ n → t₁ < t₂ → p t₂) → card t₁ ≤ n → p t₁)
    (s : Multiset α) :
    strongDownwardInduction H s = H s fun ht _hst => strongDownwardInduction H _ ht := by
  rw [strongDownwardInduction]

Equational form of strong downward induction for multisets

Informal description

Let $p$ be a predicate on multisets of type $\alpha$ and $n$ a natural number. Given a proof $H$ that for any multiset $t_1$, if $p$ holds for all multisets $t_2$ with cardinality at most $n$ and $t_1 < t_2$, then $p$ holds for $t_1$ provided its cardinality is at most $n$, we have that for any multiset $s$, the application of the strong downward induction principle equals $H$ applied to $s$ and the function that applies strong downward induction to any multiset with cardinality at most $n$.

Multiset.strongDownwardInductionOn definition

 {p : Multiset α → Sort*} {n : ℕ} :
  ∀ s : Multiset α, (∀ t₁, (∀ {t₂ : Multiset α}, card t₂ ≤ n → t₁ < t₂ → p t₂) → card t₁ ≤ n → p t₁) → card s ≤ n → p s

Full source

/-- Analogue of `strongDownwardInduction` with order of arguments swapped. -/
@[elab_as_elim]
def strongDownwardInductionOn {p : Multiset α → Sort*} {n : ℕ} :
    ∀ s : Multiset α,
      (∀ t₁, (∀ {t₂ : Multiset α}, card t₂ ≤ n → t₁ < t₂ → p t₂) → card t₁ ≤ n → p t₁) →
        card s ≤ n → p s :=
  fun s H => strongDownwardInduction H s

Strong downward induction on multisets

Informal description

Given a predicate $p$ on multisets of type $\alpha$ and a natural number $n$, the function `strongDownwardInductionOn` takes a multiset $s$ with cardinality at most $n$ and a proof $H$ that for any multiset $t_1$, if $p$ holds for all multisets $t_2$ with cardinality at most $n$ and $t_1 < t_2$, then $p$ holds for $t_1$ provided its cardinality is at most $n$. The function returns a proof that $p$ holds for $s$.

Multiset.strongDownwardInductionOn_eq theorem

 {p : Multiset α → Sort*} (s : Multiset α) {n : ℕ}
  (H : ∀ t₁, (∀ {t₂ : Multiset α}, card t₂ ≤ n → t₁ < t₂ → p t₂) → card t₁ ≤ n → p t₁) :
  s.strongDownwardInductionOn H = H s fun {t} ht _h => t.strongDownwardInductionOn H ht

Full source

theorem strongDownwardInductionOn_eq {p : Multiset α → Sort*} (s : Multiset α) {n : ℕ}
    (H : ∀ t₁, (∀ {t₂ : Multiset α}, card t₂ ≤ n → t₁ < t₂ → p t₂) → card t₁ ≤ n → p t₁) :
    s.strongDownwardInductionOn H = H s fun {t} ht _h => t.strongDownwardInductionOn H ht := by
  dsimp only [strongDownwardInductionOn]
  rw [strongDownwardInduction]

Equational form of strong downward induction on multisets

Informal description

Let $p$ be a predicate on multisets of type $\alpha$ and let $n$ be a natural number. For any multiset $s$ and any function $H$ that, given a multiset $t_1$, proves $p(t_1)$ under the assumptions that (1) for all multisets $t_2$ with cardinality at most $n$ such that $t_1 < t_2$, $p(t_2)$ holds, and (2) the cardinality of $t_1$ is at most $n$, we have that the application of strong downward induction on $s$ with $H$ equals $H$ applied to $s$ and the function that applies strong downward induction to any multiset $t$ with cardinality at most $n$.

Multiset.chooseX definition

: ∀ _hp : ∃! a, a ∈ l ∧ p a, { a // a ∈ l ∧ p a }

Full source

/-- Given a proof `hp` that there exists a unique `a ∈ l` such that `p a`, `chooseX p l hp` returns
that `a` together with proofs of `a ∈ l` and `p a`. -/
def chooseX : ∀ _hp : ∃! a, a ∈ l ∧ p a, { a // a ∈ l ∧ p a } :=
  Quotient.recOn l (fun l' ex_unique => List.chooseX p l' (ExistsUnique.exists ex_unique))
    (by
      intros a b _
      funext hp
      suffices all_equal : ∀ x y : { t // t ∈ b ∧ p t }, x = y by
        apply all_equal
      rintro ⟨x, px⟩ ⟨y, py⟩
      rcases hp with ⟨z, ⟨_z_mem_l, _pz⟩, z_unique⟩
      congr
      calc
        x = z := z_unique x px
        _ = y := (z_unique y py).symm
        )

Unique element selection in a multiset with proof

Informal description

Given a multiset $l$ and a predicate $p$ on its elements, if there exists a unique element $a \in l$ such that $p(a)$ holds, then `Multiset.chooseX p l hp` returns a pair consisting of this element $a$ together with proofs that $a \in l$ and $p(a)$. Here, $hp$ is a proof of the existence and uniqueness of such an element $a$.

Multiset.choose definition

(hp : ∃! a, a ∈ l ∧ p a) : α

Full source

/-- Given a proof `hp` that there exists a unique `a ∈ l` such that `p a`, `choose p l hp` returns
that `a`. -/
def choose (hp : ∃! a, a ∈ l ∧ p a) : α :=
  chooseX p l hp

Selection of unique element in a multiset

Informal description

Given a multiset $l$ and a predicate $p$ on its elements, if there exists a unique element $a \in l$ such that $p(a)$ holds (with proof $hp$), then `Multiset.choose p l hp` returns this element $a$.

Multiset.choose_spec theorem

(hp : ∃! a, a ∈ l ∧ p a) : choose p l hp ∈ l ∧ p (choose p l hp)

Full source

theorem choose_spec (hp : ∃! a, a ∈ l ∧ p a) : choosechoose p l hp ∈ lchoose p l hp ∈ l ∧ p (choose p l hp) :=
  (chooseX p l hp).property

Selected element satisfies membership and predicate in multiset

Informal description

Given a multiset $l$ and a predicate $p$ on its elements, if there exists a unique element $a \in l$ such that $p(a)$ holds (with proof $hp$), then the element selected by `choose p l hp` satisfies both $a \in l$ and $p(a)$.

Multiset.choose_mem theorem

(hp : ∃! a, a ∈ l ∧ p a) : choose p l hp ∈ l

Full source

theorem choose_mem (hp : ∃! a, a ∈ l ∧ p a) : choosechoose p l hp ∈ l :=
  (choose_spec _ _ _).1

Membership of chosen element in multiset

Informal description

Given a multiset $l$ and a predicate $p$ on its elements, if there exists a unique element $a \in l$ such that $p(a)$ holds (with proof $hp$), then the element selected by $\mathrm{choose}(p, l, hp)$ is a member of $l$.

Multiset.choose_property theorem

(hp : ∃! a, a ∈ l ∧ p a) : p (choose p l hp)

Full source

theorem choose_property (hp : ∃! a, a ∈ l ∧ p a) : p (choose p l hp) :=
  (choose_spec _ _ _).2

Selected element satisfies predicate in multiset

Informal description

Given a multiset $l$ and a predicate $p$ on its elements, if there exists a unique element $a \in l$ such that $p(a)$ holds (with proof $hp$), then the element selected by $\mathrm{choose}(p, l, hp)$ satisfies the predicate $p$.

Multiset.subsingletonEquiv definition

[Subsingleton α] : List α ≃ Multiset α

Full source

/-- The equivalence between lists and multisets of a subsingleton type. -/
def subsingletonEquiv [Subsingleton α] : ListList α ≃ Multiset α where
  toFun := ofList
  invFun :=
    (Quot.lift id) fun (a b : List α) (h : a ~ b) =>
      (List.ext_get h.length_eq) fun _ _ _ => Subsingleton.elim _ _
  left_inv _ := rfl
  right_inv m := Quot.inductionOn m fun _ => rfl

Equivalence between lists and multisets for subsingleton types

Informal description

Given a type $\alpha$ that is a subsingleton (i.e., all elements are equal), there is a natural equivalence between lists over $\alpha$ and multisets over $\alpha$. The forward direction maps a list to the corresponding multiset, while the inverse direction maps a multiset back to a list (which is well-defined since all elements are equal).

Multiset.coe_subsingletonEquiv theorem

[Subsingleton α] : (subsingletonEquiv α : List α → Multiset α) = ofList

Full source

@[simp]
theorem coe_subsingletonEquiv [Subsingleton α] :
    (subsingletonEquiv α : List α → Multiset α) = ofList :=
  rfl

Canonical Embedding of Lists as Multisets for Subsingleton Types

Informal description

For a subsingleton type $\alpha$ (where all elements are equal), the function `subsingletonEquiv α` from lists to multisets is equal to the canonical embedding `ofList`.

Multiset.sizeOf_lt_sizeOf_of_mem theorem

[SizeOf α] {x : α} {s : Multiset α} (hx : x ∈ s) : SizeOf.sizeOf x < SizeOf.sizeOf s

Full source

@[deprecated "Deprecated without replacement." (since := "2025-02-07")]
theorem sizeOf_lt_sizeOf_of_mem [SizeOf α] {x : α} {s : Multiset α} (hx : x ∈ s) :
    SizeOf.sizeOf x < SizeOf.sizeOf s := by
  induction s using Quot.inductionOn
  exact List.sizeOf_lt_sizeOf_of_mem hx

Size Comparison for Elements in a Multiset: $\text{sizeOf}(x) < \text{sizeOf}(s)$ if $x \in s$

Informal description

For any type $\alpha$ with a `SizeOf` instance, if an element $x \in \alpha$ is a member of a multiset $s$ (i.e., $x \in s$), then the size of $x$ is strictly less than the size of $s$.