Zulip Chat Archive
Stream: mathlib4
Topic: !4#3165
Violeta Hernández (Mar 29 2023 at 08:04):
I'm having trouble with set separation.
Violeta Hernández (Mar 29 2023 at 08:06):
Violeta Hernández (Mar 29 2023 at 08:06):
Here I want to use the separation notation defined for ZFC sets. But if I try and do that it just defaults to building a Set ZFSet.
Violeta Hernández (Mar 29 2023 at 08:07):
Even if I write something like ({ y ∈ x | p y } : ZFSet)
Mario Carneiro (Mar 29 2023 at 08:45):
mathlib4 doesn't have a sep class anymore
Mario Carneiro (Mar 29 2023 at 08:45):
or at least, if there is one it doesn't work correctly
Mario Carneiro (Mar 29 2023 at 08:45):
Violeta Hernández (Mar 29 2023 at 08:46):
Is this a thing that will change in the future?
Mario Carneiro (Mar 29 2023 at 08:49):
:shrug:
Eric Wieser (Mar 29 2023 at 09:01):
docs4#Sep exists
Violeta Hernández (Mar 29 2023 at 15:38):
I'm having some more trouble
Violeta Hernández (Mar 29 2023 at 15:38):
This time with docs#Set.map_definable_aux
Violeta Hernández (Mar 29 2023 at 15:43):
The issue is that, as is, the definable condition is an unused argument
Violeta Hernández (Mar 29 2023 at 15:43):
So the linter is complaining
Violeta Hernández (Mar 29 2023 at 15:43):
I have this old PR #15216 where I do in fact prove this computably, though it's probably rotted by now
Matthew Ballard (Mar 29 2023 at 15:45):
If x is unused according to the linter but _ doesn't work, you can use _x
Violeta Hernández (Mar 29 2023 at 15:45):
There are various possible solutions here:
- disable the unused argument linter (if possible)
- remove the
Definableargument throughout the Lean 4 port - get the constructive proof of
map_definable_auxdone
Violeta Hernández (Mar 29 2023 at 15:45):
Oh that works
Violeta Hernández (Mar 29 2023 at 15:46):
Still, I think it would be good to discuss the Definable class
Violeta Hernández (Mar 29 2023 at 15:46):
It makes some proofs "constructive", but we can't really do any computation with sets in any case, so I don't believe it's worth it
Violeta Hernández (Mar 29 2023 at 15:47):
Matthew Ballard said:
If
xis unused according to the linter but_doesn't work, you can use_x
This doesn't work either. The thing is, the argument is genuinely unused, but presumably shouldn't be in the future.
Violeta Hernández (Mar 29 2023 at 15:49):
@Mario Carneiro I vaguely recall discussing Definable in the past, but I don't remember what the conclusion was
Jannis Limperg (Mar 29 2023 at 15:59):
You can always use set_option linter.unusedVariables false in ... if this is a genuine false positive.
Violeta Hernández (Mar 29 2023 at 16:01):
I'll do that for now
Violeta Hernández (Mar 29 2023 at 16:24):
I'm having further trouble here
Violeta Hernández (Mar 29 2023 at 16:24):
Violeta Hernández (Mar 29 2023 at 16:24):
Apparently Lean is eagerly getting rid of the coercion, then telling me there is no coercion
Violeta Hernández (Mar 29 2023 at 16:24):
(coe here is defined in terms of ofSet)
Ruben Van de Velde (Mar 29 2023 at 16:31):
Mark the ofSet definition with @[coe]
Violeta Hernández (Mar 29 2023 at 16:31):
Thanks!
Ruben Van de Velde (Mar 29 2023 at 16:34):
I thought we were going to add that to the error message
Violeta Hernández (Mar 29 2023 at 16:39):
Alright, the port is complete!
Violeta Hernández (Mar 29 2023 at 16:39):
(Modulo open Mathlb3 PRs I want to port simultaneously)
Eric Wieser (Mar 29 2023 at 16:46):
(Modulo open Mathlb3 PRs I want to port simultaneously)
My advice on how to handle this is:
- Finish up the mathlib3 PRs
- Wait for mathport to process the files they touch
- Run
start_port.shagain, which will spit out a commit sha - Either merge or rebase on that commit sha (if this is a non-trivial I can give some extra advice at the time)
Violeta Hernández (Mar 29 2023 at 16:56):
By "finish up" do you mean get the PRs merged?
Violeta Hernández (Mar 29 2023 at 16:56):
If so it's probably easier to do the porting manually, they're not big PRs
Eric Wieser (Mar 29 2023 at 17:03):
It's more work to review forward-ports than it is to review the initial port
Eric Wieser (Mar 29 2023 at 17:03):
Given there is exactly one file unblocked by set_theory.zfc.basic, I would recommend you just finish off everything you want to do in mathlib3 with that file before finishing porting it
Ruben Van de Velde (Mar 29 2023 at 17:33):
Alternatively, abandon the lean 3 work and do everything in mathlib 4 after the port
Eric Wieser (Mar 29 2023 at 17:58):
I think if we want to encourage that approach we need a way to truly freeze a file; once it's been refactored in Lean4, forward-porting is going to be impossible
Eric Wieser (Mar 29 2023 at 17:59):
(unless of course you mean "after the port of all of mathlib")
Ruben Van de Velde (Mar 29 2023 at 18:52):
Yeah, that's a good point. I was thinking about adding more than refactoring
Mario Carneiro (Mar 29 2023 at 19:31):
Violeta Hernández said:
It makes some proofs "constructive", but we can't really do any computation with sets in any case, so I don't believe it's worth it
It's not about computation, it's about being able to construct a model of ZF in lean without choice
Violeta Hernández (Mar 30 2023 at 06:45):
Ah, I understand.
Violeta Hernández (Mar 30 2023 at 06:45):
Should that goal be scoped to the basic.lean file? It's probably going to be quite painful to deal with ordinals in a choice-agnostic way.
Mario Carneiro (Mar 30 2023 at 07:56):
Sure, I mean ordinals in IZF are weird already, so unless we want LEM to be an axiom we can't really do ZF without choice in lean
Last updated: Dec 20 2023 at 11:08 UTC