stability of insertion sort

Stream: mathlib4

[Asei Inoue]

I don't understand this theorem

variable [IsAntisymm α r] [IsTotal α r] [IsTrans α r]

/--
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.Pairwise r) (hc : c <+~ l) :
    c <+ insertionSort r l := by
  classical
  obtain ⟨d, hc, hd⟩ := hc
  induction l generalizing c d with
  | nil         => grind [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 (pairwise_insertionSort ..)

/--
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] <+~ l) :
    [a, b] <+ insertionSort r l :=
  sublist_insertionSort' (pairwise_pair.mpr hab) h

end Correctness

see: https://github.com/leanprover-community/mathlib4/blob/1ba359a5224b907d17bc42436366e87c48365ff7/Mathlib/Data/List/Sort.lean#L278-L306

If we assume a linear order, it feels like every sorting algorithm would end up being stable (since if (a \le b) and (b \le a), then necessarily (a = b)). That makes me feel that the statement of this theorem is meaningless. Wouldn’t a more appropriate way to express stability be to interpose a function ( \mathit{key} : \alpha \to \beta )? What do you think?

[Aaron Liu]

indeed this theorem seems to be meaningless, since I can prove it with docs#List.sublist_of_subperm_of_pairwise which is directly after in the same file