Theorems in the Decidable namespace

Stream: mathlib4

[Jovan Gerbscheid]

It was suggested that we could remove theorems that have Decidable hypotheses, since the same theorem can be stated and proved without this hypothesis. The only reason for having these is to support non-classical logic, removing the need for em (as opposed to definitions using a Decidable hypotheses, which need the decidability to unfold nicely).

Here is the list of theorems in Decidable. I commented out the ones that are in core Lean. Do we want to keep or remove the ones that are in Mathlib?

#check Decidable.List.Lex.ne_iff
#check Decidable.List.eq_or_ne_mem_of_mem
#check Decidable.Partrec.const'
#check Decidable.and_forall_ne
-- #check Decidable.and_iff_not_or_not
-- #check Decidable.and_or_imp
-- #check Decidable.byContradiction
-- #check Decidable.by_contra
#check Decidable.by_contradiction -- in Mathlib.Deprecated
-- #check Decidable.em
#check Decidable.eq_iff_le_not_lt
#check Decidable.eq_or_lt_of_le
#check Decidable.eq_or_ne
#check Decidable.exists_ne
-- #check Decidable.exists_not_of_not_forall -- in Batteries
#check Decidable.forall_or_left
#check Decidable.forall_or_right
-- #check Decidable.iff_congr_left
-- #check Decidable.iff_congr_right
-- #check Decidable.iff_iff_and_or_not_and_not
-- #check Decidable.iff_iff_not_or_and_or_not
-- #check Decidable.iff_not_comm
-- #check Decidable.imp_iff_left_iff
-- #check Decidable.imp_iff_not_or
-- #check Decidable.imp_iff_or_not
-- #check Decidable.imp_iff_right_iff
-- #check Decidable.imp_or
-- #check Decidable.imp_or'
-- #check Decidable.isFalse.sizeOf_spec
-- #check Decidable.isTrue.sizeOf_spec
#check Decidable.le_iff_eq_or_lt
#check Decidable.le_iff_lt_or_eq
#check Decidable.lt_or_eq_of_le
#check Decidable.mul_lt_mul''
#check Decidable.ne_iff_lt_iff_le
#check Decidable.ne_or_eq
-- #check Decidable.not_and_iff_or_not
-- #check Decidable.not_and_iff_or_not_not
-- #check Decidable.not_and_iff_or_not_not'
-- #check Decidable.not_and_not_right
-- #check Decidable.not_exists_not
-- #check Decidable.not_forall
-- #check Decidable.not_forall_not
#check Decidable.not_forall₂
-- #check Decidable.not_iff
-- #check Decidable.not_iff_comm
-- #check Decidable.not_iff_not
-- #check Decidable.not_imp_comm
-- #check Decidable.not_imp_iff_and_not
-- #check Decidable.not_imp_not
-- #check Decidable.not_imp_self
-- #check Decidable.not_imp_symm
-- #check Decidable.not_not
-- #check Decidable.not_or_of_imp
-- #check Decidable.not_or_self
-- #check Decidable.of_not_imp
-- #check Decidable.of_not_not
-- #check Decidable.or_congr_left'
-- #check Decidable.or_congr_right'
-- #check Decidable.or_iff_not_and_not
-- #check Decidable.or_iff_not_imp_left
-- #check Decidable.or_iff_not_imp_right
#check Decidable.or_not_of_imp
-- #check Decidable.or_not_self
-- #check Decidable.peirce

[Violeta Hernández]

See also #mathlib4 > Decidable namespace

[Violeta Hernández]

I completely agree with getting rid of these theorems, but when I last brought it up there was some amount of pushback.

[Mario Carneiro]

The purpose of these theorems is clear and exactly what you said. Why are you wanting to get rid of them?

[Jovan Gerbscheid]

The idea is that mathlib is a library for classical mathematics. I doubt that there is or will be anyone using these lemmas from Mathlib for proving things intuitionistically.

And if we did care about certain lemmas not using em, then there should be some automation in place to verify that these lemmas don't accidentally use a classical axiom.

The disadvantage of having them in mathlib is for example confusing people like me about why they exist.

[Mario Carneiro]

I doubt that there is or will be anyone using these lemmas from Mathlib for proving things intuitionistically.

Not with that attitude!

[Mario Carneiro]

There should indeed be some automation in place. I wrote such a thing but never really deployed it because at the time there were a lot of "false" positives caused by usage in core

[Eric Wieser]

I think we should have an intuitionist attribute in batteries, which both enforces that choice is avoided, and holds a docstring explaining why the theorem might be a duplicate

[Violeta Hernández]

My own opinion is also along the same lines. Mathlib and its tactics make little if any consideration for non-classical logics, and it's weird we make an exception for the off-chance Decidable namespace duplicate. But it'd be cool to see that change!

[Eric Wieser]

If core isn't interested at all in supporting this, I think an ok compromise would be to allow Kim to remove the failing cases of such attributes downstream when doing a version bump, and then let interested parties re-classicalize the theorems off the critical path

[Mario Carneiro]

I'm working toward a future where mathlib is not aggressively anti-intuitionist, although sometimes progress feels pretty depressingly negative

[Johan Commelin]

Yeah, I second that.

• Nobody should have to explain why they are working classically.
• But at the same time, if some parts are already available intuitionistically, then I don't see a reason to remove that.

Part of me is still hoping to see some applications of internal logic to "real world classical" maths. And there are multiple people working on that.

[Tristan Figueroa-Reid]

Mario Carneiro said:

I'm working toward a future where mathlib is not aggressively anti-intuitionist, although sometimes progress feels pretty depressingly negative

Even in my limited PRs to mathlib4, I have experienced pushback if I try to add equivalent Decidable lemmas. I could see a world in which there are generated theorems for classical variants, but that seems much more of a pain to implement than "simple" attributes that auto-generate pairing theorems (e.g. @[to_additive])

[Yury G. Kudryashov]

We have a linter in progress (it works but it's too slow) that ensures that we don't assume Decidable unless the theorem is in the Decidable namespace or the instance is needed to formulate (not prove) the theorem. I see no reason to remove theorems in the Decidable namespace. It's OK to add a library note about this though.

[Yury G. Kudryashov]

OTOH, I don't like the idea of having Decidable copy of every theorem in Mathlib. I'm not sure what's the right middle ground.

[Johan Commelin]

I'm not too worried about the duplication. It will probably amount to a small subset of Logic/ and maybe a bit of Order/.

[Patrick Massot]

Johan Commelin said:

• But at the same time, if some parts are already available intuitionistically, then I don't see a reason to remove that.

I disagree with that. There is a clear reason to remove existing intuitionistic lemmas: they encourage people to continue arguing periodically about how Mathlib is too classical. I think a real clarification would help with that.

[Mario Carneiro]

Yury G. Kudryashov said:

It's OK to add a library note about this though.

There is already a library note [Decidable namespace] next to each and every theorem in the namespace

[Mario Carneiro]

As far as I can tell, all of this is documented pretty explicitly in the code, so the people above complaining about how it's unclear can only be talking about our processes and general messaging, not these specific lines of code.

[Eric Wieser]

I think the fact that library notes don't produce links anywhere is the issue here

[Yury G. Kudryashov]

Mario Carneiro said:

Yury G. Kudryashov said:

It's OK to add a library note about this though.

There is already a library note [Decidable namespace] next to each and every theorem in the namespace

I'm sorry for writing this w/o looking at the code.