Documentation

Mathlib.Tactic.ComputeDegree

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

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 #

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:

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

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

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

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
@[deprecated Mathlib.Tactic.ComputeDegree.natDegree_natCast_le]
theorem Mathlib.Tactic.ComputeDegree.natDegree_nat_cast_le {R : Type u_1} [Semiring R] (n : ) :
(n).natDegree 0

Alias of Mathlib.Tactic.ComputeDegree.natDegree_natCast_le.

theorem Mathlib.Tactic.ComputeDegree.coeff_add_of_eq {R : Type u_1} [Semiring R] {n : } {a : R} {b : R} {f : Polynomial R} {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 : R} {b : R} {f : Polynomial R} {g : Polynomial R} (h_mul_left : f.natDegree df) (h_mul_right : g.natDegree dg) (h_mul_left : f.coeff df = a) (h_mul_right : 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] {n : } {a : R} {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] {n : } {a : R} {f : Polynomial R} (hf : f.degree n) :
(a f).degree n
theorem Mathlib.Tactic.ComputeDegree.coeff_smul {R : Type u_1} [Semiring R] {n : } {a : R} {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 : WithBot } {m : WithBot } {o : WithBot } {c : R} {p : Polynomial R} (h_deg_le : p.degree m) (coeff_eq : p.coeff (WithBot.unbot' 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
@[deprecated Mathlib.Tactic.ComputeDegree.natDegree_intCast_le]
theorem Mathlib.Tactic.ComputeDegree.natDegree_int_cast_le {R : Type u_1} [Ring R] (n : ) :
(n).natDegree 0

Alias of Mathlib.Tactic.ComputeDegree.natDegree_intCast_le.

theorem Mathlib.Tactic.ComputeDegree.coeff_sub_of_eq {R : Type u_1} [Ring R] {n : } {a : R} {b : R} {f : Polynomial R} {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)
@[deprecated Mathlib.Tactic.ComputeDegree.coeff_intCast_ite]
theorem Mathlib.Tactic.ComputeDegree.coeff_int_cast_ite {R : Type u_1} [Ring R] {n : } {a : } :
(a).coeff n = (if n = 0 then a else 0)

Alias of Mathlib.Tactic.ComputeDegree.coeff_intCast_ite.

twoHeadsArgs e takes an Expression 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.

    Equations
    • One or more equations did not get rendered due to their size.
    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.

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

        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.
        Instances For

          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.
          Instances For

            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
            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 clos 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 clos them.

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

                Equations
                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
                  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
                    Instances For