English
A refined stability result: under antisymmetry, totality and transitivity of r, if c is sorted and c <+~ l (weaker sublist notion), then c <+ insertionSort r l.
Русский
Улучшенная устойчивость: при антисимметричности, суммарности и транзитивности отношения r, если c упорядочено и \(c <+~ l\) (слабейшая подпоследовательность), тогда \(c <+ insertionSort r l\).
LaTeX
$$$ c.Sorted r \\land c <+~ l \\Rightarrow c <+ insertionSort r l $$$
Lean4
/-- 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 ..)
