ZFC hom renames

Stream: maths

[Violeta Hernández]

I'd like to get input from @Mario Carneiro on this. @Yaël Dillies was suggesting a rename of the Class hom lemmas (e.g. docs#Class.mem_hom_left, docs#Class.union_hom) to use coe instead (e.g. Class.coe_mem, Class.union_coe).

[Violeta Hernández]

I agree with the rename, but I recall that renaming things in this specific file was iffier than for others.

[Kevin Buzzard]

Why not just hold off on these kinds of questions until after the port to lean 4? Why not try and get this stuff ported instead and then have the discussion about changing the lean 4 files?

[Yaël Dillies]

because changing the Lean 4 files can only happen once the port is over, namely in 6 months?

[Johan Commelin]

$ rg "import set_theory.zfc"
src/set_theory/zfc/ordinal.lean
7:import set_theory.zfc.basic

[Johan Commelin]

There is only 1 file in mathlib that depends on this file (set_theory/zfc/ordinal.lean is a leaf).

[Johan Commelin]

So I think that after porting this file, it should feel free to change even if the port isn't done yet.

[Johan Commelin]

I'm not aware of plans to make other files in mathlib depend on these two files.

[Oliver Nash]

Yaël Dillies said:

because changing the Lean 4 files can only happen once the port is over, namely in 6 months?

Of course people should work on what they enjoy and we are grateful for all contributions but I think it's worth noting that the port will happen more quickly if people divert effort away from Mathlib3 and into the port.

[Mario Carneiro]

I have no objection to the renames, but agree with others that this is added work for the port for no good reason

[Violeta Hernández]

Alright, I was worrying this might conflict with the Metamath in Lean thingy you had mentioned in the past

[Violeta Hernández]

(should have mentioned that specific concern earlier, sorry)

[Mario Carneiro]

Those theorems are not used by the generator, only the definitions are important and the theorems are used in the hand written postprocessing file

[Violeta Hernández]

Regarding the ZFC Mathlib 4 port, it's almost done

[Violeta Hernández]

So hopefully that excuses the following bikeshedding

[Violeta Hernández]

I don't remember if I asked before but, what's the point of docs#Class.of_Set and docs#Class.to_Set?

[Violeta Hernández]

They are exactly identical to the coercion operator and the membership relation, respectively

[Eric Wieser]

In Lean 4, the coercion operator usually requires an underlying definition, because coe is unfolded (re Class.of_Set)

[Violeta Hernández]

That's good to keep in mind

[Violeta Hernández]

Still, if these are entirely auxiliary definitions, I believe they'd be better off being named Class.coe and Class.mem

[Violeta Hernández]

That way it's clear you're supposed to use the other ones

[Eric Wieser]

That way it's clear you're supposed to use the other ones

The up arrow and the function that implements it are syntactically the same in lean 4

[Eric Wieser]

So you should only call it Class.coe if you want that name to appear in the goal view when you hover over the arrow

[Eric Wieser]

I guess since all the lemmas currently call it coe calling the function Class.coe is the least effort

[Violeta Hernández]

Ah, I hadn't grasped the "syntactic" bit

[Violeta Hernández]

Well, if this behavior will change in Lean 4, I can postpone the bikeshedding until then

[Eric Wieser]

The mem stuff hasn't changed, so you could still bikeshed that if you felt the urge

[Violeta Hernández]

Sure, why not

[Violeta Hernández]

It's trivial to port this to Lean 4

[Violeta Hernández]

More so in comparison to the other 1700 lines that file has

[Violeta Hernández]

Oh wait, I'm noticing we already have a Class.mem

[Violeta Hernández]

image.png

[Violeta Hernández]

Surely this means to_Set should go?

[Eric Wieser]

I think you could reasonably delete both mem and to_Set

[Violeta Hernández]

The rest of the file follows the pattern of not inlining instances

[Violeta Hernández]

I recall I had some opposition when I tried to change that a few months ago

[Violeta Hernández]

So I'd rather keep mem for now

[Violeta Hernández]

#18694

[Mario Carneiro]

to_Set and Class.mem are not the same, the argument order is reversed (and this is important, because it is intended to be used partially applied)

[Mario Carneiro]

you should read it as to_Set (B : Class) : Set Class := {A | A \in B}

[Eric Wieser]

Should we change it to actually say that?

[Mario Carneiro]

This file doesn't use Set A, it uses A -> Prop and lambdas, and so it's actually
to_Set (B : Class) : Class -> Prop := fun A => A \in B at which point the usual style guide kicks in and moves A before the colon

[Mario Carneiro]

but we could use the docstring to emphasize that it is actually a unary function with a function codomain even though it looks like a binary function

[Mario Carneiro]

of course there is no difference for the type theory but it affects the sensibility of the name to_Set

[Eric Wieser]

Are you talking about docs4#Set or docs#Set?

[Mario Carneiro]

docs4#Set

[Mario Carneiro]

the A -> Prop one

[Violeta Hernández]

Mario Carneiro said:

This file doesn't use Set A, it uses A -> Prop and lambdas

That's the convention we settled on for classes specifically, under the logic that in vanilla ZFC, classes are really predicates with another name. That discussion is summarized in the docs#Class docstring.

For everything else, I believe it would be best if we used whichever of these two makes the most syntactic sense.

We already use set Class in docs#Class_to_Cong, so there's precedent for this.

[Violeta Hernández]

On this note, isn't to_Set also identical to Class_to_Cong? Both literally and syntactically.