feat: List.mergeSort (#5092)

Defines `mergeSort`, a naive stable merge sort algorithm, replaces it
via a `@[csimp]` lemma with something faster at runtime, and proves the
following results:

* `mergeSort_sorted`: `mergeSort` produces a sorted list.
* `mergeSort_perm`: `mergeSort` is a permutation of the input list.
* `mergeSort_of_sorted`: `mergeSort` does not change a sorted list.
* `mergeSort_cons`: proves `mergeSort le (x :: xs) = l₁ ++ x :: l₂` for
some `l₁, l₂`
so that `mergeSort le xs = l₁ ++ l₂`, and no `a ∈ l₁` satisfies `le a
x`.
* `mergeSort_stable`: if `c` is a sorted sublist of `l`, then `c` is
still a sublist of `mergeSort le l`.

src/Init/Data/Bool.lean

@@ -549,3 +549,19 @@ export Bool (cond_eq_if)
 
 @[simp] theorem true_eq_decide_iff {p : Prop} [h : Decidable p] : true = decide p ↔ p := by
   cases h with | _ q => simp [q]
+
+/-! ### coercions -/
+
+/--
+This should not be turned on globally as an instance because it degrades performance in Mathlib,
+but may be used locally.
+-/
+def boolPredToPred : Coe (α → Bool) (α  → Prop) where
+  coe r := fun a => Eq (r a) true
+
+/--
+This should not be turned on globally as an instance because it degrades performance in Mathlib,
+but may be used locally.
+-/
+def boolRelToRel : Coe (α → α → Bool) (α → α → Prop) where
+  coe r := fun a b => Eq (r a b) true

src/Init/Data/List.lean

@@ -22,3 +22,4 @@ import Init.Data.List.Sublist
 import Init.Data.List.TakeDrop
 import Init.Data.List.Zip
 import Init.Data.List.Perm
+import Init.Data.List.Sort

src/Init/Data/List/Basic.lean

@@ -962,6 +962,26 @@ def IsInfix (l₁ : List α) (l₂ : List α) : Prop := Exists fun s => Exists f
 
 @[inherit_doc] infixl:50 " <:+: " => IsInfix
 
+/-! ### splitAt -/
+
+/--
+Split a list at an index.
+```
+splitAt 2 [a, b, c] = ([a, b], [c])
+```
+-/
+def splitAt (n : Nat) (l : List α) : List α × List α := go l n [] where
+  /--
+  Auxiliary for `splitAt`:
+  `splitAt.go l xs n acc = (acc.reverse ++ take n xs, drop n xs)` if `n < xs.length`,
+  and `(l, [])` otherwise.
+  -/
+  go : List α → Nat → List α → List α × List α
+  | [], _, _ => (l, []) -- This branch ensures the pointer equality of the result with the input
+                        -- without any runtime branching cost.
+  | x :: xs, n+1, acc => go xs n (x :: acc)
+  | xs, _, acc => (acc.reverse, xs)
+
 /-! ### rotateLeft -/
 
 /--

src/Init/Data/List/Lemmas.lean

@@ -276,6 +276,9 @@ theorem getElem?_cons_zero {l : List α} : (a::l)[0]? = some a := by simp
   simp only [← get?_eq_getElem?]
   rfl
 
+theorem getElem?_cons : (a :: l)[i]? = if i = 0 then some a else l[i-1]? := by
+  cases i <;> simp
+
 theorem getElem?_len_le : ∀ {l : List α} {n}, length l ≤ n → l[n]? = none
   | [], _, _ => rfl
   | _ :: l, _+1, h => by
@@ -2368,6 +2371,27 @@ theorem dropLast_append {l₁ l₂ : List α} :
     dropLast (a :: replicate n a) = replicate n a := by
   rw [← replicate_succ, dropLast_replicate, Nat.add_sub_cancel]
 
+/-!
+### splitAt
+
+We don't provide any API for `splitAt`, beyond the `@[simp]` lemma
+`splitAt n l = (l.take n, l.drop n)`,
+which is proved in `Init.Data.List.TakeDrop`.
+-/
+
+theorem splitAt_go (n : Nat) (l acc : List α) :
+    splitAt.go l xs n acc =
+      if n < xs.length then (acc.reverse ++ xs.take n, xs.drop n) else (l, []) := by
+  induction xs generalizing n acc with
+  | nil => simp [splitAt.go]
+  | cons x xs ih =>
+    cases n with
+    | zero => simp [splitAt.go]
+    | succ n =>
+      rw [splitAt.go, take_succ_cons, drop_succ_cons, ih n (x :: acc),
+        reverse_cons, append_assoc, singleton_append, length_cons]
+      simp only [Nat.succ_lt_succ_iff]
+
 /-! ## Manipulating elements -/
 
 /-! ### replace -/

src/Init/Data/List/Nat/Range.lean

@@ -260,9 +260,24 @@ theorem enumFrom_map_snd : ∀ (n) (l : List α), map Prod.snd (enumFrom n l) =
 theorem snd_mem_of_mem_enumFrom {x : Nat × α} {n : Nat} {l : List α} (h : x ∈ enumFrom n l) : x.2 ∈ l :=
   enumFrom_map_snd n l ▸ mem_map_of_mem _ h
 
-theorem mem_enumFrom {x : α} {i j : Nat} (xs : List α) (h : (i, x) ∈ xs.enumFrom j) :
-    j ≤ i ∧ i < j + xs.length ∧ x ∈ xs :=
-  ⟨le_fst_of_mem_enumFrom h, fst_lt_add_of_mem_enumFrom h, snd_mem_of_mem_enumFrom h⟩
+theorem snd_eq_of_mem_enumFrom {x : Nat × α} {n : Nat} {l : List α} (h : x ∈ enumFrom n l) :
+    x.2 = l[x.1 - n]'(by have := le_fst_of_mem_enumFrom h; have := fst_lt_add_of_mem_enumFrom h; omega) := by
+  induction l generalizing n with
+  | nil => cases h
+  | cons hd tl ih =>
+    cases h with
+    | head h => simp
+    | tail h m =>
+      specialize ih m
+      have : x.1 - n = x.1 - (n + 1) + 1 := by
+        have := le_fst_of_mem_enumFrom m
+        omega
+      simp [this, ih]
+
+theorem mem_enumFrom {x : α} {i j : Nat} {xs : List α} (h : (i, x) ∈ xs.enumFrom j) :
+    j ≤ i ∧ i < j + xs.length ∧
+      x = xs[i - j]'(by have := le_fst_of_mem_enumFrom h; have := fst_lt_add_of_mem_enumFrom h; omega) :=
+  ⟨le_fst_of_mem_enumFrom h, fst_lt_add_of_mem_enumFrom h, snd_eq_of_mem_enumFrom h⟩
 
 theorem enumFrom_cons' (n : Nat) (x : α) (xs : List α) :
     enumFrom n (x :: xs) = (n, x) :: (enumFrom n xs).map (Prod.map (· + 1) id) := by
@@ -329,6 +344,14 @@ theorem fst_lt_of_mem_enum {x : Nat × α} {l : List α} (h : x ∈ enum l) : x.
 theorem snd_mem_of_mem_enum {x : Nat × α} {l : List α} (h : x ∈ enum l) : x.2 ∈ l :=
   snd_mem_of_mem_enumFrom h
 
+theorem snd_eq_of_mem_enum {x : Nat × α} {l : List α} (h : x ∈ enum l) :
+    x.2 = l[x.1]'(fst_lt_of_mem_enum h) :=
+  snd_eq_of_mem_enumFrom h
+
+theorem mem_enum {x : α} {i : Nat} {xs : List α} (h : (i, x) ∈ xs.enum) :
+    i < xs.length ∧ x = xs[i]'(fst_lt_of_mem_enum h) :=
+  by simpa using mem_enumFrom h
+
 theorem map_enum (f : α → β) (l : List α) : map (Prod.map id f) (enum l) = enum (map f l) :=
   map_enumFrom f 0 l
 

src/Init/Data/List/Nat/TakeDrop.lean

@@ -70,20 +70,20 @@ theorem get?_take_eq_none {l : List α} {n m : Nat} (h : n ≤ m) :
     (l.take n).get? m = none := by
   simp [getElem?_take_eq_none h]
 
-theorem getElem?_take_eq_if {l : List α} {n m : Nat} :
+theorem getElem?_take {l : List α} {n m : Nat} :
     (l.take n)[m]? = if m < n then l[m]? else none := by
   split
-  · next h => exact getElem?_take h
+  · next h => exact getElem?_take_of_lt h
   · next h => exact getElem?_take_eq_none (Nat.le_of_not_lt h)
 
-@[deprecated getElem?_take_eq_if (since := "2024-06-12")]
+@[deprecated getElem?_take (since := "2024-06-12")]
 theorem get?_take_eq_if {l : List α} {n m : Nat} :
     (l.take n).get? m = if m < n then l.get? m else none := by
-  simp [getElem?_take_eq_if]
+  simp [getElem?_take]
 
 theorem head?_take {l : List α} {n : Nat} :
     (l.take n).head? = if n = 0 then none else l.head? := by
-  simp [head?_eq_getElem?, getElem?_take_eq_if]
+  simp [head?_eq_getElem?, getElem?_take]
   split
   · rw [if_neg (by omega)]
   · rw [if_pos (by omega)]
@@ -95,7 +95,7 @@ theorem head_take {l : List α} {n : Nat} (h : l.take n ≠ []) :
   simp_all
 
 theorem getLast?_take {l : List α} : (l.take n).getLast? = if n = 0 then none else l[n - 1]?.or l.getLast? := by
-  rw [getLast?_eq_getElem?, getElem?_take_eq_if, length_take]
+  rw [getLast?_eq_getElem?, getElem?_take, length_take]
   split
   · rw [if_neg (by omega)]
     rw [Nat.min_def]
@@ -128,7 +128,7 @@ theorem take_take : ∀ (n m) (l : List α), take n (take m l) = take (min n m)
 theorem take_set_of_lt (a : α) {n m : Nat} (l : List α) (h : m < n) :
     (l.set n a).take m = l.take m :=
   List.ext_getElem? fun i => by
-    rw [getElem?_take_eq_if, getElem?_take_eq_if]
+    rw [getElem?_take, getElem?_take]
     split
     · next h' => rw [getElem?_set_ne (by omega)]
     · rfl
@@ -203,7 +203,7 @@ theorem map_eq_append_split {f : α → β} {l : List α} {s₁ s₂ : List β}
 theorem take_prefix_take_left (l : List α) {m n : Nat} (h : m ≤ n) : take m l <+: take n l := by
   rw [isPrefix_iff]
   intro i w
-  rw [getElem?_take, getElem_take', getElem?_eq_getElem]
+  rw [getElem?_take_of_lt, getElem_take', getElem?_eq_getElem]
   simp only [length_take] at w
   exact Nat.lt_of_lt_of_le (Nat.lt_of_lt_of_le w (Nat.min_le_left _ _)) h
 
@@ -334,7 +334,7 @@ theorem set_eq_take_append_cons_drop {l : List α} {n : Nat} {a : α} :
   · ext1 m
     by_cases h' : m < n
     · rw [getElem?_append_left (by simp [length_take]; omega), getElem?_set_ne (by omega),
-        getElem?_take h']
+        getElem?_take_of_lt h']
     · by_cases h'' : m = n
       · subst h''
         rw [getElem?_set_eq ‹_›, getElem?_append_right, length_take,
@@ -373,40 +373,67 @@ theorem drop_take : ∀ (m n : Nat) (l : List α), drop n (take m l) = take (m -
     congr 1
     omega
 
-theorem take_reverse {α} {xs : List α} {n : Nat} (h : n ≤ xs.length) :
+theorem take_reverse {α} {xs : List α} {n : Nat} :
     xs.reverse.take n = (xs.drop (xs.length - n)).reverse := by
-  induction xs generalizing n <;>
-    simp only [reverse_cons, drop, reverse_nil, Nat.zero_sub, length, take_nil]
-  next xs_hd xs_tl xs_ih =>
-  cases Nat.lt_or_eq_of_le h with
-  | inl h' =>
-    have h' := Nat.le_of_succ_le_succ h'
-    rw [take_append_of_le_length, xs_ih h']
-    rw [show xs_tl.length + 1 - n = succ (xs_tl.length - n) from _, drop]
-    · rwa [succ_eq_add_one, Nat.sub_add_comm]
-    · rwa [length_reverse]
-  | inr h' =>
-    subst h'
-    rw [length, Nat.sub_self, drop]
-    suffices xs_tl.length + 1 = (xs_tl.reverse ++ [xs_hd]).length by
-      rw [this, take_length, reverse_cons]
-    rw [length_append, length_reverse]
-    rfl
-
-@[deprecated (since := "2024-06-15")] abbrev reverse_take := @take_reverse
-
-theorem drop_reverse {α} {xs : List α} {n : Nat} (h : n ≤ xs.length) :
+  by_cases h : n ≤ xs.length
+  · induction xs generalizing n <;>
+      simp only [reverse_cons, drop, reverse_nil, Nat.zero_sub, length, take_nil]
+    next xs_hd xs_tl xs_ih =>
+    cases Nat.lt_or_eq_of_le h with
+    | inl h' =>
+      have h' := Nat.le_of_succ_le_succ h'
+      rw [take_append_of_le_length, xs_ih h']
+      rw [show xs_tl.length + 1 - n = succ (xs_tl.length - n) from _, drop]
+      · rwa [succ_eq_add_one, Nat.sub_add_comm]
+      · rwa [length_reverse]
+    | inr h' =>
+      subst h'
+      rw [length, Nat.sub_self, drop]
+      suffices xs_tl.length + 1 = (xs_tl.reverse ++ [xs_hd]).length by
+        rw [this, take_length, reverse_cons]
+      rw [length_append, length_reverse]
+      rfl
+  · have w : xs.length - n = 0 := by omega
+    rw [take_of_length_le, w, drop_zero]
+    simp
+    omega
+
+theorem drop_reverse {α} {xs : List α} {n : Nat} :
     xs.reverse.drop n = (xs.take (xs.length - n)).reverse := by
-  conv =>
-    rhs
-    rw [← reverse_reverse xs]
-  rw [← reverse_reverse xs] at h
-  generalize xs.reverse = xs' at h ⊢
-  rw [take_reverse]
-  · simp only [length_reverse, reverse_reverse] at *
+  by_cases h : n ≤ xs.length
+  · conv =>
+      rhs
+      rw [← reverse_reverse xs]
+    rw [← reverse_reverse xs] at h
+    generalize xs.reverse = xs' at h ⊢
+    rw [take_reverse]
+    · simp only [length_reverse, reverse_reverse] at *
+      congr
+      omega
+  · have w : xs.length - n = 0 := by omega
+    rw [drop_of_length_le, w, take_zero, reverse_nil]
+    simp
+    omega
+
+theorem reverse_take {l : List α} {n : Nat} :
+    (l.take n).reverse = l.reverse.drop (l.length - n) := by
+  by_cases h : n ≤ l.length
+  · rw [drop_reverse]
+    congr
+    omega
+  · have w : l.length - n = 0 := by omega
+    rw [w, drop_zero, take_of_length_le]
+    omega
+
+theorem reverse_drop {l : List α} {n : Nat} :
+    (l.drop n).reverse = l.reverse.take (l.length - n) := by
+  by_cases h : n ≤ l.length
+  · rw [take_reverse]
     congr
     omega
-  · simp only [length_reverse, sub_le]
+  · have w : l.length - n = 0 := by omega
+    rw [w, take_zero, drop_of_length_le, reverse_nil]
+    omega
 
 /-! ### rotateLeft -/
 

src/Init/Data/List/Pairwise.lean

@@ -226,6 +226,18 @@ theorem pairwise_iff_forall_sublist : l.Pairwise R ↔ (∀ {a b}, [a,b] <+ l 
         intro a b hab
         apply h; exact hab.cons _
 
+theorem Pairwise.rel_of_mem_take_of_mem_drop
+    {l : List α} (h : l.Pairwise R) (hx : x ∈ l.take n) (hy : y ∈ l.drop n) : R x y := by
+  apply pairwise_iff_forall_sublist.mp h
+  rw [← take_append_drop n l, sublist_append_iff]
+  refine ⟨[x], [y], rfl, by simpa, by simpa⟩
+
+theorem Pairwise.rel_of_mem_append
+    {l₁ l₂ : List α} (h : (l₁ ++ l₂).Pairwise R) (hx : x ∈ l₁) (hy : y ∈ l₂) : R x y := by
+  apply pairwise_iff_forall_sublist.mp h
+  rw [sublist_append_iff]
+  exact ⟨[x], [y], rfl, by simpa, by simpa⟩
+
 theorem pairwise_of_forall_mem_list {l : List α} {r : α → α → Prop} (h : ∀ a ∈ l, ∀ b ∈ l, r a b) :
     l.Pairwise r := by
   rw [pairwise_iff_forall_sublist]

src/Init/Data/List/Perm.lean

@@ -400,6 +400,40 @@ theorem Pairwise.perm {R : α → α → Prop} {l l' : List α} (hR : l.Pairwise
 theorem Perm.pairwise {R : α → α → Prop} {l l' : List α} (hl : l ~ l') (hR : l.Pairwise R)
     (hsymm : ∀ {x y}, R x y → R y x) : l'.Pairwise R := hR.perm hl hsymm
 
+/--
+If two lists are sorted by an antisymmetric relation, and permutations of each other,
+they must be equal.
+-/
+theorem Perm.eq_of_sorted : ∀ {l₁ l₂ : List α}
+    (_ : ∀ a b, a ∈ l₁ → b ∈ l₂ → le a b → le b a → a = b)
+    (_ : l₁.Pairwise le) (_ : l₂.Pairwise le) (_ : l₁ ~ l₂), l₁ = l₂
+  | [], [], _, _, _, _ => rfl
+  | [], b :: l₂, _, _, _, h => by simp_all
+  | a :: l₁, [], _, _, _, h => by simp_all
+  | a :: l₁, b :: l₂, w, h₁, h₂, h => by
+    have am : a ∈ b :: l₂ := h.subset (mem_cons_self _ _)
+    have bm : b ∈ a :: l₁ := h.symm.subset (mem_cons_self _ _)
+    have ab : a = b := by
+      simp only [mem_cons] at am
+      rcases am with rfl | am
+      · rfl
+      · simp only [mem_cons] at bm
+        rcases bm with rfl | bm
+        · rfl
+        · exact w _ _ (mem_cons_self _ _) (mem_cons_self _ _)
+            (rel_of_pairwise_cons h₁ bm) (rel_of_pairwise_cons h₂ am)
+    subst ab
+    simp only [perm_cons] at h
+    have := Perm.eq_of_sorted
+      (fun x y hx hy => w x y (mem_cons_of_mem a hx) (mem_cons_of_mem a hy))
+      h₁.tail h₂.tail h
+    simp_all
+
+theorem Nodup.perm {l l' : List α} (hR : l.Nodup) (hl : l ~ l') : l'.Nodup :=
+  Pairwise.perm hR hl (by intro x y h h'; simp_all)
+
+theorem Perm.nodup {l l' : List α} (hl : l ~ l') (hR : l.Nodup) : l'.Nodup := hR.perm hl
+
 theorem Perm.nodup_iff {l₁ l₂ : List α} : l₁ ~ l₂ → (Nodup l₁ ↔ Nodup l₂) :=
   Perm.pairwise_iff <| @Ne.symm α
 

src/Init/Data/List/Sort.lean

@@ -0,0 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.List.Sort.Basic
+import Init.Data.List.Sort.Impl
+import Init.Data.List.Sort.Lemmas