compute_total_degree

Stream: general

[Bolton Bailey]

I saw #6221 on the queue and I thought it might be useful to have something similar for my project (which currently lives in #5297) to compute total degrees of MvPolynomials. @Damiano Testa does this PR work for MvPolynomials/do you think it would be easy for me to basically replicate declaration-by-declaration for MvPolynomials?

[Damiano Testa]

The PR certainly does not work out of the box for MvPolynomials. It would certainly be possible to adapt it, but I do not know how easy it would be.

[Damiano Testa]

If/when the current PR gets merged, I will take a look at MvPolynomials, but Polynomials seem like the natural initial testing ground!

[Bolton Bailey]

Is this tactic usable to introduce new hypotheses? Can I write something like ccompute_degree (X^2 + X + 1) as hd and have hd : degree (X^2 + X + 1) = 2 appear in my hypotheses?

[Damiano Testa]

At the moment, no, but you can write

  have hd : degree (X ^ 2 + X + 1) = 2 := by compute_degree

and it will try to compute the degree. It should be easy to add this functionality, but I did not want to make the PR longer to simplify the review process.

[Damiano Testa]

Note that, internally, the tactic does not use the value that you give for the expected degree and computes its own guess, so the = 2 in the example is really superfluous information.

[Damiano Testa]

However, in its current form, the tactic requires that something be present (and it should tell you that it expected to see a 2, if you give it a different number.

[Bolton Bailey]

Right ok. My goal is a tactic that takes an equality p = q of MvPolynomials and then applies the Schwartz-Zippel lemma to "prove" the equality by generating a probabilistic test of the fact that p-q = 0. The S-Z lemma depends on having an upper bound on the total degree, so it seems like at some point I will want to be able to produce a proof of an upper bound without necessarily having the degree to start with (in fact, the point is that p-q has degree 0 but that we don't know this at the start, only that we have a particular bound on the degree).

[Bolton Bailey]

Thinking about it more, I guess one approach is just to hard-code a large number like 10^24 as the degree bound, and this would work pretty consistently for the use cases I imagine, but would not actually require knowing the degree. But if I wanted to use the test for very high-degree polynomials, it could eat into the soundness of the test, so I might want to just run code to tell me a degree bound at that point.

[Bolton Bailey]

I guess the point is that computing totalDegree = x would seem to be disanalogous to the single-variable polynomial setting, but I don't need to do that. I just need to be able to prove goals of the form totalDegree <= 10^24, and this seems like it could work exactly the same way it does in the single variable setting (this I take it is by recursively bounding the degree of subexpressions).

[Damiano Testa]

Proving upper bounds on the degree is much simpler than computing the degree. The tactic could be significantly shorter if that is all you wanted.

Making it work for total_degree should not be hard, but would also require a substantial amount of changes, since currently all the matching and lemmas are about Polynomials.

[Damiano Testa]

Are the polynomials that you produce "actual" polynomials, in the same sense that 3 is a natural number, or are they polynomials in the sense that n is a natural number?

[Bolton Bailey]

My goal is to be able to "prove" the things that ring does, but asymptotically faster. I want to convert ring expressions into polynomials over their atoms and prove them equivalent as polynomials.

[Damiano Testa]

If they are "black box" polynomials, the current tactic will not really be very useful. compute_degree expects something like natDegree (C 4 * X ^ 8 + 5) = 7, with atomic building blocks such as X, C _, monomial _ _ and then "algebraic operations" combining them.

It attempts to do something meaningful with expressions such as f : R[X], but it won't use anything from context to make even the most trivial estimate as to what the degree of f could be.

[Damiano Testa]

Do you have a sample of what kinds of expressions you would like to pass to the tactic?

[Bolton Bailey]

What I would like to do is something like the following:

1. I start with an expression like \forall (a b : R), (a + b)^2 = a^2 + 2 * a * b + b^2

2. I transform the atoms into evaluations of MvPolynomials (is this what the Qq library is for?) something like
   let f (quoted_z : TypeOfExpressions) : R := <quoted_a maps to a, quoted_b maps to b and so forth>
   Now the goal is equivalent to
   (eval f (X quoted_a) + eval f (X quoted_b))^2 = (eval f (X quoted_a) )^2 + 2 * (eval f (X quoted_a) ) * (eval f (X quoted_b)) + (eval f (X quoted_b))^2
   Which simplifies to
   eval f (X quoted_a + X quoted_b)^2 = eval f (X quoted_a)^2 + C 2 * X quoted_a * X quoted_b + (X quoted_b)^2

3. Apply congr to reduce to

(X quoted_a + X quoted_b)^2 = (X quoted_a)^2 + C 2 * X quoted_a * X quoted_b + (X quoted_b)^2

4. Bound the degree of these polynomials (which are over the type of quoted expressions) and prove them equal.

[Bolton Bailey]

So I think all I need really is X and C, I don't need monomial.

[Damiano Testa]

I had some Lean 3 code for converting (some) atoms in an algebraic expression in independent variables of a polynomial. It would have to be rewritten, but my recollection is that it was fairly easy to write an implementation that works most of the time, but tricky to do it robustly.

[Damiano Testa]

With respect to the computation of the degree of multi-variable polynomials, I am fairly confident that this is easier to automate robustly. The compute_degree tactic got a make-over (thanks Kyle!) and hopefully will be merged soon. Once that one is in, I will take a look into extending it to also work for multivariable polynomials.

[Damiano Testa]

On the topic of getting the tactic to take an optional polynomial as an argument and having compute_degree h : pol leave h : degree pol = ... in context, this should not be hard. There is the small question of passing the information of whether you want the natDegree or the degree, whether you want to name or not the resulting hypothesis, but technically everything should be there.

[Damiano Testa]

What I think would make the extension easier to use is to allow underscores in the term pol and let the tactic guess that you want to compute the degree of the first subexpression of something in context that unifies with what you gave it. Here is an example.

[Damiano Testa]

In context, there is hm : Monic (X ^ 3 + (2 * X ^ 2 + 5)). Writing

• compute_degree _ adds the hypothesis degree (X ^ 3 + (2 * X ^ 2 + 5)) = 3 to the context;
• compute_degree 2 * _ + _ adds the hypothesis degree (2 * X ^ 2 + 5) = 2 to the context.

This should also be relatively straightforward. Still, I would wait for this until the current version of the tactic is merged!

[Damiano Testa]

In fact, regardless of the underscores, maybe this extension could be called have_degree/have_natDegree, rather that compute_degree.

[Damiano Testa]

compute_degree got merged! Thank you, Kyle!

If you have a goal of the form natDegree (reasonably explicit polynomial) = n (or variations with degree or ≤, then chances are that compute_degree will make progress on it! And compute_degree! will try harder.

If you use it and you have questions, bug reports, suggestions, do let me know!

[Eric Rodriguez]

Hi Damiano, been loving compute_degree! Is it an easy modification for it to support stuff like (A : R) \smul X ^ n : R[X]? I see it has support for monomial, and likely I should be writing things in that sort of form...

[Damiano Testa]

Eric, I am very happy that you enjoy compute_degree!

I think that adding support for \smul should be relatively straightforward, since the lemmas docs#Polynomial.natDegree_smul_le and docs#Polynomial.degree_smul_le are already in place.

The lemma docs#Polynomial.natDegree_smul_ite seems to be missing, so the whole PR is probably a couple of extra lines of tactic code, the extra lemma and a couple of tests.

If you can supply a "real-world" test for the tactic, I can take care of the rest of the PR! :wink:

[Damiano Testa]

#8666 waiting for a good test!

[Michael Stoll]

Can compute_degree perhaps be taught to also deal with goals of the form Monic f?

[Damiano Testa]

Michael, it certainly can, and it is probably also quite a simple extension. I wonder if maybe the name of the tactic should change, though.

[Damiano Testa]

The tactic essentially breaks up the degree computation in two parts:

• the easy part is showing an inequality and this normally is always successful;
• the hard part is showing that the coefficient of top degree is non-zero and this is where the tactic typically can get stuck.

Also, when faced with a goal degree f = n, the tactic does not actually use the information that n is given, but replaces straight away the actual degree with a metavariable. This means that it is able to get its own estimate of the degree and to compare it with the given one. So, when trying to prove monicity, you would still begin with a metavariable for the degree and close the final goal with rfl to get the actual degree.

To prove monic, you then have a goal of coeff ... = 1 instead of coeff ... ≠ 0: such goals probably get stuck in similar ways! So, I expect a similar performance of Monic f and degree f = n.

[Damiano Testa]

This addition is slightly lengthier than the support for smul, but probably still quite short.

[Damiano Testa]

@Michael Stoll, do you have some use-case for the monic extension? It might be that this simple-minded macro already goes a long way to proving monicity.

open Polynomial

macro "monicity" : tactic =>
  `(tactic| (apply monic_of_natDegree_le_of_coeff_eq_one <;> compute_degree))

macro "monicity!" : tactic =>
  `(tactic| (apply monic_of_natDegree_le_of_coeff_eq_one <;> compute_degree!))

example {R} [Semiring R] [Nontrivial R] : Monic (1 * X ^ 5 + X ^ 6 * monomial 10 1 : R[X]) := by
  monicity!

[Michael Stoll]

In the context of my seminar, one project is to formalize Eisenstein integers, and one possibility would start somewhat like the following.

import Mathlib

open BigOperators Polynomial

noncomputable
abbrev minpol := (X^2 + X + 1 : ℤ[X])

abbrev EisensteinInt := AdjoinRoot minpol

namespace EisensteinInt

open AdjoinRoot

lemma deg_minpol_eq_two : natDegree minpol = 2 := by
  simp only [minpol]
  compute_degree!

lemma monic_minpol : Monic minpol := by
  simp only [minpol, Monic, leadingCoeff, deg_minpol_eq_two]
  compute_degree

This is where the question came up.

[Eric Rodriguez]

Damiano Testa said:

Michael Stoll, do you have some use-case for the monic extension? It might be that this simple-minded macro already goes a long way to proving monicity.

macro "monicity" : tactic =>
  `(tactic| (apply monic_of_natDegree_le_of_coeff_eq_one <;> compute_degree))

macro "monicity!" : tactic =>
  `(tactic| (apply monic_of_natDegree_le_of_coeff_eq_one <;> compute_degree!))

example {R} [Semiring R] [Nontrivial R] : Monic (1 * X ^ 5 + X ^ 6 * monomial 10 1 : R[X]) := by
  monicity!

may be worth PRing this straight away!

I also got reminded by Michael's proofs that leadingCoeff is another good target. If you're looking for a new name, maybe norm_poly to match norm_num in some way?

[Damiano Testa]

#8668 adds monicity.

[Damiano Testa]

As for the name, I remember that maybe it was suggested that compute_degree might be a norm_num extension. Maybe this is even more the case for all of these auxiliary tactics/macros that are based on it.

[Damiano Testa]

By the way, while I think that the extension to support smul is probably quite robust (at least, as robust as the rest of compute_degree), I feel a little less confident about the monicity macro.

[Damiano Testa]

@Michael Stoll, with the two macros above, this also works

lemma monic_minpol : Monic minpol := by
  unfold minpol
  monicity