Should Sets be coerced?

Stream: mathlib4

[Miguel Marco]

As commented here, I am writing an API for restricting Sets to subtypes. In particular, if we have a type X and a set A : Set X, I defined a function restrict: Set X → Set ↑A in the natural way, and defined an infix notation ↓∩ for it.

On the other hand, there is also another natural function Set ↑A → Set X that would be the image of the coercion map from ↑A to X. So I wonder if it would make sense to make one of these maps a coercion. Would that break something?

And in case it does make sense, which of the two maps should be the coercion?

[Michael Stoll]

I think the more natural map is from Set ↑Ato Set X; it's the one that is injective. So if there is a coercion, it should be this one. But I'll leave the discussion whether it makes sense to have a coercion here to more experienced people.

[Eric Wieser]

I think this used to be a coercion via coeM, but we turned it off by disabling the monad instance on sets

[Miguel Marco]

What was the reason for disabling it?

[Kyle Miller]

We turned it off because inserting arbitrary coercions, using the special coercion elaborator for Monads, didn't seem appropriate, and it also led to weird internal-looking terms.

Have you done any experiment coercing these sets yet? One of the things we did at the same time was introduce a coercion instance for subtypes.

import Mathlib.Tactic

set_option autoImplicit true

variable (s : Set α) (t : Set s)

#check (t : Set α)
/-
Subtype.val '' t : Set α
-/

[Kyle Miller]

Question about restrict: given that it's the following, does it need an extra notation for it?

variable (s' : Set α)
#check ((↑) ⁻¹' s' : Set s)
/-
Subtype.val ⁻¹' s' : Set ↑s
-/

Though of course s ↓∩ s' would look cleaner and have nicer-looking algebraic rules.

[Miguel Marco]

I just pushed a first prototype here. I think it is a convenient API (I used the opposite order for the notation... not sure which is the right one).

[Miguel Marco]

I haven't experimented yet with coercions. That will be my next step.

[Kyle Miller]

I see, the notation is reverse from what I was expecting. I'd have thought A ↓∩ B would give you A intersected with B in Set A. The mnemonic is that the arrow is that B is being intersected "down to" A.

I also seeing A at the front, since that's sort of the main part of the restriction operator.

[Miguel Marco]

The way i read it is exactly that B ↓∩ A would mean "you take B and intersect it down to A". Incidentally, the one you propose is more compatible with the already existing restrict function.

I am fine with both notations, but would like to have more opinions before fixing one.

Will try to define a coercion and write some more simplification lemmas for that, and for the combination of both maps.

[Kyle Miller]

Miguel Marco said:

Will try to define a coercion

Could you say what you mean here? I'm afraid you might have misunderstood my earlier message -- the coercion already exists.

[Miguel Marco]

There is s coercion from subtypes to types, but I can't coerce a set in a subtype to a set in the ambient type:

This:

example : (Set ↑A) → Set α := by
  intro T
  exact (T : Set α)

does not work.

[Kyle Miller]

Yes there is, that was the point of my code block, to demonstrate that it existed. This works:

import Mathlib.Tactic

variable {α : Type*} (A : Set α)

example : (Set ↑A) → Set α := by
  intro T
  exact (T : Set α)

[Kyle Miller]

docs#Set.instCoeHeadSetElem

(This coercion is shockingly slow... Maybe someone might have some time to diagnose the issue?)

[Miguel Marco]

Oh, I see, I guess I didn't import the right file. Thanks

[Miguel Marco]

One small problem I am having now is that the infoview does not use the notation ↑D; instead, it shows Subtype.val '' D . Is there something else I should import or open?

[Eric Wieser]

Arguably this is a feature; if it showed ↑D then you wouldn't know that you should be looking for lemmas about val and image

[Miguel Marco]

I see. In my case i find it more confusing (specially, I think my students will find it confusing).

[Eric Wieser]

It wouldn't surprise me if the confusion can be better avoided by not using sets of subtypes in the first place; but maybe that's not possible

[Eric Wieser]

(for instance, by using (A B : Set α) (h : B ⊆ A) instead of (A : Set α) (B : Set A))

[Kyle Miller]

Yeah, generally it's better to not work with subtypes if you can help it, but sometimes you can't help it.

[Kyle Miller]

Here's a delaborator for this coercion, lightly tested:

import Mathlib.Tactic

open Lean PrettyPrinter Delaborator SubExpr in
@[delab app.Set.image]
def delab_set_image_subtype : Delab := do
  let #[α, _, f, _] := (← getExpr).getAppArgs | failure
  guard <| f.isAppOfArity ``Subtype.val 2
  let some _ := α.coeTypeSet? | failure
  let e ← withAppArg delab
  `(↑$e)

variable {α : Type*} (A : Set α) (S : Set A)

#check (S : Set α)
/- ↑S : Set α -/

[Miguel Marco]

I want to deal with the subspace topology, so I really need subsets of subtypes, and to relate them with subsets of the ambient type.

[Miguel Marco]

I think I have something ready. Do you think it would be worth adding it to mathlib?

[Kevin Buzzard]

Kyle Miller said:

docs#Set.instCoeHeadSetElem

(This coercion is shockingly slow... Maybe someone might have some time to diagnose the issue?)

import Mathlib.Tactic

variable {α : Type*} (A : Set α)

count_heartbeats in -- 9027
example : (Set ↑A) → Set α := by
  intro T
  exact (T : Set α)

Is 9027 slow?

[Kevin Buzzard]

Here's the instance trace https://gist.github.com/kbuzzard/ba8688ea0007eb30785f1bf2bb7fc337 . Lean's taking 1/3 of a second to go on a merry adventure all around normed ring typeclasses and lattice/order typeclasses and continuous semilinear equiv typeclasses -- but for all I know this is normal and expected.

[Matthew Ballard]

It is hitting FunLike in there

[Kevin Buzzard]

I'm currently lost in a maze of @instCoeTC_2's, all alike

[Matthew Ballard]

#8386 might help

[Matthew Ballard]

Down to 170

[Kevin Buzzard]

All I've learnt so far (by completely unfolding the instance trace, by piping it to a file) is that one way to look for CoeT (Set ↑A) T (Set α) is to look for CoeHTCT (Set ↑A) (Set α) and then for CoeHTC (Set ↑A) (Set α) and then for CoeOTC (Set ↑A) (Set α) and then (via docs#instCoeOTC) for CoeOut (Type u_1) _tc.1 and then (via docs#instCoeOut) for CoeFun (Type u_1) fun x ↦ _tc.1 and then, as you can see from the name, the fun starts (warning: very long line)

[Meta.synthInstance.instances] #[@ZeroHomClass.toDFunLike, @AddHomClass.toDFunLike, @OneHomClass.toDFunLike, @MulHomClass.toDFunLike, @EmbeddingLike.toDFunLike, @RelHomClass.toDFunLike, @StarHomClass.toDFunLike, @SMulHomClass.toDFunLike, @TopHomClass.toDFunLike, @BotHomClass.toDFunLike, @SupHomClass.toDFunLike, @InfHomClass.toDFunLike, @sSupHomClass.toDFunLike, @sInfHomClass.toDFunLike, @NonnegHomClass.toDFunLike, @SubadditiveHomClass.toDFunLike, @SubmultiplicativeHomClass.toDFunLike, @MulLEAddHomClass.toDFunLike, @NonarchimedeanHomClass.toDFunLike, @ContinuousMapClass.toDFunLike, @LocallyBoundedMapClass.toDFunLike, @DilationClass.toDFunLike]

and that's quite a lot to get through. I guess this is exactly what #8386 is trying to avoid.

[Miguel Marco]

I opened a PR in case someone wants to review it.

[Kevin Buzzard]

It has a red x so it's not on the #queue so you're unlikely to get reviewers.

[Miguel Marco]

I don't see what I can do to get rid of the x, a test was skipped for some reason, but all the rest pass.

[Kevin Buzzard]

The error is that you have added a new file but have not edited Mathlib.lean so that it imports the file.

[Miguel Marco]

Oh, I see, thanks.

[Kevin Buzzard]

I'm not sure where you're looking. Another error is that you have a definition without a docstring on line 34 of the file you added, and there are several other errors which you can see on github.

[Miguel Marco]

Ah, silly me. I wasn't scrolling down in the tests list.

[Miguel Marco]

I finally got all the test passed. Thanks for the hint.

[Eric Wieser]

Miguel Marco said:

I don't see what I can do to get rid of the x, a test was skipped for some reason, but all the rest pass.

(just to be clear, posting in Zulip if you have a red X and don't know what to do about it is exactly the right thing to do :smile: )

[Winston Yin (尹維晨)]

Miguel Marco said:

I opened a PR in case someone wants to review it.

I'll take a look. My PR which could've benefited from some subtype topology API was just merged yesterday/today (#8886, bonus points for being a lucky Chinese number), but there's a TODO there where I want to try out your API. Thanks for working on it for mathlib!

[Eric Wieser]

Perhaps I'm coming in a little late with this, but: I am wary of the proposed definition being a good idea, just as I was for docs#Subgroup.subgroupOf. We already have 68 lemmas about (↑) ⁻¹' s (or 14 with the stricter @Set.preimage (Set.Elem _) _ Subtype.val query). Making new semireducible definitions comes with a cost, and in this case that cost is duplicating many of these lemmas, as well as many existing lemmas about preimages.

[Eric Wieser]

Using an abbrev instead of a def would eliminate this cost, though it doesn't help users who don't realize they should be looking for lemmas about preimages

[Anatole Dedecker]

I just posted a related message here (but my concerns are slightly different)

[Yaël Dillies]

I agree we shouldn't be having those new definitions

[Eric Wieser]

Would you argue we should remove the existing Subgroup.subgroupOf too? If we decided that we should have that, then probably we should have the Set version too for consistency.

[Yaël Dillies]

Yes. It should be made notation

[Miguel Marco]

you mean make it abbrev instead of def?

[Yaël Dillies]

No, make it notation

[Miguel Marco]

I tried to replace the definition with

notation:65 lhs:65 " ↓∩ " rhs:66 => (((↑) ⁻¹' rhs) : Set lhs)

but then again the infoview does not show the ↓∩ notation. I am trying to write a delaborator for that... but I haven't figured out the right way to do it.