Init.Data.List.Sort.Lemmas

List.MergeSort.Internal.splitInTwo_fst theorem

 (l : { l : List α // l.length = n }) :
  (splitInTwo l).1 = ⟨l.1.take ((n + 1) / 2), by simp [splitInTwo, splitAt_eq, l.2]; omega⟩

Full source

@[simp] theorem splitInTwo_fst (l : { l : List α // l.length = n }) :
    (splitInTwo l).1 = ⟨l.1.take ((n+1)/2), by simp [splitInTwo, splitAt_eq, l.2]; omega⟩ := by
  simp [splitInTwo, splitAt_eq]

First Half of Split List Has Length $\lfloor (n+1)/2 \rfloor$

Informal description

For any list $l$ of type $\alpha$ with length $n$ (i.e., $l \in \{l' : \text{List } \alpha \mid \text{length}(l') = n\}$), the first component of splitting $l$ into two parts is equal to the first $\lfloor (n+1)/2 \rfloor$ elements of $l$, with a proof that this sublist has the correct length.

List.MergeSort.Internal.splitInTwo_snd theorem

 (l : { l : List α // l.length = n }) :
  (splitInTwo l).2 = ⟨l.1.drop ((n + 1) / 2), by simp [splitInTwo, splitAt_eq, l.2]; omega⟩

Full source

@[simp] theorem splitInTwo_snd (l : { l : List α // l.length = n }) :
    (splitInTwo l).2 = ⟨l.1.drop ((n+1)/2), by simp [splitInTwo, splitAt_eq, l.2]; omega⟩ := by
  simp [splitInTwo, splitAt_eq]

Second Component of Split List Equals Dropped Sublist

Informal description

For any list $l$ of length $n$ (with elements of type $\alpha$), the second component of the pair obtained by splitting $l$ into two parts is equal to the sublist obtained by dropping the first $\lfloor (n + 1)/2 \rfloor$ elements of $l$.

List.MergeSort.Internal.splitInTwo_fst_append_splitInTwo_snd theorem

(l : { l : List α // l.length = n }) : (splitInTwo l).1.1 ++ (splitInTwo l).2.1 = l.1

Full source

theorem splitInTwo_fst_append_splitInTwo_snd (l : { l : List α // l.length = n }) : (splitInTwo l).1.1 ++ (splitInTwo l).2.1 = l.1 := by
  simp

Reconstruction of List from Split Parts: $l_1 \mathbin{+\kern-0.5em+} l_2 = l$

Informal description

For any list $l$ of elements of type $\alpha$ with length $n$, the concatenation of the first and second components obtained by splitting $l$ via `splitInTwo` reconstructs the original list $l$. That is, if $(l_1, l_2) = \text{splitInTwo}(l)$, then $l_1 \mathbin{+\kern-0.5em+} l_2 = l$.

List.MergeSort.Internal.splitInTwo_cons_cons_zipIdx_fst theorem

 (i : Nat) (l : List α) :
  (splitInTwo ⟨(a, i) :: (b, i + 1) :: l.zipIdx (i + 2), rfl⟩).1.1 = (splitInTwo ⟨a :: b :: l, rfl⟩).1.1.zipIdx i

Full source

theorem splitInTwo_cons_cons_zipIdx_fst (i : Nat) (l : List α) :
    (splitInTwo ⟨(a, i) :: (b, i+1) :: l.zipIdx (i+2), rfl⟩).1.1 =
      (splitInTwo ⟨a :: b :: l, rfl⟩).1.1.zipIdx i := by
  simp only [length_cons, splitInTwo_fst, length_zipIdx]
  ext1 j
  rw [getElem?_take, getElem?_zipIdx, getElem?_take]
  split
  · rw [getElem?_cons, getElem?_cons, getElem?_cons, getElem?_cons]
    split
    · simp; omega
    · split
      · simp; omega
      · simp only [getElem?_zipIdx]
        congr
        ext <;> simp; omega
  · simp

First Half of Split Indexed List Equals Indexed First Half of Split Unindexed List

Informal description

For any natural number $i$ and list $l$ of elements of type $\alpha$, the first component of splitting the list $(a, i) :: (b, i+1) :: \mathrm{zipIdx}\ l\ (i+2)$ into two parts is equal to the first component of splitting $a :: b :: l$ into two parts, with each element paired with its index starting from $i$. In other words, splitting a list where the first two elements are already paired with indices $i$ and $i+1$ (and the rest are zipped with indices starting from $i+2$) gives the same result as first splitting the unindexed list $a :: b :: l$ and then pairing the elements in the first half with their corresponding indices starting from $i$.

List.MergeSort.Internal.splitInTwo_cons_cons_zipIdx_snd theorem

 (i : Nat) (l : List α) :
  (splitInTwo ⟨(a, i) :: (b, i + 1) :: l.zipIdx (i + 2), rfl⟩).2.1 =
    (splitInTwo ⟨a :: b :: l, rfl⟩).2.1.zipIdx (i + (l.length + 3) / 2)

Full source

theorem splitInTwo_cons_cons_zipIdx_snd (i : Nat) (l : List α) :
    (splitInTwo ⟨(a, i) :: (b, i+1) :: l.zipIdx (i+2), rfl⟩).2.1 =
      (splitInTwo ⟨a :: b :: l, rfl⟩).2.1.zipIdx (i+(l.length+3)/2) := by
  simp only [length_cons, splitInTwo_snd, length_zipIdx]
  ext1 j
  rw [getElem?_drop, getElem?_zipIdx, getElem?_drop]
  rw [getElem?_cons, getElem?_cons, getElem?_cons, getElem?_cons]
  split
  · simp; omega
  · split
    · simp; omega
    · simp only [getElem?_zipIdx]
      congr
      ext <;> simp; omega

Index Preservation in Second Split Component for Paired Lists

Informal description

For any natural number $i$ and list $l$ of elements of type $\alpha$, the second component of the split of the list $(a, i) :: (b, i+1) :: \mathrm{zipIdx}\ l\ (i+2)$ is equal to the second component of the split of $a :: b :: l$, with each element paired with its index starting from $i + \lfloor (|l| + 3)/2 \rfloor$. Here: - $\mathrm{zipIdx}\ l\ n$ pairs each element of $l$ with its index starting from $n$ - $\mathrm{splitInTwo}$ splits a list into two parts of roughly equal length - $|l|$ denotes the length of list $l$

List.MergeSort.Internal.splitInTwo_fst_sorted theorem

(l : { l : List α // l.length = n }) (h : Pairwise le l.1) : Pairwise le (splitInTwo l).1.1

Full source

theorem splitInTwo_fst_sorted (l : { l : List α // l.length = n }) (h : Pairwise le l.1) : Pairwise le (splitInTwo l).1.1 := by
  rw [splitInTwo_fst]
  exact h.take

Pairwise Order Preserved in First Half of Split List

Informal description

For any list $l$ of elements of type $\alpha$ with length $n$, if the elements of $l$ are pairwise related by a relation $\le$, then the first half of the list obtained by splitting $l$ into two parts also has its elements pairwise related by $\le$.

List.MergeSort.Internal.splitInTwo_snd_sorted theorem

(l : { l : List α // l.length = n }) (h : Pairwise le l.1) : Pairwise le (splitInTwo l).2.1

Full source

theorem splitInTwo_snd_sorted (l : { l : List α // l.length = n }) (h : Pairwise le l.1) : Pairwise le (splitInTwo l).2.1 := by
  rw [splitInTwo_snd]
  exact h.drop

Pairwise Relation Preserved in Second Sublist After Splitting

Informal description

For any list $l$ of length $n$ (with elements of type $\alpha$) and any binary relation `le` on $\alpha$, if `le` holds pairwise for all elements in $l$, then `le` also holds pairwise for all elements in the second sublist obtained by splitting $l$ into two parts.

List.MergeSort.Internal.splitInTwo_fst_le_splitInTwo_snd theorem

 {l : { l : List α // l.length = n }} (h : Pairwise le l.1) :
  ∀ a b, a ∈ (splitInTwo l).1.1 → b ∈ (splitInTwo l).2.1 → le a b

Full source

theorem splitInTwo_fst_le_splitInTwo_snd {l : { l : List α // l.length = n }} (h : Pairwise le l.1) :
    ∀ a b, a ∈ (splitInTwo l).1.1 → b ∈ (splitInTwo l).2.1 → le a b := by
  rw [splitInTwo_fst, splitInTwo_snd]
  intro a b ma mb
  exact h.rel_of_mem_take_of_mem_drop ma mb

Elements in First Half of Split List Are $\le$ Elements in Second Half for Pairwise Ordered Lists

Informal description

For any list $l$ of length $n$ (with elements of type $\alpha$) that is pairwise ordered with respect to a relation $\le$, if $a$ is an element in the first half of the split list and $b$ is an element in the second half, then $a \le b$ holds. Here, the first half consists of the first $\lfloor (n+1)/2 \rfloor$ elements, and the second half consists of the remaining elements.

List.zipIdxLE_trans theorem

 (trans : ∀ a b c, le a b → le b c → le a c) (a b c : α × Nat) : zipIdxLE le a b → zipIdxLE le b c → zipIdxLE le a c

Full source

theorem zipIdxLE_trans (trans : ∀ a b c, le a b → le b c → le a c)
    (a b c : α × Nat) : zipIdxLE le a b → zipIdxLE le b c → zipIdxLE le a c := by
  simp only [zipIdxLE]
  split <;> split <;> split <;> rename_i ab₂ ba₂ bc₂
  · simp_all
    intro ab₁
    intro h
    refine ⟨trans _ _ _ ab₂ bc₂, ?_⟩
    rcases h with (cd₂ | bc₁)
    · exact Or.inl (Decidable.byContradiction
        (fun ca₂ => by simp_all [trans _ _ _ (by simpa using ca₂) ab₂]))
    · exact Or.inr (Nat.le_trans ab₁ bc₁)
  · simp_all
  · simp_all
    intro h
    refine ⟨trans _ _ _ ab₂ bc₂, ?_⟩
    left
    rcases h with (cb₂ | _)
    · exact (Decidable.byContradiction
        (fun ca₂ => by simp_all [trans _ _ _ (by simpa using ca₂) ab₂]))
    · exact (Decidable.byContradiction
        (fun ca₂ => by simp_all [trans _ _ _ bc₂ (by simpa using ca₂)]))
  · simp_all
  · simp_all
  · simp_all
  · simp_all
  · simp_all

Transitivity of Lexicographic Order with Indexed Elements

Informal description

For any transitive relation `le` on a type `α`, and for any elements `a`, `b`, `c` of type `α × ℕ`, if `zipIdxLE le a b` and `zipIdxLE le b c` hold, then `zipIdxLE le a c` holds. Here, `zipIdxLE le x y` is the lexicographic order on pairs `(x₁, n)` and `(y₁, m)` where `x₁, y₁ ∈ α` and `n, m ∈ ℕ`, defined by `le x₁ y₁` or (`x₁ = y₁` and `n ≤ m`).

List.zipIdxLE_total theorem

(total : ∀ a b, le a b || le b a) (a b : α × Nat) : zipIdxLE le a b || zipIdxLE le b a

Full source

theorem zipIdxLE_total (total : ∀ a b, le a b || le b a)
    (a b : α × Nat) : zipIdxLEzipIdxLE le a b || zipIdxLE le b a := by
  simp only [zipIdxLE]
  split <;> split
  · simpa using Nat.le_total a.2 b.2
  · simp
  · simp
  · have := total a.1 b.1
    simp_all

Total Order Property of Indexed Pairs under `zipIdxLE`

Informal description

Given a total order relation `le` on a type `α` (meaning for any `a b : α`, either `le a b` or `le b a` holds), then for any two pairs `(a, n)` and `(b, m)` in `α × ℕ`, either `zipIdxLE le (a, n) (b, m)` or `zipIdxLE le (b, m) (a, n)` holds.

List.cons_merge_cons theorem

 (s : α → α → Bool) (a b l r) :
  merge (a :: l) (b :: r) s = if s a b then a :: merge l (b :: r) s else b :: merge (a :: l) r s

Full source

theorem cons_merge_cons (s : α → α → Bool) (a b l r) :
    merge (a::l) (b::r) s = if s a b then a :: merge l (b::r) s else b :: merge (a::l) r s := by
  simp only [merge]

Merge Step for Cons Lists with Comparison Function

Informal description

Given a comparison function $s : \alpha \to \alpha \to \mathtt{Bool}$ and elements $a, b \in \alpha$ with lists $l, r : \mathtt{List}\ \alpha$, the merge of the lists $a :: l$ and $b :: r$ under $s$ is defined as: \[ \mathtt{merge}\ (a :: l)\ (b :: r)\ s = \begin{cases} a :: \mathtt{merge}\ l\ (b :: r)\ s & \text{if } s\ a\ b \text{ is true}, \\ b :: \mathtt{merge}\ (a :: l)\ r\ s & \text{otherwise}. \end{cases} \]

List.cons_merge_cons_pos theorem

(s : α → α → Bool) (l r) (h : s a b) : merge (a :: l) (b :: r) s = a :: merge l (b :: r) s

Full source

@[simp] theorem cons_merge_cons_pos (s : α → α → Bool) (l r) (h : s a b) :
    merge (a::l) (b::r) s = a :: merge l (b::r) s := by
  rw [cons_merge_cons, if_pos h]

Merge Step for Cons Lists When Comparison Holds

Informal description

Given a comparison function $s : \alpha \to \alpha \to \mathtt{Bool}$, two lists $l, r : \mathtt{List}\ \alpha$, and elements $a, b \in \alpha$ such that $s(a, b)$ holds, the merge of the lists $a :: l$ and $b :: r$ under $s$ satisfies: \[ \mathtt{merge}\ (a :: l)\ (b :: r)\ s = a :: \mathtt{merge}\ l\ (b :: r)\ s. \]

List.cons_merge_cons_neg theorem

(s : α → α → Bool) (l r) (h : ¬s a b) : merge (a :: l) (b :: r) s = b :: merge (a :: l) r s

Full source

@[simp] theorem cons_merge_cons_neg (s : α → α → Bool) (l r) (h : ¬ s a b) :
    merge (a::l) (b::r) s = b :: merge (a::l) r s := by
  rw [cons_merge_cons, if_neg h]

Merge Step for Cons Lists When Comparison Fails

Informal description

Given a comparison function $s : \alpha \to \alpha \to \mathtt{Bool}$, two lists $l, r : \mathtt{List}\ \alpha$, and elements $a, b \in \alpha$ such that $s(a, b)$ does not hold, the merge of the lists $a :: l$ and $b :: r$ under $s$ satisfies: \[ \mathtt{merge}\ (a :: l)\ (b :: r)\ s = b :: \mathtt{merge}\ (a :: l)\ r\ s. \]

List.length_merge theorem

(s : α → α → Bool) (l r) : (merge l r s).length = l.length + r.length

Full source

@[simp] theorem length_merge (s : α → α → Bool) (l r) :
    (merge l r s).length = l.length + r.length := by
  match l, r with
  | [], r => simp
  | l, [] => simp
  | a::l, b::r =>
    rw [cons_merge_cons]
    split
    · simp +arith [length_merge s l (b::r)]
    · simp +arith [length_merge s (a::l) r]

Length Preservation in List Merge

Informal description

For any binary predicate `s` on elements of type `α` and any two lists `l` and `r` of type `List α`, the length of the merged list `merge l r s` is equal to the sum of the lengths of `l` and `r`. That is, $|\text{merge}(l, r, s)| = |l| + |r|$.

List.mem_merge theorem

{a : α} {xs ys : List α} : a ∈ merge xs ys le ↔ a ∈ xs ∨ a ∈ ys

Full source

/--
The elements of `merge le xs ys` are exactly the elements of `xs` and `ys`.
-/
-- We subsequently prove that `mergeSort_perm : merge le xs ys ~ xs ++ ys`.
theorem mem_merge {a : α} {xs ys : List α} : a ∈ merge xs ys lea ∈ merge xs ys le ↔ a ∈ xs ∨ a ∈ ys := by
  induction xs generalizing ys with
  | nil => simp [merge]
  | cons x xs ih =>
    induction ys with
    | nil => simp [merge]
    | cons y ys ih =>
      simp only [merge]
      split <;> rename_i h
      · simp_all [or_assoc]
      · simp only [mem_cons, or_assoc, Bool.not_eq_true, ih, ← or_assoc]
        apply or_congr_left
        simp only [or_comm (a := a = y), or_assoc]

Membership in Merged List: $a \in \text{merge}\ xs\ ys\ le \leftrightarrow a \in xs \lor a \in ys$

Informal description

For any element $a$ and lists $xs, ys$ of type $\alpha$, the element $a$ belongs to the merged list $\text{merge}\ xs\ ys\ le$ if and only if $a$ belongs to $xs$ or $a$ belongs to $ys$.

List.mem_merge_left theorem

(s : α → α → Bool) (h : x ∈ l) : x ∈ merge l r s

Full source

theorem mem_merge_left (s : α → α → Bool) (h : x ∈ l) : x ∈ merge l r s :=
  mem_merge.2 <| .inl h

Membership Preservation in Left Merge: $x \in l \implies x \in \text{merge}(l, r, s)$

Informal description

For any element $x$ in a list $l$ of type $\alpha$, and for any binary predicate $s$ on elements of type $\alpha$, the element $x$ belongs to the merged list $\text{merge}(l, r, s)$ for any list $r$ of type $\alpha$.

List.mem_merge_right theorem

(s : α → α → Bool) (h : x ∈ r) : x ∈ merge l r s

Full source

theorem mem_merge_right (s : α → α → Bool) (h : x ∈ r) : x ∈ merge l r s :=
  mem_merge.2 <| .inr h

Membership Preservation in Merge Operation (Right Side)

Informal description

For any element $x$ and lists $l, r$ of type $\alpha$, if $x$ is an element of $r$, then $x$ is also an element of the merged list $\text{merge}\ l\ r\ s$, where $s$ is a binary comparison function on $\alpha$.

List.merge_stable theorem

 :
  ∀ (xs ys) (_ : ∀ x y, x ∈ xs → y ∈ ys → x.2 ≤ y.2),
    (merge xs ys (zipIdxLE le)).map (·.1) = merge (xs.map (·.1)) (ys.map (·.1)) le

Full source

theorem merge_stable : ∀ (xs ys) (_ : ∀ x y, x ∈ xs → y ∈ ys → x.2 ≤ y.2),
    (merge xs ys (zipIdxLE le)).map (·.1) = merge (xs.map (·.1)) (ys.map (·.1)) le
  | [], ys, _ => by simp [merge]
  | xs, [], _ => by simp [merge]
  | (i, x)(i, x) :: xs, (j, y)(j, y) :: ys, h => by
    simp only [merge, zipIdxLE, map_cons]
    split <;> rename_i w
    · rw [if_pos (by simp [h _ _ (mem_cons_self ..) (mem_cons_self ..)])]
      simp only [map_cons, cons.injEq, true_and]
      rw [merge_stable, map_cons]
      exact fun x' y' mx my => h x' y' (mem_cons_of_mem (i, x) mx) my
    · simp only [↓reduceIte, map_cons, cons.injEq, true_and, reduceCtorEq]
      rw [merge_stable, map_cons]
      exact fun x' y' mx my => h x' y' mx (mem_cons_of_mem (j, y) my)

Stability of Merge Operation Under Component Projection

Informal description

For any two lists `xs` and `ys` of pairs, if for all pairs `x ∈ xs` and `y ∈ ys` the second component of `x` is less than or equal to the second component of `y` (i.e., $x_2 \leq y_2$), then the list obtained by: 1. Merging `xs` and `ys` using the comparison function `zipIdxLE le` (which compares the second components), and then 2. Mapping each pair to its first component is equal to the list obtained by: 1. Mapping both `xs` and `ys` to their first components, and then 2. Merging the resulting lists using the original comparison function `le`. In symbols: $$(\text{merge}\ xs\ ys\ (\text{zipIdxLE}\ le)).\text{map}\ (\cdot.1) = \text{merge}\ (xs.\text{map}\ (\cdot.1))\ (ys.\text{map}\ (\cdot.1))\ le$$

List.sorted_merge theorem

 (trans : ∀ (a b c : α), le a b → le b c → le a c) (total : ∀ (a b : α), le a b || le b a) (l₁ l₂ : List α)
  (h₁ : l₁.Pairwise le) (h₂ : l₂.Pairwise le) : (merge l₁ l₂ le).Pairwise le

Full source

/--
If the ordering relation `le` is transitive and total (i.e. `le a b || le b a` for all `a, b`)
then the `merge` of two sorted lists is sorted.
-/
theorem sorted_merge
    (trans : ∀ (a b c : α), le a b → le b c → le a c)
    (total : ∀ (a b : α), le a b || le b a)
    (l₁ l₂ : List α) (h₁ : l₁.Pairwise le) (h₂ : l₂.Pairwise le) : (merge l₁ l₂ le).Pairwise le := by
  induction l₁ generalizing l₂ with
  | nil => simpa only [merge]
  | cons x l₁ ih₁ =>
    induction l₂ with
    | nil => simpa only [merge]
    | cons y l₂ ih₂ =>
      simp only [merge]
      split <;> rename_i h
      · apply Pairwise.cons
        · intro z m
          rw [mem_merge, mem_cons] at m
          rcases m with (m|rfl|m)
          · exact rel_of_pairwise_cons h₁ m
          · exact h
          · exact trans _ _ _ h (rel_of_pairwise_cons h₂ m)
        · exact ih₁ _ h₁.tail h₂
      · apply Pairwise.cons
        · intro z m
          rw [mem_merge, mem_cons] at m
          simp only [Bool.not_eq_true] at h
          rcases m with (⟨rfl|m⟩|m)
          · simpa [h] using total y z
          · exact trans _ _ _ (by simpa [h] using total x y) (rel_of_pairwise_cons h₁ m)
          · exact rel_of_pairwise_cons h₂ m
        · exact ih₂ h₂.tail

Merge Preserves Sortedness for Transitive and Total Relations

Informal description

Let $\alpha$ be a type with a binary relation $\le$ that is transitive (i.e., for all $a, b, c \in \alpha$, if $a \le b$ and $b \le c$ then $a \le c$) and total (i.e., for all $a, b \in \alpha$, either $a \le b$ or $b \le a$). If $l_1$ and $l_2$ are lists of elements of $\alpha$ that are pairwise sorted with respect to $\le$, then the merged list $\text{merge}(l_1, l_2, \le)$ is also pairwise sorted with respect to $\le$.

List.merge_of_le theorem

: ∀ {xs ys : List α} (_ : ∀ a b, a ∈ xs → b ∈ ys → le a b), merge xs ys le = xs ++ ys

Full source

theorem merge_of_le : ∀ {xs ys : List α} (_ : ∀ a b, a ∈ xs → b ∈ ys → le a b),
    merge xs ys le = xs ++ ys
  | [], ys, _
  | xs, [], _ => by simp [merge]
  | x :: xs, y :: ys, h => by
    simp only [merge, cons_append]
    rw [if_pos, merge_of_le]
    · intro a b ma mb
      exact h a b (mem_cons_of_mem _ ma) mb
    · exact h x y mem_cons_self mem_cons_self

Merge Equals Concatenation When All Elements in First List Are Less Than or Equal to All Elements in Second List

Informal description

For any two lists `xs` and `ys` of elements of type `α`, if for all elements `a ∈ xs` and `b ∈ ys` the relation `le a b` holds, then the merge of `xs` and `ys` under the comparison function `le` is equal to the concatenation of `xs` and `ys`, i.e., $\text{merge}(xs, ys, le) = xs \mathbin{+\kern-0.5em+} ys$.

List.merge_perm_append theorem

: ∀ {xs ys : List α}, merge xs ys le ~ xs ++ ys

Full source

theorem merge_perm_append : ∀ {xs ys : List α}, mergemerge xs ys le ~ xs ++ ys
  | [], ys => by simp [merge]
  | xs, [] => by simp [merge]
  | x :: xs, y :: ys => by
    simp only [merge]
    split
    · exact merge_perm_append.cons x
    · exact (merge_perm_append.cons y).trans
        ((Perm.swap x y _).trans (perm_middle.symm.cons x))

Merge Permutation: $\text{merge}(xs, ys, le) \sim xs ++ ys$

Informal description

For any two lists `xs` and `ys` of elements of type `α`, the merge of `xs` and `ys` under a comparison function `le` is a permutation of the concatenation of `xs` and `ys`. In other words, the merged list contains exactly the same elements as `xs ++ ys`, possibly in a different order.

List.Perm.merge theorem

(s₁ s₂ : α → α → Bool) (hl : l₁ ~ l₂) (hr : r₁ ~ r₂) : merge l₁ r₁ s₁ ~ merge l₂ r₂ s₂

Full source

theorem Perm.merge (s₁ s₂ : α → α → Bool) (hl : l₁ ~ l₂) (hr : r₁ ~ r₂) :
    mergemerge l₁ r₁ s₁ ~ merge l₂ r₂ s₂ :=
  Perm.trans (merge_perm_append ..) <| Perm.trans (Perm.append hl hr) <| Perm.symm (merge_perm_append ..)

Permutation Preservation Under Merge: $l_1 \sim l_2 \land r_1 \sim r_2 \Rightarrow \text{merge}(l_1, r_1, s_1) \sim \text{merge}(l_2, r_2, s_2)$

Informal description

For any two pairs of lists $(l_1, l_2)$ and $(r_1, r_2)$ of elements of type $\alpha$, if $l_1$ is a permutation of $l_2$ (denoted $l_1 \sim l_2$) and $r_1$ is a permutation of $r_2$ (denoted $r_1 \sim r_2$), then for any two comparison functions $s_1$ and $s_2$, the merge of $l_1$ and $r_1$ under $s_1$ is a permutation of the merge of $l_2$ and $r_2$ under $s_2$ (i.e., $\text{merge}(l_1, r_1, s_1) \sim \text{merge}(l_2, r_2, s_2)$).

List.mergeSort_nil theorem

: [].mergeSort r = []

Full source

@[simp] theorem mergeSort_nil : [].mergeSort r = [] := by rw [List.mergeSort]

Merge Sort Preserves Empty List

Informal description

The merge sort algorithm applied to the empty list `[]` with any comparison function `r` returns the empty list `[]`.

List.mergeSort_singleton theorem

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

Full source

@[simp] theorem mergeSort_singleton (a : α) : [a].mergeSort r = [a] := by rw [List.mergeSort]

Merge Sort Preserves Singleton Lists

Informal description

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

List.mergeSort_perm theorem

: ∀ (l : List α) (le), mergeSort l le ~ l

Full source

theorem mergeSort_perm : ∀ (l : List α) (le), mergeSortmergeSort l le ~ l
  | [], _ => by simp [mergeSort]
  | [a], _ => by simp [mergeSort]
  | a :: b :: xs, le => by
    simp only [mergeSort]
    have : (splitInTwo ⟨a :: b :: xs, rfl⟩).1.1.length < xs.length + 1 + 1 := by simp [splitInTwo_fst]; omega
    have : (splitInTwo ⟨a :: b :: xs, rfl⟩).2.1.length < xs.length + 1 + 1 := by simp [splitInTwo_snd]; omega
    exact (merge_perm_append le).trans
      (((mergeSort_perm _ _).append (mergeSort_perm _ _)).trans
        (Perm.of_eq (splitInTwo_fst_append_splitInTwo_snd _)))
termination_by l => l.length

Permutation Property of Merge Sort

Informal description

For any list $l$ of elements of type $\alpha$ and any binary relation `le` on $\alpha$, the result of `mergeSort l le` is a permutation of $l$, i.e., the sorted list contains the same elements as the original list, possibly in a different order.

List.length_mergeSort theorem

(l : List α) : (mergeSort l le).length = l.length

Full source

@[simp] theorem length_mergeSort (l : List α) : (mergeSort l le).length = l.length :=
  (mergeSort_perm l le).length_eq

Length Preservation in Merge Sort: $\text{length}(\text{mergeSort}(l)) = \text{length}(l)$

Informal description

For any list $l$ of elements of type $\alpha$ and any binary relation `le` on $\alpha$, the length of the sorted list `mergeSort l le` is equal to the length of the original list $l$.

List.mem_mergeSort theorem

{a : α} {l : List α} : a ∈ mergeSort l le ↔ a ∈ l

Full source

@[simp] theorem mem_mergeSort {a : α} {l : List α} : a ∈ mergeSort l lea ∈ mergeSort l le ↔ a ∈ l :=
  (mergeSort_perm l le).mem_iff

Membership Preservation in Merge Sort: $a \in \text{mergeSort}(l) \leftrightarrow a \in l$

Informal description

For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the element $a$ is in the list `mergeSort l le` if and only if $a$ is in the original list $l$. In other words, the merge sort algorithm preserves the membership of elements.

List.sorted_mergeSort theorem

 (trans : ∀ (a b c : α), le a b → le b c → le a c) (total : ∀ (a b : α), le a b || le b a) :
  (l : List α) → (mergeSort l le).Pairwise le

Full source

/--
The result of `mergeSort` is sorted,
as long as the comparison function is transitive (`le a b → le b c → le a c`)
and total in the sense that `le a b || le b a`.

The comparison function need not be irreflexive, i.e. `le a b` and `le b a` is allowed even when `a ≠ b`.
-/
theorem sorted_mergeSort
    (trans : ∀ (a b c : α), le a b → le b c → le a c)
    (total : ∀ (a b : α), le a b || le b a) :
    (l : List α) → (mergeSort l le).Pairwise le
  | [] => by simp [mergeSort]
  | [a] => by simp [mergeSort]
  | a :: b :: xs => by
    rw [mergeSort]
    apply sorted_merge @trans @total
    apply sorted_mergeSort trans total
    apply sorted_mergeSort trans total
termination_by l => l.length

Merge Sort Produces Sorted List for Transitive and Total Relations

Informal description

Let $\alpha$ be a type equipped with a binary relation $\le$ that is transitive (i.e., for all $a, b, c \in \alpha$, if $a \le b$ and $b \le c$ then $a \le c$) and total (i.e., for all $a, b \in \alpha$, either $a \le b$ or $b \le a$). Then for any list $l$ of elements of $\alpha$, the result of merge sorting $l$ with respect to $\le$ is a list that is pairwise sorted with respect to $\le$.

List.mergeSort_sorted abbrev

Full source

@[deprecated sorted_mergeSort (since := "2024-09-02")] abbrev mergeSort_sorted := @sorted_mergeSort

Merge Sort Produces Sorted List for Transitive and Total Relations

Informal description

For any list $l$ of elements of type $\alpha$ and any transitive and total relation $\le$ on $\alpha$, the result of merge sorting $l$ with respect to $\le$ is a list that is sorted with respect to $\le$.

List.mergeSort_of_sorted theorem

: ∀ {l : List α} (_ : Pairwise le l), mergeSort l le = l

Full source

/--
If the input list is already sorted, then `mergeSort` does not change the list.
-/
theorem mergeSort_of_sorted : ∀ {l : List α} (_ : Pairwise le l), mergeSort l le = l
  | [], _ => by simp [mergeSort]
  | [a], _ => by simp [mergeSort]
  | a :: b :: xs, h => by
    have : (splitInTwo ⟨a :: b :: xs, rfl⟩).1.1.length < xs.length + 1 + 1 := by simp [splitInTwo_fst]; omega
    have : (splitInTwo ⟨a :: b :: xs, rfl⟩).2.1.length < xs.length + 1 + 1 := by simp [splitInTwo_snd]; omega
    rw [mergeSort]
    rw [mergeSort_of_sorted (splitInTwo_fst_sorted ⟨a :: b :: xs, rfl⟩ h)]
    rw [mergeSort_of_sorted (splitInTwo_snd_sorted ⟨a :: b :: xs, rfl⟩ h)]
    rw [merge_of_le (splitInTwo_fst_le_splitInTwo_snd h)]
    rw [splitInTwo_fst_append_splitInTwo_snd]
termination_by l => l.length

Merge Sort Preserves Sorted Lists

Informal description

For any list `l` of elements of type `α` that is already sorted with respect to a relation `le` (i.e., `Pairwise le l` holds), the `mergeSort` algorithm leaves the list unchanged: `mergeSort l le = l`.

List.mergeSort_zipIdx theorem

{l : List α} : (mergeSort (l.zipIdx) (zipIdxLE le)).map (·.1) = mergeSort l le

Full source

/--
This merge sort algorithm is stable,
in the sense that breaking ties in the ordering function using the position in the list
has no effect on the output.

That is, elements which are equal with respect to the ordering function will remain
in the same order in the output list as they were in the input list.

See also:
* `sublist_mergeSort`: if `c <+ l` and `c.Pairwise le`, then `c <+ mergeSort le l`.
* `pair_sublist_mergeSort`: if `[a, b] <+ l` and `le a b`, then `[a, b] <+ mergeSort le l`)
-/
theorem mergeSort_zipIdx {l : List α} :
    (mergeSort (l.zipIdx) (zipIdxLE le)).map (·.1) = mergeSort l le :=
  go 0 l
where go : ∀ (i : Nat) (l : List α),
    (mergeSort (l.zipIdx i) (zipIdxLE le)).map (·.1) = mergeSort l le
  | _, []
  | _, [a] => by simp [mergeSort]
  | _, a :: b :: xs => by
    have : (splitInTwo ⟨a :: b :: xs, rfl⟩).1.1.length < xs.length + 1 + 1 := by simp [splitInTwo_fst]; omega
    have : (splitInTwo ⟨a :: b :: xs, rfl⟩).2.1.length < xs.length + 1 + 1 := by simp [splitInTwo_snd]; omega
    simp only [mergeSort, zipIdx]
    rw [splitInTwo_cons_cons_zipIdx_fst]
    rw [splitInTwo_cons_cons_zipIdx_snd]
    rw [merge_stable]
    · rw [go, go]
    · simp only [mem_mergeSort, Prod.forall]
      intros j x k y mx my
      have := mem_zipIdx mx
      have := mem_zipIdx my
      simp_all
      omega
termination_by _ l => l.length

Stability of Merge Sort: Preservation of Relative Order via Indexing

Informal description

For any list $l$ of elements of type $\alpha$, applying the merge sort algorithm to the list of pairs $(x, i)$ where $x$ is an element of $l$ and $i$ is its index (using the ordering `zipIdxLE le`), and then projecting back to the first components, yields the same result as applying merge sort directly to $l$ with the ordering `le`. In other words, the stability of merge sort ensures that the relative order of equal elements (according to `le`) is preserved. Symbolically: $$\text{map} (\pi_1) (\text{mergeSort} (\text{zipIdx}\ l) (\text{zipIdxLE}\ le)) = \text{mergeSort}\ l\ le$$ where $\pi_1$ denotes the projection to the first component of a pair.

List.mergeSort_enum abbrev

Full source

@[deprecated mergeSort_zipIdx (since := "2025-01-21")] abbrev mergeSort_enum := @mergeSort_zipIdx

Stability of Merge Sort via Enumeration: Preservation of Relative Order

Informal description

For any list $l$ of elements of type $\alpha$, applying the merge sort algorithm to the enumerated version of $l$ (where each element is paired with its position index) using the indexed ordering relation, and then projecting back to the original elements, yields the same result as applying merge sort directly to $l$ with the original ordering relation. Symbolically: $$\text{map} (\pi_1) (\text{mergeSort} (\text{enum}\ l) (\text{enumLE}\ le)) = \text{mergeSort}\ l\ le$$ where $\pi_1$ denotes the projection to the first component of a pair and $\text{enumLE}\ le$ is the ordering relation extended to account for indices.

List.mergeSort_cons theorem

 {le : α → α → Bool} (trans : ∀ (a b c : α), le a b → le b c → le a c) (total : ∀ (a b : α), le a b || le b a) (a : α)
  (l : List α) : ∃ l₁ l₂, mergeSort (a :: l) le = l₁ ++ a :: l₂ ∧ mergeSort l le = l₁ ++ l₂ ∧ ∀ b, b ∈ l₁ → !le a b

Full source

theorem mergeSort_cons {le : α → α → Bool}
    (trans : ∀ (a b c : α), le a b → le b c → le a c)
    (total : ∀ (a b : α), le a b || le b a)
    (a : α) (l : List α) :
    ∃ l₁ l₂, mergeSort (a :: l) le = l₁ ++ a :: l₂ ∧ mergeSort l le = l₁ ++ l₂ ∧
      ∀ b, b ∈ l₁ → !le a b := by
  rw [← mergeSort_zipIdx]
  rw [zipIdx_cons]
  have nd : Nodup ((a :: l).zipIdx.map (·.2)) := by rw [zipIdx_map_snd]; exact nodup_range' _
  have m₁ : (a, 0)(a, 0) ∈ mergeSort ((a :: l).zipIdx) (zipIdxLE le) :=
    mem_mergeSort.mpr mem_cons_self
  obtain ⟨l₁, l₂, h⟩ := append_of_mem m₁
  have s := sorted_mergeSort (zipIdxLE_trans trans) (zipIdxLE_total total) ((a :: l).zipIdx)
  rw [h] at s
  have p := mergeSort_perm ((a :: l).zipIdx) (zipIdxLE le)
  rw [h] at p
  refine ⟨l₁.map (·.1), l₂.map (·.1), ?_, ?_, ?_⟩
  · simpa using congrArg (·.map (·.1)) h
  · rw [← mergeSort_zipIdx.go 1, ← map_append]
    congr 1
    have q : mergeSortmergeSort (l.zipIdx 1) (zipIdxLE le) ~ l₁ ++ l₂ :=
      (mergeSort_perm (l.zipIdx 1) (zipIdxLE le)).trans
        (p.symm.trans perm_middle).cons_inv
    apply Perm.eq_of_sorted (le := zipIdxLE le)
    · rintro ⟨a, i⟩ ⟨b, j⟩  ha hb
      simp only [mem_mergeSort] at ha
      simp only [← q.mem_iff, mem_mergeSort] at hb
      simp only [zipIdxLE]
      simp only [Bool.if_false_right, Bool.and_eq_true, Prod.mk.injEq, and_imp]
      intro ab h ba h'
      simp only [Bool.decide_eq_true] at ba
      replace h : i ≤ j := by simpa [ab, ba] using h
      replace h' : j ≤ i := by simpa [ab, ba] using h'
      cases Nat.le_antisymm h h'
      constructor
      · have := mem_zipIdx ha
        have := mem_zipIdx hb
        simp_all
      · rfl
    · exact sorted_mergeSort (zipIdxLE_trans trans) (zipIdxLE_total total) ..
    · exact s.sublist ((sublist_cons_self (a, 0) l₂).append_left l₁)
    · exact q
  · intro b m
    simp only [mem_map, Prod.exists] at m
    obtain ⟨j, _, m, rfl⟩ := m
    replace p := p.map (·.2)
    have nd' := nd.perm p.symm
    rw [map_append] at nd'
    have j0 := nd'.rel_of_mem_append
      (mem_map_of_mem m) (mem_map_of_mem mem_cons_self)
    simp only [ne_eq] at j0
    have r := s.rel_of_mem_append m mem_cons_self
    simp_all [zipIdxLE]

Decomposition of Merge Sort on Cons List: $\text{mergeSort}(a :: l, \le) = l_1 ++ (a :: l_2)$ with $\text{mergeSort}(l, \le) = l_1 ++ l_2$ and $\forall b \in l_1, \neg (a \le b)$

Informal description

Let $\alpha$ be a type equipped with a binary relation $\le : \alpha \to \alpha \to \text{Bool}$ that is transitive (i.e., for all $a, b, c \in \alpha$, if $a \le b$ and $b \le c$ then $a \le c$) and total (i.e., for all $a, b \in \alpha$, either $a \le b$ or $b \le a$). Then for any element $a \in \alpha$ and any list $l$ of elements of $\alpha$, there exist lists $l_1$ and $l_2$ such that: 1. $\text{mergeSort}(a :: l, \le) = l_1 ++ (a :: l_2)$, 2. $\text{mergeSort}(l, \le) = l_1 ++ l_2$, and 3. For every $b \in l_1$, $\neg (a \le b)$.

List.sublist_mergeSort theorem

 (trans : ∀ (a b c : α), le a b → le b c → le a c) (total : ∀ (a b : α), le a b || le b a) :
  ∀ {ys : List α} (_ : ys.Pairwise le) (_ : ys <+ xs), ys <+ mergeSort xs le

Full source

/--
Another statement of stability of merge sort.
If `c` is a sorted sublist of `l`,
then `c` is still a sublist of `mergeSort le l`.
-/
theorem sublist_mergeSort
    (trans : ∀ (a b c : α), le a b → le b c → le a c)
    (total : ∀ (a b : α), le a b || le b a) :
    ∀ {ys : List α} (_ : ys.Pairwise le) (_ : ys <+ xs),
    ys <+ mergeSort xs le
  | _, _, .slnil => nil_sublist _
  | ys, hc, @Sublist.cons _ _ l a h => by
    obtain ⟨l₁, l₂, h₁, h₂, -⟩ := mergeSort_cons trans total a l
    rw [h₁]
    have h' := sublist_mergeSort trans total hc h
    rw [h₂] at h'
    exact h'.middle a
  | _, _, @Sublist.cons₂ _ l₁ l₂ a h => by
    rename_i hc
    obtain ⟨l₃, l₄, h₁, h₂, h₃⟩ := mergeSort_cons trans total a l₂
    rw [h₁]
    have h' := sublist_mergeSort trans total hc.tail h
    rw [h₂] at h'
    simp only [Bool.not_eq_true', tail_cons] at h₃ h'
    exact
      sublist_append_of_sublist_right (Sublist.cons₂ a
        ((fun w => Sublist.of_sublist_append_right w h') fun b m₁ m₃ =>
          (Bool.eq_not_self true).mp ((rel_of_pairwise_cons hc m₁).symm.trans (h₃ b m₃))))

Stability of Merge Sort: Sublist Preservation for Pairwise Lists

Informal description

Let $\alpha$ be a type equipped with a binary relation $\le : \alpha \to \alpha \to \text{Bool}$ that is transitive (i.e., for all $a, b, c \in \alpha$, if $a \le b$ and $b \le c$ then $a \le c$) and total (i.e., for all $a, b \in \alpha$, either $a \le b$ or $b \le a$). Then for any list $xs$ of elements of $\alpha$ and any sublist $ys$ of $xs$ that is pairwise with respect to $\le$, $ys$ remains a sublist of $\text{mergeSort}(xs, \le)$.

List.mergeSort_stable abbrev

Full source

@[deprecated sublist_mergeSort (since := "2024-09-02")]
abbrev mergeSort_stable := @sublist_mergeSort

Stability of Merge Sort: Preservation of Relative Order for Comparable Elements

Informal description

Let $\alpha$ be a type equipped with a binary relation $\le : \alpha \to \alpha \to \text{Bool}$ that is transitive (i.e., for all $a, b, c \in \alpha$, if $a \le b$ and $b \le c$ then $a \le c$) and total (i.e., for all $a, b \in \alpha$, either $a \le b$ or $b \le a$). Then for any list $l$ of elements of $\alpha$, the merge sort algorithm preserves the relative order of any two elements $a, b \in l$ that satisfy $a \le b$.

List.pair_sublist_mergeSort theorem

 (trans : ∀ (a b c : α), le a b → le b c → le a c) (total : ∀ (a b : α), le a b || le b a) (hab : le a b)
  (h : [a, b] <+ l) : [a, b] <+ mergeSort l le

Full source

/--
Another statement of stability of merge sort.
If a pair `[a, b]` is a sublist of `l` and `le a b`,
then `[a, b]` is still a sublist of `mergeSort le l`.
-/
theorem pair_sublist_mergeSort
    (trans : ∀ (a b c : α), le a b → le b c → le a c)
    (total : ∀ (a b : α), le a b || le b a)
    (hab : le a b) (h : [a, b][a, b] <+ l) : [a, b][a, b] <+ mergeSort l le :=
  sublist_mergeSort trans total (pairwise_pair.mpr hab) h

Stability of Merge Sort: Preservation of Ordered Sublists $[a, b]$

Informal description

Let $\alpha$ be a type equipped with a binary relation $\le : \alpha \to \alpha \to \text{Bool}$ that is transitive (i.e., for all $a, b, c \in \alpha$, if $a \le b$ and $b \le c$ then $a \le c$) and total (i.e., for all $a, b \in \alpha$, either $a \le b$ or $b \le a$). If $[a, b]$ is a sublist of a list $l$ and $a \le b$, then $[a, b]$ remains a sublist of $\text{mergeSort}(l, \le)$.

List.mergeSort_stable_pair abbrev

Full source

@[deprecated pair_sublist_mergeSort(since := "2024-09-02")]
abbrev mergeSort_stable_pair := @pair_sublist_mergeSort

Stability of Merge Sort: Preservation of Ordered Pairs $[a, b]$

Informal description

Let $\alpha$ be a type equipped with a binary relation $\le : \alpha \to \alpha \to \text{Bool}$ that is transitive (i.e., for all $a, b, c \in \alpha$, if $a \le b$ and $b \le c$ then $a \le c$) and total (i.e., for all $a, b \in \alpha$, either $a \le b$ or $b \le a$). For any list $l$ of elements of $\alpha$, if $[a, b]$ is a sublist of $l$ and $a \le b$, then $[a, b]$ remains a sublist of $\text{mergeSort}(l, \le)$.

List.map_merge theorem

 {f : α → β} {r : α → α → Bool} {s : β → β → Bool} {l l' : List α} (hl : ∀ a ∈ l, ∀ b ∈ l', r a b = s (f a) (f b)) :
  (l.merge l' r).map f = (l.map f).merge (l'.map f) s

Full source

theorem map_merge {f : α → β} {r : α → α → Bool} {s : β → β → Bool} {l l' : List α}
    (hl : ∀ a ∈ l, ∀ b ∈ l', r a b = s (f a) (f b)) :
    (l.merge l' r).map f = (l.map f).merge (l'.map f) s := by
  match l, l' with
  | [], _ => simp
  | _, [] => simp
  | _ :: _, _ :: _ =>
    simp only [List.forall_mem_cons] at hl
    simp only [forall_and] at hl
    simp only [List.map, List.cons_merge_cons]
    rw [← hl.1.1]
    split
    · rw [List.map, map_merge, List.map]
      simp only [List.forall_mem_cons, forall_and]
      exact ⟨hl.2.1, hl.2.2⟩
    · rw [List.map, map_merge, List.map]
      simp only [List.forall_mem_cons]
      exact ⟨hl.1.2, hl.2.2⟩

Map-Merge Commutativity: $\text{map } f \circ \text{merge } = \text{merge } \circ (\text{map } f \times \text{map } f)$

Informal description

Let $f : \alpha \to \beta$ be a function, and let $r : \alpha \to \alpha \to \text{Bool}$ and $s : \beta \to \beta \to \text{Bool}$ be binary relations on $\alpha$ and $\beta$ respectively. For any two lists $l, l'$ of elements of type $\alpha$, if for all $a \in l$ and $b \in l'$ we have $r(a, b) = s(f(a), f(b))$, then the map of the merge of $l$ and $l'$ under $r$ is equal to the merge of the mapped lists $l.map f$ and $l'.map f$ under $s$. In other words: \[ \text{map } f (\text{merge } l \ l' \ r) = \text{merge } (l.map f) \ (l'.map f) \ s \]

List.map_mergeSort theorem

 {r : α → α → Bool} {s : β → β → Bool} {f : α → β} {l : List α} (hl : ∀ a ∈ l, ∀ b ∈ l, r a b = s (f a) (f b)) :
  (l.mergeSort r).map f = (l.map f).mergeSort s

Full source

theorem map_mergeSort {r : α → α → Bool} {s : β → β → Bool} {f : α → β} {l : List α}
    (hl : ∀ a ∈ l, ∀ b ∈ l, r a b = s (f a) (f b)) :
    (l.mergeSort r).map f = (l.map f).mergeSort s :=
  match l with
  | [] => by simp
  | [x] => by simp
  | a :: b :: l => by
    simp only [mergeSort, splitInTwo_fst, splitInTwo_snd, map_cons]
    rw [map_merge (fun a am b bm => hl a (mem_of_mem_take (by simpa using am))
      b (mem_of_mem_drop (by simpa using bm)))]
    rw [map_mergeSort (s := s) (fun a am b bm => hl a (mem_of_mem_take (by simpa using am))
      b (mem_of_mem_take (by simpa using bm)))]
    rw [map_mergeSort (s := s) (fun a am b bm => hl a (mem_of_mem_drop (by simpa using am))
      b (mem_of_mem_drop (by simpa using bm)))]
    rw [map_take, map_drop]
    simp
  termination_by length l

Commutativity of Mapping and Merge-Sorting: $\text{map } f \circ \text{mergeSort } r = \text{mergeSort } s \circ \text{map } f$

Informal description

Let $r : \alpha \to \alpha \to \text{Bool}$ and $s : \beta \to \beta \to \text{Bool}$ be binary relations, and let $f : \alpha \to \beta$ be a function. For any list $l$ of elements of type $\alpha$, if for all $a, b \in l$ we have $r(a, b) = s(f(a), f(b))$, then mapping $f$ over the merge-sorted list of $l$ with respect to $r$ is equal to merge-sorting the mapped list $f \circ l$ with respect to $s$. In other words: $$ \text{map } f (\text{mergeSort } r \ l) = \text{mergeSort } s (\text{map } f \ l) $$