compute_degree and monicity: tactics for explicit polynomials

This file defines two related tactics: compute_degree and monicity.

Using compute_degree when the goal is of one of the seven forms

• natDegree f ≤ d (or <),
• degree f ≤ d (or <),
• natDegree f = d,
• degree f = d,
• coeff f d = r, if d is the degree of f, tries to solve the goal. It may leave side-goals, in case it is not entirely successful.

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

Both tactics admit a ! modifier (compute_degree! and monicity!) instructing Lean to try harder to close the goal.

See the doc-strings for more details.

Future work

• Currently, compute_degree does not deal correctly with some edge cases. For instance,

  example [Semiring R] : natDegree (C 0 : R[X]) = 0 := by
    compute_degree
  --  ⊢ 0 ≠ 0
  

  Still, it may not be worth to provide special support for natDegree f = 0.
• Make sure that numerals in coefficients are treated correctly.
• Make sure that compute_degree works with goals of the form degree f ≤ ↑d, with an explicit coercion from ℕ on the RHS.
• Add support for proving goals of the from natDegree f ≠ 0 and degree f ≠ 0.
• Make sure that degree, natDegree and coeff are equally supported.

Implementation details

Assume that f : R[X] is a polynomial with coefficients in a semiring R and d is either in ℕ or in WithBot ℕ.

If the goal has the form natDegree f < d, then we convert it to two separate goals:

• natDegree f ≤ ?_, on which we apply the following steps;
• ?_ < d; where ?_ is a metavariable that compute_degree computes in its process. We proceed similarly for degree f < d.

If the goal has the form natDegree f = d, then we convert it to three separate goals:

• natDegree f ≤ d;
• coeff f d = r;
• r ≠ 0.

Similarly, an initial goal of the form degree f = d gives rise to goals of the form

• degree f ≤ d;
• coeff f d = r;
• r ≠ 0.

Next, we apply successively lemmas whose side-goals all have the shape

• natDegree f ≤ d;
• degree f ≤ d;
• coeff f d = r;

plus possibly "numerical" identities and choices of elements in ℕ, WithBot ℕ, and R.

Recursing into f, we break apart additions, multiplications, powers, subtractions,... The leaves of the process are

• numerals, C a, X and monomial a n, to which we assign degree 0, 1 and a respectively;
• fvars f, to which we tautologically assign degree natDegree f.

Simple lemmas about natDegree

The lemmas in this section all have the form natDegree <some form of cast> ≤ 0. Their proofs are weakenings of the stronger lemmas natDegree <same> = 0. These are the lemmas called by compute_degree on (almost) all the leaves of its recursion.

theorem Mathlib.Tactic.ComputeDegree.natDegree_C_le {R : Type u_1} [Semiring R] (a : R) : (Polynomial.C a).natDegree ≤ 0

theorem Mathlib.Tactic.ComputeDegree.natDegree_natCast_le {R : Type u_1} [Semiring R] (n : ℕ) : (↑n).natDegree ≤ 0

theorem Mathlib.Tactic.ComputeDegree.natDegree_zero_le {R : Type u_1} [Semiring R] : Polynomial.natDegree 0 ≤ 0

theorem Mathlib.Tactic.ComputeDegree.natDegree_one_le {R : Type u_1} [Semiring R] : Polynomial.natDegree 1 ≤ 0

theorem Mathlib.Tactic.ComputeDegree.coeff_add_of_eq {R : Type u_1} [Semiring R] {n : ℕ} {a b : R} {f g : Polynomial R} (h_add_left : f.coeff n = a) (h_add_right : g.coeff n = b) : (f + g).coeff n = a + b

theorem Mathlib.Tactic.ComputeDegree.coeff_mul_add_of_le_natDegree_of_eq_ite {R : Type u_1} [Semiring R] {d df dg : ℕ} {a b : R} {f g : Polynomial R} (h_mul_left : f.natDegree ≤ df) (h_mul_right : g.natDegree ≤ dg) : f.coeff df = a → g.coeff dg = b → ∀ (ddf : df + dg ≤ d), (f * g).coeff d = if d = df + dg then a * b else 0

theorem Mathlib.Tactic.ComputeDegree.coeff_pow_of_natDegree_le_of_eq_ite' {R : Type u_1} [Semiring R] {m n o : ℕ} {a : R} {p : Polynomial R} (h_pow : p.natDegree ≤ n) (h_exp : m * n ≤ o) (h_pow_bas : p.coeff n = a) : (p ^ m).coeff o = if o = m * n then a ^ m else 0

theorem Mathlib.Tactic.ComputeDegree.natDegree_smul_le_of_le {R : Type u_1} [Semiring R] {S : Type u_2} [SMulZeroClass S R] {n : ℕ} {a : S} {f : Polynomial R} (hf : f.natDegree ≤ n) : (a • f).natDegree ≤ n

theorem Mathlib.Tactic.ComputeDegree.degree_smul_le_of_le {R : Type u_1} [Semiring R] {S : Type u_2} [SMulZeroClass S R] {n : ℕ} {a : S} {f : Polynomial R} (hf : f.degree ≤ ↑n) : (a • f).degree ≤ ↑n

theorem Mathlib.Tactic.ComputeDegree.coeff_smul {R : Type u_1} [Semiring R] {S : Type u_2} [SMulZeroClass S R] {n : ℕ} {a : S} {f : Polynomial R} : (a • f).coeff n = a • f.coeff n

theorem Mathlib.Tactic.ComputeDegree.natDegree_eq_of_le_of_coeff_ne_zero' {R : Type u_1} [Semiring R] {deg m o : ℕ} {c : R} {p : Polynomial R} (h_natDeg_le : p.natDegree ≤ m) (coeff_eq : p.coeff o = c) (coeff_ne_zero : c ≠ 0) (deg_eq_deg : m = deg) (coeff_eq_deg : o = deg) : p.natDegree = deg

The following two lemmas should be viewed as a hand-made "congr"-lemmas. They achieve the following goals.

• They introduce two fresh metavariables replacing the given one deg, one for the natDegree ≤ computation and one for the coeff = computation. This helps compute_degree, since it does not "pre-estimate" the degree, but it "picks it up along the way".
• They split checking the inequality coeff p n ≠ 0 into the task of finding a value c for the coeff and then proving that this value is non-zero by coeff_ne_zero.

theorem Mathlib.Tactic.ComputeDegree.degree_eq_of_le_of_coeff_ne_zero' {R : Type u_1} [Semiring R] {deg m o : WithBot ℕ} {c : R} {p : Polynomial R} (h_deg_le : p.degree ≤ m) (coeff_eq : p.coeff (WithBot.unbotD 0 deg) = c) (coeff_ne_zero : c ≠ 0) (deg_eq_deg : m = deg) (coeff_eq_deg : o = deg) : p.degree = deg

theorem Mathlib.Tactic.ComputeDegree.coeff_congr_lhs {R : Type u_1} [Semiring R] {m n : ℕ} {f : Polynomial R} {r : R} (h : f.coeff m = r) (natDeg_eq_coeff : m = n) : f.coeff n = r

theorem Mathlib.Tactic.ComputeDegree.coeff_congr {R : Type u_1} [Semiring R] {m n : ℕ} {f : Polynomial R} {r : R} (h : f.coeff m = r) (natDeg_eq_coeff : m = n) {s : R} (rs : r = s) : f.coeff n = s

theorem Mathlib.Tactic.ComputeDegree.natDegree_intCast_le {R : Type u_1} [Ring R] (n : ℤ) : (↑n).natDegree ≤ 0

theorem Mathlib.Tactic.ComputeDegree.coeff_sub_of_eq {R : Type u_1} [Ring R] {n : ℕ} {a b : R} {f g : Polynomial R} (hf : f.coeff n = a) (hg : g.coeff n = b) : (f - g).coeff n = a - b

theorem Mathlib.Tactic.ComputeDegree.coeff_intCast_ite {R : Type u_1} [Ring R] {n : ℕ} {a : ℤ} : (↑a).coeff n = ↑(if n = 0 then a else 0)

def Mathlib.Tactic.ComputeDegree.twoHeadsArgs (e : Lean.Expr) : Lean.Name × Lean.Name × (Lean.Name ⊕ Lean.Name) × List Bool

twoHeadsArgs e takes an Expression e as input and recurses into e to make sure that e looks like lhs ≤ rhs, lhs < rhs or lhs = rhs and that lhs is one of natDegree f, degree f, coeff f d. It returns

• the function being applied on the LHS (natDegree, degree, or coeff), or else .anonymous if it's none of these;
• the name of the relation (Eq, LE.le or LT.lt), or else .anonymous if it's none of these;
• either
  • .inl zero, .inl one, or .inl many if the polynomial in a numeral;
  • or .inr of the head symbol of f;
  • or .inl .anonymous if inapplicable;
• if it exists, whether the rhs is a metavariable;
• if the LHS is coeff f d, whether d is a metavariable.

This is all the data needed to figure out whether compute_degree can make progress on e and, if so, which lemma it should apply.

Sample outputs:

• natDegree (f + g) ≤ d => (natDegree, LE.le, HAdd.hAdd, d.isMVar, none) (similarly for =);
• degree (f * g) = d => (degree, Eq, HMul.hMul, d.isMVar, none) (similarly for ≤);
• coeff (1 : ℕ[X]) c = x => (coeff, Eq, one, x.isMVar, c.isMVar) (no ≤ option!).

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.ComputeDegree.getCongrLemma (twoH : Lean.Name × Lean.Name × List Bool) (debug : Bool := false) : Lean.Name

getCongrLemma (lhs_name, rel_name, Mvars?) returns the name of a lemma that preprocesses one of the seven targets

• natDegree f ≤ d;
• natDegree f < d;
• natDegree f = d;
• degree f ≤ d;
• degree f < d;
• degree f = d.
• coeff f d = r.

The end goals are of the form

• natDegree f ≤ ?_, degree f ≤ ?_, coeff f ?_ = ?_, or ?_ < d with fresh metavariables;
• coeff f m ≠ s with m, s not necessarily metavariables;
• several equalities/inequalities between expressions and assignments for metavariables.

getCongrLemma gets called at the very beginning of compute_degree and whenever an intermediate goal does not have the right metavariables. Note that the side-goals of the congruence lemma are neither of the form natDegree f = d nor of the form degree f = d.

getCongrLemma admits an optional "debug" flag: getCongrLemma data true prints the name of the congruence lemma that it returns.

def Mathlib.Tactic.ComputeDegree.dispatchLemma (twoH : Lean.Name × Lean.Name × (Lean.Name ⊕ Lean.Name) × List Bool) (debug : Bool := false) : Lean.Name

dispatchLemma twoH takes its input twoH from the output of twoHeadsArgs.

Using the information contained in twoH, it decides which lemma is the most appropriate.

dispatchLemma is essentially the main dictionary for compute_degree.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.ComputeDegree.dispatchLemma (Lean.Name.anonymous, fst, snd) debug = `id
• Mathlib.Tactic.ComputeDegree.dispatchLemma (fst, Lean.Name.anonymous, snd) debug = `id

def Mathlib.Tactic.ComputeDegree.try_rfl (mvs : List Lean.MVarId) : Lean.MetaM (List Lean.MVarId)

try_rfl mvs takes as input a list of MVarIds, scans them partitioning them into two lists: the goals containing some metavariables and the goals not containing any metavariable.

If a goal containing a metavariable has the form ?_ = x, x = ?_, where ?_ is a metavariable and x is an expression that does not involve metavariables, then it closes this goal using rfl, effectively assigning the metavariable to x.

If a goal does not contain metavariables, it tries rfl on it.

It returns the list of MVarIds, beginning with the ones that initially involved (Expr) metavariables followed by the rest.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.ComputeDegree.splitApply (mvs static : List Lean.MVarId) : Lean.MetaM (List Lean.MVarId × List Lean.MVarId)

splitApply mvs static takes two lists of MVarIds. The first list, mvs, corresponds to goals that are potentially within the scope of compute_degree: namely, goals of the form natDegree f ≤ d, degree f ≤ d, natDegree f = d, degree f = d, coeff f d = r.

splitApply determines which of these goals are actually within the scope, it applies the relevant lemma and returns two lists: the left-over goals of all the applications, followed by the concatenation of the previous static list, followed by the newly discovered goals outside of the scope of compute_degree.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.ComputeDegree.miscomputedDegree? (deg : Lean.Expr) : List Lean.Expr → List Lean.MessageData

miscomputedDegree? deg false_goals takes as input

• an Expression deg, representing the degree of a polynomial (i.e. an Expression of inferred type either ℕ or WithBot ℕ);
• a list of MVarIds false_goals.

Although inconsequential for this function, the list of goals false_goals reduces to False if norm_nummed. miscomputedDegree? extracts error information from goals of the form

• a ≠ b, assuming it comes from ⊢ coeff_of_given_degree ≠ 0 --- reducing to False means that the coefficient that was supposed to vanish, does not;
• a ≤ b, assuming it comes from ⊢ degree_of_subterm ≤ degree_of_polynomial --- reducing to False means that there is a term of degree that is apparently too large;
• a = b, assuming it comes from ⊢ computed_degree ≤ given_degree --- reducing to False means that there is a term of degree that is apparently too large.

The cases a ≠ b and a = b are not a perfect match with the top coefficient: reducing to False is not exactly correlated with a coefficient being non-zero. It does mean that compute_degree reduced the initial goal to an unprovable state (unless there was already a contradiction in the initial hypotheses!), but it is indicative that there may be some problem.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.ComputeDegree.miscomputedDegree? deg [] = []

def Mathlib.Tactic.ComputeDegree.computeDegree : Lean.ParserDescr

compute_degree is a tactic to solve goals of the form

• natDegree f = d,
• degree f = d,
• natDegree f ≤ d (or <),
• degree f ≤ d (or <),
• coeff f d = r, if d is the degree of f.

The tactic may leave goals of the form d' = d, d' ≤ d, d' < d, or r ≠ 0, where d' in ℕ or WithBot ℕ is the tactic's guess of the degree, and r is the coefficient's guess of the leading coefficient of f.

compute_degree applies norm_num to the left-hand side of all side goals, trying to close them.

The variant compute_degree! first applies compute_degree. Then it uses norm_num on all the remaining goals and tries assumption.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.ComputeDegree.tacticCompute_degree! : Lean.ParserDescr

compute_degree is a tactic to solve goals of the form

• natDegree f = d,
• degree f = d,
• natDegree f ≤ d (or <),
• degree f ≤ d (or <),
• coeff f d = r, if d is the degree of f.

The tactic may leave goals of the form d' = d, d' ≤ d, d' < d, or r ≠ 0, where d' in ℕ or WithBot ℕ is the tactic's guess of the degree, and r is the coefficient's guess of the leading coefficient of f.

compute_degree applies norm_num to the left-hand side of all side goals, trying to close them.

The variant compute_degree! first applies compute_degree. Then it uses norm_num on all the remaining goals and tries assumption.

Equations

• Mathlib.Tactic.ComputeDegree.tacticCompute_degree! = Lean.ParserDescr.node `Mathlib.Tactic.ComputeDegree.tacticCompute_degree! 1024 (Lean.ParserDescr.nonReservedSymbol "compute_degree!" false)

def Mathlib.Tactic.ComputeDegree.monicityMacro : Lean.ParserDescr

monicity tries to solve a goal of the form Monic f. It converts the goal into a goal of the form natDegree f ≤ n and one of the form f.coeff n = 1 and calls compute_degree on those two goals.

The variant monicity! starts like monicity, but calls compute_degree! on the two side-goals.

Equations

• Mathlib.Tactic.ComputeDegree.monicityMacro = Lean.ParserDescr.node `Mathlib.Tactic.ComputeDegree.monicityMacro 1024 (Lean.ParserDescr.nonReservedSymbol "monicity" false)

def Mathlib.Tactic.ComputeDegree.tacticMonicity! : Lean.ParserDescr

monicity tries to solve a goal of the form Monic f. It converts the goal into a goal of the form natDegree f ≤ n and one of the form f.coeff n = 1 and calls compute_degree on those two goals.

The variant monicity! starts like monicity, but calls compute_degree! on the two side-goals.

Equations

• Mathlib.Tactic.ComputeDegree.tacticMonicity! = Lean.ParserDescr.node `Mathlib.Tactic.ComputeDegree.tacticMonicity! 1024 (Lean.ParserDescr.nonReservedSymbol "monicity!" false)

We register compute_degree with the hint tactic.