Zulip Chat Archive

Stream: mathlib4

Topic: Changing `Rel` to `Set (α × β)`, to help uniform spaces

Patrick Massot (May 12 2025 at 12:33):

@Yaël Dillies I think we should try to converge on this one. The PR currently doesn’t compile. Is it because you are actively working on it? Or did it rot? I don’t mind splitting stuff from the uniform space file as long as the definition of uniform space doesn’t change and you don’t call entourages things that are necessarily symmetric.

Yaël Dillies (May 12 2025 at 14:18):

It's because I started doing the thing above of making Rel into an "actual thing" rather than being another name for α → β → Prop. The issue is that a lot of files actually do rely on Rel not being an "actual thing" and freely pass between Rel α β and α → β → Prop. I think it's quite bad that things are done this way, but as you can see from #23181 I am finding it difficult to fix (although I do think #23181 would be an improvement when it finally passes CI

Yaël Dillies (May 12 2025 at 14:18):

Incidentally I was on holiday for two weeks, so didn't have spare time to fix it

Patrick Massot (May 12 2025 at 14:47):

Ok, so you need more time. This is fine, I was mostly worried that everything was blocked by some lack of decision.

Yaël Dillies (May 12 2025 at 19:37):

Correct, although I would be happy with some input on whether you think I am going in the right direction here

Yaël Dillies (May 12 2025 at 19:38):

eg maybe @Junyan Xu is against me changing the definition of docs#RelSeries in #23181

Eric Wieser (May 12 2025 at 19:44):

Yaël Dillies said:

In the uniform space world, the uncurried approach is forced upon by docs#Filter, and in particular docs#uniformity which has type Filter (α × α).

Could this be resolved by switching to docs#Order.PFilter, since the lattice structure on relations matches the lattice of their sets?

Eric Wieser (May 12 2025 at 19:44):

(I think Filter vs PFilter has been discussed quite a lot in the past...)

Aaron Liu (May 12 2025 at 19:46):

Order.PFilter has its order backwards from normal filters though...

Yaël Dillies (May 12 2025 at 19:55):

Eric Wieser said:

ould this be resolved by switching to docs#Order.PFilter, since the lattice structure on relations matches the lattice of their sets?

I have thought about this but:

PFilter is severely underdeveloped, to the point where I think it should be first removed, then added again.
This would be quite impactful to the uniform spaces library, although I see no insurmontable roadblock

Patrick Massot (May 12 2025 at 20:33):

We cannot switch to PFilter unless you manage to rewrite the whole topology library in a way that is completely invisible to users.

Patrick Massot (May 12 2025 at 20:34):

The current setup is simply too great.

Eric Wieser (May 13 2025 at 00:30):

Defining Filter as a special case of PFilter and then slowly generalizing would be a way to do that without too much pain, but that of course doesn't mean it would be worth it

Yaël Dillies (Jun 08 2025 at 12:31):

I have news for this topic. I finally gathered my courage and two hours of my time to get #25587 building. It is a proposal to redefine Rel as

abbrev Rel (α β : Type*) := Set (α × β)

This makes it less see-through (not in the transparency sense, but in the API leakage sense) and directly usable in the theory of uniform spaces

Yaël Dillies (Jun 08 2025 at 12:32):

Please read the PR description, it is pretty long and informative

Jireh Loreaux (Jun 08 2025 at 15:52):

From the PR description:

A relation can still be defined explicitly with nice notation: What was previously fun a b ↦ R a b becomes {(a, b) | R a b}.

I was confused about this at first, but then I realized that you meant: "... still be defined from a function R : α → β → Prop with nice notation ..."

Edward van de Meent (Jun 08 2025 at 16:10):

so... the goal of this PR is to exchange one kind of defeq abuse with another?

Edward van de Meent (Jun 08 2025 at 16:13):

Also from the PR description:

The use of α × β means that one can't abuse the defeq of Rel α β with the function type α → β → Prop.

The use of Set is an extra layer of indirection to avoid automation confusing Rel α β with α × β → Prop.

It can directly be used in the theory of uniform spaces because of the syntactic equality between Rel α α and Set (α × α).

sounds like you're not really sure if you do or do not want to use defeq...

Edward van de Meent (Jun 08 2025 at 16:17):

in particular it seems to me like these points respectively basically say:

we don't want to use Rel α β := α → β → Prop as defeq
we also don't want to use Rel α β := α × β → Prop as defeq
we do want to use Rel α α := Set (α × α) as defeq

all of those points were listed as advantages, but i don't agree that these are advantages...

Jireh Loreaux (Jun 08 2025 at 17:13):

Edward, note that the point is that you don't want to abuse defeq at default transparency (as per usual), but making Rel (the function version) an abbrev is pretty much pointless, but Rel (the Set version) an abbrev is still useful. This is what Yaël has done.

Edward van de Meent (Jun 08 2025 at 17:16):

aha, so the idea is "we're making Rel an abbrev, but the function version is not suited to that, whereas the Set version is"?

Yaël Dillies (Jun 08 2025 at 17:17):

Jireh Loreaux said:

I was confused about this at first, but then I realized that you meant: "... still be defined from a function R : α → β → Prop with nice notation ..."

Thanks for pointing out! I have edited

Eric Wieser (Jun 08 2025 at 19:24):

But simply making it an abbrev would kill the point of having a separate less see-through type to perform relation operations on.

I don't understand this claim; even if see-through, it provides value via dot notation

Yaël Dillies (Jun 15 2025 at 14:44):

Yes, but tactics are free to unfold the type and therefore deprive you of dot notation

Yaël Dillies (Jun 15 2025 at 14:44):

#25587 is ready for review again, with a slightly smaller diff thanks to Eric

Yaël Dillies (Jul 02 2025 at 17:26):

May I bump #25587 about refactoring Rel? @Rémy Degenne just redid the final definitions that this preliminary PR is leading to

Eric Wieser (Jul 06 2025 at 14:13):

So is the plan now to change docs#RelHom to use the new spelling? What about docs#DecidableRel ? docs#List.Sorted ?

Eric Wieser (Jul 06 2025 at 14:17):

I'm curious if @Mario Carneiro has any thoughts here (pinging since I assume the thread title made you skip this thread)

Yaël Dillies (Jul 06 2025 at 14:17):

I have no further plans. My own use case with uniform spaces and metric nets is unlocked. For the time being, there is docs#Rel.Hom, which is a specialisation of RelHom to docs#Rel

Mario Carneiro (Jul 06 2025 at 16:49):

I have to admit I preferred when Rel A B meant A -> B -> Prop reducibly

Yaël Dillies (Jul 11 2025 at 15:55):

The next two PRs in the sequence are ready for review:

Yaël Dillies (Jul 11 2025 at 15:55):

#26988 feat(Rel): more API

Yaël Dillies (Jul 11 2025 at 15:57):

#23181 refactor(Topology/UniformSpace): use Rel

Fabrizio Montesi (Jul 11 2025 at 20:03):

I notice this only now because of the title about uniform spaces, sorry for joining late. Have you considered renaming Rel to something else or moving it? If Rel is the 'standard' type for relations, it's weird that things like < are not Rels.

I guess those of us who used the old version can also just make our own abbrev and use the results about Relation?

Yaël Dillies (Jul 11 2025 at 20:14):

Rel never was the standard type for relations. The standard type always was α → β → Prop. I've simply made Rel into something distinct enough to the standard type that it is useful

Kenny Lau (Jul 11 2025 at 20:22):

cc @Fabrizio Montesi

Fabrizio Montesi (Jul 12 2025 at 09:16):

Yaël Dillies said:

Rel never was the standard type for relations. The standard type always was α → β → Prop. I've simply made Rel into something distinct enough to the standard type that it is useful

Oh, it seems we've misused/misinterpreted it downstream then. Since Rel was an abbreviation for the standard thing, we took it as a convenience with accompanying theorems for working on the usual thing.

We'll update our own APIs so not to use Rel unless we really want pairs, and switch to using theorems for Relation. Is Relation gonna stay as is? I'm asking also because I expect people in our Lean projects to ask me if they could define Relation as an abbreviation for the usual thing. (The old Rel.)

Yaël Dillies (Jul 12 2025 at 09:46):

I have no plans to destroy the Relation API :sweat_smile:

Eric Wieser (Jul 13 2025 at 14:07):

I'm beginning to think we should revert the Rel change, and reintroduce the API it presents as ~~CurriedRel or~~ Prod.Rel or Set.Rel instead

Fabrizio Montesi (Jul 13 2025 at 14:33):

If it happens, I like the latter two better. CurriedRel (or CRel) evokes the standard type.

Eric Wieser (Jul 13 2025 at 15:08):

Sorry, I always confuse curried and uncurried. Indeed CurriedRel means the wrong thing!

Eric Wieser (Jul 24 2025 at 23:02):

Some more threads of fallout:

Eric Wieser (Jul 24 2025 at 23:03):

(edit: inlined above)

Eric Wieser (Jul 24 2025 at 23:25):

#27447 moves Rel into the Set namespace, so that we can put the old Rel (at least, the abbrev) back where it was

Fabrizio Montesi (Jul 25 2025 at 07:46):

FWIW, I think the move to the Set namespace makes good sense.

Eric Wieser (Jul 25 2025 at 10:28):

The above now passes CI. Ideally we would decide whether to merge it before the next mathlib tag is cut.

Fabrizio Montesi (Jul 25 2025 at 12:57):

@Eric Wieser Do you see anything wrong with (not necessarily in mathlib, we could do it elsewhere):

Calling the old Rel Function.Rel?
Giving an API and notation to Function.Rel (I want union, inversion, etc.), which would basically just call appropriate stuff in Relation or similar.

Eric Wieser (Jul 25 2025 at 13:00):

#27447 currently reintroduces it as Rel, rather than Function.Rel

Notification Bot (Jul 25 2025 at 13:11):

8 messages were moved from this topic to #Is there code for X? > Union of relations by Eric Wieser.

Yaël Dillies (Jul 25 2025 at 15:44):

What do people think of SetRel instead of Set.Rel, to avoid name clashes?

Fabrizio Montesi (Jul 26 2025 at 07:47):

Fabrizio Montesi said:

Eric Wieser Do you see anything wrong with (not necessarily in mathlib, we could do it elsewhere):

Calling the old Rel Function.Rel?

Giving an API and notation to Function.Rel (I want union, inversion, etc.), which would basically just call appropriate stuff in Relation or similar.

Forget all that. I now realise that the old Rel API made me (wrongly) think that the Lean core API and mathlib were lacking several things about relations, which are actually in there. Thanks @Eric Wieser for all the pointers.

Yaël Dillies (Jul 26 2025 at 08:37):

That seems like a strong argument that my change to Rel shouldn't be reverted? "Downstream users discover they have been using the wrong API this whole time"

Eric Wieser (Jul 26 2025 at 09:48):

I think moving the API was reasonable, but I think some downstream users are using Rel as just a nice spelling to avoid writing Prop

Fabrizio Montesi (Jul 26 2025 at 09:49):

Yaël Dillies said:

That seems like a strong argument that my change to Rel shouldn't be reverted? "Downstream users discover they have been using the wrong API this whole time"

I was just gonna write something in that spirit. And for the same reason I think it shouldn't be called just Rel. Set.Rel with appropriate doc would be fine.