-
Notifications
You must be signed in to change notification settings - Fork 246
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat: add Inv, Abs, and natAbs positivity extensions #1190
Conversation
Mathlib/Tactic/Positivity/Basic.lean
Outdated
|
||
/-- Port note: in mathlib3 this alias is `private`, but mathlib4's `alias` does not | ||
(yet) support that. -/ | ||
alias abs_pos ↔ _ abs_pos_of_ne_zero |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Mathlib3's alias
doesn't support private either. I think the statement should just be written out.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done -- rewritten as a private theroem
.
Mathlib/Tactic/Positivity/Basic.lean
Outdated
alias abs_pos ↔ _ abs_pos_of_ne_zero | ||
|
||
/-- The `positivity` extension which identifies expressions of the form `|a|`. -/ | ||
@[positivity |(_ : α)|, Abs.abs _] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
These two patterns are the same. The reason add and mul have two patterns instead of one is because they match both HAdd.hAdd
and Add.add
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done, and similar for evalInv
.
bors r+ |
Adds `positivity` extensions for inversion, absolute value, and natAbs. Compare the the mathlib3 versions [here](https://github.com/leanprover-community/mathlib/blob/3813d4ea1c6a34dbb472de66e73b8c6855b03964/src/tactic/positivity.lean#L535-L546), [here](https://github.com/leanprover-community/mathlib/blob/3813d4ea1c6a34dbb472de66e73b8c6855b03964/src/tactic/positivity.lean#L616-L631), and [here](https://github.com/leanprover-community/mathlib/blob/09258fb7f75d741b7eda9fa18d5c869e2135d9f1/src/tactic/positivity.lean#L633-L650). For the absolute value case, I got stuck trying to make it work in the fully `Qq`-ified style, so I fell back to the `AppBuilder` style that's closer to how mathlib3 does it.
Pull request successfully merged into master. Build succeeded:
|
Adds
positivity
extensions for inversion, absolute value, and natAbs.Compare the the mathlib3 versions here, here, and here.
For the absolute value case, I got stuck trying to make it work in the fully
Qq
-ified style, so I fell back to theAppBuilder
style that's closer to how mathlib3 does it.