PR for new field_simp implementation

Stream: mathlib4

[Michael Rothgang]

That PR is now up for review: #28658

[Michael Stoll]

What is the difference between simp [field] (which this PR seems to turn most instances of field_simp into) and field_simp?

[Michael Stoll]

I've also seen simp [field_simps]. This is a bit confusing...

[Michael Stoll]

What I find a bit strange is that in some cases, ring after field_simp could be removed, but in other cases, it had to be added.

[Michael Stoll]

There is even one case where field_simp; ring turns into field_simp; simp [field, div_pow]; ring.

[Notification Bot]

5 messages were moved here from #new members > Algebraic simplification / CAS by Heather Macbeth.

[Heather Macbeth]

Michael Stoll said:

What is the difference between simp [field] (which this PR seems to turn most instances of field_simp into) and field_simp?

See the PR description:

There is a big diff: the old field_simp subsumed simp, and this was often exploited. We offer a simproc version of the new field_simp, and switching to a simp call with this simproc fixes about 80% of the cases that break; the rest are handled individually (typically by alternating simp and field_simp calls).

The simproc version of the new field_simp is (provisionally) named field.

[Heather Macbeth]

Michael Stoll said:

What I find a bit strange is that in some cases, ring after field_simp could be removed, but in other cases, it had to be added.

The field_simp tactic aims to reduce to the form ⊢ A / D = B / D and then clear D to give ⊢ A = B, but (both in the current and the former implementation) has never made a guarantee about what expressions of that form it reduces to.

The new implementation sometimes gets different A and B than the old implementation did. Sometimes they used to be the same and are now different, so a final ring is necessary to prove A = B. Sometimes they used to be different and are now the same, so a final ring can be removed.

[Heather Macbeth]

Michael Stoll said:

I've also seen simp [field_simps]. This is a bit confusing...

This is a temporary hack to replicate the behaviour of the old implementation (which basically consisted of calling simp with the custom simp-set field_simps and with a custom discharger).

[Michael Stoll]

@Heather Macbeth Thanks for clarifying!
Are there some guidelines as to when one should use the simproc and when the field_simp tactic?

[Heather Macbeth]

Personally, I think it's better style to separate your simp-ing from your field_simp-ing: the resulting proofs are easier to read. Maybe in the long run we will develop consensus on this and disable the simproc.

However, as you see from the diff, providing the simproc makes it a lot easier to transition to the new implementation, since so many invocations of the current field_simp exploit the simp-ing capability!

[Joseph Myers]

There are a few TODO comments in mathlib referring to issue #15486 about slow field_simp, can those go back to using field_simp or similar with the new implementation?

[Heather Macbeth]

Yes, I think it will be safe to bring back those field_simps! I had extracted one of those examples (docs#InnerProductGeometry.cos_angle_sub_add_angle_sub_rev_eq_neg_cos_angle) as a performance test for field_simp, and it goes from 19983 heartbeats in the old implementation to 2979 heartbeats in the new implementation.

[Izan Beltran]

Thanks to all the authors!!! I am trying it and looks great :)

[Jovan Gerbscheid]

I have a feature request for field_simp. It currently multiplies out the division in a goal like a / b = c. But I would like it to also multiply out the division in goals like a / b < c or a / b ≤ c, by using a lemma like div_le_iff₀. It can use the same discharger as the rest of field_simp. This feature is also missing in the old field_simp implementation.

[Bhavik Mehta]

The authors will know better than me, but I mentioned this exact improvement to some of them as well, and my understanding is that it's planned, but not included in this PR for ease of review

[Heather Macbeth]

@Jovan Gerbscheid This is the peril of having two simultaneous Zulip threads on the same topic! See comment at #PR reviews > #28658 New `field_simp` @ 💬.

[Michael Stoll]

Is the following meant to be in scope? I would say it should be.

import Mathlib

example {c M : ℝ} (h : M ≠ 0) (n : ℕ) : (c / M) ^ n * M ^ n = c ^ n := by
  field_simp -- has no effect
  rw [div_pow, div_mul_cancel₀ _ <| pow_ne_zero n h]

(I noticed this when trying to bump Mathlib in my Heights repo. This led to a field_simp breaking. The relevant goal is

import Mathlib

example {M : ℝ} {c : ℂ} (hc : ‖c‖ < M) {n : ℕ} (hn : n > 0) :
    M * (1 + (‖c‖ / M) ^ n) = (M ^ n + ‖c‖ ^ n) / M ^ (n - 1) := by
  -- this used `field_simp` followed by some rewrites
  sorry

and I would have hoped that the new field_simp would be able to solve that on its own...)

[Heather Macbeth]

The new field_simp doesn't handle variable exponents, only numeric exponents. If you rw [div_pow], field_simp works after that.

[Heather Macbeth]

Or simp [field, div_pow] for a one-liner.

[Heather Macbeth]

Also, we also haven't (yet) made any improvements to the discharger, so you'll need to provide a by-hand proof that M is nonzero (or strictly positive), same as always. The following cleans it up pretty well:

have : 0 < M := lt_of_le_of_lt (by positivity) hc
simp [field, div_pow]

[Ruben Van de Velde]

It seems like the new field_simp doesn't complain if you pass it lemmas or definitions that it doesn't (know how to) do anything with

[Heather Macbeth]

@Ruben Van de Velde That's true, but I'm a little surprised you're noticing it! The old field_simp would have done this only since simp introduced that feature, quite recently (in v4.22.0 maybe?).

[Ruben Van de Velde]

Really? Pnt+ used it aggressively

[Heather Macbeth]

At least, I don't remember any such feature on the slightly older versions we were working with when we wrote the field_simp refactor. Do you have an example? How was PNT+ using the feature?

[Ruben Van de Velde]

The adaptations are at https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/387. I can point at specific instances when I'm back at my desk if that's helpful

[Heather Macbeth]

Please do! I don't immediately see from the diff where this would be coming up.

[Ruben Van de Velde]

https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/387/files#diff-c48bc7c964033abf9cf5153893de7388b0df489b8cddaef69bfe758fc4081e1bR1306 for example, field_simp [F, f, f'] → simp [F, f, f']; field_simp

[Heather Macbeth]

I'm writing without having experimented myself (can't do that until this evening), but let me check I understand: This is coming up because sometimes with the old field_simp (which subsumed simp) a proof was field_simp [a, b, c], and now such a proof needs to be changed to simp [a, b]; field_simp [c]? And in such cases it's hard to tell whether each of the a, b, c belongs to the simp part or the field_simp part?

[Ruben Van de Velde]

That's the situation, yeah. I'm not sure if I'd say it's hard, but it would be nice if field_simp gave a warning if you gave it something it doesn't know how to use, similar to how simp warns on unused lemmas now

[Ruben Van de Velde]

I believe I hit a few places where this made field_simp do quite a bit less, and the proof only started breaking quite a bit lower down (maybe there were haves in between?), so it took a moment to realize that I needed to scroll back up to look for a field_simp. That said, the flexible linter probably would have caught that those proofs were brittle in the first place

[Heather Macbeth]

Just checking, you are aware of the simproc version (simp [field, ...])? One motivation for providing this was that it makes bumping easier.

[Heather Macbeth]

(But the simproc version does have some limitations too, see here for details)

[Ruben Van de Velde]

Yeah, I've used both with not much thought as to which one I picked :sweat_smile:

The idea was to eventually remove the simproc, right?

[Artie Khovanov]

are there plans for a corresponding ring simproc? writing simp [field] or simpa [field] is really useful!

[Artie Khovanov]

and relatedly a field_nf for field_simp; ring_nf?