with_top, enat, and with_zero

Stream: general

[Aaron Anderson]

I find myself wishing that enat and with_top, and with_zero and with_bot, had definition equality.
Instead, in each case, one is an option and the other is a roption.

[Aaron Anderson]

I might find myself motivated to try making one of these changes, say, to make enat an abbreviation for with_top nat. Is there a good reason not to do that? I'm not terribly well-versed in the philosophy of decidability here, but I think it doesn't matter much for enat at least. After all, there is already an equiv there.

[Kevin Buzzard]

I find it frustrating that some of these things are definitionally equal because it can lead to leaks where r : with_zero G suddenly magically becomes r : option G and then stuff can break. I also had this vague idea that in Lean 4 we were going to be encouraged to make new structures for all of these? Or am I talking nonsense?

[Aaron Anderson]

Well, I've already found one answer to my question, which is that somehow roptions get around the decidability of ∃ n, P n in the definition of enat.find.

[Aaron Anderson]

Kevin Buzzard said:

I find it frustrating that some of these things are definitionally equal because it can lead to leaks where r : with_zero G suddenly magically becomes r : option G and then stuff can break. I also had this vague idea that in Lean 4 we were going to be encouraged to make new structures for all of these? Or am I talking nonsense?

Perhaps with with_zero and with_bot I'm overreaching with definitional hubris (not that they feel like they should be implemented differently)

[Aaron Anderson]

but the fact that there are times we want with_top nat and times we want enat is really disturbing...

[Kevin Buzzard]

I don't think I ever want enat...

[Kevin Buzzard]

Isn't it just some constructivist nonsense?

[Aaron Anderson]

I'm pretty sure the reason is literally so that you can define enat.find P whenever P is decidable, without needing ∃ n, P n to be decidable.

[Eric Wieser]

Aaron Anderson said:

but the fact that there are times we want with_top nat and times we want enat is really disturbing...

What's the killer feature of with_top, if the killer feature of enat is avoiding decidability for docs#enat.find?

[Eric Wieser]

Is the problem just that one has less API than the other?

[Aaron Anderson]

The problem to me is that I’d like to use the APIs interchangeably (also, I’d like to be able to define additive valuations using with_top, but maybe that’s not critical)

[Aaron Anderson]

I would then just say to change with_top and with_bot to roptions, but maybe soon I will find out a reason that that’s a bad idea

[Kevin Buzzard]

The killer feature of with_top is that option is so easy to use, you just do proofs by cases or with the equation compiler

[Aaron Anderson]

However, with_zero seems to have worked fine as a roption...

[Eric Wieser]

I don't think the earlier statement about docs#enat.find was correct, it has exactly the same decidable assumptions as docs#nat.find

[Aaron Anderson]

That’s correct, but I can’t seem to replicate it with with_top nat

[Aaron Anderson]

At least, not computably

[Johan Commelin]

The killer feature of with_top is probably that you can use the equation compiler to split between nat and infty.

[Gabriel Ebner]

In my eyes, the biggest API problem with enat (and also related to not being able to use the equation compiler) is that it encourages the use of roption.get. That function is pretty unergonomic since you always need to provide a proof that the enat is finite as a second argument.
The roption definition of enat is a tradeoff: enat.find becomes computable, but other operations such as ≤ become noncomputable. I don't think this tradeoff is worth it, and I believe that def enat := with_top nat would be the better choice.

[Yaël Dillies]

If everybody agrees, I'll prepare a PR for that to change.

[Eric Wieser]

Aaron Anderson said:

However, with_zero seems to have worked fine as a roption...

Not sure what you mean by that, src#with_zero is an option, and has been for at least two years.

[Kevin Buzzard]

Yes it's enat which is the roption, and this fact basically renders it unusable for me (I don't know the API and don't see any reason why it shouldn't just be an option but no doubt others do!).

[Yaël Dillies]

Yeah sorry I meant that I will change the def of enat to with_top ℕ. And Aaron probably tried to make with_zero a roption.

[Eric Wieser]

Is it worth keeping enat around as renat?

[Eric Wieser]

Otherwise, is anything else using roption?

[Yaël Dillies]

Yeah, all of Mario's computability stuff.

[Yaël Dillies]

What's weird is to define concrete types with it. That's option's job.

[Eric Wieser]

I think it would probably be good to get @Mario Carneiro to sign off on removal as opposed to renaming

[Eric Wieser]

Certainly enat via roption is annoying to mathematicians, but perhaps it's still useful and just needs to be more hidden.

[Yaël Dillies]

From the above discussion, the argument in favor of roption is mostly to have enat.find computable.

[Kevin Buzzard]

I think that this would be a rather painful refactor and it's not clear to me what we're gaining.

There are tons of places in mathlib where the constructivists have done something and I would have done something different. For example finset is constructive, finsupp and dfinsupp are constructive, enat is constructive etc; I find all of these things hard to work with for various reasons. But just because we now have set.finite and finsum and nat.card doesn't mean that I'm pressing for the removal of finset -- indeed people like Bhavik swear by it for the kind of mathematics they're doing.

[Gabriel Ebner]

I think that this would be a rather painful refactor and it's not clear to me what we're gaining.

A big one that was already mentioned in this thread is support for the equation compiler. We can also reuse all lemmas about with_top. The refactor should be relatively quick (there's only 268 lines mentioning the word enat in mathlib and half of them in data/nat/enat.lean).

[Gabriel Ebner]

I think a big argument for a constructive finset is that you can actually compute with it. You can prove equalities between finsets using dec_trivial, you can print them in the VM, etc.

It is much harder to compute with (the roption version of) enat. Almost no property of enats is decidable: equality is not decidable, order is not decidable. So no dec_trivial. Printing an enat to a string is of course not computable either.

[Mario Carneiro]

I still think roption is the more mathematically natural choice given its topology, but I understand the arguments in favor of option, and the equation compiler in particular is something that API lemmas can't paper over. And the duplication with with_top nat is undesirable. So there is probably no point in me blocking this on purist grounds when it isn't actually helping anyone.

To the extent that the option / roption distinction has been hidden behind an API, it should not be that bad to refactor, although some care (a typeclass?) will be needed to ensure that multiplicity on int comes out computable (which is useful for dec_trivial).

[Gabriel Ebner]

(deleted)