fix: Rename theorems that use sorted instead of pairwise (#10743)

This PR renames theorems that use `sorted` in their name to instead use
`pairwise`.


Closes #10742.

---------

Co-authored-by: Markus Himmel <[email protected]>

Author: linesthatinterlace

src/Init/Data/List/Perm.lean

@@ -491,7 +491,7 @@ theorem Perm.pairwise {R : α → α → Prop} {l l' : List α} (hl : l ~ l') (h
 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 α}
+theorem Perm.eq_of_pairwise : ∀ {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
@@ -511,11 +511,14 @@ theorem Perm.eq_of_sorted : ∀ {l₁ l₂ : List α}
             (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
+    have := Perm.eq_of_pairwise
       (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
 
+@[deprecated Perm.eq_of_pairwise (since := "2025-10-23")]
+abbrev Perm.eq_of_sorted := @Perm.eq_of_pairwise
+
 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)
 

src/Init/Data/List/Sort/Lemmas.lean

@@ -16,9 +16,9 @@ public section
 /-!
 # Basic properties of `mergeSort`.
 
-* `sorted_mergeSort`: `mergeSort` produces a sorted list.
+* `pairwise_mergeSort`: `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_of_pairwise`: `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`.
 * `sublist_mergeSort`: if `c` is a sorted sublist of `l`, then `c` is still a sublist of `mergeSort le l`.
@@ -77,14 +77,20 @@ theorem splitInTwo_cons_cons_zipIdx_snd (i : Nat) (l : List α) :
       congr
       ext <;> simp; omega
 
-theorem splitInTwo_fst_sorted (l : { l : List α // l.length = n }) (h : Pairwise le l.1) : Pairwise le (splitInTwo l).1.1 := by
+theorem splitInTwo_fst_pairwise (l : { l : List α // l.length = n }) (h : Pairwise le l.1) : Pairwise le (splitInTwo l).1.1 := by
   rw [splitInTwo_fst]
   exact h.take
 
-theorem splitInTwo_snd_sorted (l : { l : List α // l.length = n }) (h : Pairwise le l.1) : Pairwise le (splitInTwo l).2.1 := by
+@[deprecated splitInTwo_fst_pairwise (since := "2025-10-23")]
+abbrev splitInTwo_fst_sorted := @splitInTwo_fst_pairwise
+
+theorem splitInTwo_snd_pairwise (l : { l : List α // l.length = n }) (h : Pairwise le l.1) : Pairwise le (splitInTwo l).2.1 := by
   rw [splitInTwo_snd]
   exact h.drop
 
+@[deprecated splitInTwo_snd_pairwise (since := "2025-10-23")]
+abbrev splitInTwo_snd_sorted := @splitInTwo_fst_pairwise
+
 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]
@@ -208,7 +214,7 @@ attribute [local instance] boolRelToRel
 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
+theorem pairwise_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
@@ -238,6 +244,9 @@ theorem sorted_merge
           · exact rel_of_pairwise_cons h₂ m
         · exact ih₂ h₂.tail
 
+@[deprecated pairwise_merge (since := "2025-10-23")]
+abbrev sorted_merge := @pairwise_merge
+
 theorem merge_of_le : ∀ {xs ys : List α} (_ : ∀ a b, a ∈ xs → b ∈ ys → le a b),
     merge xs ys le = xs ++ ys
   | [], ys, _
@@ -295,35 +304,41 @@ 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
+theorem pairwise_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
   | [a] => by simp
   | a :: b :: xs => by
     rw [mergeSort]
-    apply sorted_merge @trans @total
-    apply sorted_mergeSort trans total
-    apply sorted_mergeSort trans total
+    apply pairwise_merge @trans @total
+    apply pairwise_mergeSort trans total
+    apply pairwise_mergeSort trans total
 termination_by l => l.length
 
+@[deprecated pairwise_mergeSort (since := "2025-10-23")]
+abbrev sorted_mergeSort := @pairwise_mergeSort
+
 /--
 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
+theorem mergeSort_of_pairwise : ∀ {l : List α} (_ : Pairwise le l), mergeSort l le = l
   | [], _ => by simp
   | [a], _ => by simp
   | 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 [mergeSort_of_pairwise (splitInTwo_fst_pairwise ⟨a :: b :: xs, rfl⟩ h)]
+    rw [mergeSort_of_pairwise (splitInTwo_snd_pairwise ⟨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
 
+@[deprecated mergeSort_of_pairwise (since := "2025-10-23")]
+abbrev mergeSort_of_sorted := @mergeSort_of_pairwise
+
 /--
 This merge sort algorithm is stable,
 in the sense that breaking ties in the ordering function using the position in the list
@@ -359,8 +374,6 @@ where go : ∀ (i : Nat) (l : List α),
       omega
 termination_by _ l => l.length
 
-
-
 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)
@@ -373,7 +386,7 @@ theorem mergeSort_cons {le : α → α → Bool}
   have m₁ : (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)
+  have s := pairwise_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
@@ -384,8 +397,8 @@ theorem mergeSort_cons {le : α → α → Bool}
     have q : mergeSort (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
+    apply Perm.eq_of_pairwise (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]
@@ -400,7 +413,7 @@ theorem mergeSort_cons {le : α → α → Bool}
         have := mem_zipIdx hb
         simp_all
       · rfl
-    · exact sorted_mergeSort (zipIdxLE_trans trans) (zipIdxLE_total total) ..
+    · exact pairwise_mergeSort (zipIdxLE_trans trans) (zipIdxLE_total total) ..
     · exact s.sublist ((sublist_cons_self (a, 0) l₂).append_left l₁)
     · exact q
   · intro b m

src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean

@@ -546,7 +546,7 @@ theorem equiv_iff_toListModel_perm {t t' : Impl α β} :
 theorem Equiv.toListModel_eq [Ord α] [OrientedOrd α]
     {t t' : Impl α β} (h : t.Equiv t') (htb : t.Ordered) (htb' : t'.Ordered) :
     t.toListModel = t'.toListModel := by
-  refine List.Perm.eq_of_sorted ?_ htb htb' h.1
+  refine List.Perm.eq_of_pairwise ?_ htb htb' h.1
   intro a b ha hb hlt hgt
   rw [OrientedOrd.eq_swap, hlt] at hgt
   contradiction