about `PartENat`

Stream: mathlib4

[Jireh Loreaux]

In reviewing #5908 (cc: @Peter Nelson), I came across the existence of docs#PartENat for the first time, which seems to be a computable version of docs#ENat, but otherwise it's the same. Is there anywhere this computability is actually being used? If not, how do we feel about disentangling usage of PartENat in favor of ENat? I think in at least one place, namely, docs#Cardinal.toPartENat (and hence the rest of the cardinality library) there is no reason to use a computable version (@Violeta Hernández). I guess using PartENat makes docs#multiplicity computable, but is this something we care about? @Chris Hughes since I think you created PartENat.

In #5908, it seems that it's only being used because we have docs#PartENat.card, but no docs#ENat.card :tear:.

[Chris Hughes]

I created PartENat. I would have used option, but Mario told me to use roption, which I think is called Part now. I'm not going to strongly defend PartENat.

[Gabriel Ebner]

PartENat is not any more computable than ENat, it's differently computable. With ENat equality is computable while with PartENat finding the smallest number satisfying a decidable predicate is computable. Each of the operations is noncomputable in the other formalism.

[Kyle Miller]

(@Yury G. Kudryashov Do I remember correctly that you were refactoring things involving PartENat/ENat in mathlib3? I thought I remembered it being enat.card at some point.)

[Yury G. Kudryashov]

I started this refactor, then postponed it till after the port. Now I'll need to see what's already done in Mathlib 4.

[Peter Nelson]

That's indeed the reason #5908 uses it - the interactions with it are minimal, but things would have been slightly smoother if there existed ENat.card and a few very basic API lemmas for is (maybe half a dozen). It would be trivial to modify that PR if ENat.card were introduced, or to do so in the future if/when that happens.

[Peter Nelson]

And yes, count me as being in favour of the disentanglement (partly just because ENat has the nice notation).

[Riccardo Brasca]

@María Inés de Frutos Fernández you may be interested in this conversation

[María Inés de Frutos Fernández]

I would vote for keeping only ENat as well. In my experience, it is nicer to work with if you also want to consider with_top Z and the natural map to it.

[Yury G. Kudryashov]

I will try to recover my old lean3 branch with ENat.card and port it to lean4.

[Jireh Loreaux]

@Yury G. Kudryashov if it ends up being a lot of work and not worth trying to salvage, let me know and I can just do it in Lean 4 directly.

[Yury G. Kudryashov]

I have some ideas about how it should be done, so I would prefer to do it myself.

[Peter Nelson]

Any update on this, @Yury G. Kudryashov ? To throw my two very minor cents in, it'd be nice to have the ∞ symbol in place of ⊤ , like we do for the reals.

[Alex J. Best]

Maybe we can accomplish that with a scoped notation or something?

[Yury G. Kudryashov]

I'm sorry for another delay. If I don't do it in a week, then I officially release the hold.

[Kyle Miller]

Alex J. Best said:

Maybe we can accomplish that with a scoped notation or something?

That should work. If you use notation3, you can also get it to pretty print. Here's a quick test with ENat:

notation3 "∞" => (⊤ : ENat)

#check ∞ -- ∞
#check (⊤ : Bool) -- ⊤

[Yury G. Kudryashov]

Will it work with open scoped ENNReal?