Merge Sort

Stream: mathlib4

[Marcus Rossel]

In lean4#5092, Lean core got its own mergeSort. As a result, Kim Morrison mentioned that:

working out a clean way to get rid of Mathlib's mergeSort', and allowing us to proceed with just one version, would be great.

The problem is that:

in Mathlib we want a Prop valued comparator, while in Lean we want a Bool valued comparator.

I am open to changing the design of mergeSort in the Lean repository to help resolve this difficulty.

And as @Eric Wieser mentions:

I realize [that a Bool valued comparator] is consistent with docs#List.filter [...], but the general pattern is at odds with mathlib

---

I have no idea which solution is the right one, but to get the ball rolling I was wondering if any people involved in Mathlib have experience with resolving such a discrepancy? I can't imagine this being the first instance of Lean core wanting Bool where Mathlib wants Prop.

[Eric Wieser]

I think in the past Lean core has just said "sorry, this is changing and now you have to change too", but the fallout has been at worst minorly irritating

[Eric Wieser]

We adapted to List.filter changing to use Bool during the port. Initially we tried changing Multiset.filter to match, but in the end decided that this did more harm than good

[Eric Wieser]

What's the rationale for preferring Bool to Decidable in core?

[Kim Morrison]

As far as I understand, it is to avoid any performance overhead from Decidable, and to not scare the programmers with Prop!

[Marcus Rossel]

A quick search for mergeSort in Mathlib shows that it's only ever used to sort multisets, which is in turn only used to construct an instance of Denumerable (Multiset α). So mergeSort seems to be of little importance from a math perspective. Accordingly, it probably makes sense to prefer the CS perspective and use Bool. The fix would then simply be to remove Mathlib's mergeSort, adjust the two files related to multisets and be done with it.

[Eric Wieser]

It's used to sort finsets too

[Eric Wieser]

I think we should leave Finset.sort and Multiset.sort as taking Prop not bool, and put up with the list mismatch as we have done elsewhere

[Eric Wieser]

Kim Morrison said:

And to not scare the programmers with Prop!

This argument seems a little weird to me, we already do this with if which such programmers are far more likely to use than mergeSort!

[Marcus Rossel]

Eric Wieser said:

It's used to sort finsets too

By virtue of finsets being based on multisets, right?

[Eric Wieser]

Marcus Rossel said:

The fix would then simply be to remove Mathlib's mergeSort,

Just to check here: we still plan to keep every lemma in Mathlib about mergeSort that doesn't exist already in core, right?

[Marcus Rossel]

@Eric Wieser Good point, I guess that might make things a bit more tricky. Though the number of lemmas seems manageable.

[Kim Morrison]

I see map_mergeSort, but not much else. I think everything else has a direct replacement (although is stated slightly differently, as discussed above).

[Marcus Rossel]

How would I go about creating a branch for Mathlib based on lean4#5092 such that it could later be merged when Mathlib is bumped to the next Lean release?

[Eric Wieser]

Tangentially: it would be great if there were a version of the docs for Lean nightly (either with or without the mathlib nightly branches), to make it easier to discuss upcoming changes like this

[Eric Wieser]

Though I guess some care would need to be taken to avoid confusing users about which doc is which

[Eric Wieser]

Kim Morrison said:

I see map_mergeSort, but not much else. I think everything else has a direct replacement (although is stated slightly differently, as discussed above).

Keeping the typeclass-enabled version of docs#List.sorted_mergeSort seems pretty handy: the Lean core List.mergeSort_sorted has a non #naming-compliant name, and some inconvenient assumptions to deal with

[Kim Morrison]

Marcus Rossel said:

How would I go about creating a branch for Mathlib based on lean4#5092 such that it could later be merged when Mathlib is bumped to the next Lean release?

Mathlib will probably have moved to v4.12.0-rc1 by the time you see this message. :-)

[Kim Morrison]

Eric Wieser said:

Kim Morrison said:

I see map_mergeSort, but not much else. I think everything else has a direct replacement (although is stated slightly differently, as discussed above).

Keeping the typeclass-enabled version of docs#List.sorted_mergeSort seems pretty handy: the Lean core List.mergeSort_sorted has a non #naming-compliant name, and some inconvenient assumptions to deal with

I will change the name to sorted_mergeSort, but I agree that Mathlib should provide a wrapper that handles the hypotheses via Mathlib-specific typeclasses.

[Kim Morrison]

lean#5242

[Kim Morrison]

I'm again cleaning up the mergeSort' / mergeSort duplication. I seem to have it working now and will make a PR (but which will need to wait for v4.13.0 to hit master).

[Kim Morrison]

Separately, I'd like to move map_mergeSort up to Lean. @Eric Wieser and @François G. Dorais, is "upstream map_mergeSort lean#5377" okay with you?

[Kim Morrison]

#16902

[François G. Dorais]

@Kim Morrison The PR for map_mergeSort looks pretty clean to me after a quick walk through. No issues on my end. This basic algorithm belongs in core. (If you want a review then I can probably do so in the near future, but that doesn't seem to be what you want.)

[Eric Wieser]

the old mergeSort' in Mathlib (which was not a stable sort algorithm)

This surprises me; do you have an example showing non-stability?

[Kim Morrison]

Try anything. :-) Jeremy's implementation would split the lists by unriffling, rather than taking a prefix and a suffix.

[Kim Morrison]

This immediately breaks stability.