Commit 2023-09-02 12:08 f327170d

View on Github →

feat: tactic compute_degree (#6221) This PR ports the whole compute_degree tactic from mathlib3. The tactic makes progress on goals of the form

  • natDegree f ≤ d,
  • degree f ≤ d,
  • natDegree f = d,
  • degree f = d,
  • coeff f n = r. The variant compute_degree! applies norm_num and assumption to all left-over goals. For instance, here is a valid computation of the degree of the 105-th cyclotomic polynomial:
example : natDegree
    (1 + X + X ^ 2 - X ^ 5 - X ^ 6 - 2 * X ^ 7 - X ^ 8 - X ^ 9 + X ^ 12 + X ^ 13 + X ^ 14 +
        X ^ 15 + X ^ 16 + X ^ 17 - X ^ 20 - X ^ 22 - X ^ 24 - X ^ 26 - X ^ 28 + X ^ 31 + X ^ 32 +
        X ^ 33 + X ^ 34 + X ^ 35 + X ^ 36 - X ^ 39 - X ^ 40 - 2 * X ^ 41 - X ^ 42 - X ^ 43 +
        X ^ 46 + X ^ 47 + X ^ 48 : ℤ[X]) = 48 := by
  compute_degree!

(Lean takes approximately 3s on my computer to prove the computation above.) Affected files:

Mathlib/Lean/Expr/Basic.lean
Mathlib/Tactic/ComputeDegree.lean
test/ComputeDegree.lean

Estimated changes

added def Lean.Expr.le?