[Merged by Bors] - feat(data/finset): add card_insert_of_mem #3137
Conversation
kbuzzard
added
the
awaiting-review
robertylewis
changed the title
src/data/finset.lean
Outdated
| @@ -1395,6 +1395,9 @@ by cases s; simp only [multiset.card_eq_one, finset.card, ← val_inj, singleton | |||
| by simpa only [card_cons, card, insert_val] using | |||
| congr_arg multiset.card (ndinsert_of_not_mem h) | |||
|
|
|||
| @[simp] theorem card_insert_of_mem [decidable_eq α] {a : α} {s : finset α} | |||
There was a problem hiding this comment.
I think this shouldn't be a simp lemma because insert_eq_of_mem is already. This is proved by simp [h]. @gebner should the linter have caught this, or does it not do conditional rules?
There was a problem hiding this comment.
I am unfortunately still showing my ignorance of how simp works. I think that I used to tag nothing with simp, and now I tag everything! But I do understand "we will not gain anything by telling the simplifier this, because in every case when it can apply, something else (a bit simpler) also applies". I'll remove the tag.
There was a problem hiding this comment.
@robertylewis Conditional rules are out-of-scope, yes. We still check that the lhs is in simp normal-form though.
There was a problem hiding this comment.
I am unfortunately still showing my ignorance of how
simpworks. I think that I used to tag nothing with simp, and now I tag everything! But I do understand "we will not gain anything by telling the simplifier this, because in every case when it can apply, something else (a bit simpler) also applies". I'll remove the tag.
There's a difference between "unconditional" and "conditional" simp rules. This one is conditional, because of the hypothesis a ∈ s. If the rewrite rule matches, then simp will try to prove a ∈ s, and only go ahead with the original rewrite if this succeeds.
The linter that checks for
we will not gain anything by telling the simplifier this,
doesn't handle conditional rules, so it didn't notice the issue here.
|
The CI failure looks like a GitHub glitch, so, bors merge |
github-actions
bot
added
ready-to-merge
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
A Zulip user was asking where this function was; they found card_insert_of_not_mem. Note that insert_eq_of_mem is strictly stronger (the cardinalities are equal because the finsets are equal). Is this worth putting in the library?