mathport: big operators

Stream: mathlib4

[Yury G. Kudryashov]

Did precedence of big operators change from mathlib 3 to mathlib 4? I have to add () here and there.

[Yury G. Kudryashov]

I mean, add them to the mathport output.

[Yury G. Kudryashov]

It looks like a mathport bug, not a difference between mathlib3 and mathlib4.

[Yury G. Kudryashov]

E.g., compare source with mathport output

[Yury G. Kudryashov]

@Mario Carneiro :up:

[Mario Carneiro]

note that these are generally bugs in the core formatter / selected delaborators or parenthesizers, not mathport itself (which just uses those formatters)

[Mario Carneiro]

Is it actually correct to not put parentheses there?

[Mario Carneiro]

do you have a self contained example of the desired parenthesization?

[Yury G. Kudryashov]

No, it is not correct.

[Yury G. Kudryashov]

This works as the statement of that lemma:

theorem norm_volume_sub_integral_face_upper_sub_lower_smul_le {f : (Fin (n + 1) → ℝ) → E}
    {f' : (Fin (n + 1) → ℝ) →L[ℝ] E} (hfc : ContinuousOn f (Box.Icc I)) {x : Fin (n + 1) → ℝ}
    (hxI : x ∈ (Box.Icc I)) {a : E} {ε : ℝ} (h0 : 0 < ε)
    (hε : ∀ y ∈ (Box.Icc I), ‖f y - a - f' (y - x)‖ ≤ ε * ‖y - x‖) {c : ℝ≥0}
    (hc : I.distortion ≤ c) :
    ‖(∏ j, (I.upper j - I.lower j)) • f' (Pi.single i 1) -
      (integral (I.face i) ⊥ (f ∘ i.insertNth (α := fun _ ↦ ℝ) (I.upper i)) BoxAdditiveMap.volume -
        integral (I.face i) ⊥ (f ∘ i.insertNth (α := fun _ ↦ ℝ) (I.lower i)) BoxAdditiveMap.volume)‖ ≤
      2 * ε * c * ∏ j, (I.upper j - I.lower j) := by

[Yury G. Kudryashov]

What means "self contained example"? How do I emulate the mathport output?

[Mario Carneiro]

I mean just without all the box integral stuff, just a simple example of precedence ordering

[Mario Carneiro]

you don't need to give a mathport example

[Mario Carneiro]

we can test the formatter without mathport

[Yury G. Kudryashov]

I think, just ∏ j, f j - g j should work.

[Mario Carneiro]

imports?

[Yury G. Kudryashov]

Whait a minute

[Yury G. Kudryashov]

import Mathlib.Algebra.BigOperators.Basic

open scoped BigOperators

example : ∃ f g : Fin 5 → ℤ, ∏ j, f j - g j ≠ ∏ j, (f j - g j) :=
  _

[Yury G. Kudryashov]

How do I test it?

[Mario Carneiro]

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/missing.20ppSpace.20for.20mathport.3F/near/362934262

[Yury G. Kudryashov]

mathport prints RHS as LHS (here j in g j is an autoimplicit variable)

[Mario Carneiro]

(note when you use the method there you get a bunch of daggers on identifiers, this can be ignored)

[Mario Carneiro]

I'm getting:

import Mathlib.Algebra.BigOperators.Basic

open scoped BigOperators

open Lean PrettyPrinter
def fmt (stx : CoreM Syntax) : CoreM Format := do PrettyPrinter.ppTerm ⟨← stx⟩

#eval fmt `(∃ f g : Fin 5 → ℤ, ∏ j, f j - g j ≠ ∏ j, f j - g j)
-- ∃ f✝ g✝ : Fin✝ 5 → ℤ, ∏ j✝, f✝ j✝ - g✝ j✝ ≠ ∏ j✝, f✝ j✝ - g✝ j✝

[Mario Carneiro]

and this seems to be correct (the scoping is in fact as described)

[Yury G. Kudryashov]

You mean,

import Mathlib.Algebra.BigOperators.Basic

open scoped BigOperators

open Lean PrettyPrinter
def fmt (stx : CoreM Syntax) : CoreM Format := do PrettyPrinter.ppTerm ⟨← stx⟩

#eval fmt `(∃ f g : Fin 5 → ℤ, ∏ j, f j - g j ≠ ∏ j, (f j - g j))

[Mario Carneiro]

∏ j, f j - g j actually means ∏ j, (f j - g j) when parsed and printed

[Mario Carneiro]

so there doesn't seem to be an issue here, unless your point is that the notation is not declared correctly and this should not parse

[Yury G. Kudryashov]

No, ∏ j, f j - g j means fun {j} => (∏ j, f j) - g j

[Mario Carneiro]

oh, you are right

[Yury G. Kudryashov]

import Mathlib.Algebra.BigOperators.Basic

open scoped BigOperators

example : ∃ f g : Fin 5 → ℤ, ∏ j, f j - g j ≠ ∏ j, (f j - g j) :=
  _

says

Expected type:
⊢ ∀ {j : Fin 5}, ∃ f g, ∏ j : Fin 5, f j - g j ≠ ∏ j : Fin 5, (f j - g j)

[Yury G. Kudryashov]

But this input preserves () in the output.

[Yury G. Kudryashov]

Does it mean that the bug is somewhere else?

[Mario Carneiro]

The method I showed using the fmt function preserves exactly the syntax tree as written, without elaboration/delaboration

[Mario Carneiro]

this is a bit closer to what mathport is doing

[Mario Carneiro]

when you use the pretty printer normally the syntax being printed was delaborated from an expression, and this process can add or remove parens

[Mario Carneiro]

you can create ASTs without any parens and see if the parenthesizer will add them:

#eval do fmt `(∃ f g : Fin 5 → ℤ, ∏ j, $(← `(f j - g j)) = ∏ j, $(← `(f j - g j)))
-- ∃ f✝ g✝ : Fin✝ 5 → ℤ, ∏ j✝, (f✝ j✝ - g✝ j✝) = ∏ j✝, (f✝ j✝ - g✝ j✝)

[Yury G. Kudryashov]

I see them in the output...

[Mario Carneiro]

which seems like things are working as intended

[Yury G. Kudryashov]

But we loose parentheses somewhere on the path from mathlib3 to mathport output.

[Mario Carneiro]

can you make a lean 3 mwe to send through mathport?

[Mario Carneiro]

I guess it would be something like this?

import algebra.big_operators.basic

open_locale big_operators

example : ∃ (f g : fin 5 → ℤ) x, (∏ j, (f j - g j)) • x = 0 := sorry

[Mario Carneiro]

Okay here's a oneshot reproducer:

import algebra.big_operators.basic

open_locale big_operators

variables (f g : fin 5 → ℤ)
example : (∏ j, (f j - g j)) = 0 := sorry

->

import Mathbin.Algebra.BigOperators.Basic

open scoped BigOperators

variable (f g : Fin 5 → ℤ)

example : (∏ j, f j - g j) = 0 :=
  sorry

[Mario Carneiro]

A clue: before adding parentheses, the syntax that mathport is rendering is

(«term_=_»
 (BigOperators.Algebra.BigOperators.Basic.finset.prod_univ
  "∏"
  (Std.ExtendedBinder.extBinders (Std.ExtendedBinder.extBinder (Lean.binderIdent `j) []))
  ", "
  («term_-_» (Term.app `f [`j]) "-" (Term.app `g [`j])))
 "="
 (num "0"))

while if I try to construct the same thing manually:

import Mathlib.Algebra.BigOperators.Basic

open scoped BigOperators

open Lean PrettyPrinter
#eval show CoreM _ from return f!"{← `(∏ j, $(← `(f j - g j)))}"

I get

(BigOperators.bigprod
 "∏"
 (Std.ExtendedBinder.extBinder (Lean.binderIdent `j._@.Mathlib.Test._hyg.1) [])
 ","
 («term_-_»
  (Term.app `f._@.Mathlib.Test._hyg.1 [`j._@.Mathlib.Test._hyg.1])
  "-"
  (Term.app `g._@.Mathlib.Test._hyg.1 [`j._@.Mathlib.Test._hyg.1])))

instead. Note that the syntax kind is completely different, BigOperators.Algebra.BigOperators.Basic.finset.prod_univ instead of BigOperators.bigprod, and BigOperators.bigprod does not seem to accept a list of binders like prod_univ

[Mario Carneiro]

I think this is a "notation alignment" issue - BigOperators.Algebra.BigOperators.Basic.finset.prod_univ was a notation3 which mathport itself defined, and which does not match BigOperators.bigprod used in mathlib4

[Mario Carneiro]

and now we have a mathport-free repro:

import Mathlib.Algebra.BigOperators.Basic

notation3 "∏ "(...)", "r:(scoped f => Finset.prod Finset.univ f) => r

variable (f g : Fin 5 → ℤ)
example : (∏ j, (f j - g j)) = 0 :=
  _ -- ⊢ (∏ (j : Fin 5), f j - g j) = 0

[Yury G. Kudryashov]

So, is this a bug in notation3 or some precedence is missing in the notation declaration?

[Mario Carneiro]

notation3 lacks the syntax to declare precedences, and mathport is currently dropping this information (which is present in the lean 3 version). A fix is up at !4#4712 / mathport#240