[Merged by Bors] - refactor(data/finset/noncomm_prod): Use set.pairwise
#16859
Conversation
YaelDillies
added
WIP
| rintro rfl, | ||
| exact hn.left hx | ||
| end | ||
| by { rw coe_to_finset at hl, exact hn.pairwise_of_set_pairwise hl } | ||
|
|
||
| lemma pairwise_iff_coe_to_finset_pairwise (hn : l.nodup) (hs : symmetric r) : | ||
| (l.to_finset : set α).pairwise r ↔ l.pairwise r := |
There was a problem hiding this comment.
Seems we're missing the backward direction without the l.nodup condition, but maybe another PR ...
There was a problem hiding this comment.
No lemma should be stated in terms of (l.to_finset : set α) anymore anyway. I will remove these lemmas in a later PR.
| @[simp] lemma nodup.pairwise_coe [is_symm α r] (hl : l.nodup) : | ||
| {a | a ∈ l}.pairwise r ↔ l.pairwise r := |
There was a problem hiding this comment.
Is the name better as nodup.pairwise_coe_iff? Also we don't actually have a coercion from list to set now.
There was a problem hiding this comment.
Hmm, I now wonder why finset.set.has_coe_t is not via a set_like instance. (Of course list and multiset can't have set_like instances since taking membership predicate isn't injective.)
There was a problem hiding this comment.
I prefer the name as is to match the general convention from list/multiset/finset of omitting the _iff quite eagerly. However I agree that the coe bit is a bit bad because there won't ever be a coercion, as all coercions are meant to be injective.
There was a problem hiding this comment.
Maybe we can just fix that in a later PR? This is very tangential to the current.
There was a problem hiding this comment.
all coercions are meant to be injective.
I don't think that's a universal rule? int.cast_coe certainly aren't always injective, and #16567 adds has_lift_t for algebras which also uses coe but isn't always surjective.
There was a problem hiding this comment.
Hmm... true, but I don't know of a non-injective coercion that's explicitly between concrete types, as is the case here.
There was a problem hiding this comment.
Maybe we can just fix that in a later PR? This is very tangential to the current.
I think so! (but it's indeed a new lemma introduced in this PR.)
There was a problem hiding this comment.
Actually we have multiset.has_coe from list to multiset which is a quotient map, so it's surjective and seldom injective. There are many other examples of quotient maps as coercions in mathlib as well:
quotient_group.has_quotient.quotient.has_coe_t
quiver.weakly_connected_component.has_coe_t
add_circle.has_coe_t
So I don't see why we shouldn't make multiset.to_finset (also surjective) a coercion and then by transitivity we get coercion from list all the way down to set.
There was a problem hiding this comment.
Oh, I think the problem is that a ∈ m.to_finset isn't be defeq to a ∈ m for m : multiset α. Maybe that's why multiset.to_finset isn't a coercion. But we may still have coercions from multiset and list to set, even though they're neither injective nor surjective ...
|
maintainer merge (By accident, this PR has never been marked awaiting-review, so probably not many people have looked at it, but I think it's good to go!) |
|
🚀 Pull request has been placed on the maintainer queue by alreadydone. |
|
It's a bit odd having this be tagged WIP, so let me delegate this to @YaelDillies to be sure they think it's ready to be merged! bors d+ |
|
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
the
delegated
|
Sorry! What happened is that it went from "PR I'm working on at night" to "quickly needed" without me noticing, and then I forgot to update the label. It's actually ready. bors merge |
Redefine the various `noncomm_prod`s using `set.pairwise`. This has the advantage of having a solid API around monotonicity in the set or in the relation and avoiding checking the trivial `i = j` case.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
set.pairwiseset.pairwise
eric-wieser
added
the
hacktoberfest-accepted
Redefine the various
noncomm_prods usingset.pairwise. This has the advantage of having a solid API around monotonicity in the set or in the relation and avoiding checking the triviali = jcase.