[Merged by Bors] - feat: positivity extension for zpow #8003
Conversation
dupuisf
added
awaiting-review
Mathlib/Tactic/Positivity/Basic.lean
Outdated
| let _a ← synthInstanceQ q(LinearOrderedField $α) | ||
| haveI' : $e =Q $a ^ $b := ⟨⟩ | ||
| assumeInstancesCommute | ||
| pure (by exact .nonnegative q(zpow_bit0_nonneg $a $m)) |
There was a problem hiding this comment.
Is it possible to use Even.zpow_nonneg here, instead of zpow_bit0_nonneg? Would that remove the need for the linter.deprecated false?
There was a problem hiding this comment.
Yes (see the current version), but this adds extra imports (namely Mathlib.Data.Int.Parity) to get Int.even_iff, and the way it's coded now the unusedHavesSuffices linter flags a line that doesn't seem spurious (at least I don't know how to remove it). Doesn't seem worth it unless we're actually planning to remove bit0 entirely.
There was a problem hiding this comment.
Hm... I think I agree that we should try to avoid adding that new dependency.
In your original code, you can dodge linter.deprecated by doing this:
- haveI' : $b =Q bit0 $m := ⟨⟩
+ haveI' : $b =Q $m + $m := ⟨⟩ -- b = bit0 mThat seems better to me than disabling the linter for the entire declaration.
leanprover-community-mathlib4-bot
added
the
merge-conflict
dupuisf
added
awaiting-author
leanprover-community-mathlib4-bot
removed
the
merge-conflict
dupuisf
added
awaiting-review
Mathlib/Tactic/Positivity/Basic.lean
Outdated
| let _a ← synthInstanceQ q(LinearOrderedField $α) | ||
| haveI' : $e =Q $a ^ $b := ⟨⟩ | ||
| assumeInstancesCommute | ||
| pure (by exact .nonnegative q(zpow_bit0_nonneg $a $m)) |
There was a problem hiding this comment.
Hm... I think I agree that we should try to avoid adding that new dependency.
In your original code, you can dodge linter.deprecated by doing this:
- haveI' : $b =Q bit0 $m := ⟨⟩
+ haveI' : $b =Q $m + $m := ⟨⟩ -- b = bit0 mThat seems better to me than disabling the linter for the entire declaration.
|
What's the situation here? I would like this in mathlib 😄 |
|
I reverted this to the initial version of the PR, before my first comment, and I switched to the more localized way of suppressing the linter that I suggested above. |
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
|
bors merge |
github-actions
bot
added
ready-to-merge
This PR adds a positivity extension for integer powers, i.e. `a ^ (r : ℤ)`. It's basically copy-pasted from the natural power extension. Note that this makes the imports of `Mathlib.Tactic.Positivity.Basic` slightly heavier since the required lemmas were not there (and the relevant file doesn't import positivity so I couldn't put it there either). It's probably not too bad, but I can put it in a new file if people think this would be better. Co-authored-by: David Renshaw <dwrenshaw@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
This PR adds a positivity extension for integer powers, i.e. `a ^ (r : ℤ)`. It's basically copy-pasted from the natural power extension. Note that this makes the imports of `Mathlib.Tactic.Positivity.Basic` slightly heavier since the required lemmas were not there (and the relevant file doesn't import positivity so I couldn't put it there either). It's probably not too bad, but I can put it in a new file if people think this would be better. Co-authored-by: David Renshaw <dwrenshaw@gmail.com>
This PR adds a positivity extension for integer powers, i.e.
a ^ (r : ℤ). It's basically copy-pasted from the natural power extension. Note that this makes the imports ofMathlib.Tactic.Positivity.Basicslightly heavier since the required lemmas were not there (and the relevant file doesn't import positivity so I couldn't put it there either). It's probably not too bad, but I can put it in a new file if people think this would be better.