-
Notifications
You must be signed in to change notification settings - Fork 297
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(tactic/positivity): Handle a ≠ 0
assumptions
#16529
Conversation
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.
bors d+
mul_inv_cancel := λ I, fractional_ideal.mul_inv_cancel, | ||
.. fractional_ideal.comm_semiring } | ||
.. fractional_ideal.comm_semiring, ..(coe_to_fractional_ideal_injective le_rfl).nontrivial } |
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.
Not sure why this is included here?
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.
The simpa
call failed because simp
now closes the goal thanks to the change to bot_ne_top
. It was easier to golf than to fix.
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
fix analysis.special_functions.pow
bors merge |
Make `positivity` handle `a ≠ 0` assumptions. This involves * adding a third constructor to `positivity.strictness`, that I've called `nonzero`. It is meant to hold proofs of `a ≠ 0`, not `0 ≠ a` * modifying the existing extensions to handle that new case. * changing `positivity.orelse'` to account for the fact that if we can prove `0 ≤ a` and `a ≠ 0` then we can prove `0 < a`. * making `compare_hyp` handle `eq` and `ne` hypotheses. ## Other changes * Introduce `tac1 ≤|≥ tac2` as notation for `positivity.orelse' tac1 tac2`. This has the same precedence as the `<|>` notation for `orelse`. * Make `positivity` extensions fail with more informative error messages. This is useless when running `positivity` alone but: * It clearly marks within the code what each failure means * The errors can show up when calling an extension directly. Not sure why you would do that, but you could. * Add a `has_to_format strictness` instance. This is mostly useful for debugging.
Pull request successfully merged into master. Build succeeded: |
a ≠ 0
assumptionsa ≠ 0
assumptions
Make
positivity
handlea ≠ 0
assumptions. This involvespositivity.strictness
, that I've callednonzero
. It is meant to hold proofs ofa ≠ 0
, not0 ≠ a
positivity.orelse'
to account for the fact that if we can prove0 ≤ a
anda ≠ 0
then we can prove0 < a
.compare_hyp
handleeq
andne
hypotheses.Other changes
tac1 ≤|≥ tac2
as notation forpositivity.orelse' tac1 tac2
. This has the same precedence as the<|>
notation fororelse
.positivity
extensions fail with more informative error messages. This is useless when runningpositivity
alone but:has_to_format strictness
instance. This is mostly useful for debugging.