feat: more lemmas and perf update

[fgdorais]

• Mathlib patch at #8005

• fixed le, lt, min, max to be more efficient
• fixed lemma names to match naming convention

[fgdorais]

@eric-wieser Would you mind checking this out to see if I missed anything? I'll work on the Mathlib patch tomorrow.

[fgdorais]

@joehendrix I tagged this one WIP just because I want to check-in with @eric-wieser. It's also ready for review by others. Feel free to change the label as you find most appropriate.

[eric-wieser]

This looks good, thanks! Its not clear to me what the purpose of these aliases is; arguably having lots of ways to spell the same thing makes it harder for people to spot the patterns in the naming. If you do really want to keep them, I think it would be appropriate to add a /-! comment before the first batch of aliases explaining the motivation.

[digama0]

I'm fine with the name change and without the aliases. They seem to be for backward compatibility, as they are the pre-renamed names.

I think we could start a policy of using @[deprecated] alias which stick around for one stable release cycle as a means of more gently doing these renames. What do you think @joehendrix ?

[fgdorais]

I added brief comments as @eric-wieser suggested.

@digama0 I'm not sure what you're recommending but my personal philosophy is to try to accommodate everyone, when possible. People who think of xor as infix would naturally come up with one version, people who believe xor is prefix would naturally come up with the other. I think Std shouldn't prefer one over the other but they should definitely be aliases. I'm happy to make the Mathlib prefrered version the root alias, but I think the alternative should exist without deprecation. I think Std should be impartial to the extent possible. (This is not the same as all-accommodating: Std can choose not to implement a rare variation with no explanations required.)

[digama0]

People who think of xor as infix would naturally come up with one version, people who believe xor is prefix would naturally come up with the other. I think Std shouldn't prefer one over the other but they should definitely be aliases.

Well, this is what we have a naming convention for. We should make a rule for how to name these things and stick to it, we should not make versions for multiple naming conventions unless the convention itself is ambiguous about how to name them. I would argue that in this case we can have a clear rule - binary functions are named in infix - and stick to it, at least for the basic functions one would find in Std.Logic.

[fgdorais]

Well, this is what we have a naming convention for. We should make a rule for how to name these things and stick to it, we should not make versions for multiple naming conventions unless the convention itself is ambiguous about how to name them. I would argue that in this case we can have a clear rule - binary functions are named in infix - and stick to it, at least for the basic functions one would find in Std.Logic.

Let's make some rules then! Even though I'd personally prefer no rules, having any rules at all would be progress!

[semorrison]

I would argue that in this case we can have a clear rule - binary functions are named in infix - and stick to it, at least for the basic functions one would find in Std.Logic.

Let's make some rules then! Even though I'd personally prefer no rules, having any rules at all would be progress!

I think Mario just did. :-)

[joehendrix]

I agree that we should pick one naming scheme. Having multiple aliases for the same definition has its own costs.

For simplification rules, I personally prefer prefix naming using the root symbol of the left-hand side independent of whether the operator is infix or prefix. e.g, I would naively expect not_and_self to be !(x && x) = false (which obviously is redundent make sense as a theorem).

I am open to the other options though. Hopefully better search and automation can make knowing individual lemma names like that less important.

[digama0]

I would naively expect not_and_self to be !(x && x) = false (which obviously is redundent make sense as a theorem).

Our naming convention is ambiguous with regard to parenthesis positioning. This is okay, names don't need to be unique with respect to all theorems that could possibly exist, only the ones that do exist, and in the few cases where this arises we just use ' or some other ad hoc disambiguation scheme appropriate to the context.

For simplification rules, I personally prefer prefix naming using the root symbol of the left-hand side independent of whether the operator is infix or prefix.

This decision also affects mathlib, which is using the same naming convention. (This isn't just me making up a rule on the spot, it's the rule that already exists in mathlib.) If we want to make a change here we should make sure everyone is on the same page.

[joehendrix]

Ok, let's make sure are on the same page for the naming convention. Obviously we've all written enough simp rules that these conventions aren't being made up on the spot.

It sounds like the Mathlib naming convention is to name simp theorems like this based roughly on the left-to-right order of the left-hand side as typically rendered, and the proposal is to do the same here.

I'm ok with that. Is that captured anywhere else?

[digama0]

It sounds like the Mathlib naming convention is to name simp theorems like this based roughly on the left-to-right order of the left-hand side as typically rendered,

No, it does not use rendering order, because this depends on how the author decided to write the expression and lean is pretty freeform regarding textual order. In particular dot-notation functions are named in prefix (i.e. x.toList.toArray = x should be called toArray_toList, same as if it was written toArray (toList x) = x), and binary functions are named in infix (in particular binops like add, but also max and bind. I can imagine making exceptions to this rule on a per-function basis because we probably don't want to treat every random function like Lean.Macro.trace as infix.)

[joehendrix]

Ok, let me try to specify this again:

If the lemma is a binary operator (see below), then we typically use a left-op-right ordering. Otherwise, we use a preorder naming scheme with the operator name followed by arguments.

A binary operator is either:

• A term with the type A -> A -> A (ignoring implicits, etc).
• An operator typically written in infix notation (e.g., Option.bind : Option A -> (A -> Option B) -> Option C is written using the >>= operator.

I think the goal here is to reduce the need to specify left/right.

I still personally prefer the preorder approach (mostly so I can use the top operator in IDE completion), but I think as long as there is a clear intention I am ok with adopting the Mathlib scheme.

[digama0]

My concern regarding prefix-everything is that we clearly can't follow this rule for add/sub/mul/div, the lefts and rights would proliferate and users would have to know precedence and do inorder->preorder conversion in their head just to predict the name. So some exception cases are inevitable, and it's really just a question of which functions to infix and which to prefix.

(I think your specification is fine, it covers all the cases I can think of.)

[fgdorais]

I'm okay with @joehendrix's spec. (More importantly the existence of a spec!)

For clarity: HAdd, HMul, ... fall into the second case, right?

Should the prefix alternatives be deprecated or just marginalized in some way? Note that using alias already puts a note what the root variant is. Perhaps there could be an in-between variant that recommends using the root variant without actually deprecating? Just a thought, I'm not super into this idea but it's worth mentioning.

[digama0]

I think it's good to have alias around as an option, but I don't think we should use this mechanism unless there is a clear case that the alternate names are needed to prevent confusion. Users can always add these names locally if they prefer. I think we should not have the alias at all, and only use a deprecation period if we have reason to believe the definition is already in use in the wild. (I think these were added just a few days ago, so we should be okay on this front.)

[eric-wieser]

• An operator typically written in infix notation (e.g., Option.bind : Option A -> (A -> Option B) -> Option C is written using the >>= operator.

This sounds like a pretty misleading example to me; IIRC, >>= is Bind.bind not Option.bind, and as the latter is more general than the former, but the former is not reducible, we end up having to write separate lemmas about each spelling!

[fgdorais]

I've cleaned up this PR according to the naming conventions. (Let me know if I missed something!) CI is currently working on testing the Mathlib patch.

I just deleted the prefix aliases and did not deprecate them. The reason is that if some (perhaps imaginary) Std user is attached to the prefix convention in some circumstances, deprecation would basically prevent them from updating Std and adding their preferred aliases until the deprecation window is done. That seems like a bad idea to me especially if such deprecation windows compound, which may lead users to give up on Std altogether.

[digama0]

The reason is that if some (perhaps imaginary) Std user is attached to the prefix convention in some circumstances, deprecation would basically prevent them from updating Std and adding their preferred aliases until the deprecation window is done.

That's an excellent point. We should have some mechanism for users to be able to at least remove upstream deprecation marks if they either disagree with the deprecation or want to globally allow usage of that particular deprecated function in their project without silencing all warnings.

[fgdorais]

The ideal solution might be for deprecation to have a more complex mechanism where it doesn't actually declare the named theorem but does something like what private does and stops issuing warnings once a proper declaration is made. That sounds very complicated though!

[fgdorais]

The Mathlib patch has passed CI. I can't think of any major edits to this PR, but I'm always happy to hear nitpicks! @semorrison Do we still have time to make the 4.2.0 release?

[joehendrix]

@eric-wieser It is indeed a subtle, even possibly misleading example, since one has to make the equivalence between the two bind functions.

I did that intentionally in the "spec" because #334 is currently under review, and I think the notion of "infix" is not literally syntactically equal to infix notation, but a more general semantic notion.

[semorrison]

The Mathlib patch has passed CI. I can't think of any major edits to this PR, but I'm always happy to hear nitpicks! @semorrison Do we still have time to make the 4.2.0 release?

Sorry, I didn't see this query until too late. Std is now on v4.3.0-rc1.