inf and sup don't bind similarly

Stream: general

[Rémy Degenne]

It looks like inf and sup don't behave similarly in expressions involving arithmetic operations. See the mwe below:

import order.lattice
import algebra.algebra.basic

variables {α : Type*} [lattice α] [add_monoid α] (a b c : α)

example : a + b ⊓ c = a + (b ⊓ c) := rfl
example : a + b ⊔ c = (a + b) ⊔ c := rfl

How would I change that? The two notations are defined in order/lattice:

/-- Typeclass for the `⊔` (`\lub`) notation -/
@[notation_class] class has_sup (α : Type u) := (sup : α → α → α)
/-- Typeclass for the `⊓` (`\glb`) notation -/
@[notation_class] class has_inf (α : Type u) := (inf : α → α → α)

infix ⊔ := has_sup.sup
infix ⊓ := has_inf.inf

I don't see why they interact differently with +.

[Eric Wieser]

Somewhere there is probably a reserve notation

[Reid Barton]

https://github.com/leanprover-community/mathlib/blob/master/src/tactic/reserved_notation.lean#L50

[Rémy Degenne]

Thanks! Indeed there is a difference:

reserve infixl ` ⊓ `:70
reserve infixl ` ⊔ `:65

I guess it's different in order to have a well defined binding order between these two notations? And the number for + falls somewhere in between, maybe? Where can I find the one for +?

[Reid Barton]

that one is in core with most of the others:
https://github.com/leanprover-community/lean/blob/4887d8a30621941c883f208e151e61ab268c006d/library/init/core.lean#L336

[Rémy Degenne]

Thanks. It's the first time I look at that type of issue. + and - are at 65 as well. Am I correct in thinking that if we change ⊔ to 66 then it should behave like ⊓ with respect to + and -?

[Eric Wieser]

#print notation will show you the precedence of all the notation, in case you didn't know

[Eric Wieser]

Currently we have `∑`:1024 binders `,`:0 (scoped 67) := #0 , which suggests to me that that ⊔ should be at least 68 so that ∑ i, f i ⊔ x means (∑ i, f i) ⊔ x to match the behavior on inf.

[Reid Barton]

Isn't that parenthesization backwards? I notice the original message carefully avoided specifying which behavior is desired.
For me a + b ⊔ c = (a + b) ⊔ c seems a bit more natural, I guess.

[Reid Barton]

Mostly it would be nice if it was just an error, for all the combinations--but I don't think Lean supports this

[Rémy Degenne]

Eric Wieser said:

#print notation will show you the precedence of all the notation, in case you didn't know

Thanks, I did not know that.

[Rémy Degenne]

I don't have a preference for one of the two behaviours. But I'd like it to be the same. Bumping sup to 69 to have it very close to inf looks like the easiest solution.

[Yaël Dillies]

Personally I'd have assumed their precedences were one off.

[Rémy Degenne]

I'll PR that change

[Eric Wieser]

Reid Barton said:

Isn't that parenthesization backwards? I notice the original message carefully avoided specifying which behavior is desired.
For me a + b ⊔ c = (a + b) ⊔ c seems a bit more natural, I guess.

Isn't what you consider more natural consistent with my parenthesization?

[Reid Barton]

Yes but it's not the effect that ⊔:68 would have.

[Eric Wieser]

Ah, right; then I guess:

reserve infixl ` ⊓ `:64
reserve infixl ` ⊔ `:63

would have the desired effect

[Rémy Degenne]

putting sup to 69 caused no error anywhere (the build completed just now). I will change to those values and see what I get.

[Yaël Dillies]

I quite prefer a + b ⊔ c = a + (b ⊔ c) in the sense that + is almost alien to sets, so you would read and group first set operations, then those alien pointwise addition.

[Eric Wieser]

What about on the naturals? ⊔ is alien to sets too so that's a weird comparison.

[Rémy Degenne]

to sets? I'm thinking of sup as a max in an order which is not linear. For sets you would use union

[Yaël Dillies]

Hmm... still

[Yaël Dillies]

⊔ is basically max and max a b + c = (max a b) + c

[Eric Wieser]

That argument is lousy though, because you could use it to justify maximum precedence for any operator just by replacing it with a function invocation:

+ is basically add so add a b ⊔ c = (add a b) ⊔ c

[Rémy Degenne]

Eric Wieser said:

Ah, right; then I guess:

reserve infixl ` ⊓ `:64
reserve infixl ` ⊔ `:63

would have the desired effect

The build fails very quickly with those... I don't have the courage to fix everything if it's more than a couple of errors. If that's the case and we really want those values, somebody else will have to do it.

[Eric Wieser]

Can you give an example of the expression that causes the failure?

[Rémy Degenne]

see branch#sup_bind

[Eric Wieser]

Hmm, worth also noting that * has the same precedence as ⊓ in master

[Eric Wieser]

Perhaps @Christopher Hoskin can comment on what they think the relative precedence of +*⊓⊔ should be, since the file they authored is the one causing the trouble, and also the one that mixes the notations the most.

[Rémy Degenne]

right, the error is in src/algebra/lattice_ordered_group.lean. That's not too bad, since it's not imported by many other files. If that is the only part of mathlib in which there are errors, it will be fixable easily. My original reason for looking at those precedences is related to that file, since I am putting a normed_lattice_add_comm_group instance on Lp.

[Christopher Hoskin]

Perhaps Christopher Hoskin can comment on what they think the relative precedence of +*⊓⊔ should be, since the file they authored is the one causing the trouble, and also the one that mixes the notations the most.

I 'd noticed this, but didn't realise that I'd caused the problem!

[Rémy Degenne]

You did not cause the problem, but your files are the (only?) ones in which it manifests.

[Rémy Degenne]

So you might have an opinion on the matter

[Christopher Hoskin]

I think a + b ⊔ c = a + (b ⊔ c) is what I'd intuitively assume (which doesn't make it right!)

[Eric Wieser]

What about * and ⊓? I assume we all agree on the relative precendence within +* and ⊔⊓, but that still leaves us with 6 variations to pick between

[Kevin Buzzard]

I suspect that these are unsolved problems in mathematics.

[Kevin Buzzard]

I remember having the same conversation with finite/infinite sums and products, trying to figure out what $\sum_i a_i+c$ and $\prod_i a_i + c$ should mean in Lean.

[Kevin Buzzard]

In the end someone found a random mathoverflow post which asked this and just went with the convention suggested by the highest ranked answer IIRC

[Eric Wieser]

Reid Barton said:

Mostly it would be nice if it was just an error, for all the combinations--but I don't think Lean supports this

Ideally we would just be able to declare it unsolved as Reid suggests here; does Lean 4 support this?

[Johan Commelin]

/--
There is no established mathematical convention
for the operator precedence of big operators like `∏` and `∑`.
We will have to make a choice.

Online discussions, such as https://math.stackexchange.com/q/185538/30839
seem to suggest that `∏` and `∑` should have the same precedence,
and that this should be somewhere between `*` and `+`.
The latter have precedence levels `70` and `65` respectively,
and we therefore choose the level `67`.

In practice, this means that parentheses should be placed as follows:
```lean
∑ k in K, (a k + b k) = ∑ k in K, a k + ∑ k in K, b k →
  ∏ k in K, a k * b k = (∏ k in K, a k) * (∏ k in K, b k)
```
(Example taken from page 490 of Knuth's *Concrete Mathematics*.)
-/
library_note "operator precedence of big operators"

localized "notation `∑` binders `, ` r:(scoped:67 f, finset.sum finset.univ f) := r"
  in big_operators
localized "notation `∏` binders `, ` r:(scoped:67 f, finset.prod finset.univ f) := r"
  in big_operators

localized "notation `∑` binders ` in ` s `, ` r:(scoped:67 f, finset.sum s f) := r"
  in big_operators
localized "notation `∏` binders ` in ` s `, ` r:(scoped:67 f, finset.prod s f) := r"
  in big_operators

[Kevin Buzzard]

it's all happening around priority 67 isn't it!

[Rémy Degenne]

After fixing the first errors with 63 and 64 I see other errors pop up in other files. Since changing sup to be 69 (close to the 70 of inf) does not cause any error I will PR that and suggest that we adopt quite arbitrarily the convention of least resistance.

[Eric Wieser]

I think having the priority of inf and mul equal is very unlikely to be what we want, because it means:

#check ((1 ⊓ 2) * 3)
#check ((1 * 2) ⊓ 3)

both are the default parsings

[Kevin Buzzard]

given that mathematicians don't seem to care/know and would probably instinctively put brackets whatever the lean conventions, maybe this is OK?

[Eric Wieser]

If we leave ⊓ at 70 then it has exactly the same problems with * (both have precedence 70) as ⊔ does with + (both have precedence 65) that started this thread

[Eric Wieser]

So we should either do nothing, or fix both

[Rémy Degenne]

I pushed 68 for sup and 69 for inf on branch#sup_bind_2 . If that's also errorless, then that may be a good solution?

[Yaël Dillies]

Yes, that sounds good.

[Eric Wieser]

The current behavior in master is:

variables {α : Type*} [lattice α] [has_add α] [has_mul α] (a b c : α)

-- equal precendence, so order-based
example : a + b ⊔ c = (a + b) ⊔ c := rfl
example : a ⊔ b + c = (a ⊔ b) + c := rfl
example : a * b ⊓ c = (a * b) ⊓ c := rfl
example : a ⊓ b * c = (a ⊓ b) * c := rfl
-- unequal precedence
example : a * b ⊔ c = (a * b) ⊔ c := rfl
example : a ⊔ b * c = a ⊔ (b * c) := rfl
example : a + b ⊓ c = a + (b ⊓ c) := rfl
example : a ⊓ b + c = (a ⊓ b) + c := rfl

[Yaël Dillies]

although I would maybe get away from this 65-70 range because it's already used by algebraic operations.

[Yaël Dillies]

For example, / is 70

[Eric Wieser]

So is *, which was exactly my point above

[Yaël Dillies]

Ah sorry, I missed it.

[Yaël Dillies]

There's also neg that we should take into account.

[Yaël Dillies]

I propose that we move the precedence of all binary algebraic operations (+, -, *, /) below the binary lattice ones (⊓, ⊔, ∩, ∪, \). The unary ones (-, ⁻¹, ᶜ ) can stay high.

[Eric Wieser]

Don't forget sdiff and compl

[Rob Lewis]

@Rémy Degenne did this in #10623. I think this is an improvement that doesn't involve a big refactor. Is anyone interested in trying one of the more ambitious ideas?

[Johan Commelin]

I'm voting for merging that PR.

[Johan Commelin]

More ambitious ideas can still be tried after merging.