[Merged by Bors] - feat(Tactic/ComputeDegree): add helper lemmas for compute_degree_le
#5978
Conversation
adomani
added
the
awaiting-review
Mathlib/Tactic/ComputeDegree.lean
Outdated
| section semiring | ||
| variable [Semiring R] | ||
|
|
||
| theorem add {a b : Nat} {f g : R[X]} (hf : natDegree f ≤ a) (hg : natDegree g ≤ b) : |
There was a problem hiding this comment.
IMHO, this can go near Polynomial.natDegree_add_le, e.g., under name Polynomial.natDegree_add_le_of_le. See norm_add_le_of_le for an example of this pattern already in the library.
Same for most of the lemmas below.
There was a problem hiding this comment.
Yuri, thank you for the review!
I moved almost all the lemmas to Data/Pol/Deg/Defs. In the new file, I left only the lemmas of the form natDegree ↑n ≤ 0. Given that the stronger form natDegree ↑n = 0 is already present, adding these to the "main" library seems unwanted clutter.
Let me know if you want me to move these lemmas also out of the file, and I can do it!
Mathlib/Tactic/ComputeDegree.lean
Outdated
| natDegree_pow_le.trans (Nat.mul_le_mul rfl.le ‹_›) | ||
|
|
||
| theorem C_le (a : R) : natDegree (C a) ≤ 0 := (natDegree_C a).le | ||
| theorem nat_cast_le (n : Nat) : natDegree (n : R[X]) ≤ 0 := (natDegree_nat_cast _).le |
There was a problem hiding this comment.
BTW, do you handle (2 : R[X]) (a.k.a. OfNat.ofNat 2 : R[X]) in your tactic?
There was a problem hiding this comment.
I think so. It seems that special support in this case only touches 0, 1:
example [Semiring R] : natDegree (0 : R[X]) ≤ 0 := by
compute_degree_le
example [Semiring R] : degree (1 : R[X]) ≤ 0 := by
compute_degree_le
example [Semiring R] : natDegree (2 : R[X]) ≤ 0 := by
compute_degree_le
example [Semiring R] : degree (OfNat.ofNat 2 : R[X]) ≤ 0 := by
compute_degree_leall work with the current tactic.
However, your comment highlighted a bug:
example [Semiring R] : degree (OfNat.ofNat 0 : R[X]) ≤ 0 := by
compute_degree_le
example [Semiring R] : degree (OfNat.ofNat 1 : R[X]) ≤ 0 := by
compute_degree_le
/-
tactic 'apply' failed, failed to unify
degree ↑?n ≤ 0
with
degree (OfNat.ofNat 1) ≤ ?b
-/both fail. I'll investigate this in the other PR.
There was a problem hiding this comment.
These OfNat instances use Zero and One, not Nat.cast.
There was a problem hiding this comment.
I think that I fixed this in the main tactic by using Expr.numeral? and being more systematic.
I find the new coercion/numeral system somewhat confusing. Also, I still think that the special support affects 0, 1 in this case, but from 2 onward it appears to be uniform.
| @@ -285,6 +285,8 @@ theorem natDegree_nat_cast (n : ℕ) : natDegree (n : R[X]) = 0 := by | |||
| simp only [← C_eq_nat_cast, natDegree_C] | |||
| #align polynomial.nat_degree_nat_cast Polynomial.natDegree_nat_cast | |||
|
|
|||
| theorem degree_nat_cast_le (n : Nat) : degree (n : R[X]) ≤ 0 := degree_le_of_natDegree_le (by simp) | |||
There was a problem hiding this comment.
Here and below (same for Int):
| theorem degree_nat_cast_le (n : Nat) : degree (n : R[X]) ≤ 0 := degree_le_of_natDegree_le (by simp) | |
| theorem degree_nat_cast_le (n : ℕ) : degree (n : R[X]) ≤ 0 := degree_le_of_natDegree_le (by simp) |
|
Thanks! I pushed a minor golf. Feel free to either accept it or revert it. |
|
✌️ adomani can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
and removed
awaiting-review
|
bors r+ |
…#5978) This PR is a prequel to #5882: it simply adds the helper lemmas about polynomials that the tactic uses. [Zulip discussion ](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235882.20.60compute_degree_le.60) Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
compute_degree_lecompute_degree_le
…#5978) This PR is a prequel to #5882: it simply adds the helper lemmas about polynomials that the tactic uses. [Zulip discussion ](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235882.20.60compute_degree_le.60) Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
This PR is a prequel to #5882: it simply adds the helper lemmas about polynomials that the tactic uses.
Zulip discussion