data.real.basic mathlib4#1514

Stream: mathlib4

[Ruben Van de Velde]

I probably won't have much time today, so if anyone wants to help with mathlib4#1514, go ahead!

[Reid Barton]

I got it building except that (locally) I sorried all the proofs in the CommRing instance.
Somewhat inclined to just manually port the new proof from #8146

[Eric Wieser]

presumably a version of #8146 that doesn't change the defeq of pow?

[Eric Wieser]

Or has your opinion changed in between the comment there and the comment here?

[Reid Barton]

Right, I was trying to figure out what my opinion was about smul

[Eric Wieser]

The timeouts in that PR are currently caused by the smul change, but it's not clear to me whether the problem is the defeq change or the syntactic change

[Eric Wieser]

I haven't yet had a chance to fix them, but I know how to fix the problem if it's syntactic

[Reid Barton]

I think my opinion about smul is it's reasonable to change the definition, but maybe more practical not to.

[Reid Barton]

I added a construction of CommRing in the style of #8146 but now the rest of the file is very slow/timing out.
Maybe related to lean4#2003?

[Reid Barton]

I'm not going to have time to work on this over the weekend, so someone else should feel free to take over.

[Johan Commelin]

Can we write the construction of CommRing instance (and maybe others) in a workaround manner so that the file speeds up again?

[Ruben Van de Velde]

It seems like I managed to fix everything except the very last theorem cauSeq_converges which gets lost on the first line

  let S := { x : ℝ | const abs x < f }

If anyone want to take a look, please go ahead

[Ruben Van de Velde]

I'm gonna try merging master, who knows

[Ruben Van de Velde]

Ruben Van de Velde said:

I'm gonna try merging master, who knows

Did not help

[Eric Wieser]

Ruben Van de Velde said:

It seems like I managed to fix everything except the very last theorem cauSeq_converges which gets lost on the first line

  let S := { x : ℝ | const abs x < f }

If anyone want to take a look, please go ahead

What's the error there? I ran into an error on that line in mathlib 3 after a refactor

[Eric Wieser]

The solution was to add one := 1 etc explicitly

[Ruben Van de Velde]

Times out

[Reid Barton]

I redid the definition of CommRing in the original style and now the rest of the file is fine

[Reid Barton]

Johan and I looked into the timeouts today, they were complicated, but definitely related in part to lean4#2003

[Reid Barton]

It seems that Lean has a much easier time unifying instances when they are syntactically constructors, rather than complicated function things (even though there is no apparent reason why this should matter)

[Reid Barton]

@Eric Wieser Data.Real.Basic is now passing except for the test file; I think you mentioned something about this somewhere?

[Eric Wieser]

I think it's a trivial syntax error

[Eric Wieser]

The thing I mentioned before was fixed by adding the unsafe keyword

[Reid Barton]

ah ok

[Heather Macbeth]

Reid Barton said:

It seems that Lean has a much easier time unifying instances when they are syntactically constructors, rather than complicated function things (even though there is no apparent reason why this should matter)

Maybe this is the lean4#2003 issue again?
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/port.20benchmark/near/320915653
cc @Sebastian Ullrich @Gabriel Ebner

[Eric Wieser]

Reid Barton said:

It seems that Lean has a much easier time unifying instances when they are syntactically constructors, rather than complicated function things (even though there is no apparent reason why this should matter)

In lean 3 we had this issue too , and solved it with { one := 1, .. fancy_constructor }. Did that not work when porting this file?

[Eric Wieser]

Or phrased another way; is that not syntactically a constructor?

[Reid Barton]

hmm I only tried the where one := 1; __ := fancy_constructor form

[Eric Wieser]

Does __ mean something different?

[Reid Barton]

I don't know

[Reid Barton]

there's too many of these notations

[Reid Barton]

also with

[Mario Carneiro]

__ := s should be identical to using s with, it's a mathlib/std addition to instance syntax to allow using the s with notation in where blocks

[Mario Carneiro]

.. s is gone, but you can write { s, t with } if you want to mix multiple sources into an instance

[Eric Wieser]

And all of these desugar to constructor applications?

[Johan Commelin]

In this file, a whole bunch of instances got named, even though there were no names in the mathport output.

[Johan Commelin]

Is that intentional? Should we do it consistently?

[Johan Commelin]

Or shall we remove all the names again?

[Johan Commelin]

(I just pushed a fix for the test in test/Real. So I hope this will be ready to go in the nearish future.)

[Johan Commelin]

CI is happy now

[Reid Barton]

where [...] __ := s desugared to a let

[Ruben Van de Velde]

I probably named them because they were referred to by name and the autogenerated ones can get ridiculous (or if they were near other instances I was naming)

[Ruben Van de Velde]

I'm reviewing now

[Ruben Van de Velde]

Good to go, I think