deprecate Mathlib.Data.Nat.PartENat?

Stream: mathlib4

[Kim Morrison]

This is a leaf file, since 2018. I don't really see what it would be useful for, and I just ran into it during a (tedious, long, painful) refactor that unfortunately needs doing.

Could we get it out of the way so no one needs to run into it next time?

If there are projects using it I'm happy to hear that, but otherwise, let's clean up!

[Violeta Hernández]

I'd like to see the entirety of Part go. I understand there's computational nuances that make it different from Option but I don't think said nuances are relevant to Mathlib at all. Just my two cents.

[Aaron Liu]

Part is useful computationally, but usually I find it's too general (arbitrary proof is needed), whereas Option is too restrictive (failure must be decidable)

[Kim Morrison]

chore: deprecate PartENat #29231

[Jovan Gerbscheid]

Am I right to understand that the only purpose of Part instead of Option is to avoid using classical logic?

[Aaron Liu]

the purpose of Part is to make certain things computable

[Jovan Gerbscheid]

Do you have an example where #eval isn't otherwise possible?

[Aaron Liu]

Jovan Gerbscheid said:

Do you have an example where #eval isn't otherwise possible?

when you have a function (x : α) → P x → β where P : α → Prop is a predicate which is not recursively enumerable, you can make this into a α → Part β but you can't make this into a function α → Option β using partial_fixpoint

[Aaron Liu]

if the predicate is RE then you can make a computable α → Option β with partial_fixpoint, but it will never return none (it will run forever instead)

[Aaron Liu]

if the predicate is decidable then you can make this into a total function α → Option β which is computable and always terminates

[Aaron Liu]

I don't have any non-RE predicates on me now, so no concrete example

[Jovan Gerbscheid]

Sure, but can you #eval a Part? If not, I feel like this is a "no" to my question

[Aaron Liu]

you can docs#Part.get a Part

[Aaron Liu]

if you don't feel like providing a proof then you can docs#Part.unwrap it (but this is unsound)

[Aaron Liu]

and these are all computable

[Jovan Gerbscheid]

But surely such a thing belongs in Batteries?

[Aaron Liu]

maybe

[Jovan Gerbscheid]

So from what I understand, if we make e.g. Array.find?' that returns a Part, then using that is equivalent (in the runtime) to using Array.find, but it delays the moment at which a proof needs to be given, because Array.find requires the proof upfront.

[Aaron Liu]

yeah that sounds right, modulo the fact that I can't find Array.find anywhere

[Jovan Gerbscheid]

I'm sure lean will get around to making that API at some point. Or they will make Array.find return a Part :laughing:

[Aaron Liu]

unfortunately the important operation Part.ωSup is noncomputable, and there's no way to make it computable since Part is too general

[Jovan Gerbscheid]

Wait, there is Part API for things that aren't computable when the whole point was computability?

[Aaron Liu]

yeah it's a bit weird

[Aaron Liu]

right now the behavior of getting a none is "undefined behavior", if that were weakened to "infinite loop" then Part.ωSup could be computable

[Jovan Gerbscheid]

Huh, but you prove in get that you can't get a none?

[Aaron Liu]

yes

[Aaron Liu]

here I have a thread #Is there code for X? > Divergence monad @ 💬