# mathlibdocumentation

tactic.compute_degree

# compute_degree_le a tactic for computing degrees of polynomials #

This file defines the tactic compute_degree_le.

Using compute_degree_le when the goal is of the form f.nat_degree ≤ d, tries to solve the goal. It may leave side-goals, in case it is not entirely successful.

See the doc-string for more details.

## Future work #

• Deal with goals of the form f.(nat_)degree = d (PR #14040 does exactly this).
• Add better functionality to deal with exponents that are not necessarily closed natural numbers.
• Add support for proving goals of the from f.(nat_)degree ≠ 0.
• Make sure that degree and nat_degree are equally supported.

## Implementation details #

We start with a goal of the form f.(nat_)degree ≤ d. Recurse into f breaking apart sums, products and powers. Take care of numerals, C a, X (^ n), monomial a n separately.

guess_degree e assumes that e is an expression in a polynomial ring, and makes an attempt at guessing the nat_degree of e. Heuristics for guess_degree:

• 0, 1, C a, guess 0,
• polynomial.X, guess 1,
• bit0/1 f, -f, guess guess_degree f,
• f + g, f - g, guess max (guess_degree f) (guess_degree g),
• f * g, guess guess_degree f + guess_degree g,
• f ^ n, guess guess_degree f * n,
• monomial n r, guess n,
• f not as above, guess f.nat_degree.

The guessed degree should coincide with the behaviour of resolve_sum_step: resolve_sum_step cannot solve a goal f.nat_degree ≤ d if guess_degree f < d.

resolve_sum_step assumes that the current goal is of the form f.nat_degree ≤ d, failing otherwise. It tries to make progress on the goal by progressing into f if f is

• a sum, difference, opposite, product, or a power;
• a monomial;
• C a;
• 0, 1 or bit0 a, bit1 a (to deal with numerals).

The side-goals produced by resolve_sum_step are either again of the same shape f'.nat_degree ≤ d or of the form m ≤ n, where m n : ℕ.

If d is less than guess_degree f, this tactic will create unsolvable goals.

norm_assum simply tries norm_num and assumption. It is used to try to discharge as many as possible of the side-goals of compute_degree_le. Several side-goals are of the form m ≤ n, for natural numbers m, n or of the form c ≠ 0, with c a coefficient of the polynomial f in question.

eval_guessing n e takes a natural number n and an expression e and gives an estimate for the evaluation of eval_expr' ℕ e. It is tailor made for estimating degrees of polynomials.

It decomposes e recursively as a sequence of additions, multiplications and max. On the atoms of the process, eval_guessing tries to use eval_expr' ℕ, resorting to using n if eval_expr' ℕ fails.

For use with degree of polynomials, we mostly use n = 0.

A general description of compute_degree_le_aux is in the doc-string of compute_degree. The difference between the two is that compute_degree_le_aux makes no effort to close side-goals, nor fails if the goal does not change.

compute_degree_le tries to solve a goal of the form f.nat_degree ≤ d or f.degree ≤ d, where f : R[X] and d : ℕ or d : with_bot ℕ.

If the given degree d is smaller than the one that the tactic computes, then the tactic suggests the degree that it computed.

Examples:

open polynomial
open_locale polynomial

variables {R : Type*} [semiring R] {a b c d e : R}

example {F} [ring F] {a : F} {n : ℕ} (h : n ≤ 10) :
nat_degree (X ^ n + C a * X ^ 10 : F[X]) ≤ 10 :=
by compute_degree_le

example : nat_degree (7 * X : R[X]) ≤ 1 :=
by compute_degree_le

example {p : R[X]} {n : ℕ} {p0 : p.nat_degree = 0} :
(p ^ n).nat_degree ≤ 0 :=
by compute_degree_le



compute_degree_le tries to solve a goal of the form f.nat_degree ≤ d or f.degree ≤ d, where f : R[X] and d : ℕ or d : with_bot ℕ.

If the given degree d is smaller than the one that the tactic computes, then the tactic suggests the degree that it computed.

Examples:

open polynomial
open_locale polynomial

variables {R : Type*} [semiring R] {a b c d e : R}

example {F} [ring F] {a : F} {n : ℕ} (h : n ≤ 10) :
nat_degree (X ^ n + C a * X ^ 10 : F[X]) ≤ 10 :=
by compute_degree_le

example : nat_degree (7 * X : R[X]) ≤ 1 :=
by compute_degree_le

example {p : R[X]} {n : ℕ} {p0 : p.nat_degree = 0} :
(p ^ n).nat_degree ≤ 0 :=
by compute_degree_le