mathlib documentation

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 #

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.

source
meta def tactic.compute_degree.guess_degree  :
expr → tactic expr

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.

source
meta def tactic.compute_degree.resolve_sum_step  :
expr → tactic unit

resolve_sum_step e takes the type of the current goal e as input. It tries to make progress on the goal e by reducing it to subgoals. It assumes that e is of the form f.nat_degree ≤ d, failing otherwise.

resolve_sum_step progresses 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.

source
meta def tactic.compute_degree.norm_assum  :
tactic unit

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.

source
meta def tactic.compute_degree.eval_guessing (n : ℕ) :
expr → tactic ℕ

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.

source
meta def tactic.interactive.compute_degree_le  :
tactic unit

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
```
source
def tactic_doc.tactic.compute_degree_le  :
tactic_doc_entry

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
```