[Merged by Bors] - feat(tactic/positivity): Extension for finset.card#16637
[Merged by Bors] - feat(tactic/positivity): Extension for finset.card#16637YaelDillies wants to merge 4 commits intomasterfrom
finset.card#16637Conversation
eric-wieser
left a comment
There was a problem hiding this comment.
Is it straightforward to extend this to fintype.card?
You mean by looking for a |
Vierkantor
left a comment
There was a problem hiding this comment.
LGTM with Eric's suggestion.
bors d+
| /-- Extension for the `positivity` tactic: `finset.card s` is positive if `s` is nonempty. -/ | ||
| @[positivity] | ||
| meta def positivity_finset_card : expr → tactic strictness | ||
| | `(finset.card %%s) := do -- TODO: Partial decision procedure for `finset.nonempty` |
There was a problem hiding this comment.
As we discussed via PMs on Zulip last week, this TODO might be only relevant once we get access to Aesop, since this decision procedure can easily start cycling.
I do think that it's fine to make the user add finset.nonempty hypotheses before calling positivity, so this looks good to me.
|
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
A best effort `positivity` extension for `finset.card`. This looks for an assumption of the form `s.nonempty` in context to prove `0 < s.card`.
|
Build failed: |
|
This is fallout from bors merge |
A best effort `positivity` extension for `finset.card`. This looks for an assumption of the form `s.nonempty` in context to prove `0 < s.card`.
|
Pull request successfully merged into master. Build succeeded: |
finset.cardfinset.card
A best effort
positivityextension forfinset.card. This looks for an assumption of the forms.nonemptyin context to prove0 < s.card.