Computing nat_degrees of polynomials

Stream: Is there code for X?

[Damiano Testa]

Dear All,

once/if move_add gets merged into mathlib, it will be simpler to implement a tactic that will compute nat_degrees of relatively "explicit" polynomials. In its simplest form, given a sum of terms of the form C a * X ^ n, where

• a is in a semiring,
• n is a closed term of type nat,
• the term of highest degree is unique,
• there is floating around an assumption that says that the coefficient of the term of highest degree is non-zero,

the tactic would be able to compute the nat_degree of such an expression. Of course, each of the various items above can be given more attention and the scope of the tactic could increase.

My question is: would such a tactic be desired? Patrick said that it would be good as a norm_num extension, for instance.

Before I start making progress on this, I would like to know whether this would be useful or not!

Thanks!

[Damiano Testa]

The suggestion where this arose.

[Alex J. Best]

I definitely think it would be useful, these sort of goals are very annoying. Ideally it would also be able to handle degree leading_term and monic goals appropriately

[Damiano Testa]

Dear All,

I've playing around with a tactic to compute nat_degrees of polynomials. Currently, it is quite gullible and not tested very much, but below is what I have. It is based on move_add (branch#aa_sort).

When it should work for now.
If the goal is nat_degree (expression) = n, compute_degree should close the goal if:

• the leading term of expression is X ^ n,
• all remaining terms are of the form C a * X ^ a or monomial a r (and have degree smaller than n).

Repetitions in degrees of non-highest terms is allowed.

It is easy to implement improvements, and I am planning to do that. If you have any comment, though, I would be very happy to hear them!

import tactic.move_add
import data.polynomial.degree.lemmas
open polynomial
open_locale polynomial

variables {R : Type*} [semiring R] [nontrivial R] {f g h : R[X]} {a b c d e : R}

section silly_poly_lemmas

lemma polynomial.nat_degree_monomial_le {R : Type*} [semiring R] (a : R) (n : ℕ) :
  (polynomial.monomial n a).nat_degree ≤ n :=
begin
  classical,
  rw polynomial.nat_degree_monomial,
  split_ifs; simp,
end
lemma polynomial.nat_degree_C_mul_X_le {R : Type*} [semiring R] (a : R) :
  ((C a : polynomial R) * (X : polynomial R)).nat_degree ≤ 1 :=
(nat_degree_C_mul_le _ _).trans nat_degree_X_le

end silly_poly_lemmas

open tactic interactive expr

namespace tactic.interactive
setup_tactic_parser

meta def guess_deg (e : expr) : tactic expr :=
do
  let n0 := to_expr ``(nat.zero),
  let n1 := to_expr ``(nat.zero.succ),
  pX ← to_expr ``(polynomial.X),
  match e.app_fn with
  | `(coe_fn $ polynomial.monomial %%n) := return n
  | `(coe_fn $ polynomial.C) := n0
  | a := do
          bo ← succeeds $ unify e pX,
          if bo then n1 else
            ( do let margs := e.get_app_args,
              margs.nth 4 >>= return ) <|>
            ( do val ← to_expr ``(polynomial.nat_degree),
              return $ expr.mk_app val [e] )
          end

meta def get_factors_add : expr → tactic expr
| `(has_mul.mul %%a %%b) := do
                              ga ← get_factors_add a,
                              gb ← get_factors_add b,
                              mk_app `has_add.add [ga, gb] >>= return
| e := guess_deg e >>= return


meta def compute_degree : tactic unit :=
do `(polynomial.nat_degree %%tl = %%tr) ← target,
  let n0 := to_expr ``(nat.zero),
  let summ := (get_summands tl),
  rere ← summ.mmap get_factors_add,
  mario ← rere.mmap (eval_expr ℕ),
  let m := mario.maximum,
  let m' := m.get_or_else 0,
  let szd := summ.zip mario,
  let fil : list pexpr := ((szd.filter (λ e : expr × ℕ, e.2 = m')).map (λ e, pexpr.of_expr e.1)),
  let ffil : list (bool × pexpr) := ([ff].zip fil),
  move_add_with_errors ffil none,
  `[rw [polynomial.nat_degree_add_eq_right_of_nat_degree_lt, polynomial.nat_degree_X_pow],
    rw [polynomial.nat_degree_X_pow],
    refine nat.lt_succ_of_le _,
    repeat { refine (polynomial.nat_degree_add_le _ _).trans _,
             refine max_le _ _ },
    repeat { rw ← polynomial.monomial_eq_C_mul_X },
    repeat { rw polynomial.monomial_mul_monomial },
    repeat { refine (polynomial.nat_degree_monomial_le _ _).trans _ },
    repeat { refine (polynomial.nat_degree_C_mul_le _ _).trans _ },
    repeat { norm_num },  -- norm_num could be used earlier, but is *slightly* slower
    repeat { assumption } -- these assumptions are
                          -- the type of the semiring and
                          -- the instance that it is a semiring.
                          -- They appear to arise from `pX` in `guess_deg`,
                          -- which has no way of figuring out what `R` is.
     ]

end tactic.interactive

example {h : C d ≠ 0} (f10 : f.nat_degree ≤ 10) :
  nat_degree (monomial 5 c * monomial 1 c + monomial 7 d + monomial 9 1 +
    C a * X ^ 0 + C b * X ^ 5 + C c * X ^ 2 + X ^ 10 + C e * X) = 10 :=
begin
  compute_degree,
end

[Damiano Testa]

A first easy addition will be to extract the coefficient from the leading term and scan the context to look for an assumption saying that it is non-zero. This will make the tactic work for non-monic polynomials, provided there is in context a proof of the fact that the leading coefficient is non-zero.

[Damiano Testa]

Alex, I like your suggestions, I will work on them. I'm just starting from this part!

[Damiano Testa]

@Alex J. Best , since you had expressed interest in such automation, I now have a concrete proposal! PR #14040 defines two tactics:

• compute_degree_le, whose aim is to close goals of the form f.nat_degree ≤ d,
• compute_degree, whose aim is to close goals of the form f.nat_degree = d.

In both cases, the exponents should be closed expressions of type nat. Also, there is the requirement that a unique term of highest degree appears and that this term is of the form X ^ n, X or, assuming also that a ≠ 0 is in context, C a * X ^ n, C a * X.

It should be easy to generalize these assumptions, allowing for more interesting polynomials, but I would rather leave this for some other PR!

[Eric Rodriguez]

Why isn't this being merged into the direct norm_num architecture?

[Damiano Testa]

I feel that norm_num is very polished and sophisticated, while this is somewhat crude and rough. Maybe, after some iterations of the review process, it might go into norm_num. Note that this is the second tactic that I write...

[Damiano Testa]

Also, right now it is somewhat buggy and fails in some situations where I would like it to actually work out-of-the-box.

[Damiano Testa]

For instance, to get the functionality with the C a * X ^ ?? fully working, I would have to figure out how to get nontriviality to kick in, once there is an assumption of the form a ≠ 0. This is a meta-problem, not really a maths one!

[Eric Wieser]

Conceivably you could just use assumption to prove that a ≠ 0

[Eric Wieser]

Or require it be used as norm_num [h], which I think is already possible syntax

[Damiano Testa]

Yes, assumption is ok. At some point in the process, though, after it used the assumption, it seems to still be looking for a non-triviality assumption. It might be a non-triviality assumption in some lemma that could likely be replaced or weakened, but I have not yet debugged it.

[Eric Wieser]

Well, if R is trivial then docs#polynomial.unique says everything is of nat_degree 0

[Eric Wieser]

But I guess your point is that you have nontrivial in your assumptions and the meta code isn't finding it?

[Damiano Testa]

Well, nontrivial is a consequence of a ≠ 0 but is not automatically an instance, so some lemmas used, I think, fail in some applications. I will debug it: it should be easy and I also think that I probably want to handle the lead term separately anyway.

[Michael Stoll]

Damiano Testa said:

Alex J. Best , since you had expressed interest in such automation, I now have a concrete proposal! PR #14040 defines two tactics:

• compute_degree_le, whose aim is to close goals of the form f.nat_degree ≤ d,
• compute_degree, whose aim is to close goals of the form f.nat_degree = d.

It would make sense to add degree_ne_zero or similar, since this is a common condition in the context of proving existence of roots of polynomials in alg. closed fields, or more generally when need non-units in the polynomial ring.

[Damiano Testa]

Getting the degree_ne_zero part should be easy: thanks for the suggestion!

[Damiano Testa]

(Note that for the moment this is only for nat_degree, but adapting to degree should also be straightforward.)

[Damiano Testa]

Ok, I think that the issue is that docs#polynomial.nat_degree_X_pow proves the exact degree, not the inequality and for this uses the nontrivial assumption. There seems to not be docs#polynomial.nat_degree_X_pow_le [lemma not existing] (and possibly a few other edge cases), which prove the inequality with no extra typeclass assumptions. I think that with this, the tactic will work better.

Still, I will chop off the computation of the degree of the highest term, since it will make for easier and more streamlined logic/code.

[Damiano Testa]

I have streamlined the code a bit and, thanks for several very helpful answers in the metaprogramming stream, I was able to get the nontriviality assumptions to kick in! Right now, PR #14040 has a fairly stable compute_degree and compute_degree_le tactics that close goals of the form f.nat_degree = d and f.nat_degree ≤ d, where f is an "explicit" polynomial.

The PR looks large, but the only relevant file is under 300 lines long and several of these lines are extended comments and doc-strings and doc-module.

[Damiano Testa]

The strategy is to isolate a term of "highest degree" and proceed from there. This means that getting the tactic to also close monic and leading_coeffs goals should be relatively straightforward. However, since this PR also depends on the previous move_add PR, I will wait to implement these further features.

[Damiano Testa]

Moreover, I am conscious of the "imminent" switch to Lean4 and have started seeing how to implement move_add in Lean4.

[Eric Wieser]

Do these work for .degree too? If not, perhaps the lemma should be called compute_nat_degree!

[Damiano Testa]

Making them work for degree is a todo, actually a very easy one! I have a preference for maintaining the name short.

[Damiano Testa]

If you want, I will get them to work with degree as well: since the interesting case is when you are trying to compute the degree of a polynomial of non-zero nat_degree, I can simply convert degree to nat_degree and leave the tactic unchanged otherwise. If it fails, it means that you were trying to use the tactic to prove that the degree of a constant polynomial was zero.

[Eric Wieser]

Does it make sense to make this a norm_num plugin?

[Damiano Testa]

This was Patrick's suggestion as well. I am happy to make it a plug-in, but I do not really know what it entails (or how to do it).

[Eric Wieser]

Does looking at src#tactic.norm_fin.eval_ineq help at all?

[Eric Wieser]

In fact, src#tactic.norm_num.eval_gcd is probably a better template

[Eric Wieser]

You just have to return the pair (degree_it_evaluates_to, proof_its_that_degree)

[Damiano Testa]

Ok, degree_it_evaluates_to I have and is easy.

Should I extract the proof term from the tactic or should I provide the tactic that produces the proof?

[Damiano Testa]

(I am looking at the template, but I am still processing it!)

[Damiano Testa]

For the moment, I am simply skipping the mk_instance_cache, right?

[Damiano Testa]

I have not yet figured out the norm_num thing, but have added support for degree. As you can imagine it has not been tested much, but works in some examples!

[Damiano Testa]

So far, the support for degree is limited computing exact degree (no ≤ allowed) and discards the case in which the degree is ⊥.

[Damiano Testa]

Dear All,

I split off #14762 from the main PR #14040 to compute degrees of polynomials. This contains the easier step of proving that the degree of a polynomial is at most something.

For instance

example {R : Type*} [semiring R] {n : ℕ} (a : R) (h : 1 + n ≤ 10) :
  degree (5 * X ^ 5 + (X * monomial n 1 + X * X) + C a + C a * X ^ 10) ≤ 10 :=
by compute_degree_le

works.