Redefine {Fin/Multi}set.sort to take linear order?

Stream: mathlib4

[Bolton Bailey]

Currently Finset.sort and Multiset.sort take a [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] relation as an argument. It seems that in practice, when this relation is explicitly given, it's almost always the less-than-or-equal relation.

Do people think it would make sense to rename Finset.sort and Multiset.sort to something like sortBy so that sort itself can be used specifically for less-than-or-equals with LinearOrder? I think this would be easier to remember and would also potentially make mathlib more consistent with languages like rust or python, where I think functions named sort typically assume a <= instance.

[Eric Wieser]

I think while docs#List.mergeSort has the signature it does, consistency here is probably least confusing

[Eric Wieser]

Maybe the answer is to use a default argument for r as that does?

[Bolton Bailey]

I was going to say that a similar renaming could be done on mergeSort, but the default argument idea is interesting.

[Bolton Bailey]

Is there a reason why the default argument on mergeSort uses by exact fun a b => a ≤ b instead of simply fun a b => a ≤ b?

[Aaron Liu]

because you don't know if your type has a ≤ so you want to delay elaboration from compile time to runtime use time

[Aaron Liu]

if you do simply do fun a b => a ≤ b then you will get "failed to synthesize LE α"

[Bolton Bailey]

I was concerned it was something hacky like that.

[Bolton Bailey]

I guess we don't have a better way to express wanting to delay elaboration?

[Eric Wieser]

Note that this isn't delaying elaboration in the usual meaning of by exact, this is (x := y) being optParam while (x := by exact y) being autoParam

[Eric Wieser]

That is, (x := by exact y) and (x := (by exact y)) mean very different things

[Aaron Liu]

optParam stores the value and autoParam stores the syntax object which will be elaborated at the use site

[Bolton Bailey]

Is there any way to communicate that I want autoParam without using by or exact? If the point of saying by exact is just to take advantage of some tactic mode thing that makes it turn out autoparam, then it would be clearer to the reader what is happening if I could just say something like foo (x : α := autoParam(y))

[Bolton Bailey]

Incidentally, does the leanguage reference have an entry for default arguments? I have tried looking for information about how that works before, but haven't found it.

[Bolton Bailey]

Aaron Liu said:

optParam stores the value and autoParam stores the syntax object which will be elaborated at the use site

Would you mind if I added this exact sentence to the docstring for docs#autoParam ?

[Bolton Bailey]

And I guess per the docs, the syntax I am looking for is actually foo (x : autoParam α y)

[Eric Wieser]

But it's really autoParam α tacticSyntaxForY

[Bhavik Mehta]

I've sometimes used this with the >= relation, and I think I've used it for an order without an LE in the past but I can't recall what exactly... I think the autoParam idea sounds great

[Eric Wieser]

One downside of the autoParam is that it makes it much easier to accidentally state theorems without passing the argument, and ending up with something less general as a result

[Bhavik Mehta]

That's a general "downside" with autoParams, right? Not specific to this situation

[Eric Wieser]

I guess the RFC here would be a version of autoParams which are disabled in the context of a theorem signature

[Eric Wieser]

Maybe that's lintable