tactic for polynomial equality

Stream: mathlib4

[Arend Mellendijk]

It's currently quite annoying to prove equality of polynomials using ring, because ring isn't aware that Polynomial.C is a homomorphism:

example (a : ℚ) : (.C a + Polynomial.X)^2 = .X ^ 2 + .C (2 * a) * .X + .C (a^2) := by
  ring
  /-
  a : ℚ
  ⊢ Polynomial.C a * Polynomial.X * 2 + Polynomial.C a ^ 2 + Polynomial.X ^ 2 =
    Polynomial.X * Polynomial.C (a * 2) + Polynomial.X ^ 2 + Polynomial.C (a ^ 2)
  -/
  sorry

I have a prototype tactic for proving equations of this form, granted that the exponents are explicit natural numbers.

example (a : ℚ) : (.C a + Polynomial.X)^2 = .X ^ 2 + .C (2 * a) * .X + .C (a^2) := by
  poly
  /-
  a : ℚ
  ⊢ a + a = 2 * a
  a : ℚ
  ⊢ a * a = a ^ 2
  -/

It works quite like ring in that it puts both polynomials into a normal form, except this tactic can then equate the coefficients in the base ring and produce side goals for the user.

Is there interest for a tactic like this in mathlib? This is my first serious metaprogramming project. It's quite close to being usable, but cleaning up the code would take some time.

[Kevin Buzzard]

Why not teach the tactic that C is a ring homomorphism and have it work for all commutative rings?

[Johan Commelin]

It is quite ironic that ring uses (its own version of) polynomials under the hood, but is then actually not so good at proving equalities between Polynomials :rofl:

[Arend Mellendijk]

Kevin Buzzard said:

Why not teach the tactic that C is a ring homomorphism and have it work for all commutative rings?

The reason I chose polynomials is that there is a very clear normal form - group the coefficients by .X^n and move all of them into a single .C. In a more general setting it's not obvious to me (a) what to group by and (b) how to normalise the coefficients.

[Arend Mellendijk]

Johan Commelin said:

It is quite ironic that ring uses (its own version of) polynomials under the hood, but is then actually not so good at proving equalities between Polynomials :rofl:

I'll point out ring uses rational polynomials with explicit constants under the hood, so dealing with coefficients in an arbitrary ring is not so obvious!

[Yaël Dillies]

If we were using a • X ^ n (like quite literally every other algebra) instead of C a * X ^ n, we could simply use module and module_nf

[Yaël Dillies]

I guess you could create a tactic that does the following:

• Turn C a * into a •
• Run module or module_nf accordingly
• In the normal form version, turn back a • into C a *

[Yaël Dillies]

But I would much rather we drop the Polynomial/MvPolynomial particularism of using C a instead of • and algebraMap

[Arend Mellendijk]

I'm not familiar with module, but it doesn't seem to play very nice with polynomials:

example (a b: ℚ) : (b • 1 + a • X) * (b • 1 + a • X)
  = ((b^2) • 1) + ((2*a*b) • X) + ((a^2) • (X : Polynomial ℚ)^2) := by
  match_scalars
  /-
  a b : ℚ
  ⊢ 1 = 0
  a b : ℚ
  ⊢ 0 = b ^ 2 * 1
  a b : ℚ
  ⊢ 0 = 2 * a * b * 1
  a b : ℚ
  ⊢ 0 = a ^ 2 * 1
  -/
  repeat sorry

[Riccardo Brasca]

It doesn't play very nice with multiplication I think. If you replace all the * by • (by hand), it should work.

[Arend Mellendijk]

Not quite...

import Mathlib
open Polynomial

example (a b: ℚ) : (b • (1 : Polynomial ℚ) + a • X) • (b • (1 : Polynomial ℚ) + a • X)
  = ((b^2) • 1) + ((2*a*b) • X) + ((a^2) • (X : Polynomial ℚ)^2) := by
  match_scalars
  /-
  a b : ℚ
  ⊢ (b • 1 + a • X) * (↑b * 1) = ↑b ^ 2 * 1
  a b : ℚ
  ⊢ (b • 1 + a • X) * (↑a * 1) = ↑2 * ↑a * ↑b * 1
  a b : ℚ
  ⊢ 0 = ↑a ^ 2 * 1
  -/
  repeat sorry

[Riccardo Brasca]

Well, you mix various module structure, the first • is external multiplication by R on R[X], but the third one is just multiplication in R[X]

[Arend Mellendijk]

Right, but if we want a tactic that can solve polynomial equations we surely want it to handle multiplication inR[X]!

[Riccardo Brasca]

Yes of course. I am just saying that the tactic should do something before calling module.

[Damiano Testa]

I think that you should probably first normalize to get as close as possible to each individual summand being of the form constant * X ^ n and then replace the *.

[Riccardo Brasca]

As in

example (a b: ℚ) : (b • (1 : Polynomial ℚ) + a • X) • (b • (1 : Polynomial ℚ) + a • X)
  = ((b^2) • 1) + ((2*a*b) • X) + ((a^2) • (X : Polynomial ℚ)^2) := by
  rw [smul_eq_mul, add_mul, mul_add, mul_add, smul_mul_smul_comm, smul_mul_smul_comm,
    smul_mul_smul_comm, smul_mul_smul_comm]
  simp only [← pow_two, one_mul, mul_one, one_pow]
  module

[Arend Mellendijk]

Damiano Testa said:

I think that you should probably first normalize to get as close as possible to each individual summand being of the form constant * X ^ n and then replace the *.

To be clear, this is essentially what my prototype tactic does. Perhaps I'm duplicating work by matching the coefficients manually rather than calling module or match_scalars

[Damiano Testa]

If you can piggy-back on the existing module tactic, then your add-on only needs to take care of "expanding and merging powers", which means simpler and more robust implementation.

[Yaël Dillies]

It sounds like you want to write an algebra tactic that replaces algebraMap a * b and b * algebraMap a with a • b, algebraMap a with a • 1, then run module

[Arend Mellendijk]

I disagree - the example above is written entirely in terms of • and module fails to solve it as it doesn't handle multiplication in the algebra itself.

[Yaël Dillies]

Isn't that quite precisely what I said?

[Yaël Dillies]

My point is that your tactic shouldn't be Polynomial-specific

[Damiano Testa]

The tactic should also be aware of distributing multiplications over additions.

[Arend Mellendijk]

and normalizing terms on the RHS of an smul: match_scalars views X*X and X^2 as different things

[Damiano Testa]

If you end up outsourcing coefficient matching to match_scalars, it would be nice if you could also get match_scalars to label each goal with the name of the coefficient being matched.

[Damiano Testa]

So, the goal's list when applying it to a polynomial would tell you from which degree each side goals comes.

[Arend Mellendijk]

Thinking about ringhoms in terms of smul has carified things for me:

The reason module breaks for an R-algebra A is that it is completely oblivious to multiplication: . a • (x*y) won't match a • (y*x). To make it work we'd have to (a) distribute out all of the multiplications in A and (b) for every "product of atoms" we reorder the product into a canonical ordering (e.g. x*y*x => x^2*y).

Now I could write a tactic that first uses simp to distribute out all the products and exponents, then goes through the resulting expression, normalising all of the subterms of type A that are products of atoms. I worry that this approach is brittle. It also comes with an inherent performance penalty: (a+b)^8 gets expanded into 256 terms by simp

Another option is to essentially extend module/ring and parse the entire expression into a normal form. That would be a sum of r_i • a_i where each a_i is a normalised product of atoms. At that point there isn't much reason to call out to module - we already have the coefficients in a neat list. If we keep the r_i in ring normal form, this would also solve the exponential blowup problem mentioned before, but that would be a fair bit of work.

I'm not sure yet which way is best, but the second option seems more fruitful.