Mathlib.Data.List.Sort

List.Sorted definition

Full source

/-- `Sorted r l` is the same as `List.Pairwise r l`, preferred in the case that `r`
  is a `<` or `≤`-like relation (transitive and antisymmetric or asymmetric) -/
def Sorted :=
  @Pairwise

Sorted list with respect to a relation

Informal description

A list `l` is said to be `Sorted` with respect to a relation `r` if the elements of `l` are pairwise related by `r`. This definition is preferred when `r` is a `<` or `≤`-like relation (i.e., transitive and antisymmetric or asymmetric).

List.decidableSorted instance

[DecidableRel r] (l : List α) : Decidable (Sorted r l)

Full source

instance decidableSorted [DecidableRel r] (l : List α) : Decidable (Sorted r l) :=
  List.instDecidablePairwise _

Decidability of List Sorting with Respect to a Decidable Relation

Informal description

For any decidable relation `r` on a type `α`, the predicate `List.Sorted r` on lists of elements of `α` is decidable. That is, given a list `l : List α`, we can algorithmically determine whether `l` is sorted with respect to `r`.

List.Sorted.le_of_lt theorem

[Preorder α] {l : List α} (h : l.Sorted (· < ·)) : l.Sorted (· ≤ ·)

Full source

protected theorem Sorted.le_of_lt [Preorder α] {l : List α} (h : l.Sorted (· < ·)) :
    l.Sorted (· ≤ ·) :=
  h.imp le_of_lt

Strictly Sorted List is Non-Strictly Sorted

Informal description

Let $\alpha$ be a type equipped with a preorder. For any list $l$ of elements of $\alpha$, if $l$ is sorted with respect to the strict order relation $<$, then $l$ is also sorted with respect to the non-strict order relation $\leq$.

List.Sorted.lt_of_le theorem

[PartialOrder α] {l : List α} (h₁ : l.Sorted (· ≤ ·)) (h₂ : l.Nodup) : l.Sorted (· < ·)

Full source

protected theorem Sorted.lt_of_le [PartialOrder α] {l : List α} (h₁ : l.Sorted (· ≤ ·))
    (h₂ : l.Nodup) : l.Sorted (· < ·) :=
  h₁.imp₂ (fun _ _ => lt_of_le_of_ne) h₂

Strict Sorting from Non-Strict Sorting and No Duplicates: $\text{Sorted}(\leq, l) \land \text{Nodup}(l) \implies \text{Sorted}(<, l)$

Informal description

Let $\alpha$ be a type equipped with a partial order. For any list $l$ of elements of $\alpha$, if $l$ is sorted with respect to the non-strict order relation $\leq$ and $l$ has no duplicate elements, then $l$ is also sorted with respect to the strict order relation $<$.

List.Sorted.ge_of_gt theorem

[Preorder α] {l : List α} (h : l.Sorted (· > ·)) : l.Sorted (· ≥ ·)

Full source

protected theorem Sorted.ge_of_gt [Preorder α] {l : List α} (h : l.Sorted (· > ·)) :
    l.Sorted (· ≥ ·) :=
  h.imp le_of_lt

Sorted List under $>$ Implies Sorted under $\geq$

Informal description

For any list $l$ of elements in a preorder $\alpha$, if $l$ is sorted with respect to the strict greater-than relation $>$, then $l$ is also sorted with respect to the non-strict greater-than-or-equal relation $\geq$.

List.Sorted.gt_of_ge theorem

[PartialOrder α] {l : List α} (h₁ : l.Sorted (· ≥ ·)) (h₂ : l.Nodup) : l.Sorted (· > ·)

Full source

protected theorem Sorted.gt_of_ge [PartialOrder α] {l : List α} (h₁ : l.Sorted (· ≥ ·))
    (h₂ : l.Nodup) : l.Sorted (· > ·) :=
  h₁.imp₂ (fun _ _ => lt_of_le_of_ne) <| by simp_rw [ne_comm]; exact h₂

Sorted List under $\geq$ with No Duplicates Implies Sorted under $>$

Informal description

For any list $l$ of elements in a partially ordered set $\alpha$, if $l$ is sorted with respect to the relation $\geq$ and has no duplicate elements, then $l$ is also sorted with respect to the relation $>$.

List.sorted_nil theorem

: Sorted r []

Full source

@[simp]
theorem sorted_nil : Sorted r [] :=
  Pairwise.nil

Empty List is Sorted

Informal description

The empty list is sorted with respect to any relation $r$.

List.Sorted.of_cons theorem

: Sorted r (a :: l) → Sorted r l

Full source

theorem Sorted.of_cons : Sorted r (a :: l) → Sorted r l :=
  Pairwise.of_cons

Sublist of Sorted List is Sorted

Informal description

If a list $a :: l$ is sorted with respect to a relation $r$, then the sublist $l$ is also sorted with respect to $r$.

List.Sorted.tail theorem

{r : α → α → Prop} {l : List α} (h : Sorted r l) : Sorted r l.tail

Full source

theorem Sorted.tail {r : α → α → Prop} {l : List α} (h : Sorted r l) : Sorted r l.tail :=
  Pairwise.tail h

Tail of a Sorted List is Sorted

Informal description

For any relation $r$ on a type $\alpha$ and any list $l$ of elements of $\alpha$, if $l$ is sorted with respect to $r$, then the tail of $l$ is also sorted with respect to $r$.

List.rel_of_sorted_cons theorem

{a : α} {l : List α} : Sorted r (a :: l) → ∀ b ∈ l, r a b

Full source

theorem rel_of_sorted_cons {a : α} {l : List α} : Sorted r (a :: l) → ∀ b ∈ l, r a b :=
  rel_of_pairwise_cons

Head Element Relates to All in Sorted List

Informal description

For any element $a$ and list $l$, if the list $a :: l$ is sorted with respect to a relation $r$, then for every element $b$ in $l$, the relation $r(a, b)$ holds.

List.Sorted.cons theorem

 {r : α → α → Prop} [IsTrans α r] {l : List α} {a b : α} (hab : r a b) (h : Sorted r (b :: l)) : Sorted r (a :: b :: l)

Full source

nonrec theorem Sorted.cons {r : α → α → Prop} [IsTrans α r] {l : List α} {a b : α}
    (hab : r a b) (h : Sorted r (b :: l)) : Sorted r (a :: b :: l) :=
  h.cons <| forall_mem_cons.2 ⟨hab, fun _ hx => _root_.trans hab <| rel_of_sorted_cons h _ hx⟩

Conservation of Sortedness Under Prepend in Transitive Relations

Informal description

Let $r$ be a transitive binary relation on a type $\alpha$. For any list $l$ of elements of $\alpha$ and any elements $a, b \in \alpha$, if $r(a, b)$ holds and the list $b :: l$ is sorted with respect to $r$, then the list $a :: b :: l$ is also sorted with respect to $r$.

List.sorted_cons_cons theorem

 {r : α → α → Prop} [IsTrans α r] {l : List α} {a b : α} : Sorted r (b :: a :: l) ↔ r b a ∧ Sorted r (a :: l)

Full source

theorem sorted_cons_cons {r : α → α → Prop} [IsTrans α r] {l : List α} {a b : α} :
    SortedSorted r (b :: a :: l) ↔ r b a ∧ Sorted r (a :: l) := by
  constructor
  · intro h
    exact ⟨rel_of_sorted_cons h _ mem_cons_self, h.of_cons⟩
  · rintro ⟨h, ha⟩
    exact ha.cons h

Characterization of Sortedness for Two-Element Prefix in Transitive Relations

Informal description

Let $r$ be a transitive binary relation on a type $\alpha$. For any list $l$ of elements of $\alpha$ and any elements $a, b \in \alpha$, the list $b :: a :: l$ is sorted with respect to $r$ if and only if $r(b, a)$ holds and the list $a :: l$ is sorted with respect to $r$.

List.Sorted.head!_le theorem

[Inhabited α] [Preorder α] {a : α} {l : List α} (h : Sorted (· < ·) l) (ha : a ∈ l) : l.head! ≤ a

Full source

theorem Sorted.head!_le [Inhabited α] [Preorder α] {a : α} {l : List α} (h : Sorted (· < ·) l)
    (ha : a ∈ l) : l.head! ≤ a := by
  rw [← List.cons_head!_tail (List.ne_nil_of_mem ha)] at h ha
  cases ha
  · exact le_rfl
  · exact le_of_lt (rel_of_sorted_cons h a (by assumption))

Head of Strictly Sorted List is Minimal Element

Informal description

Let $\alpha$ be a type with a preorder and inhabited instance. For any list $l$ of elements of $\alpha$ that is sorted with respect to the strict order $<$, and any element $a \in l$, the head of $l$ (with a default value if $l$ is empty) is less than or equal to $a$.

List.Sorted.le_head! theorem

[Inhabited α] [Preorder α] {a : α} {l : List α} (h : Sorted (· > ·) l) (ha : a ∈ l) : a ≤ l.head!

Full source

theorem Sorted.le_head! [Inhabited α] [Preorder α] {a : α} {l : List α} (h : Sorted (· > ·) l)
    (ha : a ∈ l) : a ≤ l.head! := by
  rw [← List.cons_head!_tail (List.ne_nil_of_mem ha)] at h ha
  cases ha
  · exact le_rfl
  · exact le_of_lt (rel_of_sorted_cons h a (by assumption))

Head Element is Greatest in Decreasingly Sorted List

Informal description

Let $\alpha$ be a type with a preorder and an inhabited instance. For any list $l$ of elements of $\alpha$ sorted in decreasing order with respect to the relation $>$, and any element $a \in l$, we have $a \leq \text{head!}(l)$, where $\text{head!}(l)$ is the first element of $l$ (with a default value if $l$ is empty).

List.sorted_cons theorem

{a : α} {l : List α} : Sorted r (a :: l) ↔ (∀ b ∈ l, r a b) ∧ Sorted r l

Full source

@[simp]
theorem sorted_cons {a : α} {l : List α} : SortedSorted r (a :: l) ↔ (∀ b ∈ l, r a b) ∧ Sorted r l :=
  pairwise_cons

Characterization of Sorted Lists via Head and Tail Relation

Informal description

For any element $a$ and list $l$ of type $\alpha$, the list $a :: l$ is sorted with respect to a relation $r$ if and only if $r(a, b)$ holds for every element $b$ in $l$, and $l$ itself is sorted with respect to $r$.

List.Sorted.nodup theorem

{r : α → α → Prop} [IsIrrefl α r] {l : List α} (h : Sorted r l) : Nodup l

Full source

protected theorem Sorted.nodup {r : α → α → Prop} [IsIrrefl α r] {l : List α} (h : Sorted r l) :
    Nodup l :=
  Pairwise.nodup h

Sorted Lists with Irreflexive Relations Have No Duplicates

Informal description

For any irreflexive relation $r$ on a type $\alpha$ and any list $l$ of elements of $\alpha$, if $l$ is sorted with respect to $r$, then $l$ has no duplicate elements.

List.Sorted.filter theorem

{l : List α} (f : α → Bool) (h : Sorted r l) : Sorted r (filter f l)

Full source

protected theorem Sorted.filter {l : List α} (f : α → Bool) (h : Sorted r l) :
    Sorted r (filter f l) :=
  h.sublist filter_sublist

Preservation of Sorting Under Filtering

Informal description

For any list $l$ sorted with respect to a relation $r$, and any predicate $f$ on elements of $l$, the filtered list obtained by applying $f$ to $l$ remains sorted with respect to $r$.

List.sublist_of_subperm_of_sorted theorem

 [IsAntisymm α r] {l₁ l₂ : List α} (hp : l₁ <+~ l₂) (hs₁ : l₁.Sorted r) (hs₂ : l₂.Sorted r) : l₁ <+ l₂

Full source

theorem sublist_of_subperm_of_sorted [IsAntisymm α r] {l₁ l₂ : List α} (hp : l₁ <+~ l₂)
    (hs₁ : l₁.Sorted r) (hs₂ : l₂.Sorted r) : l₁ <+ l₂ := by
  let ⟨_, h, h'⟩ := hp
  rwa [← eq_of_perm_of_sorted h (hs₂.sublist h') hs₁]

Sublist Property for Sorted Subpermutations under Antisymmetric Relations

Informal description

Let $r$ be an antisymmetric relation on a type $\alpha$, and let $l_1$ and $l_2$ be lists of elements of $\alpha$. If $l_1$ is a subpermutation of $l_2$ (denoted $l_1 <+~ l_2$), and both $l_1$ and $l_2$ are sorted with respect to $r$, then $l_1$ is a sublist of $l_2$ (denoted $l_1 <+ l_2$).

List.sorted_singleton theorem

(a : α) : Sorted r [a]

Full source

@[simp 1100] -- Higher priority shortcut lemma.
theorem sorted_singleton (a : α) : Sorted r [a] := by
  simp

Singleton List is Sorted

Informal description

For any element $a$ of type $\alpha$, the singleton list $[a]$ is sorted with respect to any relation $r$.

List.sorted_lt_range theorem

(n : ℕ) : Sorted (· < ·) (range n)

Full source

theorem sorted_lt_range (n : ℕ) : Sorted (· < ·) (range n) := by
  rw [Sorted, pairwise_iff_get]
  simp

Range List is Strictly Increasing

Informal description

For any natural number $n$, the list `range n` (which is the list `[0, 1, ..., n-1]`) is sorted with respect to the strict less-than relation `<`.

List.sorted_replicate theorem

(n : ℕ) (a : α) : Sorted r (replicate n a) ↔ n ≤ 1 ∨ r a a

Full source

theorem sorted_replicate (n : ℕ) (a : α) : SortedSorted r (replicate n a) ↔ n ≤ 1 ∨ r a a :=
  pairwise_replicate

Sorted Replicate List Condition: $n \leq 1$ or $r(a, a)$

Informal description

For any natural number $n$ and element $a$ of type $\alpha$, the list obtained by replicating $a$ $n$ times is sorted with respect to a relation $r$ if and only if either $n \leq 1$ or $r(a, a)$ holds.

List.sorted_le_replicate theorem

(n : ℕ) (a : α) [Preorder α] : Sorted (· ≤ ·) (replicate n a)

Full source

theorem sorted_le_replicate (n : ℕ) (a : α) [Preorder α] : Sorted (· ≤ ·) (replicate n a) := by
  simp [sorted_replicate]

Replicated List is Non-Strictly Increasing

Informal description

For any natural number $n$ and element $a$ of type $\alpha$ equipped with a preorder, the list obtained by replicating $a$ $n$ times is sorted with respect to the non-strict less-than-or-equal-to relation $\leq$.

List.sorted_le_range theorem

(n : ℕ) : Sorted (· ≤ ·) (range n)

Full source

theorem sorted_le_range (n : ℕ) : Sorted (· ≤ ·) (range n) :=
  (sorted_lt_range n).le_of_lt

Range List is Non-Strictly Increasing

Informal description

For any natural number $n$, the list `[0, 1, ..., n-1]` is sorted with respect to the non-strict less-than-or-equal-to relation $\leq$.

List.sorted_lt_range' theorem

(a b) {s} (hs : s ≠ 0) : Sorted (· < ·) (range' a b s)

Full source

lemma sorted_lt_range' (a b) {s} (hs : s ≠ 0) :
    Sorted (· < ·) (range' a b s) := by
  induction b generalizing a with
  | zero => simp
  | succ n ih =>
    rw [List.range'_succ]
    refine List.sorted_cons.mpr ⟨fun b hb ↦ ?_, @ih (a + s)⟩
    exact lt_of_lt_of_le (Nat.lt_add_of_pos_right (Nat.zero_lt_of_ne_zero hs))
      (List.left_le_of_mem_range' hb)

Strictly Increasing Property of Range' with Non-Zero Step

Informal description

For any natural numbers $a$, $b$, and a non-zero step size $s$, the list $\text{range'}(a, b, s)$ is strictly increasing (sorted with respect to the strict less-than relation $<$).

List.sorted_le_range' theorem

(a b s) : Sorted (· ≤ ·) (range' a b s)

Full source

lemma sorted_le_range' (a b s) :
    Sorted (· ≤ ·) (range' a b s) := by
  by_cases hs : s ≠ 0
  · exact (sorted_lt_range' a b hs).le_of_lt
  · rw [ne_eq, Decidable.not_not] at hs
    simpa [hs] using sorted_le_replicate b a

Non-Strictly Increasing Property of Range' with Any Step Size

Informal description

For any natural numbers $a$, $b$, and step size $s$, the list $\text{range'}(a, b, s)$ is sorted with respect to the non-strict less-than-or-equal-to relation $\leq$.

List.Sorted.rel_get_of_lt theorem

{l : List α} (h : l.Sorted r) {a b : Fin l.length} (hab : a < b) : r (l.get a) (l.get b)

Full source

theorem Sorted.rel_get_of_lt {l : List α} (h : l.Sorted r) {a b : Fin l.length} (hab : a < b) :
    r (l.get a) (l.get b) :=
  List.pairwise_iff_get.1 h _ _ hab

Relation Holds for Elements in Sorted List at Increasing Indices

Informal description

Let $l$ be a list of elements of type $\alpha$ that is sorted with respect to a relation $r$. For any two indices $a$ and $b$ in the list (represented as elements of $\text{Fin } l.\text{length}$), if $a < b$, then $r(l_a, l_b)$ holds, where $l_a$ and $l_b$ denote the elements of $l$ at positions $a$ and $b$ respectively.

List.Sorted.rel_get_of_le theorem

[IsRefl α r] {l : List α} (h : l.Sorted r) {a b : Fin l.length} (hab : a ≤ b) : r (l.get a) (l.get b)

Full source

theorem Sorted.rel_get_of_le [IsRefl α r] {l : List α} (h : l.Sorted r) {a b : Fin l.length}
    (hab : a ≤ b) : r (l.get a) (l.get b) := by
  obtain rfl | hlt := Fin.eq_or_lt_of_le hab; exacts [refl _, h.rel_get_of_lt hlt]

Relation Holds for Elements in Sorted List at Non-Decreasing Indices

Informal description

Let $r$ be a reflexive relation on a type $\alpha$ and $l$ be a list of elements of $\alpha$ that is sorted with respect to $r$. For any two indices $a$ and $b$ in the list (represented as elements of $\text{Fin } l.\text{length}$), if $a \leq b$, then $r(l_a, l_b)$ holds, where $l_a$ and $l_b$ denote the elements of $l$ at positions $a$ and $b$ respectively.

List.Sorted.rel_of_mem_take_of_mem_drop theorem

{l : List α} (h : List.Sorted r l) {k : ℕ} {x y : α} (hx : x ∈ List.take k l) (hy : y ∈ List.drop k l) : r x y

Full source

theorem Sorted.rel_of_mem_take_of_mem_drop {l : List α} (h : List.Sorted r l) {k : ℕ} {x y : α}
    (hx : x ∈ List.take k l) (hy : y ∈ List.drop k l) : r x y := by
  obtain ⟨iy, hiy, rfl⟩ := getElem_of_mem hy
  obtain ⟨ix, hix, rfl⟩ := getElem_of_mem hx
  rw [getElem_take, getElem_drop]
  rw [length_take] at hix
  exact h.rel_get_of_lt (Nat.lt_add_right _ (Nat.lt_min.mp hix).left)

Relation Holds Between Elements in Take and Drop of Sorted List

Informal description

Let $l$ be a list of elements of type $\alpha$ that is sorted with respect to a relation $r$. For any natural number $k$ and elements $x, y \in \alpha$, if $x$ is in the first $k$ elements of $l$ (i.e., $x \in \text{take}\ k\ l$) and $y$ is in the remaining elements of $l$ (i.e., $y \in \text{drop}\ k\ l$), then $r(x, y)$ holds.

List.Sorted.decide theorem

[DecidableRel r] (l : List α) (h : Sorted r l) : Sorted (fun a b => decide (r a b) = true) l

Full source

/--
If a list is sorted with respect to a decidable relation,
then it is sorted with respect to the corresponding Bool-valued relation.
-/
theorem Sorted.decide [DecidableRel r] (l : List α) (h : Sorted r l) :
    Sorted (fun a b => decide (r a b) = true) l := by
  refine h.imp fun {a b} h => by simpa using h

Preservation of Sorting under Boolean Decidability

Informal description

Let $r$ be a decidable relation on a type $\alpha$ and $l$ be a list of elements of $\alpha$. If $l$ is sorted with respect to $r$, then $l$ is also sorted with respect to the Boolean-valued relation $\lambda a b, \text{decide}(r\ a\ b) = \text{true}$.

List.sorted_ofFn_iff theorem

{r : α → α → Prop} : (ofFn f).Sorted r ↔ ((· < ·) ⇒ r) f f

Full source

theorem sorted_ofFn_iff {r : α → α → Prop} : (ofFn f).Sorted r ↔ ((· < ·) ⇒ r) f f := by
  simp_rw [Sorted, pairwise_iff_get, get_ofFn, Relator.LiftFun]
  exact Iff.symm (Fin.rightInverse_cast _).surjective.forall₂

Characterization of Sortedness for Lists Generated from Finite Functions

Informal description

For any relation $r$ on a type $\alpha$ and any function $f : \text{Fin } n \to \alpha$, the list $\text{ofFn } f$ is sorted with respect to $r$ if and only if the function $f$ satisfies the implication that for any two indices $i, j \in \text{Fin } n$, if $i < j$ then $r(f(i), f(j))$ holds.

List.sorted_lt_ofFn_iff theorem

: (ofFn f).Sorted (· < ·) ↔ StrictMono f

Full source

/-- The list `List.ofFn f` is strictly sorted with respect to `(· ≤ ·)` if and only if `f` is
strictly monotone. -/
@[simp] theorem sorted_lt_ofFn_iff : (ofFn f).Sorted (· < ·) ↔ StrictMono f := sorted_ofFn_iff

Strictly sorted list characterization via strict monotonicity of $f$

Informal description

For any function $f : \text{Fin } n \to \alpha$ where $\alpha$ is a preorder, the list $\text{ofFn } f$ is strictly sorted with respect to the relation $<$ if and only if $f$ is strictly monotone (i.e., for any $i, j \in \text{Fin } n$, $i < j$ implies $f(i) < f(j)$).

List.sorted_gt_ofFn_iff theorem

: (ofFn f).Sorted (· > ·) ↔ StrictAnti f

Full source

/-- The list `List.ofFn f` is strictly sorted with respect to `(· ≥ ·)` if and only if `f` is
strictly antitone. -/
@[simp] theorem sorted_gt_ofFn_iff : (ofFn f).Sorted (· > ·) ↔ StrictAnti f := sorted_ofFn_iff

Characterization of Strictly Antitone Functions via Strictly Decreasing Lists

Informal description

For a function $f : \text{Fin } n \to \alpha$ where $\alpha$ is a preorder, the list $\text{ofFn } f$ is sorted with respect to the strict greater-than relation $>$ if and only if $f$ is strictly antitone (i.e., for any $i, j \in \text{Fin } n$, $i < j$ implies $f(j) < f(i)$).

List.sorted_le_ofFn_iff theorem

: (ofFn f).Sorted (· ≤ ·) ↔ Monotone f

Full source

/-- The list `List.ofFn f` is sorted with respect to `(· ≤ ·)` if and only if `f` is monotone. -/
@[simp] theorem sorted_le_ofFn_iff : (ofFn f).Sorted (· ≤ ·) ↔ Monotone f :=
  sorted_ofFn_iff.trans monotone_iff_forall_lt.symm

Characterization of Monotone Functions via Sorted Lists with Respect to $\leq$

Informal description

For any function $f : \text{Fin } n \to \alpha$ where $\alpha$ is a preorder, the list $\text{ofFn } f$ is sorted with respect to the relation $\leq$ if and only if $f$ is monotone (i.e., for any $i, j \in \text{Fin } n$, $i \leq j$ implies $f(i) \leq f(j)$).

List.sorted_ge_ofFn_iff theorem

: (ofFn f).Sorted (· ≥ ·) ↔ Antitone f

Full source

/-- The list `List.ofFn f` is sorted with respect to `(· ≥ ·)` if and only if `f` is antitone. -/
@[simp] theorem sorted_ge_ofFn_iff : (ofFn f).Sorted (· ≥ ·) ↔ Antitone f :=
  sorted_ofFn_iff.trans antitone_iff_forall_lt.symm

Characterization of Antitone Functions via Sorted Lists with Respect to $\geq$

Informal description

For a function $f : \text{Fin } n \to \alpha$ where $\alpha$ is a preorder, the list $\text{ofFn } f$ is sorted with respect to the relation $\geq$ if and only if $f$ is antitone (i.e., for any $i, j \in \text{Fin } n$, $i \leq j$ implies $f(j) \leq f(i)$).

List.Sorted.filterMap theorem

 {α β : Type*} {p : α → Option β} {l : List α} {r : α → α → Prop} {r' : β → β → Prop} (hl : l.Sorted r)
  (hp : ∀ (a b : α) (c d : β), p a = some c → p b = some d → r a b → r' c d) : (l.filterMap p).Sorted r'

Full source

lemma Sorted.filterMap {α β : Type*} {p : α → Option β} {l : List α}
    {r : α → α → Prop} {r' : β → β → Prop} (hl : l.Sorted r)
    (hp : ∀ (a b : α) (c d : β), p a = some c → p b = some d → r a b → r' c d) :
    (l.filterMap p).Sorted r' := by
  induction l with
  | nil => simp
  | cons a l ih =>
    rw [List.filterMap_cons]
    cases ha : p a with
    | none =>
      exact ih (List.sorted_cons.mp hl).right
    | some b =>
      rw [List.sorted_cons]
      refine ⟨fun x hx ↦ ?_, ih (List.sorted_cons.mp hl).right⟩
      obtain ⟨u, hu, hu'⟩ := List.mem_filterMap.mp hx
      exact hp a u b x ha hu' <| (List.sorted_cons.mp hl).left u hu

Preservation of Sortedness under `filterMap` with Relation Compatibility

Informal description

Let $\alpha$ and $\beta$ be types, $p : \alpha \to \text{Option } \beta$ a function, $l$ a list of elements of $\alpha$, and $r$, $r'$ relations on $\alpha$ and $\beta$ respectively. If $l$ is sorted with respect to $r$, and for any $a, b \in \alpha$ and $c, d \in \beta$ such that $p(a) = \text{some } c$, $p(b) = \text{some } d$, and $r(a, b)$ holds, then $r'(c, d)$ holds, then the list obtained by applying `filterMap p` to $l$ is sorted with respect to $r'$.

RelEmbedding.sorted_listMap theorem

(e : ra ↪r rb) {l : List α} : (l.map e).Sorted rb ↔ l.Sorted ra

Full source

@[simp]
theorem sorted_listMap (e : ra ↪r rb) {l : List α} : (l.map e).Sorted rb ↔ l.Sorted ra := by
  simp [Sorted, pairwise_map, e.map_rel_iff]

Preservation of List Sortedness under Relation Embedding

Informal description

Let $e : (\alpha, r_a) \hookrightarrow (\beta, r_b)$ be a relation embedding between types $\alpha$ and $\beta$ with respect to relations $r_a$ and $r_b$. For any list $l$ of elements of $\alpha$, the mapped list $e(l)$ is sorted with respect to $r_b$ if and only if $l$ is sorted with respect to $r_a$.

RelEmbedding.sorted_swap_listMap theorem

(e : ra ↪r rb) {l : List α} : (l.map e).Sorted (Function.swap rb) ↔ l.Sorted (Function.swap ra)

Full source

@[simp]
theorem sorted_swap_listMap (e : ra ↪r rb) {l : List α} :
    (l.map e).Sorted (Function.swap rb) ↔ l.Sorted (Function.swap ra) := by
  simp [Sorted, pairwise_map, e.map_rel_iff]

Preservation of List Sortedness under Relation Embedding with Swapped Relations

Informal description

Let $e : (\alpha, r_a) \hookrightarrow (\beta, r_b)$ be a relation embedding between types $\alpha$ and $\beta$ with respect to relations $r_a$ and $r_b$. For any list $l$ of elements of $\alpha$, the mapped list $e(l)$ is sorted with respect to the swapped relation $\operatorname{swap} r_b$ (where $\operatorname{swap} r_b\, y\, x = r_b\, x\, y$) if and only if $l$ is sorted with respect to the swapped relation $\operatorname{swap} r_a$.

OrderEmbedding.sorted_lt_listMap theorem

(e : α ↪o β) {l : List α} : (l.map e).Sorted (· < ·) ↔ l.Sorted (· < ·)

Full source

@[simp]
theorem sorted_lt_listMap (e : α ↪o β) {l : List α} :
    (l.map e).Sorted (· < ·) ↔ l.Sorted (· < ·) :=
  e.ltEmbedding.sorted_listMap

Preservation of List Sortedness under Strict Order Embedding

Informal description

Let $e : \alpha \hookrightarrow \beta$ be an order embedding between two preordered types $\alpha$ and $\beta$. For any list $l$ of elements of $\alpha$, the mapped list $e(l)$ is sorted with respect to the strict order $<$ on $\beta$ if and only if $l$ is sorted with respect to the strict order $<$ on $\alpha$.

OrderEmbedding.sorted_gt_listMap theorem

(e : α ↪o β) {l : List α} : (l.map e).Sorted (· > ·) ↔ l.Sorted (· > ·)

Full source

@[simp]
theorem sorted_gt_listMap (e : α ↪o β) {l : List α} :
    (l.map e).Sorted (· > ·) ↔ l.Sorted (· > ·) :=
  e.ltEmbedding.sorted_swap_listMap

Preservation of List Sortedness under Order Embedding for Strict Greater-Than Relation

Informal description

Let $e : \alpha \hookrightarrow \beta$ be an order embedding between preordered types $\alpha$ and $\beta$. For any list $l$ of elements of $\alpha$, the mapped list $e(l)$ is sorted with respect to the strict greater-than relation $>$ on $\beta$ if and only if $l$ is sorted with respect to the strict greater-than relation $>$ on $\alpha$.

RelIso.sorted_listMap theorem

(e : ra ≃r rb) {l : List α} : (l.map e).Sorted rb ↔ l.Sorted ra

Full source

@[simp]
theorem sorted_listMap (e : ra ≃r rb) {l : List α} : (l.map e).Sorted rb ↔ l.Sorted ra :=
  e.toRelEmbedding.sorted_listMap

Preservation of List Sortedness under Relation Isomorphism

Informal description

Let $e : (\alpha, r_a) \simeq (\beta, r_b)$ be a relation isomorphism between types $\alpha$ and $\beta$ with respect to relations $r_a$ and $r_b$. For any list $l$ of elements of $\alpha$, the mapped list $e(l)$ is sorted with respect to $r_b$ if and only if $l$ is sorted with respect to $r_a$.

RelIso.sorted_swap_listMap theorem

(e : ra ≃r rb) {l : List α} : (l.map e).Sorted (Function.swap rb) ↔ l.Sorted (Function.swap ra)

Full source

@[simp]
theorem sorted_swap_listMap (e : ra ≃r rb) {l : List α} :
    (l.map e).Sorted (Function.swap rb) ↔ l.Sorted (Function.swap ra) :=
  e.toRelEmbedding.sorted_swap_listMap

Preservation of List Sortedness under Relation Isomorphism with Swapped Relations

Informal description

Let $e : (\alpha, r_a) \simeq (\beta, r_b)$ be a relation isomorphism between types $\alpha$ and $\beta$ with respect to relations $r_a$ and $r_b$. For any list $l$ of elements of $\alpha$, the mapped list $e(l)$ is sorted with respect to the swapped relation $\operatorname{swap} r_b$ (where $\operatorname{swap} r_b\, y\, x = r_b\, x\, y$) if and only if $l$ is sorted with respect to the swapped relation $\operatorname{swap} r_a$.

OrderIso.sorted_lt_listMap theorem

(e : α ≃o β) {l : List α} : (l.map e).Sorted (· < ·) ↔ l.Sorted (· < ·)

Full source

@[simp]
theorem sorted_lt_listMap (e : α ≃o β) {l : List α} :
    (l.map e).Sorted (· < ·) ↔ l.Sorted (· < ·) :=
  e.toOrderEmbedding.sorted_lt_listMap

Preservation of List Sortedness under Order Isomorphism for Strict Order

Informal description

Let $e : \alpha \simeq_o \beta$ be an order isomorphism between preordered types $\alpha$ and $\beta$. For any list $l$ of elements of $\alpha$, the mapped list $e(l)$ is sorted with respect to the strict order $<$ on $\beta$ if and only if $l$ is sorted with respect to the strict order $<$ on $\alpha$.

OrderIso.sorted_gt_listMap theorem

(e : α ≃o β) {l : List α} : (l.map e).Sorted (· > ·) ↔ l.Sorted (· > ·)

Full source

@[simp]
theorem sorted_gt_listMap (e : α ≃o β) {l : List α} :
    (l.map e).Sorted (· > ·) ↔ l.Sorted (· > ·) :=
  e.toOrderEmbedding.sorted_gt_listMap

Preservation of List Sortedness under Order Isomorphism for Strict Greater-Than Relation

Informal description

Let $e : \alpha \simeq_o \beta$ be an order isomorphism between preordered types $\alpha$ and $\beta$. For any list $l$ of elements of $\alpha$, the mapped list $e(l)$ is sorted with respect to the strict greater-than relation $>$ on $\beta$ if and only if $l$ is sorted with respect to the strict greater-than relation $>$ on $\alpha$.

StrictMono.sorted_le_listMap theorem

(hf : StrictMono f) : (l.map f).Sorted (· ≤ ·) ↔ l.Sorted (· ≤ ·)

Full source

theorem sorted_le_listMap (hf : StrictMono f) :
    (l.map f).Sorted (· ≤ ·) ↔ l.Sorted (· ≤ ·) :=
  (OrderEmbedding.ofStrictMono f hf).sorted_listMap

Preservation of Sortedness under Strictly Monotone Mapping: $f(l)$ is $\leq$-sorted iff $l$ is $\leq$-sorted

Informal description

Let $f : \alpha \to \beta$ be a strictly monotone function between a linearly ordered type $\alpha$ and a preordered type $\beta$. For any list $l$ of elements of $\alpha$, the mapped list $f(l)$ is sorted with respect to the non-strict order $\leq$ in $\beta$ if and only if $l$ is sorted with respect to $\leq$ in $\alpha$.

StrictMono.sorted_ge_listMap theorem

(hf : StrictMono f) : (l.map f).Sorted (· ≥ ·) ↔ l.Sorted (· ≥ ·)

Full source

theorem sorted_ge_listMap (hf : StrictMono f) :
    (l.map f).Sorted (· ≥ ·) ↔ l.Sorted (· ≥ ·) :=
  (OrderEmbedding.ofStrictMono f hf).sorted_swap_listMap

Preservation of Sortedness under Strictly Monotone Functions for $\geq$ Relation

Informal description

Let $f : \alpha \to \beta$ be a strictly monotone function between a linearly ordered type $\alpha$ and a preordered type $\beta$. For any list $l$ of elements of $\alpha$, the mapped list $f(l)$ is sorted with respect to the relation $\geq$ in $\beta$ if and only if $l$ is sorted with respect to $\geq$ in $\alpha$.

StrictMono.sorted_lt_listMap theorem

(hf : StrictMono f) : (l.map f).Sorted (· < ·) ↔ l.Sorted (· < ·)

Full source

theorem sorted_lt_listMap (hf : StrictMono f) :
    (l.map f).Sorted (· < ·) ↔ l.Sorted (· < ·) :=
  (OrderEmbedding.ofStrictMono f hf).sorted_lt_listMap

Preservation of Strictly Sorted Lists under Strictly Monotone Maps

Informal description

Let $f : \alpha \to \beta$ be a strictly monotone function between two preordered types $\alpha$ and $\beta$. For any list $l$ of elements of $\alpha$, the mapped list $f(l)$ is sorted with respect to the strict order $<$ on $\beta$ if and only if $l$ is sorted with respect to the strict order $<$ on $\alpha$.

StrictMono.sorted_gt_listMap theorem

(hf : StrictMono f) : (l.map f).Sorted (· > ·) ↔ l.Sorted (· > ·)

Full source

theorem sorted_gt_listMap (hf : StrictMono f) :
    (l.map f).Sorted (· > ·) ↔ l.Sorted (· > ·) :=
  (OrderEmbedding.ofStrictMono f hf).sorted_gt_listMap

Preservation of Strictly Decreasing List Order under Strictly Monotone Mapping

Informal description

Let $f : \alpha \to \beta$ be a strictly monotone function between preordered types $\alpha$ and $\beta$. For any list $l$ of elements of $\alpha$, the mapped list $f(l)$ is sorted with respect to the strict greater-than relation $>$ on $\beta$ if and only if $l$ is sorted with respect to the strict greater-than relation $>$ on $\alpha$.

StrictAnti.sorted_le_listMap theorem

(hf : StrictAnti f) : (l.map f).Sorted (· ≤ ·) ↔ l.Sorted (· ≥ ·)

Full source

theorem sorted_le_listMap (hf : StrictAnti f) :
    (l.map f).Sorted (· ≤ ·) ↔ l.Sorted (· ≥ ·) :=
  hf.dual_right.sorted_ge_listMap

Preservation of Non-Decreasing Sortedness under Strictly Antitone Maps: $f(l)$ is $\leq$-sorted iff $l$ is $\geq$-sorted

Informal description

Let $f : \alpha \to \beta$ be a strictly antitone function between preordered types $\alpha$ and $\beta$. For any list $l$ of elements of $\alpha$, the mapped list $f(l)$ is sorted with respect to the relation $\leq$ in $\beta$ if and only if $l$ is sorted with respect to the relation $\geq$ in $\alpha$.

StrictAnti.sorted_ge_listMap theorem

(hf : StrictAnti f) : (l.map f).Sorted (· ≥ ·) ↔ l.Sorted (· ≤ ·)

Full source

theorem sorted_ge_listMap (hf : StrictAnti f) :
    (l.map f).Sorted (· ≥ ·) ↔ l.Sorted (· ≤ ·) :=
  hf.dual_right.sorted_le_listMap

Preservation of Non-Strict Decreasing List Order under Strictly Antitone Mapping: $f(l)$ is $\geq$-sorted iff $l$ is $\leq$-sorted

Informal description

Let $f : \alpha \to \beta$ be a strictly antitone function between preordered types $\alpha$ and $\beta$. For any list $l$ of elements of $\alpha$, the mapped list $f(l)$ is sorted with respect to the non-strict greater-than-or-equal relation $\geq$ on $\beta$ if and only if $l$ is sorted with respect to the non-strict less-than-or-equal relation $\leq$ on $\alpha$.

StrictAnti.sorted_lt_listMap theorem

(hf : StrictAnti f) : (l.map f).Sorted (· < ·) ↔ l.Sorted (· > ·)

Full source

theorem sorted_lt_listMap (hf : StrictAnti f) :
    (l.map f).Sorted (· < ·) ↔ l.Sorted (· > ·) :=
  hf.dual_right.sorted_gt_listMap

Preservation of Strictly Decreasing List Order under Strictly Antitone Mapping

Informal description

Let $f : \alpha \to \beta$ be a strictly antitone function between preordered types $\alpha$ and $\beta$. For any list $l$ of elements of $\alpha$, the mapped list $f(l)$ is sorted with respect to the strict less-than relation $<$ on $\beta$ if and only if $l$ is sorted with respect to the strict greater-than relation $>$ on $\alpha$.

StrictAnti.sorted_gt_listMap theorem

(hf : StrictAnti f) : (l.map f).Sorted (· > ·) ↔ l.Sorted (· < ·)

Full source

theorem sorted_gt_listMap (hf : StrictAnti f) :
    (l.map f).Sorted (· > ·) ↔ l.Sorted (· < ·) :=
  hf.dual_right.sorted_lt_listMap

Preservation of Strictly Sorted Lists under Strictly Antitone Maps: $f(l)$ is $>$-sorted iff $l$ is $<$-sorted

Informal description

Let $f : \alpha \to \beta$ be a strictly antitone function between two preordered types $\alpha$ and $\beta$. For any list $l$ of elements of $\alpha$, the mapped list $f(l)$ is sorted with respect to the strict order $>$ on $\beta$ if and only if $l$ is sorted with respect to the strict order $<$ on $\alpha$.

List.orderedInsert definition

(a : α) : List α → List α

Full source

/-- `orderedInsert a l` inserts `a` into `l` at such that
  `orderedInsert a l` is sorted if `l` is. -/
@[simp]
def orderedInsert (a : α) : List α → List α
  | [] => [a]
  | b :: l => if a ≼ b then a :: b :: l else b :: orderedInsert a l

Ordered insertion into a list

Informal description

Given a relation `≼` on type `α`, the function `orderedInsert` takes an element `a : α` and a list `l : List α`, and inserts `a` into `l` in such a way that if `l` is sorted with respect to `≼`, then the resulting list `orderedInsert a l` is also sorted. Specifically: - If `l` is empty, the result is the singleton list `[a]`. - If `l` is `b :: l'`, then `a` is inserted before `b` if `a ≼ b`, otherwise it is inserted somewhere in `l'`.

List.orderedInsert_of_le theorem

{a b : α} (l : List α) (h : a ≼ b) :
    orderedInsert r a (b :: l) = a :: b :: l

Full source

theorem orderedInsert_of_le {a b : α} (l : List α) (h : a ≼ b) :
    orderedInsert r a (b :: l) = a :: b :: l :=
  dif_pos h

Ordered Insertion Preserves Relation for Leading Elements

Informal description

For any elements $a$ and $b$ of type $\alpha$ and a list $l$ of type $\alpha$, if $a \preceq b$ holds, then inserting $a$ into the list $b :: l$ using the ordered insertion operation results in the list $a :: b :: l$.

List.insertionSort definition

: List α → List α

Full source

/-- `insertionSort l` returns `l` sorted using the insertion sort algorithm. -/
@[simp]
def insertionSort : List α → List α
  | [] => []
  | b :: l => orderedInsert r b (insertionSort l)

Insertion sort algorithm for lists

Informal description

The function `insertionSort` takes a list `l` of elements of type `α` and returns a new list with the same elements sorted according to the relation `≼`. The sorting is performed using the insertion sort algorithm, which works by repeatedly inserting each element into its correct position in a growing sorted list. Specifically: - If `l` is empty, the result is the empty list `[]`. - If `l` is `b :: l'`, then `b` is inserted into the recursively sorted `l'` using the `orderedInsert` function.

List.orderedInsert_nil theorem

(a : α) : [].orderedInsert r a = [a]

Full source

@[simp]
theorem orderedInsert_nil (a : α) : [].orderedInsert r a = [a] :=
  rfl

Ordered Insertion into Empty List Yields Singleton

Informal description

For any element $a$ of type $\alpha$ and the empty list $[\,]$, the ordered insertion of $a$ into $[\,]$ with respect to a relation $\preceq$ results in the singleton list $[a]$, i.e., $\text{orderedInsert}_\preceq(a, [\,]) = [a]$.

List.orderedInsert_length theorem

: ∀ (L : List α) (a : α), (L.orderedInsert r a).length = L.length + 1

Full source

theorem orderedInsert_length : ∀ (L : List α) (a : α), (L.orderedInsert r a).length = L.length + 1
  | [], _ => rfl
  | hd :: tl, a => by
    dsimp [orderedInsert]
    split_ifs <;> simp [orderedInsert_length tl]

Length of Ordered Insertion: $\text{length}(\text{orderedInsert}_\preceq(a, L)) = \text{length}(L) + 1$

Informal description

For any list $L$ of elements of type $\alpha$ and any element $a : \alpha$, the length of the list obtained by inserting $a$ into $L$ in order with respect to the relation $\preceq$ is equal to the length of $L$ plus one, i.e., $\text{length}(\text{orderedInsert}_\preceq(a, L)) = \text{length}(L) + 1$.

List.orderedInsert_eq_take_drop theorem

 (a : α) : ∀ l : List α, l.orderedInsert r a = (l.takeWhile fun b => ¬a ≼ b) ++ a :: l.dropWhile fun b => ¬a ≼ b

Full source

/-- An alternative definition of `orderedInsert` using `takeWhile` and `dropWhile`. -/
theorem orderedInsert_eq_take_drop (a : α) :
    ∀ l : List α,
      l.orderedInsert r a = (l.takeWhile fun b => ¬a ≼ b) ++ a :: l.dropWhile fun b => ¬a ≼ b
  | [] => rfl
  | b :: l => by
    dsimp only [orderedInsert]
    split_ifs with h <;> simp [takeWhile, dropWhile, *, orderedInsert_eq_take_drop a l]

Ordered Insertion as TakeWhile-DropWhile Concatenation

Informal description

For any element $a$ of type $\alpha$ and any list $l$ of elements of $\alpha$, the ordered insertion of $a$ into $l$ with respect to a relation $\preceq$ can be expressed as the concatenation of: 1. The longest prefix of $l$ where all elements $b$ satisfy $\neg(a \preceq b)$, and 2. The element $a$ followed by the remaining elements of $l$. In other words, $\text{orderedInsert}_\preceq(a, l) = \text{takeWhile}_\preceq(l) +\!\!+ [a] +\!\!+ \text{dropWhile}_\preceq(l)$, where: - $\text{takeWhile}_\preceq(l)$ takes elements from $l$ while $\neg(a \preceq b)$ holds - $\text{dropWhile}_\preceq(l)$ contains the remaining elements after $\text{takeWhile}_\preceq(l)$

List.insertionSort_cons_eq_take_drop theorem

 (a : α) (l : List α) :
  insertionSort r (a :: l) =
    ((insertionSort r l).takeWhile fun b => ¬a ≼ b) ++ a :: (insertionSort r l).dropWhile fun b => ¬a ≼ b

Full source

theorem insertionSort_cons_eq_take_drop (a : α) (l : List α) :
    insertionSort r (a :: l) =
      ((insertionSort r l).takeWhile fun b => ¬a ≼ b) ++
        a :: (insertionSort r l).dropWhile fun b => ¬a ≼ b :=
  orderedInsert_eq_take_drop r a _

Insertion Sort of Cons List as Take-Drop Concatenation

Informal description

For any element $a$ of type $\alpha$ and any list $l$ of elements of $\alpha$, the insertion sort of the list $a :: l$ with respect to a relation $\preceq$ is equal to the concatenation of: 1. The longest prefix of the sorted list $\text{insertionSort}_\preceq(l)$ where all elements $b$ satisfy $\neg(a \preceq b)$, and 2. The element $a$ followed by the remaining elements of $\text{insertionSort}_\preceq(l)$. In other words: $$\text{insertionSort}_\preceq(a :: l) = \text{takeWhile}_\preceq(\text{insertionSort}_\preceq(l)) +\!\!+ [a] +\!\!+ \text{dropWhile}_\preceq(\text{insertionSort}_\preceq(l))$$ where: - $\text{takeWhile}_\preceq$ takes elements while $\neg(a \preceq b)$ holds - $\text{dropWhile}_\preceq$ contains the remaining elements after $\text{takeWhile}_\preceq$

List.mem_orderedInsert theorem

{a b : α} {l : List α} : a ∈ orderedInsert r b l ↔ a = b ∨ a ∈ l

Full source

@[simp]
theorem mem_orderedInsert {a b : α} {l : List α} :
    a ∈ orderedInsert r b la ∈ orderedInsert r b l ↔ a = b ∨ a ∈ l :=
  match l with
  | [] => by simp [orderedInsert]
  | x :: xs => by
    rw [orderedInsert]
    split_ifs
    · simp [orderedInsert]
    · rw [mem_cons, mem_cons, mem_orderedInsert, or_left_comm]

Membership in Ordered Insertion: $a \in \text{orderedInsert}(b, l) \leftrightarrow a = b \lor a \in l$

Informal description

For any elements $a, b$ of type $\alpha$ and any list $l$ of elements of $\alpha$, the element $a$ is in the list obtained by inserting $b$ into $l$ in order with respect to relation $\preceq$ if and only if either $a = b$ or $a$ was already in $l$.

List.map_orderedInsert theorem

 (f : α → β) (l : List α) (x : α) (hl₁ : ∀ a ∈ l, a ≼ x ↔ f a ≼ f x) (hl₂ : ∀ a ∈ l, x ≼ a ↔ f x ≼ f a) :
  (l.orderedInsert r x).map f = (l.map f).orderedInsert s (f x)

Full source

theorem map_orderedInsert (f : α → β) (l : List α) (x : α)
    (hl₁ : ∀ a ∈ l, a ≼ x ↔ f a ≼ f x) (hl₂ : ∀ a ∈ l, x ≼ a ↔ f x ≼ f a) :
    (l.orderedInsert r x).map f = (l.map f).orderedInsert s (f x) := by
  induction l with
  | nil => simp
  | cons x xs ih =>
    rw [List.forall_mem_cons] at hl₁ hl₂
    simp only [List.map, List.orderedInsert, ← hl₁.1, ← hl₂.1]
    split_ifs
    · rw [List.map, List.map]
    · rw [List.map, ih (fun _ ha => hl₁.2 _ ha) (fun _ ha => hl₂.2 _ ha)]

Preservation of Ordered Insertion under Map

Informal description

Let $f : \alpha \to \beta$ be a function between two types $\alpha$ and $\beta$, and let $l$ be a list of elements of type $\alpha$. For any element $x \in \alpha$, if the following conditions hold for all $a \in l$: 1. $a \preccurlyeq x$ if and only if $f(a) \preccurlyeq f(x)$, 2. $x \preccurlyeq a$ if and only if $f(x) \preccurlyeq f(a)$, then the map of the ordered insertion of $x$ into $l$ under $f$ is equal to the ordered insertion of $f(x)$ into the map of $l$ under $f$. In symbols: $$ \text{map } f (\text{orderedInsert}_{\preccurlyeq} \, x \, l) = \text{orderedInsert}_{\preccurlyeq} (f x) (\text{map } f \, l). $$

List.perm_orderedInsert theorem

(a) : ∀ l : List α, orderedInsert r a l ~ a :: l

Full source

theorem perm_orderedInsert (a) : ∀ l : List α, orderedInsertorderedInsert r a l ~ a :: l
  | [] => Perm.refl _
  | b :: l => by
    by_cases h : a ≼ b
    · simp [orderedInsert, h]
    · simpa [orderedInsert, h] using ((perm_orderedInsert a l).cons _).trans (Perm.swap _ _ _)

Permutation Property of Ordered Insertion

Informal description

For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the list obtained by inserting $a$ into $l$ in order with respect to relation $r$ is a permutation of the list obtained by simply prepending $a$ to $l$. In other words, $\text{orderedInsert}_r(a, l) \sim a :: l$, where $\sim$ denotes the permutation relation between lists.

List.orderedInsert_count theorem

[DecidableEq α] (L : List α) (a b : α) : count a (L.orderedInsert r b) = count a L + if b = a then 1 else 0

Full source

theorem orderedInsert_count [DecidableEq α] (L : List α) (a b : α) :
    count a (L.orderedInsert r b) = count a L + if b = a then 1 else 0 := by
  rw [(L.perm_orderedInsert r b).count_eq, count_cons]
  simp

Count of Element in Ordered Insertion List

Informal description

For any list $L$ of elements of type $\alpha$ with decidable equality, and for any elements $a, b \in \alpha$, the count of $a$ in the list obtained by inserting $b$ into $L$ in order with respect to relation $r$ is equal to the count of $a$ in $L$ plus $1$ if $b = a$, and $0$ otherwise. In other words: $$\text{count}_a(\text{orderedInsert}_r(b, L)) = \text{count}_a(L) + \begin{cases} 1 & \text{if } b = a, \\ 0 & \text{otherwise.} \end{cases}$$

List.perm_insertionSort theorem

: ∀ l : List α, insertionSort r l ~ l

Full source

theorem perm_insertionSort : ∀ l : List α, insertionSortinsertionSort r l ~ l
  | [] => Perm.nil
  | b :: l => by
    simpa [insertionSort] using (perm_orderedInsert _ _ _).trans ((perm_insertionSort l).cons b)

Insertion Sort Preserves Permutation

Informal description

For any list $l$ of elements of type $\alpha$, the list obtained by applying the insertion sort algorithm with respect to relation $r$ is a permutation of the original list $l$, i.e., $\text{insertionSort}_r(l) \sim l$, where $\sim$ denotes the permutation relation between lists.

List.mem_insertionSort theorem

{l : List α} {x : α} : x ∈ l.insertionSort r ↔ x ∈ l

Full source

@[simp]
theorem mem_insertionSort {l : List α} {x : α} : x ∈ l.insertionSort rx ∈ l.insertionSort r ↔ x ∈ l :=
  (perm_insertionSort r l).mem_iff

Insertion Sort Preserves Membership

Informal description

For any list $l$ of elements of type $\alpha$ and any element $x \in \alpha$, the element $x$ is in the insertion-sorted list $\text{insertionSort}_r(l)$ if and only if $x$ is in the original list $l$. In other words: $$x \in \text{insertionSort}_r(l) \leftrightarrow x \in l$$

List.length_insertionSort theorem

(l : List α) : (insertionSort r l).length = l.length

Full source

@[simp]
theorem length_insertionSort (l : List α) : (insertionSort r l).length = l.length :=
  (perm_insertionSort r _).length_eq

Insertion Sort Preserves List Length

Informal description

For any list $l$ of elements of type $\alpha$, the length of the list obtained by applying the insertion sort algorithm with respect to relation $r$ is equal to the length of the original list $l$, i.e., $|\text{insertionSort}_r(l)| = |l|$.

List.insertionSort_cons theorem

{a : α} {l : List α} (h : ∀ b ∈ l, r a b) : insertionSort r (a :: l) = a :: insertionSort r l

Full source

theorem insertionSort_cons {a : α} {l : List α} (h : ∀ b ∈ l, r a b) :
    insertionSort r (a :: l) = a :: insertionSort r l := by
  rw [insertionSort]
  cases hi : insertionSort r l with
  | nil => rfl
  | cons b m =>
    rw [orderedInsert_of_le]
    apply h b <| (mem_insertionSort r).1 _
    rw [hi]
    exact mem_cons_self

Insertion Sort of Cons List with Dominant Head Element

Informal description

For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, if $a$ is related to every element $b \in l$ by the relation $r$ (i.e., $r(a, b)$ holds for all $b \in l$), then the insertion sort of the list $a :: l$ with respect to $r$ is equal to $a$ prepended to the insertion sort of $l$ with respect to $r$. In symbols: $$\text{insertionSort}_r(a :: l) = a :: \text{insertionSort}_r(l)$$

List.map_insertionSort theorem

 (f : α → β) (l : List α) (hl : ∀ a ∈ l, ∀ b ∈ l, a ≼ b ↔ f a ≼ f b) :
  (l.insertionSort r).map f = (l.map f).insertionSort s

Full source

theorem map_insertionSort (f : α → β) (l : List α) (hl : ∀ a ∈ l, ∀ b ∈ l, a ≼ b ↔ f a ≼ f b) :
    (l.insertionSort r).map f = (l.map f).insertionSort s := by
  induction l with
  | nil => simp
  | cons x xs ih =>
    simp_rw [List.forall_mem_cons, forall_and] at hl
    simp_rw [List.map, List.insertionSort]
    rw [List.map_orderedInsert _ s, ih hl.2.2]
    · simpa only [mem_insertionSort] using hl.2.1
    · simpa only [mem_insertionSort] using hl.1.2

Preservation of Insertion Sort under Map

Informal description

Let $f : \alpha \to \beta$ be a function between two types $\alpha$ and $\beta$, and let $l$ be a list of elements of type $\alpha$. If for all elements $a, b \in l$, the relation $a \preccurlyeq b$ holds if and only if $f(a) \preccurlyeq f(b)$, then the map of the insertion sort of $l$ under $f$ is equal to the insertion sort of the map of $l$ under $f$. In symbols: $$ \text{map } f (\text{insertionSort}_{\preccurlyeq} \, l) = \text{insertionSort}_{\preccurlyeq} (\text{map } f \, l). $$

List.Sorted.insertionSort_eq theorem

: ∀ {l : List α}, Sorted r l → insertionSort r l = l

Full source

/-- If `l` is already `List.Sorted` with respect to `r`, then `insertionSort` does not change
it. -/
theorem Sorted.insertionSort_eq : ∀ {l : List α}, Sorted r l → insertionSort r l = l
  | [], _ => rfl
  | [_], _ => rfl
  | a :: b :: l, h => by
    rw [insertionSort, Sorted.insertionSort_eq, orderedInsert, if_pos]
    exacts [rel_of_sorted_cons h _ mem_cons_self, h.tail]

Insertion Sort Preserves Already Sorted Lists

Informal description

For any list $l$ of elements of type $\alpha$ that is already sorted with respect to a relation $r$, applying the insertion sort algorithm with $r$ leaves the list unchanged, i.e., $\text{insertionSort}_r(l) = l$.

List.erase_orderedInsert theorem

[DecidableEq α] [IsRefl α r] (x : α) (xs : List α) : (xs.orderedInsert r x).erase x = xs

Full source

/-- For a reflexive relation, insert then erasing is the identity. -/
theorem erase_orderedInsert [DecidableEq α] [IsRefl α r] (x : α) (xs : List α) :
    (xs.orderedInsert r x).erase x = xs := by
  rw [orderedInsert_eq_take_drop, erase_append_right, List.erase_cons_head,
    takeWhile_append_dropWhile]
  intro h
  replace h := mem_takeWhile_imp h
  simp [refl x] at h

Erasing Inserted Element Preserves List under Reflexive Relation

Informal description

Let $\alpha$ be a type with a decidable equality and a reflexive relation $r$. For any element $x \in \alpha$ and any list $xs$ of elements of $\alpha$, erasing $x$ from the list obtained by inserting $x$ into $xs$ in order with respect to $r$ yields the original list $xs$. That is, $$ \text{erase}_x(\text{orderedInsert}_r(x, xs)) = xs. $$

List.erase_orderedInsert_of_not_mem theorem

[DecidableEq α] {x : α} {xs : List α} (hx : x ∉ xs) : (xs.orderedInsert r x).erase x = xs

Full source

/-- Inserting then erasing an element that is absent is the identity. -/
theorem erase_orderedInsert_of_not_mem [DecidableEq α]
    {x : α} {xs : List α} (hx : x ∉ xs) :
    (xs.orderedInsert r x).erase x = xs := by
  rw [orderedInsert_eq_take_drop, erase_append_right, List.erase_cons_head,
    takeWhile_append_dropWhile]
  exact mt ((takeWhile_prefix _).sublist.subset ·) hx

Erasing Absent Element After Ordered Insertion Preserves List

Informal description

For any list $xs$ of elements of type $\alpha$ and any element $x \notin xs$, erasing $x$ from the list obtained by inserting $x$ into $xs$ in order with respect to relation $r$ yields the original list $xs$. That is, $\text{erase}_x(\text{orderedInsert}_r(x, xs)) = xs$.

List.orderedInsert_erase theorem

 [DecidableEq α] [IsAntisymm α r] (x : α) (xs : List α) (hx : x ∈ xs) (hxs : Sorted r xs) :
  (xs.erase x).orderedInsert r x = xs

Full source

/-- For an antisymmetric relation, erasing then inserting is the identity. -/
theorem orderedInsert_erase [DecidableEq α] [IsAntisymm α r] (x : α) (xs : List α) (hx : x ∈ xs)
    (hxs : Sorted r xs) :
    (xs.erase x).orderedInsert r x = xs := by
  induction xs generalizing x with
  | nil => cases hx
  | cons y ys ih =>
    rw [sorted_cons] at hxs
    obtain rfl | hxy := Decidable.eq_or_ne x y
    · rw [erase_cons_head]
      cases ys with
      | nil => rfl
      | cons z zs =>
        rw [orderedInsert, if_pos (hxs.1 _ (.head zs))]
    · rw [mem_cons] at hx
      replace hx := hx.resolve_left hxy
      rw [erase_cons_tail (not_beq_of_ne hxy.symm), orderedInsert, ih _ hx hxs.2, if_neg]
      refine mt (fun hrxy => ?_) hxy
      exact antisymm hrxy (hxs.1 _ hx)

Ordered Insertion After Erasure Preserves Sorted List

Informal description

Let $\alpha$ be a type with decidable equality and an antisymmetric relation $r$. For any element $x \in \alpha$ and any sorted list $xs$ of elements of $\alpha$ containing $x$, inserting $x$ into the list obtained by erasing $x$ from $xs$ (with respect to $r$) yields the original list $xs$. That is, $$ \text{orderedInsert}_r(x, \text{erase}_x(xs)) = xs. $$

List.sublist_orderedInsert theorem

(x : α) (xs : List α) : xs <+ xs.orderedInsert r x

Full source

theorem sublist_orderedInsert (x : α) (xs : List α) : xs <+ xs.orderedInsert r x := by
  rw [orderedInsert_eq_take_drop]
  refine Sublist.trans ?_ (.append_left (.cons _ (.refl _)) _)
  rw [takeWhile_append_dropWhile]

Sublist Property of Ordered Insertion: $xs \subseteq \text{orderedInsert}_r(x, xs)$

Informal description

For any element $x$ of type $\alpha$ and any list $xs$ of elements of $\alpha$, the list $xs$ is a sublist of the list obtained by inserting $x$ into $xs$ in order with respect to relation $r$. That is, $xs \subseteq \text{orderedInsert}_r(x, xs)$.

List.cons_sublist_orderedInsert theorem

{l c : List α} {a : α} (hl : c <+ l) (ha : ∀ a' ∈ c, a ≼ a') : a :: c <+ orderedInsert r a l

Full source

theorem cons_sublist_orderedInsert {l c : List α} {a : α} (hl : c <+ l) (ha : ∀ a' ∈ c, a ≼ a') :
    a :: ca :: c <+ orderedInsert r a l := by
  induction l with
  | nil         => simp_all only [sublist_nil, orderedInsert, Sublist.refl]
  | cons _ _ ih =>
    unfold orderedInsert
    split_ifs with hr
    · exact .cons₂ _ hl
    · cases hl with
      | cons _ h => exact .cons _ <| ih h
      | cons₂    => exact absurd (ha _ <| mem_cons_self ..) hr

Sublist Property of Ordered Insertion: $a :: c \subseteq \text{orderedInsert}_r(a, l)$ under Given Conditions

Informal description

Let $r$ be a relation on a type $\alpha$, and let $l$ and $c$ be lists of elements of $\alpha$. For any element $a \in \alpha$, if $c$ is a sublist of $l$ and $a \preccurlyeq a'$ for every $a' \in c$, then the list $a :: c$ is a sublist of the ordered insertion of $a$ into $l$ with respect to $r$.

List.Sublist.orderedInsert_sublist theorem

[IsTrans α r] {as bs} (x) (hs : as <+ bs) (hb : bs.Sorted r) : orderedInsert r x as <+ orderedInsert r x bs

Full source

theorem Sublist.orderedInsert_sublist [IsTrans α r] {as bs} (x) (hs : as <+ bs) (hb : bs.Sorted r) :
    orderedInsertorderedInsert r x as <+ orderedInsert r x bs := by
  cases as with
  | nil => simp
  | cons a as =>
    cases bs with
    | nil => contradiction
    | cons b bs =>
      unfold orderedInsert
      cases hs <;> split_ifs with hr
      · exact .cons₂ _ <| .cons _ ‹a :: as <+ bs›
      · have ih := orderedInsert_sublist x ‹a :: as <+ bs›  hb.of_cons
        simp only [hr, orderedInsert, ite_true] at ih
        exact .trans ih <| .cons _ (.refl _)
      · have hba := pairwise_cons.mp hb |>.left _ (mem_of_cons_sublist ‹a :: as <+ bs›)
        exact absurd (trans_of _ ‹r x b› hba) hr
      · have ih := orderedInsert_sublist x ‹a :: as <+ bs› hb.of_cons
        rw [orderedInsert, if_neg hr] at ih
        exact .cons _ ih
      · simp_all only [sorted_cons, cons_sublist_cons]
      · exact .cons₂ _ <| orderedInsert_sublist x ‹as <+ bs› hb.of_cons

Sublist Preservation under Ordered Insertion in Sorted Lists

Informal description

Let $\preccurlyeq$ be a transitive relation on a type $\alpha$. Given two lists $as$ and $bs$ of elements of $\alpha$, an element $x \in \alpha$, and the following conditions: 1. $as$ is a sublist of $bs$ (denoted $as \subseteq bs$), 2. $bs$ is sorted with respect to $\preccurlyeq$, then the ordered insertion of $x$ into $as$ is a sublist of the ordered insertion of $x$ into $bs$ with respect to $\preccurlyeq$.

List.Sorted.orderedInsert theorem

(a : α) : ∀ l, Sorted r l → Sorted r (orderedInsert r a l)

Full source

theorem Sorted.orderedInsert (a : α) : ∀ l, Sorted r l → Sorted r (orderedInsert r a l)
  | [], _ => sorted_singleton a
  | b :: l, h => by
    by_cases h' : a ≼ b
    · simpa [orderedInsert, h', h] using fun b' bm => _root_.trans h' (rel_of_sorted_cons h _ bm)
    · suffices ∀ b' : α, b' ∈ List.orderedInsert r a l → r b b' by
        simpa [orderedInsert, h', h.of_cons.orderedInsert a l]
      intro b' bm
      rcases (mem_orderedInsert r).mp bm with be | bm
      · subst b'
        exact (total_of r _ _).resolve_left h'
      · exact rel_of_sorted_cons h _ bm

Ordered Insertion Preserves Sortedness

Informal description

For any element $a$ of type $\alpha$ and any list $l$ of elements of $\alpha$ that is sorted with respect to a relation $r$, the list obtained by inserting $a$ into $l$ in order with respect to $r$ is also sorted with respect to $r$.

List.sorted_insertionSort theorem

: ∀ l, Sorted r (insertionSort r l)

Full source

/-- The list `List.insertionSort r l` is `List.Sorted` with respect to `r`. -/
theorem sorted_insertionSort : ∀ l, Sorted r (insertionSort r l)
  | [] => sorted_nil
  | a :: l => (sorted_insertionSort l).orderedInsert a _

Insertion Sort Produces a Sorted List

Informal description

For any list $l$ of elements of type $\alpha$, the list obtained by applying the insertion sort algorithm with respect to a relation $r$ is sorted with respect to $r$.

List.sublist_insertionSort theorem

{l c : List α} (hr : c.Pairwise r) (hc : c <+ l) : c <+ insertionSort r l

Full source

/--
If `c` is a sorted sublist of `l`, then `c` is still a sublist of `insertionSort r l`.
-/
theorem sublist_insertionSort {l c : List α} (hr : c.Pairwise r) (hc : c <+ l) :
    c <+ insertionSort r l := by
  induction l generalizing c with
  | nil         => simp_all only [sublist_nil, insertionSort, Sublist.refl]
  | cons _ _ ih =>
    cases hc with
    | cons  _ h => exact ih hr h |>.trans (sublist_orderedInsert ..)
    | cons₂ _ h =>
      obtain ⟨hr, hp⟩ := pairwise_cons.mp hr
      exact cons_sublist_orderedInsert (ih hp h) hr

Sublist Preservation Under Insertion Sort for Sorted Sublists

Informal description

Let $r$ be a relation on a type $\alpha$, and let $l$ and $c$ be lists of elements of $\alpha$. If $c$ is a sublist of $l$ and the elements of $c$ are pairwise related by $r$ (i.e., $c$ is sorted with respect to $r$), then $c$ is also a sublist of the insertion-sorted version of $l$ with respect to $r$.

List.pair_sublist_insertionSort theorem

{a b : α} {l : List α} (hab : r a b) (h : [a, b] <+ l) : [a, b] <+ insertionSort r l

Full source

/--
Another statement of stability of insertion sort.
If a pair `[a, b]` is a sublist of `l` and `r a b`,
then `[a, b]` is still a sublist of `insertionSort r l`.
-/
theorem pair_sublist_insertionSort {a b : α} {l : List α} (hab : r a b) (h : [a, b][a, b] <+ l) :
    [a, b][a, b] <+ insertionSort r l :=
  sublist_insertionSort (pairwise_pair.mpr hab) h

Stability of Insertion Sort for Pairs

Informal description

Let $r$ be a relation on a type $\alpha$, and let $a, b$ be elements of $\alpha$ and $l$ a list of elements of $\alpha$. If $r(a, b)$ holds and the pair $[a, b]$ is a sublist of $l$, then $[a, b]$ is also a sublist of the insertion-sorted version of $l$ with respect to $r$.

List.sublist_insertionSort' theorem

{l c : List α} (hs : c.Sorted r) (hc : c <+~ l) : c <+ insertionSort r l

Full source

/--
A version of `insertionSort_stable` which only assumes `c <+~ l` (instead of `c <+ l`), but
additionally requires `IsAntisymm α r`, `IsTotal α r` and `IsTrans α r`.
-/
theorem sublist_insertionSort' {l c : List α} (hs : c.Sorted r) (hc : c <+~ l) :
    c <+ insertionSort r l := by
  classical
  obtain ⟨d, hc, hd⟩ := hc
  induction l generalizing c d with
  | nil         => simp_all only [sublist_nil, insertionSort, nil_perm]
  | cons a _ ih =>
    cases hd with
    | cons  _ h => exact ih hs _ hc h |>.trans (sublist_orderedInsert ..)
    | cons₂ _ h =>
      specialize ih (hs.erase _) _ (erase_cons_head a ‹List _› ▸ hc.erase a) h
      have hm := hc.mem_iff.mp <| mem_cons_self ..
      have he := orderedInsert_erase _ _ hm hs
      exact he ▸ Sublist.orderedInsert_sublist _ ih (sorted_insertionSort ..)

Sublist Preservation Under Insertion Sort for Sorted Sublists with Total Order

Informal description

Let $\alpha$ be a type with a transitive, antisymmetric, and total relation $r$. For any lists $l$ and $c$ of elements of $\alpha$, if $c$ is sorted with respect to $r$ and $c$ is a sublist of $l$ (denoted $c \subseteq l$), then $c$ is also a sublist of the list obtained by applying insertion sort to $l$ with respect to $r$.

List.pair_sublist_insertionSort' theorem

{a b : α} {l : List α} (hab : a ≼ b) (h : [a, b] <+~ l) :
    [a, b] <+ insertionSort r l

Full source

/--
Another statement of stability of insertion sort.
If a pair `[a, b]` is a sublist of a permutation of `l` and `a ≼ b`,
then `[a, b]` is still a sublist of `insertionSort r l`.
-/
theorem pair_sublist_insertionSort' {a b : α} {l : List α} (hab : a ≼ b) (h : [a, b][a, b] <+~ l) :
    [a, b][a, b] <+ insertionSort r l :=
  sublist_insertionSort' (pairwise_pair.mpr hab) h

Stability of Insertion Sort for Ordered Pairs in Permutations

Informal description

Let $\alpha$ be a type equipped with a relation $\preceq$ that is transitive, antisymmetric, and total. For any elements $a, b \in \alpha$ and any list $l$ of elements of $\alpha$, if $a \preceq b$ and the pair $[a, b]$ is a sublist of a permutation of $l$, then $[a, b]$ is also a sublist of the list obtained by applying insertion sort to $l$ with respect to $\preceq$.

List.Sorted.merge theorem

{l l' : List α} (h : Sorted r l) (h' : Sorted r l') : Sorted r (merge l l' (r · ·))

Full source

theorem Sorted.merge {l l' : List α} (h : Sorted r l) (h' : Sorted r l') :
    Sorted r (merge l l' (r · ·)) := by
  simpa using sorted_merge (le := (r · ·))
    (fun a b c h₁ h₂ => by simpa using _root_.trans (by simpa using h₁) (by simpa using h₂))
    (fun a b => by simpa using IsTotal.total a b)
    l l' (by simpa using h) (by simpa using h')

Merging Preserves Sortedness

Informal description

Let $r$ be a binary relation on a type $\alpha$. For any two lists $l$ and $l'$ of elements of $\alpha$, if $l$ is sorted with respect to $r$ and $l'$ is sorted with respect to $r$, then the merged list $\operatorname{merge}(l, l', r)$ is also sorted with respect to $r$.

List.sorted_mergeSort' theorem

(l : List α) : Sorted r (mergeSort l (r · ·))

Full source

/-- Variant of `sorted_mergeSort` using relation typeclasses. -/
theorem sorted_mergeSort' (l : List α) : Sorted r (mergeSort l (r · ·)) := by
  simpa using sorted_mergeSort (le := (r · ·))
    (fun _ _ _ => by simpa using trans_of r)
    (by simpa using total_of r)
    l

Merge Sort Produces Sorted List with Respect to Given Relation

Informal description

For any list $l$ of elements of type $\alpha$ and any binary relation $r$ on $\alpha$, the result of applying the merge sort algorithm to $l$ with respect to $r$ is a list that is sorted with respect to $r$.

List.mergeSort_eq_self theorem

{l : List α} : Sorted r l → mergeSort l (r · ·) = l

Full source

theorem mergeSort_eq_self {l : List α} : Sorted r l → mergeSort l (r · ·) = l :=
  eq_of_perm_of_sorted (mergeSort_perm _ _) (sorted_mergeSort' _ l)

Merge Sort Preserves Already Sorted Lists

Informal description

For any list $l$ of elements of type $\alpha$ that is already sorted with respect to a relation $r$, applying the merge sort algorithm to $l$ with respect to $r$ yields the original list $l$, i.e., $\operatorname{mergeSort}(l, r) = l$.

List.mergeSort_eq_insertionSort theorem

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

Full source

theorem mergeSort_eq_insertionSort (l : List α) :
    mergeSort l (r · ·) = insertionSort r l :=
  eq_of_perm_of_sorted ((mergeSort_perm l _).trans (perm_insertionSort r l).symm)
    (sorted_mergeSort' r l) (sorted_insertionSort r l)

Merge Sort and Insertion Sort Yield Identical Results for Any Relation $r$

Informal description

For any list $l$ of elements of type $\alpha$ and any binary relation $r$ on $\alpha$, the result of applying the merge sort algorithm to $l$ with respect to $r$ is equal to the result of applying the insertion sort algorithm to $l$ with respect to $r$, i.e., $\operatorname{mergeSort}(l, r) = \operatorname{insertionSort}(l, r)$.