Mathlib.Data.Multiset.Sort

Multiset.sort definition

(s : Multiset α) : List α

Full source

/-- `sort s` constructs a sorted list from the multiset `s`.
  (Uses merge sort algorithm.) -/
def sort (s : Multiset α) : List α :=
  Quot.liftOn s (mergeSort · (r · ·)) fun _ _ h =>
    eq_of_perm_of_sorted ((mergeSort_perm _ _).trans <| h.trans (mergeSort_perm _ _).symm)
      (sorted_mergeSort IsTrans.trans
        (fun a b => by simpa using IsTotal.total a b) _)
      (sorted_mergeSort IsTrans.trans
        (fun a b => by simpa using IsTotal.total a b) _)

Sorted list from multiset via merge sort

Informal description

Given a multiset `s` over a type `α`, the function `sort` constructs a sorted list from `s` using the merge sort algorithm. The resulting list is sorted with respect to the relation `r`.

Multiset.coe_sort theorem

(l : List α) : sort r l = mergeSort l (r · ·)

Full source

@[simp]
theorem coe_sort (l : List α) : sort r l = mergeSort l (r · ·) :=
  rfl

Sorted Multiset from List via Merge Sort: $\text{sort}_r(l) = \text{mergeSort}_r(l)$

Informal description

For any list `l` of elements of type `α`, the sorted multiset constructed from `l` using the relation `r` is equal to the result of applying the merge sort algorithm to `l` with respect to `r`. That is, $\text{sort}_r(l) = \text{mergeSort}_r(l)$.

Multiset.sort_sorted theorem

(s : Multiset α) : Sorted r (sort r s)

Full source

@[simp]
theorem sort_sorted (s : Multiset α) : Sorted r (sort r s) :=
  Quot.inductionOn s (sorted_mergeSort' _)

Sortedness of Multiset Merge Sort

Informal description

For any multiset $s$ over a type $\alpha$, the list obtained by sorting $s$ with respect to a relation $r$ is sorted with respect to $r$.

Multiset.sort_eq theorem

(s : Multiset α) : ↑(sort r s) = s

Full source

@[simp]
theorem sort_eq (s : Multiset α) : ↑(sort r s) = s :=
  Quot.inductionOn s fun _ => Quot.sound <| mergeSort_perm _ _

Sorted List from Multiset Preserves Elements

Informal description

For any multiset $s$ over a type $\alpha$, the underlying multiset of the sorted list obtained from $s$ via merge sort is equal to $s$ itself, i.e., $\overline{\text{sort}(r, s)} = s$.

Multiset.mem_sort theorem

{s : Multiset α} {a : α} : a ∈ sort r s ↔ a ∈ s

Full source

@[simp]
theorem mem_sort {s : Multiset α} {a : α} : a ∈ sort r sa ∈ sort r s ↔ a ∈ s := by rw [← mem_coe, sort_eq]

Membership Preservation in Sorted List from Multiset: $a \in \mathrm{sort}_r(s) \leftrightarrow a \in s$

Informal description

For any multiset $s$ over a type $\alpha$ and any element $a \in \alpha$, the element $a$ belongs to the sorted list $\mathrm{sort}_r(s)$ if and only if $a$ belongs to the multiset $s$.

Multiset.length_sort theorem

{s : Multiset α} : (sort r s).length = card s

Full source

@[simp]
theorem length_sort {s : Multiset α} : (sort r s).length = card s :=
  Quot.inductionOn s <| length_mergeSort

Length of Sorted List Equals Multiset Cardinality

Informal description

For any multiset $s$ over a type $\alpha$, the length of the sorted list obtained from $s$ via merge sort is equal to the cardinality of $s$.

Multiset.sort_zero theorem

: sort r 0 = []

Full source

@[simp]
theorem sort_zero : sort r 0 = [] :=
  List.mergeSort_nil

Empty multiset sorts to empty list: $\mathrm{sort}_r(0) = []$

Informal description

The sorted list of the empty multiset is the empty list, i.e., $\mathrm{sort}_r(0) = []$.

Multiset.sort_singleton theorem

(a : α) : sort r { a } = [a]

Full source

@[simp]
theorem sort_singleton (a : α) : sort r {a} = [a] :=
  List.mergeSort_singleton a

Sorted list of singleton multiset is singleton list

Informal description

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

Multiset.map_sort theorem

 (f : α → β) (s : Multiset α) (hs : ∀ a ∈ s, ∀ b ∈ s, r a b ↔ r' (f a) (f b)) : (s.sort r).map f = (s.map f).sort r'

Full source

theorem map_sort (f : α → β) (s : Multiset α)
    (hs : ∀ a ∈ s, ∀ b ∈ s, r a b ↔ r' (f a) (f b)) :
    (s.sort r).map f = (s.map f).sort r' := by
  revert s
  exact Quot.ind fun l h => map_mergeSort (l := l) (by simpa using h)

Mapping Preserves Sorted Lists of Multisets

Informal description

Let $f : \alpha \to \beta$ be a function, $s$ be a multiset over $\alpha$, and suppose that for any elements $a, b \in s$, the relation $r(a, b)$ holds if and only if $r'(f(a), f(b))$ holds. Then the sorted list obtained by applying $f$ to each element of the sorted list of $s$ (with respect to $r$) is equal to the sorted list (with respect to $r'$) of the multiset obtained by applying $f$ to each element of $s$.

Multiset.sort_cons theorem

(a : α) (s : Multiset α) : (∀ b ∈ s, r a b) → sort r (a ::ₘ s) = a :: sort r s

Full source

theorem sort_cons (a : α) (s : Multiset α) :
    (∀ b ∈ s, r a b) → sort r (a ::ₘ s) = a :: sort r s := by
  refine Quot.inductionOn s fun l => ?_
  simpa [mergeSort_eq_insertionSort] using insertionSort_cons r (a := a) (l := l)

Consistency of Sorting with Cons Operation in Multisets

Informal description

For any element $a$ of type $\alpha$ and any multiset $s$ over $\alpha$, if $a$ is related to every element $b$ in $s$ by the relation $r$ (i.e., $\forall b \in s, r(a, b)$), then the sorted list of the multiset $a$ cons $s$ with respect to $r$ is equal to $a$ cons the sorted list of $s$ with respect to $r$. In other words, $\text{sort}_r(a \cup s) = a :: \text{sort}_r(s)$ under the given condition.

Multiset.sort_range theorem

(n : ℕ) : sort (· ≤ ·) (range n) = List.range n

Full source

@[simp]
theorem sort_range (n : ℕ) : sort (· ≤ ·) (range n) = List.range n :=
  List.mergeSort_eq_self _ (sorted_le_range n)

Sorted Range Multiset Equals Range List

Informal description

For any natural number $n$, the sorted list (with respect to the standard ordering $\leq$) of the multiset containing the elements $\{0, 1, \dots, n-1\}$ is equal to the list $[0, 1, \dots, n-1]$.

Multiset.instToExprOfToLevel instance

{α : Type u} [Lean.ToLevel.{u}] [Lean.ToExpr α] : Lean.ToExpr (Multiset α)

Full source

unsafe instance {α : Type u} [Lean.ToLevelLean.ToLevel.{u}] [Lean.ToExpr α] :
    Lean.ToExpr (Multiset α) :=
  haveI u' := Lean.toLevel.{u}
  haveI α' : Q(Type u') := Lean.toTypeExpr α
  { toTypeExpr := q(Multiset $α')
    toExpr s := show Q(Multiset $α') from
      if Multiset.card s = 0 then
        q(0)
      else
        mkSetLiteralQ (α := q($α')) q(Multiset $α') (s.unquot.map Lean.toExpr)}

Expression Representation of Multisets

Informal description

For any type $\alpha$ that can be represented as an expression in Lean, the multiset of elements of type $\alpha$ can also be represented as an expression.

Multiset.instRepr instance

[Repr α] : Repr (Multiset α)

Full source

unsafe instance [Repr α] : Repr (Multiset α) where
  reprPrec s _ :=
    if Multiset.card s = 0 then
      "0"
    else
      Std.Format.bracket "{" (Std.Format.joinSep (s.unquot.map repr) ("," ++ Std.Format.line)) "}"

Representation of Multisets

Informal description

For any type $\alpha$ with a representation function, the multiset of elements of type $\alpha$ also has a representation function.