definition of enat

Stream: general

[Tomas Skrivan]

Why is enat defined as roption nat? I was expecting the definition to be something like def enat := ℕ⊕unit. For example, I have tried to write function returning previous enat and after half an hour I gave up. With the definition def enat' := ℕ⊕unit it is simple:

def prev : enat' → enat'
| (sum.inl 0) := sum.inl 0
| (sum.inl (n+1)) := sum.inl n
| (sum.inr _) := sum.inr unit.star

with appropriate coercions and notations(e.g. ∞=sum.inr unit.star) this can be really easy on the eyes.

My conjecture is that enat is quite often a result of some decision process(decidable or not), so with the definition roption nat this decision is embedded inside of enat. I find this really strange and makes enat not user friendly when used purely as a constructive object.

[Kevin Buzzard]

I was expecting it to be option nat. roption is very hard for people who aren't "constructive-aware" (like me!) to work with, I agree.

[Mario Carneiro]

One way to write prev is roption.map nat.pred

[Mario Carneiro]

we could add (classical) enat.cases_on to partially address this, but lean is stingy about changing the default equation compiler logic so that's harder

[Tomas Skrivan]

option nat would be also fine. But with enat defined as roption nat I will probably just split every function in two to handle finite and infinite case. My use case is to define classes of finitely and infinitely differentiable functions.

[Kevin Buzzard]

One code block I find helpful for dealing with enat is docs#padic_val_rat

[Kevin Buzzard]

Here, Rob Lewis wants to define the p-adic valuation of a rational number, and he uses multiplicity to compute it, but multiplicity returns an enat. He deftly turns it into an integer using roption.get

[Mario Carneiro]

There is roption.to_option already to turn the roption into an option for case analysis

[Mario Carneiro]

but using roption directly encourages a style where you don't handle the infinity case separately but it's implied from the finite case

[Mario Carneiro]

Even if it was defined as an option, I wouldn't recommend casing on it because using none : enat is bound to cause type class inference problems because none literally has type option nat not enat

[Mario Carneiro]

instead, just apply a dedicated enat.cases_on lemma that can use the right idioms for the two cases

[Mario Carneiro]

and that way, the underlying definition does not have to be scrutinized, and so you won't even be able to tell if it's option or roption under the hood

[Tomas Skrivan]

It will take me some time to digest this and understand that roption is a more favorable design choice then option here. But thanks a lot for the explanation!

[Mario Carneiro]

whether it's actually more favorable overall is not clear, but it is clear that we don't want to leak API details so any operation that demonstrates the difference should probably be avoided

[Gabriel Ebner]

I also agree, it should be with_top nat.

[Kevin Buzzard]

I agree, I shouldn't really have mentioned option.

[Yury G. Kudryashov]

We already have $C^\infty$ functions, see docs#times_cont_diff_on

[Yury G. Kudryashov]

And this definition uses with_top nat

[Tomas Skrivan]

However they are defined only between normed spaces. I want the definition of conveniently smooth map between locally convex spaces.