Nonneg ring !4#1260

Stream: mathlib4

[Yury G. Kudryashov]

I fixed a timeout in !4#1260 by changing instances before with to terms that appear in the extends chain. Can we do the same to the other? It may be harder because it has more non-structure arguments.

[Notification Bot]

Yury G. Kudryashov has marked this topic as resolved.

[Notification Bot]

Yury G. Kudryashov has marked this topic as unresolved.

[Jon Eugster]

interestingly enough, the timeout you mention seem to also be fixed by just swapping

{ Nonneg.linearOrderedSemiring, Nonneg.orderedCommSemiring with

to

{ Nonneg.orderedCommSemiring, Nonneg.linearOrderedSemiring with

It compiles now and is fully linted :smile:

[Yury G. Kudryashov]

I'm going to fix the lemmas that you commented instead of removing them. It seems that the parser added coercions at wrong places.

[Yury G. Kudryashov]

@porters Should we merge it now (and unlock some dependencies) or wait for a proper fix in the Lean core?

[Yury G. Kudryashov]

@Mario Carneiro Reporting a mathport bug (or a missing feature). We have many lemmas like (s t : Finset α) : ↑(s ∪ t) = (s ∪ t : Set α). In Lean 3, this was interpreted as (s t : finset α) : (s ∪ t).to_set = s.to_set ∪ t.to_set while Lean 4 interprets it as (s t : Finset α) : (s ∪ t).toSet = (s ∪ t).toSet changing its meaning and making it useless. Is it possible to adjust these lemmas in mathport? E.g., by adding some extra arrows.

[Kevin Buzzard]

I opened an issue about this against the lean repo but my understanding is that this change was intentional so really it should be opened against mathport instead

[Jon Eugster]

Yury G. Kudryashov said:

porters Should we merge it now (and unlock some dependencies) or wait for a proper fix in the Lean core?

I believe with per-file caching it's not too much of a bother merging now even if it has a set_option maxHeartbeat in there.

[Jireh Loreaux]

Do we think the timeouts here are again the structure eta issue in type class inference?

[Yury G. Kudryashov]

I rebased on master to see how it works with new Lean

[Yury G. Kudryashov]

It works without set_option maxHeartbeats!

[Yury G. Kudryashov]

Should we merge it now?