Commit 2025-12-05 15:16 84ddba16

refactor(Data/List/Sort): deprecate and replace List.Sorted (#30441) Deprecates Sorted and defines new special-case predicates to be used for preorders. List.Sorted is essentially an irrelevant definition, as it is identical to List.Pairwise, and we have some results about Sorted which also always apply to Pairwise or do so under certain conditions (and vice versa). We also commonly use Sorted to talk specifically about < and <=, which can be somewhat unwieldy. As a result, this PR does the following.

Deprecate List.Sorted

List.Sorted is currently just a synonym of List.Pairwise, but it isn't even an abbrev. We deprecate it here along with theorems that are just repeats from Pairwise.

Separate out InsertionSort and MergeSort content

We extract the theorems about insertion sort and merge sort that currently exist in the context of List.Sorted - they are currently in the same file but I think they could go elsewhere, potentially even into Batteries where I think they would naturally fit - they aren't really mathematical in nature IMO.

Define Sorted* predicates.

It is useful to have predicates SortedLT, SortedLE, SortedGT and SortedGE, which correspond to exactly what they sound like. These are equivalent to suitable Pairwise statements, but that is not how they are defined - one could equivalently define them using IsChain, or, as I do here, using monotonicity of List.get. While the latter is how they are defined, I use irreducible definitions - it is not permitted to use the definitions directly. Instead, API is provided so that you can easily move to/from monotonicity statements, Pairwise statements, and IsChain statements. You don't destructure lists directly here: to prove things from, say, (a :: b :: l).sortedLT, one probably accesses IsChain lemmas to extract things from this statement. But one can also use the monotonicty API to prove things usefully. Data.List.Sorted contains all of this and I think it exhibits my thinking on what should be possible. I've actually changed my mind a couple of times on how to actually define these - one could use Pairwise, IsChain or Monotone etc. to taste - but it doesn't matter, because the API is robust enough that it changes very little once one establishes the core set of facts/equivalence between these.

In particular, add better decidability instance

List.decidableSorted has the fundamental issue that List.Sorted seems conceptually meant for transitive relations, but the instance of Decidable it uses uses Pairwise's decidability, not IsChain's. This is a problem because the latter is O(n) and the former is O(n^2), where n is the length of the list. It's not a major deal one might think - but I think being able to efficiently check whether something is <-sorted or <=-sorted is important.

Adapt library to changes

I think nearly everywhere we actually use List.Sorted it is in the context of (<) or (<=), so I've changed to using these specific predicates.