Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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(Set): API for subset restriction and coercion to/from subtypes #9940
[Merged by Bors] - feat(Set): API for subset restriction and coercion to/from subtypes #9940
Changes from 31 commits
5728467
971becf
6a12b09
e08c6bc
1975bf6
4ab3575
ae9d2eb
c70e7f1
84caaac
7164b8a
719245c
30d5bb6
b5b8167
04d6ea6
5d3225e
2fade3f
62de577
a2c18ab
061639a
6f03f51
19135ec
2c6a5da
1d4a7ca
c56a2d1
541411f
5355712
6155396
7763f33
3775fa8
09e1d4f
90e8caa
46fd5f6
3457096
4ad83b2
6781c2d
6ec74cb
b5e347e
98a48d3
eb21b6a
c6bf7a3
da816ed
9eca74e
03dcb27
69a2365
cb8d85b
File filter
Filter by extension
Conversations
Jump to
There are no files selected for viewing
Check failure on line 121 in Mathlib/Data/Set/Functor.lean
Check failure on line 121 in Mathlib/Data/Set/Functor.lean
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'd argue we should state this as
because this matches the direction of
Subtype.image_preimage_coe
.Alternatively, we could flip
Subtype.image_preimage_coe
and related lemmas to match.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.
In my initial implementation, I actually used the notation
B ↓∩ A
(as in meaning, "B
is pulled down toA
), and hence, this kind of results matched other existing results. With that notation, it totally made sense to use the expression you mention.By @winstonyin suggestion I changed the notation, and then I am not so sure (It is kind of nice to "just change
B ↓∩ A
toB ∩ A
").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 think whatever the notation,
Subtype.preimage_val_eq_preimage_val_iff
should be changed if needed to have the sensible order (I don't thinkA ↓∩ B ⊆ A ↓∩ C ↔ B ∩ A ⊆ C ∩ A
is sensible). I would prefers ∩ t = s ∩ t
because prefix operators are more common than postfix operators, and I'm seeing(s ∩ .)
as a prefix operator.I had suggested the current meaning of
A ↓∩ B
. Here are the options:Use
A ↓∩ B
to mean "an intersection down to the subtype forA
". I suggested this because I am seeing this as a prefix operator(A ↓∩ .)
whereA
is configuration for the operator (it sets the type of the result too).Use
B ↓∩ A
to mean "an intersection withA
whereB
is pulled down toA
". If this notation is like a type-ascription-based-coercion, then it has some parallel with(. : Set A)
for the inverse operation, assuming that would trigger a coercion (though prefix arrow is also the inverse operation). (This is a matter of taste, but I would find the arrow on the other side to be easier to read, as inB ∩↓ A
, but again, that's just personal taste.)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 do agree that the down arrow is better placed in the side of the set that acts as subtype (that is, the place where you are "going down" to.
Your argument about prefearing a prefix operator makes sense.... but then we get that
preimage_val_subset_preimage_val_iff
will either have a weird change of order in the statment, or go in a different direction thatSubtype.image_preimage_coe
.So, I see the following possible options:
Subtype.image_preimage_coe
.Subtype.image_preimage_coe
, as @eric-wieser suggests. The problem with that option is that we get the weird change of order in the operands in the statement.B ∩↓ A
. That solves both the inconsistencies withSubtype.image_preimage_coe
and the order of operands. The problem here would be it is a postfix operator.Subtype.image_preimage_coe
. That could be quite messy, since many results in mathlib depend on it.My vote would go to 1 or 3. I personally don't like much 2. and 4. means opening a can of worms that i would rather not deal with.
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.
For what it's worth, I don't see any reason
Subtype.image_preimage_coe
needs to be in its current form, and changing it (later) to((↑) : s → α) '' (((↑) : s → α) ⁻¹' t) = s ∩ t
seems perfectly fine (and maybe better?). I'm through half of mathlib so far testing out the changes.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.
So, since some proofs in this PR would be affected by that change, shall we include that PR as a dependency for this one? Or just go on and make the change later?
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.
Now that #10433 is merged, this lemma probably belongs next to
Subtype.preimage_val_eq_preimage_val_iff
in theSubtype
namespace (and in the other file).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.
What is the right way to handle the merging of a branch that this depends on? merging main branch into this one? rebase?
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.
Merging the
master
branch should workThere 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 moved that lemma to the
Image
file.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 think this should be proven for the case of a general preimage, since the proof doesn't mention
val
.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.
(or maybe we should just have a lemma that says
⋂₀ { f B | B ∈ S } = ⋂ B ∈ S, f B
, since the latter is the preferred spelling)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.
You mean for arbitrary
f : Set α → Set β
?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 think this lemma is fine to have, at least to specialize the notation and for discoverability.
@eric-wieser
Set.preimage_sInter
is that general lemma.I guess the question is whether the RHS should instead be
⋂ B ∈ S, (A ↓∩ B)
. That way the proof of this lemma would be exactlySet.preimage_sInter
.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 think the RHS should indeed be changed (here and elsewhere)
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.
So the general idea is to avoid
⋂₀
in general, and change it to⋂
(and same for unions)?I have the opinion that it is nice to have lemmas that allow one to rewrite expressions with
⋂₀
into other expressions with⋂₀
, without converting them into⋂
. It reflects better some of the arguments we use on paper.As @kmill commented, there is already a lemma that gives the other equality.
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.
If you feel strongly about this, then the resolution would be to change
Set.preimage_sInter
to have this statement instead of the current one (in a separate PR, and after discussion on zulip). We should try to avoid making difference choices to the same question in different files.If we really were to change it, I'd argue that the RHS of the lemma should be
⋂₀ ((A ↓∩ .) '' S)
since that's the canonical spelling of a set image.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.
what do you think @kmill ?
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 it make sense to have both? Call this variant
preimage_val_sInter_eq_sInter
?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 just added it.