[Merged by Bors] - field_simp: Use positivity as a discharger

[nomeata]

The main reasons is that having h : 0 < denom in the context should suffice for field_simp to do its job, without the need to manually pass h.ne or similar.

Quite a few have := … ≠ 0 could be dropped, and some field_simp calls no longer need explicit arguments; this is promising.

This does break some proofs where field_simp was not used as a closing tactic, and it now
shuffles terms around a bit different. These were fixed. Using field_simp in the middle of a proof seems rather fragile anyways.

As a drive-by contribution, positivity now knows about π > 0.

fixes: #4835

---

[nomeata]

This is my attempt at #4835. Some questions:

• Should I refactor positivity like I do, to be able to pass an Expr to it, or should I do it differently?
• I did not match on the goal in field_simp to see if we can expect positivity to succeed, but simply try positivity every time, as that will do that check first. ok?
• If the same denom ≠ 0 precondition comes up multiple times, will this run positivity multiple times? Should we maybe remember and reuse the result (as a new hypothesis)? If so, should we remove them afterwards somehow?
• The logic in discharge of “try this, then this, then this” looks awfully manual. Is there no combinator for sequencing discharger functions?
• For field_simp only [ … ] the expectation might the that no implicit context (e.g. positivity extensions) should be used. Should positivity be disabled in only mode?
• I see field_simp [_root_.abs_of_nonneg Real.pi_pos.le, Real.pi_pos.ne.symm] because positivity cannot solve π > 0.. Should positivity be able to do that? Now it does!

[nomeata]

There will be a merge conflict with @mattrobball’s #6034, and they eliminate some of the same extra steps, but both additions seem to be useful.

[mattrobball]

Yeah. This looks great. My motivation was code like

have : n \neq 0 := sorry
have : (n : Real) := by norm_cast; exact this

A real world example is in Geometry.Manifold.Instances.Sphere which I saw when porting.

#6034 handles this. But it makes more sense to operate on the norm casted term directly. This runs into the problem that often there are simp args fed into field_simp un-normalized to work around the existing issues.

Right now I want to norm_cast all the simp theorems in the context and then go. But I haven't gotten back to it yet.

[nomeata]

What does this mean for the present PR? Go ahead, wait for yours first, do them together?

[mattrobball]

Go full speed ahead. Feel free to incorporate whatever from #6034 or nothing.

[mattrobball]

Whatever your want is good with me.

[nomeata]

In that case I’ll just be lazy and ignore your PR for now, and see if I can get this change in without learning more about normCast :-)

[sgouezel]

!bench

[nomeata]

I couldn’t find information on !bench; where will I see the result?

[mattrobball]

The bot will report back once it clears the queue

[leanprover-bot]

Here are the benchmark results for commit ce54f5e.Found no runs to compare against.

[nomeata]

I’ll be traveling without a laptop for week, and will address review comments afterwards. Should anyone want to adopt this PR and see it through, that’s fine with me as well.

[nomeata]

Back from vacation. What’s needed to make progress here?

[mattrobball]

!bench

[leanprover-bot]

Here are the benchmark results for commit dfc7782.
The entire run failed.
Found no significant differences.

[mattrobball]

!bench

[nomeata]

Looks like latest master (or the speedcenter) had stricter linting. Fixed, I hope.

[mattrobball]

#6579

[leanprover-bot]

Here are the benchmark results for commit f6de4b6.
There were significant changes against commit 916c75c:

  Benchmark                                                                Metric           Change
  ================================================================================================
+ build                                                                    native linking    -5.0%
- ~Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating   instructions      35.7%
- ~Mathlib.Analysis.Convex.Slope                                           instructions       6.2%
+ ~Mathlib.Analysis.SpecialFunctions.Stirling                              instructions      -6.0%
+ ~Mathlib.NumberTheory.Bernoulli                                          instructions      -7.3%

[nomeata]

Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating uses a bunch of field_simp, not unexpected that it got slower. A quick glance at it doesn’t show any obvious ways to fix this. Other modules sped up… not sure what to make of it.

[mattrobball]

I think field_simp should be closer to a finishing call than what that file wants to do.

I think the performance profile is good and the PR definitely improves user ergonomics.

@sgouezel do you have any concerns?

[sgouezel]

I'm perfectly happy with the performance, given how it improves readability and usability. Someone more skilled than me in meta code should still review it properly, however. If noone shows up, you can ping on Zulip.

[semorrison]

Looks great, thanks!

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style