Decidable namespace

Stream: mathlib4

[Violeta Hernández]

As I understand it, Mathlib is entirely based in classical logic and is uninterested in supporting other weaker forms of logic. So why do we have duplicated Decidable versions of classical theorems?

[Violeta Hernández]

I understand why those are there in core Lean 4, I'm not asking for that to be changed. I'm instead asking about theorems like e.g. docs#Decidable.ne_or_eq which exist within our own jurisdiction.

[Eric Wieser]

A lot of these are inherited in Lean 3, but I think "entirely based in classical logic" is a little strong. Certainly in the past there have been users interested in basic theorems about Lists etc who seemingly have interest in avoiding choice, and the maintenance burden of keeping these Decidable theorems around is quite low

[Bryan Gin-ge Chen]

Here's the original thread where the decidable namespace was proposed: #PR reviews > #2332 @ 💬

[Violeta Hernández]

Well, the reason I view this as a problem is that introducing choice in a proof is not only extremely easy to do by accident, but also not considered a breaking change in Mathlib. So it seems a bit weird to try and make guarantees around the absence of choice.

[Eric Wieser]

I think that guarantee is only promised by (the obvious subset of) things within the Decidable namespace

[Violeta Hernández]

Fair enough.

Do the other things discussed in that thread still hold today? e.g. "we won't block a PR that gets rid of choice even if the proof is longer"

[Violeta Hernández]

I have never seen anyone try to do this and I can't imagine that going smoothly

[Eric Wieser]

I think that's up to subjective reviewer judgement. If the proof gets one line longer I don't see it being a problem, if it gets 100 lines longer then I would expect it not to be merged

[Eric Wieser]

I don't think we gain anything today by explicitly announcing such PRs are not welcome, vs waiting for them to appear before making judgements on a case-by-case basis

[Violeta Hernández]

Alright then. So it's less so that Mathlib is entirely classical, and moreso that there just hasn't been too much interest in developing the non-classical theory

[Eric Wieser]

And that there is no contribution requirement in general for avoiding choice, at least once you leave very basic lemmas and enter things with mathematical content.