## Stream: general

### Topic: inf and sup don't bind similarly

#### Rémy Degenne (Dec 04 2021 at 08:51):

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 (Dec 04 2021 at 09:14):

Somewhere there is probably a reserve notation

#### Reid Barton (Dec 04 2021 at 14:56):

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

#### Rémy Degenne (Dec 04 2021 at 15:00):

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 (Dec 04 2021 at 15:05):

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 (Dec 04 2021 at 15:10):

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 (Dec 04 2021 at 15:31):

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

#### Eric Wieser (Dec 04 2021 at 15:34):

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 (Dec 04 2021 at 15:45):

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 (Dec 04 2021 at 15:46):

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 (Dec 04 2021 at 16:01):

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 (Dec 04 2021 at 16:04):

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 (Dec 04 2021 at 16:04):

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

#### Rémy Degenne (Dec 04 2021 at 16:13):

I'll PR that change

#### Eric Wieser (Dec 04 2021 at 16:51):

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 (Dec 04 2021 at 17:13):

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

#### Eric Wieser (Dec 04 2021 at 17:35):

Ah, right; then I guess:

reserve infixl  ⊓ :64
reserve infixl  ⊔ :63


would have the desired effect

#### Rémy Degenne (Dec 04 2021 at 17:38):

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 (Dec 04 2021 at 17:42):

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 (Dec 04 2021 at 17:44):

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

#### Rémy Degenne (Dec 04 2021 at 17:45):

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

Hmm... still

#### Yaël Dillies (Dec 04 2021 at 17:46):

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

#### Eric Wieser (Dec 04 2021 at 17:46):

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 (Dec 04 2021 at 17:48):

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 (Dec 04 2021 at 17:49):

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

#### Eric Wieser (Dec 04 2021 at 17:50):

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

#### Eric Wieser (Dec 04 2021 at 17:53):

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 (Dec 04 2021 at 18:00):

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 (Dec 04 2021 at 18:01):

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 (Dec 04 2021 at 18:03):

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

#### Rémy Degenne (Dec 04 2021 at 18:03):

So you might have an opinion on the matter

#### Christopher Hoskin (Dec 04 2021 at 18:05):

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

#### Eric Wieser (Dec 04 2021 at 18:10):

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 (Dec 04 2021 at 18:27):

I suspect that these are unsolved problems in mathematics.

#### Kevin Buzzard (Dec 04 2021 at 18:28):

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 (Dec 04 2021 at 18:28):

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 (Dec 04 2021 at 18:34):

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 (Dec 04 2021 at 19:09):

/--
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 (Dec 04 2021 at 19:12):

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

#### Rémy Degenne (Dec 04 2021 at 19:12):

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 (Dec 04 2021 at 19:17):

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 (Dec 04 2021 at 19:19):

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 (Dec 04 2021 at 19:20):

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 (Dec 04 2021 at 19:20):

So we should either do nothing, or fix both

#### Rémy Degenne (Dec 04 2021 at 19:22):

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 (Dec 04 2021 at 19:23):

Yes, that sounds good.

#### Eric Wieser (Dec 04 2021 at 19:23):

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 (Dec 04 2021 at 19:24):

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

#### Yaël Dillies (Dec 04 2021 at 19:25):

For example, / is 70

#### Eric Wieser (Dec 04 2021 at 19:25):

So is *, which was exactly my point above

#### Yaël Dillies (Dec 04 2021 at 19:27):

Ah sorry, I missed it.

#### Yaël Dillies (Dec 04 2021 at 19:30):

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

#### Yaël Dillies (Dec 04 2021 at 19:35):

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 (Dec 04 2021 at 19:56):

Don't forget sdiff and compl

#### Rob Lewis (Dec 08 2021 at 19:41):

@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 (Dec 10 2021 at 10:17):

I'm voting for merging that PR.

#### Johan Commelin (Dec 10 2021 at 10:18):

More ambitious ideas can still be tried after merging.

Last updated: Dec 20 2023 at 11:08 UTC