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] - fix(Data/Set/Image): simp confluence issues with image_subset_iff
#8683
Conversation
`image_subset_iff` is a questionable simp lemma because it converts an application of image into preimage unconditionally. This means that if any simp lemma applies to applications of images, there must be a corresponding lemma for applications of preimage. These lemmas are what I found missing after loogling.
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
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.
I am now convinced this is a good change.
Would you mind checking that the analogous situations for Finset
are confluent?
@@ -654,6 +654,7 @@ theorem empty_ne_univ [Nonempty α] : (∅ : Set α) ≠ univ := fun e => | |||
theorem subset_univ (s : Set α) : s ⊆ univ := fun _ _ => trivial | |||
#align set.subset_univ Set.subset_univ | |||
|
|||
@[simp] | |||
theorem univ_subset_iff {s : Set α} : univ ⊆ s ↔ s = univ := |
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.
Would you mind adding the corresponding lemma for Finset
?
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
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
I don't believe there is an analogous confluence issue for |
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.
maintainer merge
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
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.
Looks good to me, thanks!
bors r+
…8683) `image_subset_iff` is a questionable simp lemma because it converts an application of `Set.image` into an application of `Set.preimage` unconditionally. This means that if any simp lemma applies to images, there must be a corresponding lemma for preimages. These lemmas are what I found missing after loogling. I also added machine-checked examples of each confluence issue to a new file `tests/simp_confluence`.
Pull request successfully merged into master. Build succeeded: |
image_subset_iff
image_subset_iff
…8683) `image_subset_iff` is a questionable simp lemma because it converts an application of `Set.image` into an application of `Set.preimage` unconditionally. This means that if any simp lemma applies to images, there must be a corresponding lemma for preimages. These lemmas are what I found missing after loogling. I also added machine-checked examples of each confluence issue to a new file `tests/simp_confluence`.
image_subset_iff
is a questionable simp lemma because it converts an application ofSet.image
into an application ofSet.preimage
unconditionally. This means that if any simp lemma applies to images, there must be a corresponding lemma for preimages. These lemmas are what I found missing after loogling.I also added machine-checked examples of each confluence issue to a new file
tests/simp_confluence
.