Rewriting field_simp - how?

Stream: mathlib4

[Michael Rothgang]

It's been said many times that the current implementation of field_simp is slow and in need of a rewrite. I'm considering to try this (but may only get to this in October - if you have time for this now, go ahead!). Can somebody describe what needs changing and why? I would find that really helpful, and perhaps not just me.

[Damiano Testa]

I think that a quick win would be to at least give the tactic the option of creating side-goals asserting that all denominators (or factors of denominators) are non-zero.

[Damiano Testa]

This was discussed several times, and I think that it was never implemented.

[Yury G. Kudryashov]

It would be nice to turn it into a ring-style tactic with an option to choose whether to assume that all denominators are nonzero.

[Heather Macbeth]

@Michael Rothgang I just saw you had plans to rewrite field_simp "in October" :smiley:. In case this is still on your to-do list, here are a few things I'd love to see:

• conv version of field_simp
• handle inequalities: field_simp-ify LHS and RHS separately and then cross-multiply
• handle cases when only some denominators are known to be nonzero, but those ones are enough to solve the goal at hand.

For a test case for the third one:

import Mathlib

example {a b : ℝ} (ha : a ≠ 0) : a / (a * b) - 1 / b = 0 := by
  linear_combination mul_inv_cancel₀ ha / b -- works

example {a b : ℝ} (ha : a ≠ 0) : a / (a * b) - 1 / b = 0 := by
  field_simp -- fails, "simp made no progress"

[Heather Macbeth]

I also think it would be good to disable the current possibility of accessing and modifying the simp inside the field_simp implementation. This means that all the proofs in which people sneak other lemmas into a field_simp, like (choosing a random library example)

field_simp [norm_smul, smul_smul, sq_abs, Real.sq_sqrt this.le,  ← Real.sqrt_div this.le]

would have to be decoupled into a simp only step and a true field_simp step.

(In fact, I suspect that a sufficiently flexible field_simp implementation will not actually be a wrapper for simp any more, but a true custom-written tactic. If so, the above request will be fulfilled by default.)

[Michael Rothgang]

Thanks for reminding me! This is actually still on my "distant ideas" list - but looks like a nice metaprogramming project. I may actually take this on (in the second half of October, or perhaps November, as I want to wind down some other Lean work I took up in the meantime...) Thanks for the ideas!

[David Loeffler]

Adding my take on this here, since the issue came up again in another thread.

In my personal view, the main problem with field_simp at the moment isn't lack of features, but slowness: whenever I try to use it, it ends up being so sluggish that I usually end up losing patience and falling back on manual rewrites instead. I would much rather see speed improvements within the existing spec, than new features that don't solve the slowness problem.

[Daniel Weber]

Is anybody currently working on this?

[Arend Mellendijk]

I've been thinking about this recently. My motivation has been Heather's third point above: I got annoyed when it couldn't prove Real.log x / (x * (Real.log x)^2) = 1 / (x * Real.log x) using just Real.log x != 0

I think the right thing to do is to write an extension to ring (field perhaps?) that keeps more careful track of the nonzero atoms. Having skimmed the internals of ring we can mostly just build on top of the existing infrastructure. It probably wouldn't be too difficult to get something that works better than field_simp. I also think this could be quite a bit faster if we keep more careful track of the nonzero proofs.

One would definitely run into challenges with having to keep track of normal forms of expressions like a/(a+a*b), but that's also true of field_simp.

[Jovan Gerbscheid]

Note that since 3 days ago (#21326) field_simp is faster. I disabled it from trying to apply lemmas that aren't applicable to fields (and cost time to fail).

[Thomas Zhu]

My opinion is that field_simp should be given the (default?) option to assume all (factors of) denominators are aren't 0. I have almost never encountered a case where I need to call field_simp but a denominator can be 0. It can try a discharger like positivity and then fall back to leaving an extra subgoal for proving nonzero to the user.

[Daniel Weber]

Do you mean aren't zero?

[Michael Stoll]

What would also be nice (perhaps activated by a config option because it might be expensive) is for the field tactic to check if the statement still holds when one of the denominators it could not prove to be nonzero is in fact zero. E.g., x * x / x = x holds even when x = 0.

In any case, I definitely support the idea that field assumes that all relevant denominators are nonzero and leaves these as side goals when it cannot prove them. (Possibly also via a config option.)

[Daniel Weber]

I'm interesting in implementing this, and based on these suggestions I'm thinking of the following draft:

• This will be implemented as field normalization tactic, like ring (see #4837)
• There will be a nonzeroness discharging tactic (like docs#finiteness), I'm unsure about the details of it but it should fail quickly
• A default field will:
  • Try to use nonzeroness on all denominators to prove they're nonzero
  • Simplify all denominators recursively
  • Factor denominators, and try to use nonzeroness on factors it couldn't prove previously were nonzero
• You can use field [a, b, c] to make it assume a, b, c are nonzero, field [*] to make it assume all denominators are nonzero, or field [*, -a, -b] to make it assume all denominators except a, b are nonzero. It will attempt to use nonzeroness to prove they are nonzero, and when that fails it will leave that as a subgoal.
• After it has the nonzero denominators, it will bring all fractions to a common denominator, and cancel whatever it can. Possibly-zero divisors will remain in the numerator
• In the numerator, we will cancel (a * x^n) / (b * x^m) to a / b * x^(n - m) for n != m, and to (a * x) / (b * x) for n = m, even for possibly-zero x

If anybody has any comments/suggestions/concerns I'd be glad to hear them

[Michael Stoll]

It may be an option to outsource factorization to a CAS (the validity can be checked by ring). Since field will not be a self-replacing tactic like polyrith, this would work best with a locally installed CAS. Of course, it would also be good to have a Lean implementation (there is some discussion on implementing a CAS in Lean, I think), but this would be quite a lot of work and should not hold up getting a reasonable first version of field into Mathlib.

[Daniel Weber]

I think getting something basic in Lean hopefully shouldn't be too hard, and outsourcing this computation to a CAS could be slower (due to the costs of calling it) and less portable

[Kevin Buzzard]

In my experience, not worrying about CAS for now and just worrying about the case where the denominator is e.g. a * b * c^n and picking up a!=0, b!=0, c!=0 will already be very useful.

[Daniel Weber]

Sounds like a good idea, so I'll start with that. Any suggestions for behavior of the nonzeroness tactic? I think just trying assumption and if that fails trying to show 0 < x using positivity would be a good start

[Damiano Testa]

As a first implementation, I would leave try assumption.

[Damiano Testa]

Or even skip.

[Michael Stoll]

Daniel Weber said:

nonzeroness

Maybe call it nonvanishing? "Nonzeroness" looks a bit clumsy language-wise. (Disclaimer: not a native :flag_united_kingdom: :flag_united_states: speaker.)

[Ruben Van de Velde]

positivity already proves nonzeroness, btw

[Michael Stoll]

But positivity wants a partial order:

import Mathlib

example : (2 : ZMod 5) ≠ 0 := by positivity
/-
failed to synthesize
  PartialOrder (ZMod 5)
Additional diagnostic information may be available using the `set_option diagnostics true` command.
-/

and field should also work in positive characteristic, for example.

[Ruben Van de Velde]

Can we make positivity work rather than having two tactics doing nearly the same thing?

[Arend Mellendijk]

There's always just the field_simp discharger, which roughly tries assumption, norm_num, positivity and finally simp with a custom simp-set

[Daniel Weber]

That sounds good for now, and it could be changed later

[Daniel Weber]

Kevin Buzzard said:

In my experience, not worrying about CAS for now and just worrying about the case where the denominator is e.g. a * b * c^n and picking up a!=0, b!=0, c!=0 will already be very useful.

Do you think supporting a variable n here is important, or is that relatively uncommon?

[Daniel Weber]

Is there a way to simplify x^n / x^m for general x, n, m?

[Kevin Buzzard]

The only reason I mentioned powers was that I'd seen them before in explicit examples where I wanted field_simp to do better

[Daniel Weber]

I'm asking if the exponent was variable or a constant integer in those cases

[Kevin Buzzard]

I can't remember

[Kevin Buzzard]

No doubt if you implement it for constants then at some point someone will complain that they have a variable nat power and it didn't work (historically the same thing happened for ring)

[Daniel Weber]

Even ignoring factoring, I think polynomial GCD might be fairly necessary

[Kevin Buzzard]

What I'm saying is that in practice denominators are often already factored.

[Daniel Weber]

Kevin Buzzard said:

What I'm saying is that in practice denominators are often already factored.

Hmm. Taking advantage of that might be a bit tricky with ring's architecture of immediately distributing products, I'll think about how to do that

[Arend Mellendijk]

Daniel Weber said:

Is there a way to simplify x^n / x^m for general x, n, m?

Here's an idea:

import Mathlib

variable {G₀ : Type*} [GroupWithZero G₀] [DecidableEq G₀]

def zpow' (a : G₀) (n : ℤ) : G₀ :=
  if a = 0 ∧ n = 0 then 0 else a^n

example {x : G₀} (a b : ℤ) :
    zpow' x (a+b) = zpow' x a * zpow' x b := by
  simp_rw [zpow']
  by_cases hx : x = 0
  · simp [hx, zero_zpow_eq]
    split_ifs <;> simp
  simp [hx]
  apply zpow_add₀ hx

If you can show any naturally-occurring exponents are nonzero you can rewrite them into zpow' and normalise everything in terms of that.

[Michael Stoll]

Daniel Weber said:

Even ignoring factoring, I think polynomial GCD might be fairly necessary

Polynomial GCD should indeed be all that is necessary. But to do this reasonably efficiently for multivariate polynomials (that are noncomputable in Mathlib...) is still a serious task (and will necessitate to decide whether fairly random field elements are zero or not during the algorithm, I would think).

I guess a first reasonable step is to just rewrite as a quotient of polynomials on both sides of the equality, then cross-multiply and let ring do its work. Once this works reliably and is reasonably efficient, we can think of adding more bells and whistles.

[Daniel Weber]

Michael Stoll said:

and will necessitate to decide whether fairly random field elements are zero or not during the algorithm, I would think

If everything except constant integers are atoms than this shouldn't be a problem, I think

I guess a first reasonable step is to just rewrite as a quotient of polynomials on both sides of the equality, then cross-multiply and let ring do its work. Once this works reliably and is reasonably efficient, we can think of adding more bells and whistles.

This wouldn't as a normalization tactic, but I guess as a start it works. It might be easier to convert a = b to a - b = 0, simplify a - b, and if that's c / d with nonzero d you can turn the goal to c = 0

[Michael Stoll]

That should be more or less the same ($a/b - c/d = (ad - bc)/(bd)$, so we get the same effect as first changing $a/b = c/d$ to $ad = bc$ assuming $b, d \neq 0$). Whatever is easier to implement.

[Arend Mellendijk]

Michael Stoll said:

Polynomial GCD should indeed be all that is necessary. But to do this reasonably efficiently for multivariate polynomials (that are noncomputable in Mathlib...) is still a serious task (and will necessitate to decide whether fairly random field elements are zero or not during the algorithm, I would think).

I agree this is a serious task and out of scope for an initial tactic but I think the coefficients in ring are just rational literals, so equality checks wouldn't be an issue (in characteristic 0 at least).

[Michael Stoll]

To figure out $\gcd(y^2-x, y)$, you'll need to know whether $x$ is zero or not.

But it would already be helpful to determine "generic" gcds (i.e., assuming that all nontrivial polynomials are nonzero) to get at least some normalization of quotients.

[Kevin Buzzard]

Just to reiterate -- my recollections of the complaints about field_simp were usually of the form "it's too slow" or "I had A/x + B/x^2 + C/x^3 and it multiplied everything by x*x^2*x^3 instead of x^3" or "why did it not spot that the denominator was obviously non-zero" and were basically never of the form "the denominator is x^2-y^2 and I had hypotheses that x+y and x-y were nonzero, why did the machine not factor x^2-y^2" or any other complaint related to factorization in any kind of nontrivial way.

[Damiano Testa]

I agree with Kevin: anything that can be factored "syntactically", probably should be, clear that out and then worry about the "syntactic factors" being non-zero later.

[Arend Mellendijk]

You needs to take care that such factorisations are not expanded greedily by the ring tactic. Perhaps a field tactic needs to hold back a bit on the normalisation it does.

[Daniel Weber]

I've thought about this, and after looking at the implementation of ring, I'm thinking:

A monomial is $(\prod_{j \in C} \frac{a_j}{a_j})\prod a_i ^ {b_i}$ where $a_i$ are the atoms and $b_i$ are integers. If we can prove $b_i \ne 0$ then we can remove $i$ from $C$. (This is ring's ExBase and ExProd)
We have sums of monomials, analogous to ring's ExSum.

We also have a new ExDiv, which is the quotient of an ExSum by an ExProd, together with a proof that the denominator is nonzero (and as a consequence $C = \emptyset$).

When we want to add or multiply ExDivs we take a common denominator.

If we want to invert an ExDiv we attempt to prove that the numerator is nonzero. If that fails we construct an atom from the numerator and use ExProd with a power of $-1$, otherwise we can just swap the numerator and denominator

[Daniel Weber]

Regarding distributing I think only distributing things inside a sum inside a product should work fairly well

[Timo Carlin-Burns]

Is that supposed to say $\frac{a_j}{a_j}$?

[Daniel Weber]

Yes - it's 1 if $a_j$ is nonzero and 0 if it is zero