Zulip Chat Archive

Stream: mathlib4

Topic: BigOperators parsing precedence

David Renshaw (Jan 20 2023 at 14:48):

lean 3:

import algebra.big_operators.ring
open_locale big_operators

lemma sum_range_square (n : ℕ) :
    ∑i in finset.range n, (i+1)^2 = n * (n + 1) * (2*n + 1)/6 := sorry

lean 4:

import Mathlib.Algebra.BigOperators.Basic

-- lemma sum_range_square (n : ℕ) :
--    ∑i in Finset.range n, (i+1)^2 = n * (n + 1) * (2*n + 1)/6 := sorry
-- error:
-- failed to synthesize instance
--  AddCommMonoid Prop


-- need to add parens:
lemma sum_range_square (n : ℕ) :
    (∑i in Finset.range n, (i+1)^2) = n * (n + 1) * (2*n + 1)/6 := sorry

Johan Commelin (Jan 20 2023 at 14:48):

Hmm, I don't know anything about how to set up notation in Lean 4. But I agree that it's important that we try to get this right soon.

David Renshaw (Jan 20 2023 at 14:49):

https://github.com/leanprover-community/mathlib4/blob/75cca33f9caefa5e17d29fb1896d1923417cc59c/Mathlib/Algebra/BigOperators/Basic.lean#L122

David Renshaw (Jan 20 2023 at 14:49):

I think we might need to add a term:51 there

David Renshaw (Jan 20 2023 at 14:49):

let me try that...

David Renshaw (Jan 20 2023 at 14:50):

yep, that does it

David Renshaw (Jan 20 2023 at 14:50):

I'll submit a PR

David Renshaw (Jan 20 2023 at 15:09):

https://github.com/leanprover-community/mathlib4/pull/1723

Johan Commelin (Jan 20 2023 at 15:13):

@David Renshaw does this still work/apply?

library_note "operator precedence of big operators"/--
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:

∑ 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.)

David Renshaw (Jan 20 2023 at 15:14):

let me try

Johan Commelin (Jan 20 2023 at 15:14):

If it no longer applies, please update that note as well.

David Renshaw (Jan 20 2023 at 15:14):

I'm not sure about how closely the exact precedence values are lining up between lean 4 and lean 3.

David Renshaw (Jan 20 2023 at 15:20):

yeah, I think making those precedences 67 is the right thing to do

David Renshaw (Jan 20 2023 at 15:21):

doing so shakes out a bunch of bad parenthesization downstream

Last updated: Dec 20 2023 at 11:08 UTC