The Sorted predicate.

Stream: mathlib4

[Wrenna Robson]

I would like to propose re-defining the List.Sorted predicate. Currently, it is defined as a synonym of Pairwise, but not in any kind of specialised way - it is just another name for Pairwise. I think this is probably not the best way to do this, especially given it is currently a def and not an abbrev. It means there ends up being a lot of duplicated API without really much gain. List.Sorted is meant to be preferred in the case that r is a < or ≤-like relation (transitive and antisymmetric or asymmetric)

Given recent efforts to deprecated List.Chain and List.Chain' and introduce List.IsChain as a unified predicate (meaning the same as the latter), I think one possibility could be that List.Sorted is defined as List.IsChain in the case when the underlying relation is IsTrans, such that this is then equivalent to List.Pairwise. This has the advantage that the corresponding decidable instance to this could come from the decidability of IsChain, which is pretty much as efficient as you can get as a check for sortedness.

Another option would be linking it to monotonicity of List.get. We have docs#List.sorted_lt_ofFn_iff and docs#List.sorted_le_ofFn_iff, as well as docsList.Sorted.get_strictMono and docs#List.Sorted.get_mono. What if these were actually the defining property of List.Sorted? That would make some sense to me. However it limits us to only considering < or ≤ themselves - a lot less general (at least if we use the actual Monotone predicate).

We could also consider separating IsSorted and IsStrictlySorted, i.e. "the underlying relation is ≤-like" and "the underlying relation is <-like". As typeclasses I think this probably ought to correspond toIsPreorder and IsStrictOrder respectively, though if you wanted to base it on monotonicity of List.get you would probably just use Preorder. I think this has something to recommend it in some ways!

I think maybe a poll would be appropriate once I've gathered some thoughts on this - my starting point is that the current definition of List.Sorted is not the most appropriate one we could choose, but I recognise a degree of bikeshedding might be needed to settle on an alternative (and that it is possible this was chosen in the past as a compromise for some other reason).

[Robin Arnez]

Regarding monotonicity: Pairwise is basically already the predicate of monotonicity:

example (l : List α) : List.Pairwise r l ↔ ∀ i j : Fin l.length, i < j → r (l.get i) (l.get j) := by
  simp [List.pairwise_iff_getElem, Fin.forall_iff, forall_comm (α := _ < _) (β := Nat)]

example {α r} [Std.Refl r] (l : List α) : List.Pairwise r l ↔ ∀ i j : Fin l.length, i ≤ j → r (l.get i) (l.get j) := by
  simp [List.pairwise_iff_getElem, Fin.forall_iff]
  cases ‹Std.Refl _›
  grind

And loogle seems to reveal that List.Pairwise is significantly more common than both of the others (List.Sorted occurs 107 times, List.IsChain 312 (admittedly, many of them are deprecations) and List.Pairwise 922 times). So it probably makes sense to take the one with the most API as the definition; but then the question is whether we even should distinguish Pairwise and Sorted

[Wrenna Robson]

Yes, I certainly can't currently see any reason why we do this.

[Wrenna Robson]

If it had a typeclass prereq and a different decidability instance I would do - as I say I think the fact that it is meant to only apply in a transitive context is key.

[Wrenna Robson]

Inherently Pairwise is O(n^2) to check and IsChain is O(n).

[Wrenna Robson]

An example of something which is defined as Pairwise but does make sense I think is List.Nodup, defined as List.Pairwise fun (x1 x2 : α) => x1 ≠ x2.

[Wrenna Robson]

If Sorted was List.Pairwise fun (x1 x2 : α) => x1 ≤ x2 and we had a StrictlySorted with List.Pairwise fun (x1 x2 : α) => x1 < x2 that would feel reasonable. I think the reason I like the idea of using IsChain is that I feel a definition, the part of it that defines how you construct a term of a type, should be as minimal/weak as possible: but it being Pairwise is obviously the important result for proving a lot of stronger stuff (and that comes from the transitivity).

[Wrenna Robson]

I am not sure we ever use it anywhere without ≤ or <.

[Wrenna Robson]

Incidentally the typeclass prereqs for List.sorted_insertionSort are [IsTotal α r] [IsTrans α r], which is not a terrible choice I suppose for the required pre-reqs. Notably I am not sure the sorting-algorithm concept of sorting makes sense outside that?

[Julia Scheaffer]

I recently tried proving some stuff about sorting, could the Sorted predicate be defined for arbitrary sequences instead of on list specifically? As a workaround i was defining my own Sorted predicate as myContainer.toList.Sorted but having something that would work for arbitrary sequences too would be nice.

[Wrenna Robson]

When you say arbitrary sequences, what do you mean?

[Wrenna Robson]

i.e. is there a typeclass you're thinking of?

[Julia Scheaffer]

Not at the moment

[Julia Scheaffer]

If it went based on the monotonicity definition, that would work well for arbitrary ℕ → α

[Wrenna Robson]

Or indeed Fin n → α which is different.

[Julia Scheaffer]

Right, Fin n would be good for fixed size collections like vectors

[Wrenna Robson]

We also have Vector R n, Array R, and my bête noire, List.Vector R n.

[Julia Scheaffer]

I was having trouble dealing with docs#Vector and docs#List.Vector so i ended up making my own inductively defined Vector :sweat_smile:

[Wrenna Robson]

No! No!!

[Julia Scheaffer]

and then proved equivalences to Vector and List.Vector

[Wrenna Robson]

I mean fill your boots but I cannot dis-recommend that enough.

[Julia Scheaffer]

Well, I am learning :sweat_smile:

[Wrenna Robson]

It's already terrible that we have Vector and List.Vector. I would like to have Tuple as a name for Fin n → α but that hasn't happened yet.

[Wrenna Robson]

(We do have Tuple.sort though.)

[Julia Scheaffer]

Tuple.sort looks useful

[Wrenna Robson]

I think it would be more useful if it wasn't so arcane, but I don't disagree.

[Julia Scheaffer]

Having a definition of Sorted that could work for stuff like Fin n -> α would be good too

[Wrenna Robson]

I have also thought that it would be nice to have a predicate for X is the sorted version of Y - in lists this would be List.Perm X Y /\ List.Pairwise (X) <= or something like that.

[Wrenna Robson]

Like, there is a difference between "this particular thing is sorted", "this particular thing is the sorted version of this other thing", and "this particular thing is calculated from this other thing using this function, which sorts it".

[Wrenna Robson]

It doesn't matter in logical terms what sorting method you use, but in other contexts you will want to examine the algorithm.

[Wrenna Robson]

I would like also to get some content about sorting networks into Lean which I don't think we have. What was your context?

[Julia Scheaffer]

Ooh, sorting networks are a good one. I was mainly trying to learn about how to prove stuff about functions that do complex stuff. I am attempting to design a language with a friend and one of the features I want is the ability to reason about function Implementations.

I come from a computer science background, so I am very interested in cost analysis of programs, which as I understand is not something lean can do very well right now.

Sorting algorithms are one of those things that are very simple to write and usually not too hard to reason about cost and correctness, so I was learning about how lean deals with them.

[Julia Scheaffer]

I could try and write some code to formalize sorting networks if they have not been done before in Lean/mathlib

[Wrenna Robson]

I have done some work with permutation networks (it isn't in Mathlib though I would like for it to be at some point). Sorting networks I think we simply do not have and it would be great to have that in.

[Wrenna Robson]

It's outside the context of this thread but start a new one for that topic if you like and tag me in, as I'd be very interested.

[Julia Scheaffer]

I'll let you know if and when i get the basics worked out :smile: (I've got some reading to do)

[Wrenna Robson]

Brill, let me know!

[Yaël Dillies]

Julia Scheaffer said:

Having a definition of Sorted that could work for stuff like Fin n -> α would be good too

Wouldn't this just be docs#StrictMono ?

[Julia Scheaffer]

It would be docs#Monotone, adjacent elements can be equal in a sorted list

[Julia Scheaffer]

At least I am using Monotone in my sorting network code

[Wrenna Robson]

I think Julia's intent there is something that works for everything, but yes it would be

[Jihoon Hyun]

What does it mean that the list is 'sorted'? Currently in lean the list l is Sorted when l[i] < l[j] for any i < j, but in c++ for example, std::is_sorted returns true if l[i+1] < l[i] is false for every possible i, possibly weaker than docs#Monotone . If we change the definition of Sortedness, then maybe we can weaken its definition in this style.

[Wrenna Robson]

That is equivalent to IsChain with <=.

[Wrenna Robson]

Which is in turn equivalent to Sorted <=

[Wrenna Robson]

So, yes, for computing whether a list is sorted by a transitive relation you should use IsChain.

[Jihoon Hyun]

Wrenna Robson 말함:

That is equivalent to IsChain with <=.

Actually it's not, as <= may not be defined; only < is required, and equality might not be defined as in Preorder lacking antisymmetry.

[Robin Arnez]

Well, IsChain (¬· > ·) if you will

[Jihoon Hyun]

Oh, you're right.

[Wrenna Robson]

Sure I mean I am assuming it's a Preorder as otherwise it's kinda much of a muchness

[Wrenna Robson]

Update on this: #30441 I hope is close to a maintainer review and possibly merge.

[Wrenna Robson]

It's done :)

[Wrenna Robson]

I would now (relatedly) like to think about how we can best capture the predicate "ys is a sorted version of xs". But that can be for a seperate thread.