ZFC definable class

Stream: general

[Violeta Hernández]

Currently, docs#pSet.definable is implemented as a class. Should it be?

[Violeta Hernández]

My instinct says no, given what's been discussed here before: typeclasses are really only useful when there's no nontrivial equalities between objects, and sets/set functions completely break that rule

[Violeta Hernández]

On the other hand, we do have the theorem docs#classical.all_definable stating all functions are classically definable. So maybe this is meant to be used in a way more akin to decidable_eq or decidable_rel

[Violeta Hernández]

(i.e. as an afterthought :stuck_out_tongue:)

[Violeta Hernández]

Oh yeah, I should probably tag @Mario Carneiro who made this class to begin with

[Mario Carneiro]

The intention was to have definability instances for all formulas, but it was too much work at the time and classical.all_definable is an easy workaround using choice

[Mario Carneiro]

the rule for typeclasses is not about whether equalities exist but rather whether it is generally possible to prove all instances purely structurally on the value

[Mario Carneiro]

decidable is a good example of this - there are often nontrivial equalities of decidable instances but the important thing is that you prove that a thing is decidable because it is structurally so

[Violeta Hernández]

Well, in this situation, that should probably be the case

[Mario Carneiro]

There is a metatheorem that says that any ZFC formula is definable, but I don't think it is easy to derive this using only typeclass search because you have to combine many arities of definability

[Violeta Hernández]

Though wouldn't this also be the case for e.g. continuous functions? What was the rationale for not making that into a typeclass again? Feel like this was brought up last time I started a similar discussion

[Mario Carneiro]

The idea is that it shouldn't be necessary to invoke choice to use the axiom of replacement

[Mario Carneiro]

It does hit the same issues as continuous functions

[Mario Carneiro]

the full derivation setup was never done

[Mario Carneiro]

so it's basically a stub right now

[Mario Carneiro]

with the only way to prove definability being all_definable

[Mario Carneiro]

you can of course still do manual proofs for specific formulas, but a tactic would probably be best placed to do the full metatheorem

[Violeta Hernández]

I should mention that I just took care of your to-do: #15216

[Violeta Hernández]

But yeah, I agree that we need further development here

[Violeta Hernández]

Mario Carneiro said:

It does hit the same issues as continuous functions

What were those issues again?

[Mario Carneiro]

typeclass inference doesn't work well under lambdas

[Mario Carneiro]

you would like to reason that because + is continuous and f and g are continuous, \lam x, f x + g x is also continuous, and this is hard for the typeclass system to unify with the necessary instances

[Mario Carneiro]

If you write it in a first order way, like map2 (+) f g, then TC can do it

[Mario Carneiro]

but writing ZFC formulas like that would be pretty painful

[Mario Carneiro]

this is actually how computability/primrec "instances" are done right now, although it should get some automation at some point

[Mario Carneiro]

instances in quotes because they are worked out by hand

[Mario Carneiro]

you get stuff like list_cons.comp (hg.comp fst (fst.comp snd)) (snd.comp snd) where fst.comp snd and snd.comp snd are basically a way to write de bruijn variable references

[Violeta Hernández]

I see

[Violeta Hernández]

So the play here is to move away from instances and into metaprogramming

[Violeta Hernández]

Now would be a great time to actually learn about Lean metaprogramming

[Violeta Hernández]

What sorts of theorems would we want in the case of ZFC though?

[Violeta Hernández]

I can think of a few theorems for functions, like if f is definable, so is lambda x, {f x}, that kind of stuff

[Violeta Hernández]

But what about functions with more inputs?

[Mario Carneiro]

As far as theorems, we would want at least enough theorems so that manual proving would show the metatheorem

[Mario Carneiro]

So that means proving that all the primitives are definable, and forall and implies are definable

[Mario Carneiro]

this is difficult because you need some higher order notions of definability to make everything work out

[Kevin Buzzard]

@Violeta Hernández if you learn metaprogramming you can help with the Lean 4 port! I'm going to try and learn it next week!

[Violeta Hernández]

On a related note, now that I brought ZFC up

[Violeta Hernández]

docs#Class.mem_hom_left and docs#Class.mem_hom_right

[Violeta Hernández]

These seem like bad simp lemmas? For the same reason

example {α : Type*} {x : set α} {a : α} : a ∈ x ↔ x a := iff.rfl

would be a very bad simp lemma

[Yaël Dillies]

I am not so sure, because there indeed is something that decreases when going from the LHS to the RHS, namely the number of coercions.

[Violeta Hernández]

I mean, A x shouldn't be the preferred way to say x ∈ (A : set Set)

[Violeta Hernández]

(the RHS here isn't a coercion, since Class is def-eq to set Set)

[Violeta Hernández]

I see where this is coming from, since there's already another ∈ operator on Class

[Violeta Hernández]

But I'm still not a fan

[Violeta Hernández]

Is it not possible to have two different ∈ instances for a type?

[Violeta Hernández]

Having an instance has_mem Set Class and another has_mem Class Class would solve the problem at hand, but it doesn't seem to work

[Violeta Hernández]

Defining either instance makes the other no longer work

[Violeta Hernández]

I guess we could make an exception and say that A x is actually the proper way to say a set belongs to a class, even if this is blatant definitional equality abuse

[Violeta Hernández]

Here's an alternate idea, maybe we could have a predicate

def mem_set (x : Set.{u}) (A : Class.{u}) : Prop := A x

to hide the def-eq abuse

[Violeta Hernández]

Then change the theorems I mentioned to

@[simp] theorem Class.mem_hom_left (x : Set) (A : Class) : ↑x ∈ A ↔ mem_set x A := sorry

[Violeta Hernández]

We could even go as far as to give custom notation like ∈ₛ for this, but that seems unnecessary

[Violeta Hernández]

I decided to go the mem_set route, and also added of_set for the cast between set Set and Class.

[Violeta Hernández]

#15234

[Mario Carneiro]

These are all technical definitions that are being used in the metamath export. I am against changing any of them

[Mario Carneiro]

Using application on Class is only abuse if we say it is

[Violeta Hernández]

Mario Carneiro said:

These are all technical definitions that are being used in the metamath export. I am against changing any of them

Metamath export? What do you mean?

[Violeta Hernández]

I get that we can do whatever we want with this little bit of code in a leaf file, but I still think it's best to be orderly. If we consider application on set α to be definitional abuse, then the situation surely shouldn't be any different with Class = set Set.

[Violeta Hernández]

It muddles the distinction between Class and Set → Prop (though maybe we don't want to make any such distinction? If so, we should instead document this decision and change Set → Prop to Class throughout).

[Violeta Hernández]

But yeah, I really want to know what that Metamath thing you mention is about. I don't think we should shy away from refactors just because the code is used by someone else.

[Yury G. Kudryashov]

How long does the metamath export you're talking about take? If it's fast, should we run it in the CI so that nobody breaks it by accident? Or could you add comments to definitions that should not be changed because of this export?

[Violeta Hernández]

Oh wait, are you running the entirety of Metamath on top of the mathlib ZFC library?

[Violeta Hernández]

That's both impressive and dreadful

[Violeta Hernández]

I really do think that Class is in an annoying state where its conventions aren't quite consistent (we use Class sometimes and Set → Prop other times and we mix and match with def-eq) and clash with those of mathlib elsewhere (the aforementioned def-eq abuse)

[Violeta Hernández]

But I guess I can live with it if it's needed for that Metamath thing to work, as long as we document things properly

[Violeta Hernández]

But also, would changing definitions to other definitionally equal definitions really break the Metamath export? That's all I'm ultimately suggesting

[Eric Wieser]

@Violeta Hernández, when threads like this spin out PRs, can you make sure to link back to the thread from the PR?

[Violeta Hernández]

Sorry, let me fix that

[Mario Carneiro]

Violeta Hernández said:

I get that we can do whatever we want with this little bit of code in a leaf file, but I still think it's best to be orderly. If we consider application on set α to be definitional abuse, then the situation surely shouldn't be any different with Class = set Set.

We could change the definition to Class = (Set -> Prop) to address this

[Violeta Hernández]

This wouldn't give us many instances automatically

[Violeta Hernández]

If the idea is that Class is morally Set → Prop, and we just define it as set Set to get the instances automatically, that's fine by me

[Mario Carneiro]

Violeta Hernández said:

But yeah, I really want to know what that Metamath thing you mention is about. I don't think we should shy away from refactors just because the code is used by someone else.

Well, mathlib is also used as a basis for other projects. I don't think it is necessary to gratuitously break downstream projects without good reason. (That is, set_theory.zfc only looks like a leaf file because it's not used in mathlib)

[Violeta Hernández]

I mean, mathlib changes so rapidly and Lean is so unpredictable in some aspects that I imagine that most refactors inadvertently break some mathlib dependencies

[Violeta Hernández]

But sure, we should have a good reason for these changes

[Violeta Hernández]

What do you think about replacing Set → Prop by Class, and explaining in a docstring that Class is morally Set → Prop?

[Violeta Hernández]

Would that break that Metamath thing?

[Mario Carneiro]

Yury G. Kudryashov said:

How long does the metamath export you're talking about take? If it's fast, should we run it in the CI so that nobody breaks it by accident? Or could you add comments to definitions that should not be changed because of this export?

It's somewhere in the 30 min range. I generally treat it as an external project which depends on mathlib, it has very few dependencies and they are all in the set_theory.zfc file

[Mario Carneiro]

Changing definitions without changing defeqs probably won't actually break things, since the export generates a lean source file with no tactics and lots of @ to avoid any lean weirdness so the only thing that would cause problems is typechecking failure due to changed definitions

[Mario Carneiro]

See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Prime.20number.20theorem.20in.20lean/near/168472336

[Violeta Hernández]

Another question

[Violeta Hernández]

Is docs#Class.to_Set another one of those definitions used in the Metamath export?

[Violeta Hernández]

If we were to replace Set → Prop by Class, then to_Set would just be a restatement of the ∈ predicate on classes

[Violeta Hernández]

(and by the way, I also want to inline Class.mem into the has_mem instance, would that break things?)

[Violeta Hernández]

Actually, more generally: what am I allowed to change, and would it be easy for me to fix the Metamath thing if anything broke?

[Mario Carneiro]

Another project that depends on ZFC is the independence of CH

[Mario Carneiro]

metamath will use Class.mem and Class.of_Set for sure but it may not use application

[Mario Carneiro]

as for going in and refactoring the export, you might be able to but you might need a different skill set to do it since part of it is written in haskell

[Mario Carneiro]

Most of the stuff that is likely to break is in basic.lean or post.lean

[Violeta Hernández]

Oh, it's good to have that reference

[Alex J. Best]

Maybe there is some small subset of the metamath export the that could be added to archive, at least to avoid breaking the whole thing.

[Mario Carneiro]

zfc_extra.lean is kind of a for_mathlib file

[Violeta Hernández]

I could port those theorems over if you want

[Mario Carneiro]

and as you can see most of this hasn't been touched since 2019

[Mario Carneiro]

but I tend to work in areas that don't break all that often so it probably still works

[Violeta Hernández]

Are these files generated automatically?

[Mario Carneiro]

no, the files I linked are all manual, the automatic stuff is not checked in

[Mario Carneiro]

well, most of basic.lean is based on an automatically generated file

[Mario Carneiro]

it's more sensitive to changes in set.mm than it is to changes in lean/mathlib

[Violeta Hernández]

Oh perfect

[Violeta Hernández]

I'll tread carefully to avoid breaking it, but I doubt I will with what I have in mind

[Mario Carneiro]

https://github.com/digama0/mm0/blob/build/mm0-lean/mm0/set/set.lean is one of the autogenerated files (it's broken into 6 parts)

[Violeta Hernández]

#15248

[Violeta Hernández]

What's up with the line just above docs#Set.mem_Union?

[Violeta Hernández]

That's global notation, right? Which I presume overrides the meaning of ⋃ elsewhere

[Violeta Hernández]

If so, that's really silly, since that notation is only used once

[Violeta Hernández]

Regarding both this and the similar notation for Class, what should be done? Should these be localized, prefixed/suffixed with something else, or is there no point in having them?

[Kyle Miller]

Violeta Hernández said:

That's global notation, right? Which I presume overrides the meaning of ⋃ elsewhere

Yes, it's global notation if you import it, but no it doesn't necessarily override the meaning of ⋃ since Lean has a notation disambiguation system. However, this one seems problematic since it has a different sequence of parsing actions from those for set.Union. I believe this is why set.sUnion uses ⋃₀.

[Kyle Miller]

Violeta Hernández said:

If so, that's really silly, since that notation is only used once

Don't forget that just because something isn't used in mathlib doesn't mean it's not used by someone that uses mathlib as a dependency. This seems like something someone might want to use.

[Violeta Hernández]

Kyle Miller said:

However, this one seems problematic since it has a different sequence of parsing actions from those for set.Union. I believe this is why set.sUnion uses ⋃₀.

Should we suffix the notation for Set.Union too, then?

[Kyle Miller]

That seems reasonable to me. I don't know what @Mario Carneiro thinks (and I've never used the ZFC module myself), but I'd expect that the intent is that the ZFC API closely mirror the set API wherever possible.

[Violeta Hernández]

I don't have any good ideas for suffixes though...

[Violeta Hernández]

I wanted to be lazy and do a subscript Z for ZFC but that doesn't exist in Unicode

[Kyle Miller]

Oh, I thought when you said "should we suffix the notation" that we were talking about using ⋃₀, which should work.

[Violeta Hernández]

But that means we'll still have a clash

[Violeta Hernández]

Is clashing with ⋃₀ somehow better than clashing with ⋃?

[Junyan Xu]

might consider using superscript ᶻ (reference)

[Kyle Miller]

@Violeta Hernández Yes, Lean should be able to disambiguate it better because it has the same "shape" vs ⋃. That's what I was referring to with parser actions.

[Kyle Miller]

Lean takes all possible parses and uses types to try to choose a single possibility. I don't think it works when one uses binders and the other doesn't, but I haven't checked yet.

[Mario Carneiro]

I think the notation should be ⋃₀ and the name should be sUnion for consistency with data.set.basic

[Violeta Hernández]

Kyle Miller said:

Violeta Hernández Yes, Lean should be able to disambiguate it better because it has the same "shape" vs ⋃. That's what I was referring to with parser actions.

I tested this and it doesn't seem to be the case. Lean Web Editor

[Violeta Hernández]

It tries using set.sUnion instead

[Kyle Miller]

@Violeta Hernández That example uses notation `⋃₀ ` instead of prefix `⋃₀ `:110, which would instead ensure the two unions have the same parsers. (See this.)

import set_theory.zfc

prefix `⋃₀ `:110 := Set.Union

def union (x y : Set) : Set := ⋃₀ {x, y}

[Kyle Miller]

One way to check this is that with the first version you have

notation `⋃₀ ` := Set.Union
#print notation ⋃₀
/-
`⋃₀`:110 := Set.Union
`⋃₀`:110 _:110 := set.sUnion #0
-/

but with the second you have

prefix `⋃₀ `:110 := Set.Union
#print notation ⋃₀
/-
`⋃₀`:110 _:110 :=
  | set.sUnion #0
  | Set.Union #0
-/

I believe that's what you need to see (options with |) for the disambiguation system to actually work.

[Violeta Hernández]

#15352