> we want to work with our own assertions about decidability, and not let classical reasoning mess that up
I am not confident that you understood what I meant. It has nothing to do with the proofs themselves, but a mathematically uninteresting matter about whether or not you can rw/simp using the theorem due to the statement incidentally containing concrete Decidable instances (it's simply a weakness of these tactics that they are not able to make use of the fact that types are Subsingletons, so if Decidable instances aren't free variables the theorems might not be applicable). There are some old parts of the library that come from probably Lean 2, like Finset, that are fairly constructive, and, since the most developed finite sets are these Finsets, and many of their operations require Decidable instances in their definitions, many theorems about finite sets mention Decidable instances. It's a matter of how much engineering time is available among all the volunteer contributors (along with some fond feelings for Finset since it's been around so long) that we haven't switched over to using the subtype of Set satisfying Set.Finite, which is very non-constructive but would make our lives easier.
I'll emphasize that this rw/simp issue is not about classical reasoning. Even if you banish classical reasoning from the library, it plagues Decidable instances everywhere, and special attention must be made to ensure that theorem statements contain no concrete Decidable instances. Getting this right is an annoying distraction that does not enable any new features or insight.
I'll also emphasize that mathlib theorems do not have Decidable instance hypotheses that are only used in their proofs. Last I checked, there's even a linter for this.
> I don't think that's a fair description of the sibling threads.
Since we're talking about others' "misconceptions", am I right that you weren't aware that in Lean you can do well-founded recursion using a classical termination proof and get a computable function? That's the sort of thing I was trying to make sure we were on the same page about. I brought up LEM to feel out your position because that's what plenty of people mean by constructivism, and I honestly have not been able figure out what constructivism means to you and what sorts of concrete benefits you think constructivist proofs give you. If you're able to interleave a construction with classical reasoning arguing that the construction is well founded, then what is it that the CS and program verification folks are missing from Lean? That's what I'm missing here. (And if there's a good concrete answer the folks who develop Lean itself would be interested.)
To be clear, there are plenty of things missing from Lean that would definitely help CS and program verification folks, but as far as I know none of these features touch upon constructivism.
While I wouldn't say that there are no benefits to constructive reasoning, and I support the work people do on foundations, all these Decidable instances really add to the difficulty that people experience learning to do mathematics in Lean.
I'm sure there are people out there doing program verification that think about it using topos theory, but I suspect it is very few. That's hardly a justification to put resources into making proofs be constructive mathlib-wide.
The basic definition of wellfoundedness in Lean and mathlib is in fact constructive, same as in Coq. There are technical implications to being able to reason 'classically' about well-founded relations but they apparently are fairly minor, having to do with the "no infinite chain" definition of well-foundedness. https://proofassistants.stackexchange.com/questions/1077/wel... -- and actually, this requires a form of choice in addition to classical reasoning. Mathlib knows about this, it's in https://leanprover-community.github.io/mathlib_docs/order/or... .
I think I've emphasized above that constructivism is more about preserving and leveraging the implied computational content of existing proofs than insisting on constructive proofs everywhere - the latter in particular adds a lot of complexity even when it's actually feasible, so I agree that Mathlib shouldn't do that. But when something can be phrased as a computable construction or decision procedure "for free" simply by relying on straightforward direct reasoning and eschewing classical assumptions, it makes sense to enable that, including as part of a mathematical library.
I am not confident that you understood what I meant. It has nothing to do with the proofs themselves, but a mathematically uninteresting matter about whether or not you can rw/simp using the theorem due to the statement incidentally containing concrete Decidable instances (it's simply a weakness of these tactics that they are not able to make use of the fact that types are Subsingletons, so if Decidable instances aren't free variables the theorems might not be applicable). There are some old parts of the library that come from probably Lean 2, like Finset, that are fairly constructive, and, since the most developed finite sets are these Finsets, and many of their operations require Decidable instances in their definitions, many theorems about finite sets mention Decidable instances. It's a matter of how much engineering time is available among all the volunteer contributors (along with some fond feelings for Finset since it's been around so long) that we haven't switched over to using the subtype of Set satisfying Set.Finite, which is very non-constructive but would make our lives easier.
I'll emphasize that this rw/simp issue is not about classical reasoning. Even if you banish classical reasoning from the library, it plagues Decidable instances everywhere, and special attention must be made to ensure that theorem statements contain no concrete Decidable instances. Getting this right is an annoying distraction that does not enable any new features or insight.
I'll also emphasize that mathlib theorems do not have Decidable instance hypotheses that are only used in their proofs. Last I checked, there's even a linter for this.
> I don't think that's a fair description of the sibling threads.
Since we're talking about others' "misconceptions", am I right that you weren't aware that in Lean you can do well-founded recursion using a classical termination proof and get a computable function? That's the sort of thing I was trying to make sure we were on the same page about. I brought up LEM to feel out your position because that's what plenty of people mean by constructivism, and I honestly have not been able figure out what constructivism means to you and what sorts of concrete benefits you think constructivist proofs give you. If you're able to interleave a construction with classical reasoning arguing that the construction is well founded, then what is it that the CS and program verification folks are missing from Lean? That's what I'm missing here. (And if there's a good concrete answer the folks who develop Lean itself would be interested.)
To be clear, there are plenty of things missing from Lean that would definitely help CS and program verification folks, but as far as I know none of these features touch upon constructivism.
While I wouldn't say that there are no benefits to constructive reasoning, and I support the work people do on foundations, all these Decidable instances really add to the difficulty that people experience learning to do mathematics in Lean.
I'm sure there are people out there doing program verification that think about it using topos theory, but I suspect it is very few. That's hardly a justification to put resources into making proofs be constructive mathlib-wide.