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

`natDegree f ≤ d`

,`degree f ≤ d`

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

Still, it may not be worth to provide special support for`example [Semiring R] : natDegree (C 0 : R[X]) = 0 := by compute_degree -- ⊢ 0 ≠ 0`

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

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

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`

.

`twoHeadsArgs e`

takes an `Expr`

ession `e`

as input and recurses into `e`

to make sure
the `e`

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

or`LE.le`

), 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.

## Instances For

`getCongrLemma (lhs_name, rel_name, Mvars?)`

returns the name of a lemma that preprocesses
one of the five target

`natDegree f ≤ d`

;`natDegree 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 ?_ = ?_`

, 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.

## Instances For

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

.

## Instances For

`try_rfl mvs`

takes as input a list of `MVarId`

s, 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 `MVarId`

s, 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.

## Instances For

`splitApply mvs static`

takes two lists of `MVarId`

s. 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.

## Instances For

`miscomputedDegree? deg false_goals`

takes as input

- an
`Expr`

ession`deg`

, representing the degree of a polynomial (i.e. an`Expr`

ession of inferred type either`ℕ`

or`WithBot ℕ`

); - a list of
`MVarId`

s`false_goals`

.

Although inconsequential for this function, the list of goals `false_goals`

reduces to `False`

if `norm_num`

med.
`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 [] = []

## Instances For

`compute_degree`

is a tactic to solve goals of the form

`natDegree f = d`

,`degree f = d`

,`natDegree f ≤ d`

,`degree f ≤ d`

,`coeff f d = r`

, if`d`

is the degree of`f`

.

The tactic may leave goals of the form `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 whole remaining goals and tries `assumption`

.

## Equations

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

## Instances For

`compute_degree`

is a tactic to solve goals of the form

`natDegree f = d`

,`degree f = d`

,`natDegree f ≤ d`

,`degree f ≤ d`

,`coeff f d = r`

, if`d`

is the degree of`f`

.

The tactic may leave goals of the form `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 whole 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)

## Instances For

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

## Instances For

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