feat(tactic/compute_degree + test/compute_degree): introduce a tactic…

… for proving `f.(nat_)degree ≤ d` (#14762)

This PR is a prequel to #14040.  It introduces a simpler step than the actual computation of the degree.  This step is used by the "main" tactic `compute_degree` defined in #14040.

To help the reviewing process, I split this PR from the other one.

For a very small sample of some golfing that could be done with this tactic, see [this diff](https://github.com/leanprover-community/mathlib/compare/adomani_compute_degree_le..adomani_compute_degree_le_golf), from #14776.

src/tactic/compute_degree.lean

@@ -0,0 +1,166 @@
+/-
+Copyright (c) 2022 Damiano Testa. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Damiano Testa
+-/
+import data.polynomial.degree.lemmas
+
+/-! # `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. -/
+
+namespace tactic
+namespace compute_degree
+open expr polynomial
+
+/--  `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`.
+ -/
+meta def guess_degree : expr → tactic expr
+| `(has_zero.zero)           := pure `(0)
+| `(has_one.one)             := pure `(0)
+| `(- %%f)                   := guess_degree f
+| (app `(⇑C) x)              := pure `(0)
+| `(X)                       := pure `(1)
+| `(bit0 %%a)                := guess_degree a
+| `(bit1 %%a)                := guess_degree a
+| `(%%a + %%b)               := do [da, db] ← [a, b].mmap guess_degree,
+                                pure $ expr.mk_app `(max : ℕ → ℕ → ℕ) [da, db]
+| `(%%a - %%b)               := do [da, db] ← [a, b].mmap guess_degree,
+                                pure $ expr.mk_app `(max : ℕ → ℕ → ℕ) [da, db]
+| `(%%a * %%b)               := do [da, db] ← [a, b].mmap guess_degree,
+                                pure $ expr.mk_app `((+) : ℕ → ℕ → ℕ) [da, db]
+| `(%%a ^ %%b)               := do da ← guess_degree a,
+                                pure $ expr.mk_app `((*) : ℕ → ℕ → ℕ) [da, b]
+| (app `(⇑(monomial %%n)) x) := pure n
+| e                          := do `(@polynomial %%R %%inst) ← infer_type e,
+                                pe ← to_expr ``(@nat_degree %%R %%inst) tt ff,
+                                pure $ expr.mk_app pe [e]
+
+/-- `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.
+-/
+meta def resolve_sum_step : expr → tactic unit
+| `(nat_degree %%tl ≤ %%tr) := match tl with
+  | `(%%tl1 + %%tl2) := refine ``((nat_degree_add_le_iff_left _ _ _).mpr _)
+  | `(%%tl1 - %%tl2) := refine ``((nat_degree_sub_le_iff_left _ _ _).mpr _)
+  | `(%%tl1 * %%tl2) := do [d1, d2] ← [tl1, tl2].mmap guess_degree,
+    refine ``(nat_degree_mul_le.trans $ (add_le_add _ _).trans (_ : %%d1 + %%d2 ≤ %%tr))
+  | `(- %%f)         := refine ``((nat_degree_neg _).le.trans _)
+  | `(X ^ %%n)       := refine ``((nat_degree_X_pow_le %%n).trans _)
+  | (app `(⇑(@monomial %%R %%inst %%n)) x) := refine ``((nat_degree_monomial_le %%x).trans _)
+  | (app `(⇑C) x)    := refine ``((nat_degree_C %%x).le.trans (nat.zero_le %%tr))
+  | `(X)             := refine ``(nat_degree_X_le.trans _)
+  | `(has_zero.zero) := refine ``(nat_degree_zero.le.trans (nat.zero_le _))
+  | `(has_one.one)   := refine ``(nat_degree_one.le.trans (nat.zero_le _))
+  | `(bit0 %%a)      := refine ``((nat_degree_bit0 %%a).trans _)
+  | `(bit1 %%a)      := refine ``((nat_degree_bit1 %%a).trans _)
+  | `(%%tl1 ^ %%n)   := do
+      refine ``(nat_degree_pow_le.trans _),
+      refine ``(dite (%%n = 0) (λ (n0 : %%n = 0), (by simp only [n0, zero_mul, zero_le])) _),
+      n0 ← get_unused_name "n0" >>= intro,
+      refine ``((mul_comm _ _).le.trans ((nat.le_div_iff_mul_le' (nat.pos_of_ne_zero %%n0)).mp _)),
+      lem1 ← to_expr ``(nat.mul_div_cancel _ (nat.pos_of_ne_zero %%n0)) tt ff,
+      lem2 ← to_expr ``(nat.div_self (nat.pos_of_ne_zero %%n0)) tt ff,
+      focus1 (refine ``((%%n0 rfl).elim) <|> rewrite_target lem1 <|> rewrite_target lem2) <|> skip
+  | e                := fail!"'{e}' is not supported"
+  end
+| e := fail!("'resolve_sum_step' was called on\n" ++
+  "{e}\nbut it expects `f.nat_degree ≤ d`")
+
+/--  `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. -/
+meta def norm_assum : tactic unit :=
+try `[ norm_num ] >> try assumption
+
+/--  `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`. -/
+meta def eval_guessing (n : ℕ) : expr → tactic ℕ
+| `(%%a + %%b)   := (+) <$> eval_guessing a <*> eval_guessing b
+| `(%%a * %%b)   := (*) <$> eval_guessing a <*> eval_guessing b
+| `(max %%a %%b) := max <$> eval_guessing a <*> eval_guessing b
+| e              := eval_expr' ℕ e <|> pure n
+
+end compute_degree
+
+namespace interactive
+open compute_degree polynomial
+
+/--  `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. -/
+meta def compute_degree_le : tactic unit :=
+do t ← target,
+  try $ refine ``(degree_le_nat_degree.trans (with_bot.coe_le_coe.mpr _)),
+  `(nat_degree %%tl ≤ %%tr) ← target |
+    fail "Goal is not of the form\n`f.nat_degree ≤ d` or `f.degree ≤ d`",
+  expected_deg ← guess_degree tl >>= eval_guessing 0,
+  deg_bound ← eval_expr' ℕ tr <|> pure expected_deg,
+  if deg_bound < expected_deg
+  then fail sformat!"the given polynomial has a term of expected degree\nat least '{expected_deg}'"
+  else
+    repeat $ target >>= resolve_sum_step,
+    (do gs ← get_goals >>= list.mmap infer_type,
+      success_if_fail $ gs.mfirst $ unify t) <|> fail "Goal did not change",
+    try $ any_goals' norm_assum
+
+add_tactic_doc
+{ name := "compute_degree_le",
+  category := doc_category.tactic,
+  decl_names := [`tactic.interactive.compute_degree_le],
+  tags := ["arithmetic, finishing"] }
+
+end interactive
+
+end tactic

test/compute_degree.lean

@@ -0,0 +1,85 @@
+import tactic.compute_degree
+
+open polynomial
+open_locale polynomial
+
+variables {R : Type*} [semiring R] {a b c d e : R}
+
+example {p : R[X]} {n : ℕ} {p0 : p.nat_degree = 0} :
+ (p ^ n).nat_degree ≤ 0 :=
+by compute_degree_le
+
+example {p : R[X]} {n : ℕ} {p0 : p.nat_degree = 0} :
+ (p ^ n).nat_degree ≤ 0 :=
+by cases n; compute_degree_le
+
+example {p q r : R[X]} {a b c d e f m n : ℕ} {p0 : p.nat_degree = a} {q0 : q.nat_degree = b}
+  {r0 : r.nat_degree = c} :
+  (((q ^ e * p ^ d) ^ m * r ^ f) ^ n).nat_degree ≤ ((b * e + a * d) * m + c * f) * n :=
+begin
+  compute_degree_le,
+  rw [p0, q0, r0],
+end
+
+example {F} [ring F] {p : F[X]} (p0 : p.nat_degree ≤ 0) :
+  p.nat_degree ≤ 0 :=
+begin
+  success_if_fail_with_msg {compute_degree_le} "Goal did not change",
+  exact p0,
+end
+
+example {F} [ring F] {p q : F[X]} (h : p.nat_degree + 1 ≤ q.nat_degree) :
+  (- p * X).nat_degree ≤ q.nat_degree :=
+by compute_degree_le
+
+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 {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 (n : ℕ) (h : 1 + n < 11) :
+  degree (5 * X ^ n + (X * monomial n 1 + X * X) + C a + C a * X ^ 10) ≤ 10 :=
+begin
+  compute_degree_le,
+  { exact nat.lt_succ_iff.mp h },
+  { exact nat.lt_succ_iff.mp ((lt_one_add n).trans h) },
+end
+
+example {n : ℕ} (h : 1 + n < 11) :
+  degree (X + (X * monomial 2 1 + X * X) ^ 2) ≤ 10 :=
+by compute_degree_le
+
+example {m s: ℕ} (ms : m ≤ s) (s1 : 1 ≤ s) : nat_degree (C a * X ^ m + X + 5) ≤ s :=
+by compute_degree_le; assumption
+
+example : nat_degree (7 * X : R[X]) ≤ 1 :=
+by compute_degree_le
+
+example : (1 : polynomial R).nat_degree ≤ 0 :=
+by compute_degree_le
+
+example : nat_degree (monomial 5 c * monomial 1 c + monomial 7 d +
+  C a * X ^ 0 + C b * X ^ 5 + C c * X ^ 2 + X ^ 10 + C e * X) ≤ 10 :=
+by compute_degree_le
+
+example {n : ℕ} : nat_degree (0 * (X ^ 0 + X ^ n) * monomial 5 c * monomial 6 c) ≤ 9 :=
+begin
+  success_if_fail_with_msg {compute_degree_le}
+    "the given polynomial has a term of expected degree
+at least '11'",
+  rw [zero_mul, zero_mul, zero_mul, nat_degree_zero],
+  exact nat.zero_le _
+end
+
+example : nat_degree (monomial 0 c * (monomial 0 c * C 1) + monomial 0 d + C 1 + C a * X ^ 0) ≤ 0 :=
+by compute_degree_le
+
+example {F} [ring F] {n m : ℕ} (n4 : n ≤ 4) (m4 : m ≤ 4) {a : F} :
+  nat_degree (C a * X ^ n + X ^ m + bit1 1 : F[X]) ≤ 4 :=
+by compute_degree_le; assumption
+
+example {F} [ring F] : nat_degree (X ^ 4 + bit1 1 : F[X]) ≤ 4 :=
+by compute_degree_le