Tactic for polynomial/algebra

Stream: mathlib4

[Kenny Lau]

From my mini experiment it looks like actually the C form is better for tactics:

import Mathlib

open Polynomial

set_option trace.profiler true
set_option trace.profiler.useHeartbeats true
set_option diagnostics true
theorem foo {F : Type*} [Field F] (a b : F) :
    ((X + C a) * (X + C b) : F[X]) = X ^ 2 + C (a + b) * X + C (a * b) := by
  simp? [add_mul, mul_add, sq]
  module

theorem foo' {F : Type*} [Field F] (a b : F) :
    ((X + a • 1) * (X + b • 1) : F[X]) = X ^ 2 + (a + b) • X + (a * b) • 1 := by
  simp? [add_mul, mul_add, sq]
  module

[Kenny Lau]

the smul form even times out!

[Kenny Lau]

it should be relatively easy to interpolate from this example a macro polynomial to deal with such equalities

[Kenny Lau]

there's actually some sort of instance slowdown that i don't know where it's coming from whenever i deal with smul polynomials

[Michael Stoll]

500000 heatbeats are sufficient to make the smul version work; simp? says

Try this: simp only [mul_add, add_mul, Algebra.smul_mul_assoc, one_mul, Algebra.mul_smul_comm, mul_one,
    smul_add, sq]

[Kenny Lau]

for the smul version I currently have:

import Mathlib

open Polynomial

theorem foo' {F : Type*} [Field F] (a b : F) :
    ((X + a • 1) * (X + b • 1) : F[X]) = X ^ 2 + (a + b) • X + (a * b) • 1 := by
  simp only [add_mul, mul_add, add_smul, smul_add, smul_mul_assoc, mul_smul_comm, ← mul_smul]
  simp only [pow_succ, pow_zero]
  simp only [mul_one, one_mul]
  module

[Kenny Lau]

I guess we can still have C a * X ^ n be the simpNF, and then for the polynomial tactic it will just use one step to convert that to a • X ^ n

[Kenny Lau]

I actually have a dilemma now, because if we take C a * X ^ n as the simp NF then that means C (a + 1) * X ^ n should also be the simp NF

[Kenny Lau]

Poll: What is (X+a+1)^2?

[Kenny Lau]

actually, consider now the following:

import Mathlib

open Polynomial

theorem foo {F : Type*} [Field F] (a b : F) :
    ((X + C a) * (X + C b) : F[X]) = X ^ 2 + C (a + b) * X + C (a * b) := by
  simp only [C_add, C_mul, map_one, map_zero, map_sub, map_pow]
  ring

[Kenny Lau]

maybe we should just make this a macro

[Kenny Lau]

does anyone see a case where this would fail on?

[Kenny Lau]

yeah ok this easily fails:

import Mathlib

open Polynomial
open Real Complex

noncomputable def ω : ℂ := -0.5 + (sqrt 3 / 2) * I

theorem foo2 : (X - C ω) * (X - C (ω ^ 2)) = X ^ 2 + X + 1 := by
  simp only [C_add, C_mul, map_one, map_zero, map_sub, map_pow]
  ring_nf

[Kenny Lau]

ring basically has no idea that it should group powers of X

[Kenny Lau]

@Eric Wieser would there be enough interest if i were to try to write a polynomial tactic? I assume maybe you might already have some thoughts on this? I thought it might be better to first consult you before I dedicate time to writing this tactic.

[Eric Wieser]

I think a tactic for a configurable set of (free) generators would be more useful

[Kenny Lau]

@Eric Wieser i.e. algebra?

[Kenny Lau]

but the problem with generalising the tactic is that there is no way to generalise C as well?

[Kenny Lau]

or i guess we would just group everything that is not listed as a generator?

[Kenny Lau]

so calling algebra [x,y] on ax+by+cz+z^2+zx would give (a+z)x + by + (cz+z^2)?

[Kenny Lau]

I think I see a way to do that

[Kenny Lau]

I mean, finsupps are nice when you don't have to quotient by zero :slight_smile:

[Kenny Lau]

I think I'm gonna do the following (the algebra is A):

1. if fed in a specific ring hom (e.g. C), then normalise stuff into the form C (term) * x ^ m * y ^ n.
2. if fed in a ring R, then use algebraMap as the ring hom and go to step 1
3. if fed nothing, look at the smuls and try to infer R
4. if fed nothing and there are no smuls, then just use A itself

[Kenny Lau]

does this look like a good algorithm?

[Kenny Lau]

there will also be special support for nsmul and zsmul

[Kenny Lau]

examples in R[x,y,z]:

1. algebra C [x, y] turns (x + C r * y)^2 into x ^ 2 + C (2 * r) * (x * y) + C (r ^ 2) * y ^ 2
2. algebra R [x, y] is the above with C replaced with algebraMap R R[x, y, z]
3. algebra [x, y] turns (x + r • y)^2 into x^2 + (2*r)•(x*y) + (r^2)•(y^2)
4. algebra [x, y] turns (x + z * y)^2 into x^2 + (2*z)*(x*y) + (z^2)*(y^2)

[Kenny Lau]

cc @Michael Stoll @Eric Wieser

[Michael Stoll]

Sounds reasonable. Maybe algebra without parameters on a goal involving polynomials (in one or several variables) can default to algebra C [X] etc.?
But this is for after the basic setup works, I guess.

[Kenny Lau]

@Michael Stoll I intended to call it polynomial

[Notification Bot]

29 messages were moved here from #mathlib4 > How to write a polynomial? by Kenny Lau.

[Eric Wieser]

In the long run I'd prefer it if we could just drop C altogether

[Kenny Lau]

for 1 now i'm not so sure what the use of specifying [x, y] is... we could just assume that every atom not in the form C r is a generator right?

[Michael Rothgang]

CC @Arend Mellendijk: in the rare event you're not aware yet, I bet you're interested.

[Arend Mellendijk]

I'll note this topic: #mathlib4 > tactic for polynomial equality ; I have a working (if brittle) tactic for proving Polynomial equalities.

I've also already been working on a tactic for normalizing expressions in Algebras more generally, focussing also on recursively normalizing expressions in the base ring.

[Kenny Lau]

that discussion is 6 months old, are you still working on it?

[Arend Mellendijk]

I am, but I've been caught up with other things in the meantime.

[Kenny Lau]

is there somewhere where I can see your code?

[Arend Mellendijk]

The bulk of it is here: https://github.com/FLDutchmann/mathlib4/blob/arend/algebra/Mathlib/Tactic/Algebra.lean

It's basically an attempt to generalize ring with some inspiration from the module tactic. It's rather broken at the moment (lots of stack overflows) and I'm not quite sure how to normalize constants properly.

[Notification Bot]

71 messages were moved from this topic to #mathlib4 > Notation for polynomial variables by Eric Wieser.

[Arend Mellendijk]

I have written a suite of tactics for normalizing expressions for commutative rings (like ring), but which support algebraMap and scalar multiplication over a fixed base ring. I also used these to implemented tactics for proving equality of (Mv)Polynomials.

You can try them out yourself at #30374. The work is almost done, but I'd like some input on what people might expect to be able to do with these tactics before I get it ready for a mathlib PR. If you have any examples where polynomial equations are harder to prove than they should be or you would want ring to close a goal but it doesn't, I would love to see them.

More specifically,

• algebra proves equality of expressions in an algebra over a ring, like ring1
• algebra_nf puts expressions in an algebra into a normal form, like ring_nf

• match_scalars_alg (name pending) closes an equality goal by calling algebra_nf and creating side goals equating matching coefficients in the base ring. Like match_scalars.

• polynomial proves equality of (mv)polynomials

• polynomial_nf expands polynomials into a sum-of-monomials form, combining coefficients in the base ring (e.g. C a * X + C b * X normalizes to C(a+b) * X
• match_coefficients expands polynomials and produces side goals equating matching coefficients.

For some simple examples:

import Mathlib
open Polynomial

example {R : Type*} [CommRing R] (a : R) : (X + C a)^2 = X^2 + C (2*a) * X + C (a^2) := by
  -- ring does not close the goal
  polynomial

-- Supports natural number exponents like `ring`
example (a b : ℚ) (n : ℕ) : (X^n + C a)*(X^(2*n) + C b)= 0 := by
  polynomial_nf
  /- ⊢ C (a * b) + C b * X ^ n + C a * X ^ (n * 2) + X ^ (n * 3) = 0 -/
  sorry

example (a b c : ℚ) : (X + C a)^2 = X^2 + C c * X + C b := by
  match_coefficients
  /-
  ⊢ a ^ 2 = b
  ⊢ a * 2 = c
  -/
  all_goals sorry

example {R A : Type*} {a b : R} [CommSemiring R] [CommSemiring A] [Algebra R A] (x y : A) :
    (a + b) • (x*y + y) = y * b • x + a • (y*x + y) + b • y := by
  algebra

example {R A : Type*} {a b : R} [CommSemiring R] [CommSemiring A] [Algebra R A] (x y : A) :
    ((a + b) • (x + y))^2 = 0 := by
  algebra_nf
  /-
  ⊢ (a * b * 4 + a ^ 2 * 2 + b ^ 2 * 2) • (x * y) + (a * b * 2 + a ^ 2 + b ^ 2) • x ^ 2 +
    (a * b * 2 + a ^ 2 + b ^ 2) • y ^ 2 = 0
  -/
  sorry

For the algebra tactics you can also explicitly specify the base ring as algebra with R if the automatic inference doesn't work as expected.

[Kenny Lau]

@Arend Mellendijk Thanks! Since you said you're looking for examples, could you please try the following:

import Mathlib

set_option autoImplicit false

open Polynomial Complex Real

example : (X^2 + X + 1 : ℂ[X]) = (X - C ((-1 + sqrt 3 • I)/2)) * (X - C ((-1 - sqrt 3 • I)/2)) := by
  ring

[Arend Mellendijk]

Here's where it gets you:

example : (X^2 + X + 1 : ℂ[X]) = (X - C ((-1 + sqrt 3 • I)/2)) * (X - C ((-1 - sqrt 3 • I)/2)) := by
  match_coefficients
  /- 1 = 1 / 4 + (√3 • I) ^ 2 * (-1 / 4) -/
  sorry

[Kenny Lau]

nice!

[Kenny Lau]

I'm a bit confused why there are 5 names for what seems like the same tactic

[Arend Mellendijk]

The same reason ring, ring_nf and match_scalars are separate tactics, surely? And I separated out polynomial because it needs separate pre/post processing to put it into forms involving Polynomial.C, and because it's easier and less error prone to find the base ring. I know some people want to get away from Polynomial.C, but I think that's a discussion for another thread.

[Kenny Lau]

I wonder if we can e.g. make algebra more configurable on usage, so that e.g. polynomial can be just a macro for algebra [Polynomial.X] Polynomial.C

[Arend Mellendijk]

I'm not sure that's worth the effort without a concrete application. The polynomial tactics are only like 100 lines of code combined. Also polynomial actually doesn't treat Polynomial.X specially in any way - it's just another variable:

example (a : ℚ) (P : Polynomial ℚ) : (X - P * C a)*(X + P * C a) = X^2 - P ^ 2 * C (a^2) := by
  polynomial

[Kenny Lau]

Arend Mellendijk said:

a concrete application

I thought the goal is to treat algebraMap etc as a special map from the base ring to the algebra

[Kenny Lau]

so it would be useful to specify what algebraMap is in the case that it does not syntactically appear as algebraMap

[Arend Mellendijk]

Do you have any examples other than Polynomial and MvPolynomial? This probably wouldn't be too hard to implement, but the tactic would need some way of knowing that C x = algebraMap x.

[Kenny Lau]

power series

[Arend Mellendijk]

I also do a bit of processing for docs#Polynomial.map, but I don't know how much that will come up in practise.

[Kenny Lau]

Arend Mellendijk said:

the tactic would need some way of knowing that C x = algebraMap x.

I think we should assume that rfl would solve this

[Arend Mellendijk]

I'm a bit worried that there are too many edge cases here - polynomialsupports both Polynomial and MvPolynomial so it can't be as simple as algebra Polynomial.C, and by generalizing too much we lose the ability to do more processing specific to polynomials. Also Polynomial.C and MvPolynomial.C don't actually take the same arguments (there's an index type in there), so you'd have to very careful handling everything.

And for power series specifically, it would actually be very easy to make polynomial support them.

[Kenny Lau]

Arend Mellendijk said:

And for power series specifically, it would actually be very easy to make polynomial support them.

I'm concerned that this case-by-case approach would be a bit difficult to maintain, is there a way to make it more "extensible"? e.g. afaik norm_num can be extended to cover C without rewriting the whole tactic

[Kenny Lau]

Arend Mellendijk said:

Polynomial.C and MvPolynomial.C don't actually take the same arguments

I think they can be both elaborated to an expr with type R →+* A where R is the base ring and A is the algebra

[Arend Mellendijk]

Maybe just an extensible simp set? You tag some lemmas saying C = algebraMap and the tactic figures the rest out?

[Kenny Lau]

that's probably one approach

[Arend Mellendijk]

Kenny Lau said:

I think they can be both elaborated to an expr with type R →+* A where R is the base ring and A is the algebra

I think I can see how you'd do this now but there are some subtle issues. You wouldn't yet know the base ring because algebra attempts to infer it from any smuls and algebraMaps in the expression, so you'd have to find any occurrences of C and consider them as well. Annoying but doable. I'll add this to the TODOs list.

[Kenny Lau]

thanks!

[Johan Commelin]

@Arend Mellendijk Great work! Do you think algebra would eventually subsume ring?

[Arend Mellendijk]

Probably not, because (a) it uses the ring normal form internally for expressions in the base ring and (b) it's an extra layer of indirection on top of ring which would reduce performance. I haven't tested the performance claim in practise.

That said, in theory it should be able to do anything ring does. It's missing one or two features at the moment but I can see how you would implement them.

[Jovan Gerbscheid]

This is probably not in scope of your tactics, but how does your work relate to a potential tactic that supports rings where some specific elements are a root of a polynomial? This would subsume #26975. But the example above which faces the goal 1 = 1 / 4 + (√3 • I) ^ 2 * (-1 / 4), would also be finishsed by such a tactic, since both √3 and I are square roots.

[Arend Mellendijk]

Well expressions in the base ring are put into ring normal form, so if ring is somehow updated to work modulo some polynomial relations, I would guess algebraimmediately closes 1 = 1 / 4 + (√3 • I) ^ 2 * (-1 / 4).

The implementation of algebra is pretty similar to ring so to get polynomial relations to work in the algebra rather than the base ring you would have to duplicate some work, but it sounds doable to implement.

[Arend Mellendijk]

That said this is not something I put any thought into while writing the tactic.

[Artie Khovanov]

Why do we even use things like Polynomial.C instead of just using algebraMap? If we refactor usage away, we don't need a custom simpset.

[Andrew Yang]

One argument is that algebraMap doesn't work for non-commutative rings.

[Artie Khovanov]

To spell out the downside, every time you do something like this, you have to duplicate the algebraMap API if you want to do computation

[Kenny Lau]

@Artie Khovanov i did address this recently, in this proposal

[Johan Commelin]

Discussion/review seems to have stalled here. But I think this is a useful tactic!
Could some meta reviewers take this on please?

[Jovan Gerbscheid]

I made the suggestion that it may be better to keep constant factors/offsets (number literals) in the main ring instead of in the base ring. E.g if the main ring has characteristic 2 but the base ring has characteristic 0, we would like to be able to cancel out any twos. And it is always possible to lift constants from the base ring to the main ring, but not always veice versa (e.g. any ring can be given the base ring ℕ). However this would require refactoring the NurmNum IsRat machinery to use weaker type class assumptions.

[Johan Commelin]

So can that be a v2 of this tactic, and we first get the current one?