Should docs#Finset be docs#SetLike ?

Stream: mathlib4

[Yaël Dillies]

Recently, @Junyan Xu added a docs#SetLike instance for docs#Finset in #28241. While this instance is valid, @Eric Wieser had told me years ago that this was not the intended use case for SetLike, and instead that it should be reserved to subobjects. In this instance, I find it damageable that docs#Finset.toSet was deprecated, as it was a very convenient way to insert the Finset to docs#Set coercion exactly where needed.

[Yaël Dillies]

What do people think?

[Floris van Doorn]

Do you remember the reasons why Finset shouldn't be SetLike? Or can you link to a conversation where this was discussed?

[Jovan Gerbscheid]

One annoying thing is that this doesn't work:

variable (x : Finset Nat)
#check (x : Set _)

Even though this does:

variable (x : Nat →₀ Nat)
#check (x : _ → _)

[Yaël Dillies]

Absolutely. The lack of "functorial coercions" is particularly felt around the finset API

[Kenny Lau]

semirelatedly i've been struggling with that a lot in the hom classes, I think this is a well-known issue here

[Kenny Lau]

is it possible to write a macro to fix that? like alg% x

[Anne Baanen]

Yaël Dillies said:

Eric Wieser had told me years ago that this was not the intended use case for SetLike, and instead that it should be reserved to subobjects.

To make this less vague, this seems to be Eric's actual objection:

@Eric Wieser said

I think I remember what I find weird about this; no other SetLike instances implement the set notation lattice operators.

[Anne Baanen]

When I implemented a CoeSort Finset instance (back when it was spelled has_coe_to_sort finset), there was some feeling that this instance had to be missing for a reason. But it really did improve the situation.

[Anne Baanen]

I agree though that it is currently a pain to convert things to a Set _. Can we fix this by writing a better elaborator that inserts the right coercion?

[Jovan Gerbscheid]

We would need a change in core to get my above example to work. An easier alternative would be a toSet% s elaborator, which would just be a macro for SetLike.coe s

[Jovan Gerbscheid]

Are there more "functorial coercions" that could benefit from such a core change? If so, that could make for a stronger RFC.

[Etienne Marion]

I also was a bit saddened by the deprecation of Finset.toSet, because when I had a finset s it was nice to be able to write s.toSet.pi to refer to docs#Set.pi, and I now have to spell that .pi (SetLike.coe s) (although I'd be happy to hear if there is a nicer way).

[Kevin Buzzard]

In FLT I changed all X.toSets to (X : Set Y)

[Aaron Liu]

the problem with this is that now you're mentioning the type

[Floris van Doorn]

Jovan Gerbscheid said:

One annoying thing is that this doesn't work:

variable (x : Finset Nat)
#check (x : Set _)

Even though this does:

variable (x : Nat →₀ Nat)
#check (x : _ → _)

Note: this worked in Lean 2. Coercions are a lot more complicated now, but maybe we can ask the Lean FRO if they are willing to investigate whether this is feasible to support.

I'm personally happy to have a macro/notation for Finset.toSet. (Or other "simple" coercions that fire even if the expected type is not fully known).

[Etienne Marion]

Kevin Buzzard said:

In FLT I changed all X.toSets to (X : Set Y)

This does not work in my case, it seems to be because s is Finset.univ:

import Mathlib

variable {α γ : Type*} [Fintype α] {β : α → Type*}
  {f : γ → (a : α) → β a} {s : (a : α) → Set (β a)} {t : Finset α}

#check f ⁻¹' Finset.univ.toSet.pi s -- works but deprecated
#check f ⁻¹' .pi (SetLike.coe Finset.univ) s -- works but verbose
#check f ⁻¹' .pi (Finset.univ : Set α) s -- fails
#check f ⁻¹' .pi (t : Set α) s -- works

[Jovan Gerbscheid]

Oh I see, with Finset.univ, the α is a metavariable on the inside of the coercion instead of the outside of the coercion. That case would also need to be supported by this potential core support. Though it should work with the toSet% that I desceibed above.

[Kenny Lau]

would this also work with the hom problem I mentioned above?

[Kenny Lau]

mwe:

import Mathlib

variable (R : Type*) [Ring R] (f : R →+* R)
#check (f : _ →+ _)

[Floris van Doorn]

cc @Anne Baanen

[Bhavik Mehta]

cc @Kyle Miller since we discussed this coercion a little while ago

[Kenny Lau]

import Mathlib

namespace Lean.Elab.Term

-- to be replaced with attribute stuff
def homDict : Std.HashMap Name Name :=
  {(``AddMonoidHom, ``AddMonoidHomClass.toAddMonoidHom), (``Set, ``SetLike.coe)}

elab "alg% " f:term : term <= typ => do
  let (head, _) := typ.getAppFnArgs
  let .some ofClass := homDict.get? head | throwError head
  elabTerm (← `($(Lean.mkIdent ofClass) $f)) typ

end Lean.Elab.Term

axiom Foo {A B : Type*} [AddMonoid A] [AddMonoid B] (f : A →+ B) : Prop

variable (R : Type*) [Ring R] (f : R →+* R)
#check Foo f
#check Foo <| alg% f

variable (x : Finset Nat)
#check (alg% x : Set _)

[Kenny Lau]

this new alg% macro solves both problems (actually the same problem) at once (and is very easy to implement)!

[Kenny Lau]

or maybe this is an elaboration order issue again?

[Kenny Lau]

@Aaron Liu do you think this one could be solved by changing the compiler? as in, to have the compiler resolve coercions before filling in all the metavariables

[Aaron Liu]

why would the compiler be relevant

[Kenny Lau]

because the dictionary above looks like one that Lean would already have stored somewhere for constructing coercions

[Aaron Liu]

do you mean the elaborator?

[Kenny Lau]

probably, i'm still not sure what the different parts do

[Chris Henson]

The changes that this caused in CSlib were minor, but I will say that looking through the diff of that PR that I find some of replacements of Finset.toSet to (↑) a bit harder to read, especially in a composition.

[Aaron Liu]

not sure how you could do any coercions without fulling in metavariables

[Kenny Lau]

is my code above a good solution then

[Kenny Lau]

Aaron Liu said:

not sure how you could do any coercions without fulling in metavariables

my code above is essentially doing coercions just by resolving the head symbol without first waiting for all the mvars to be filled in

[Aaron Liu]

I don't like the use of Lean.mkIdent

[Aaron Liu]

Kenny Lau said:

Aaron Liu said:

not sure how you could do any coercions without fulling in metavariables

my code above is essentially doing coercions just by resolving the head symbol without first waiting for all the mvars to be filled in

so it doesn't work if the head symbol is a metavariable

[Kenny Lau]

but the head symbol is often not a metavariable, it's always RingHom, what the elab gets stuck on are its arguments

[Kenny Lau]

see my example in my code

[Kenny Lau]

Aaron Liu said:

I don't like the use of Lean.mkIdent

the head symbol is resolved from a dictionary so there's no syntax position information

[Aaron Liu]

I was referring to this message

Kenny Lau said:

Aaron Liu do you think this one could be solved by changing the compiler? as in, to have the compiler resolve coercions before filling in all the metavariables

[Aaron Liu]

If you don't fill in the metavariables first I think you will get a lot more cases where the head symbol is a mvar

[Aaron Liu]

Kenny Lau said:

Aaron Liu said:

I don't like the use of Lean.mkIdent

the head symbol is resolved from a dictionary so there's no syntax position information

Use the syntax information attached to alg%

[Aaron Liu]

oh I get it now

[Aaron Liu]

wait but you have a fullname

[Kenny Lau]

right now the thing to do (as I've been told) is to write AddMonoidHomClass.toAddMonoidHom f to have the coercion fire automatically, and what I've achieved is just an automatic (and much shorter) version of this

[Kenny Lau]

Jovan Gerbscheid said:

We would need a change in core to get my above example to work. An easier alternative would be a toSet% s elaborator, which would just be a macro for SetLike.coe s

since people upvoted this, do we just want the macro for SetLike, or would it also be a good idea to extend this to other FunLike classes in the hierarchy like in my example code above?

[Jireh Loreaux]

Kenny, there has been discussion of removing all the HomClass.toHom coercions (as actual coercions, but keeping them as defs). Along with this, we will probably rename them all to Hom.ofClass (to match their SetLike counterparts). So in cases there the expected type is known, you should be able to simply write .ofClass f.

[Jireh Loreaux]

So I don't think a dedicated elaborator will be necessary (but perhaps I'm overlooking something).

[Kenny Lau]

@Jireh Loreaux do you have a link to such a discussion?

[Jireh Loreaux]

It's been discussed privately among reviewers (primarily to make sure we had consensus among that group, as it's a nontrivial change). I will post about it publicly soon.