mathport issues

Stream: mathlib4

[Yury G. Kudryashov]

How difficult would it be to fix the following bugs in mathport?

• lemma _root_.something looses _root_;
• at least sometimes, lemma names in simp only [...] are not translated;
• dot notation is often translated incorrectly.

[Mario Carneiro]

1. relatively easy
2. it depends on the reason why the names are not translated. I would not be surprised if this is quite hard to fix
3. This requires additional information from lean 3, but it should not be impossible

[Yury G. Kudryashov]

I'll post specific issues next time I meet (2) and/or (3)

[Johan Commelin]

In my most recent ports, I think (2) and (3) account for >50% (maybe even >75%) of the "mechanical fixes".
The "non-mechanical fixes" are places where you really need to think because something changed between Lean 3 and Lean 4.

[Johan Commelin]

And nowadays it happens quite often that a file only needs mechanical fixes.

[Yury G. Kudryashov]

One more issue: in #1772, Lean treats ×ᶠ as right-associative (though it's probably a Lean bug, not a mathport bug)

[Yury G. Kudryashov]

I had to add ( ) here and there.

[Yury G. Kudryashov]

(a bug or a feature I didn't know about)

[Mario Carneiro]

mathport should not be getting parentheses wrong. It inserts parentheses only when necessary according to the lean 4 precedence of the operation

[Mario Carneiro]

can you point to a specific example of this?

[Johan Commelin]

There's also the (Quot.inductionOn foo) bar baz issue, right?

[Mario Carneiro]

that was fixed

[Johan Commelin]

cool

[Mario Carneiro]

that was also not strictly speaking an issue in incorrectly inserted parentheses, but an issue in the syntax itself that was generated which meant that the parentheses had to be inserted to distinguish it from the other (desired) interpretation

[Mario Carneiro]

i.e. the issue was more like a missing operator symbol than parentheses, the parentheses were just for disambiguation

[Johan Commelin]

@Mario Carneiro Do you think you can fix mathlib4 so that we can use x^s notation for Finset.product instead of ×ᶠ?

[Mario Carneiro]

is that a new notation or something?

[Johan Commelin]

mathlib3 uses the same notation for external product of sets and finsets.

[Johan Commelin]

But mathlib4 didn't like that, so now people are manually switching to a tmp new notation

[Mario Carneiro]

do the two notations have different names in lean3?

[Johan Commelin]

It was directly notation for set.prod and finset.product, I think.

[Johan Commelin]

I don't know if that answers your question

[Johan Commelin]

But there was no notation typeclass

[Mario Carneiro]

I mean the name := thing

[Johan Commelin]

Ooh, you mean in Lean 4?

[Mario Carneiro]

no

[Mario Carneiro]

the name := thing we added to all the localized notations in lean 3

[Mario Carneiro]

if it's just two notation overloads hopefully they have different names

[Johan Commelin]

Looks fine: https://github.com/leanprover-community/mathlib/blob/1f0096e6caa61e9c849ec2adbd227e960e9dff58/src/data/finset/prod.lean#L40

[Johan Commelin]

And here's the one for set.prod: https://github.com/leanprover-community/mathlib/blob/1f0096e6caa61e9c849ec2adbd227e960e9dff58/src/data/set/prod.lean#L39

[Johan Commelin]

So yes, they have different names

[Yaël Dillies]

Note that I made a bunch more product-like operations have this notation, but we haven't reached them yet.

[Johan Commelin]

It seems that the list is:

src/order/upper_lower.lean:infixr (name := upper_set.prod) ` ×ˢ `:82 := prod
src/order/upper_lower.lean:infixr (name := lower_set.prod) ` ×ˢ `:82 := lower_set.prod
src/data/set/prod.lean:infixr (name := set.prod) ` ×ˢ `:82 := set.prod
src/data/list/defs.lean:infixr (name := list.product) ` ×ˢ `:82 := list.product
src/data/multiset/bind.lean:infixr (name := multiset.product) ` ×ˢ `:82 := multiset.product
src/data/finset/prod.lean:infixr (name := finset.product) ` ×ˢ `:82 := finset.product

[Johan Commelin]

Apparently we didn't hit problems with list.product and multiset.product?

[Yaël Dillies]

Oh that's unexpected

[Yury G. Kudryashov]

So, ×ᶠ is defined as infixr notation for finset.product! Now I see why Lean doesn't use it as infixl for Filter.prod.

[Yury G. Kudryashov]

BTW, Lean was otherwise happy with duplicate notation.

[Reid Barton]

It must be an oversight that the notation for filter.prod was not infixr

[Yury G. Kudryashov]

It's "infix" in Lean 3.

[Mario Carneiro]

infix = infixl in lean 3

[Mario Carneiro]

(in lean 4 infix is more like "nonassociative")