4 ms·

Where does Lean get sold as a constructive system? Certainly mathlib (the main maths library in Lean) is very upfront about being classical.

zozbot234 5y ago
mathlib != Lean. I'm talking about the basic logic. People will try to sell you Lean by describing its system as constructive, but if so the quotients stuff is pure breakage as the Coq folks point out. And if Lean could support classical logic without arbitrarily breaking interop for folks who want to also prove constructive statements, we might see some additions to mathlib with a closer focus on constructive math.
- deadbeef57 5y ago
  I agree very much that mathlib != Lean. Still, I think much of the talk about Lean will mention that mathlib is classical. It was an honest question: I don't know where Lean is sold as a constructive system. (Note, I haven't read every part of Lean's documentation or website. I might be missing something obvious here.)
- foooobar 5y ago
  I don't think anyone is trying to sell Lean as a constructive system. The current developers certainly don't think of it that way, further evidenced by the fact that the typical way of doing computation in Lean does not involve definitional reduction, but using `#eval` with additional low level code for performance. Proof irrelevance (and quotients) were adopted with that in mind.
- Someody42 5y ago
  You can absolutely do constructive things in Lean, as long as you use neither the built-in "quot" type nor the three other axioms described in the docs, and then you get a system with all the desired properties I think
  - foooobar 5y ago
    Some constructivists may also take offense with proof irrelevance (and the resulting loss of normalization [1] or its incompatibility with HoTT), which you can only really avoid by avoiding Prop. [1] https://arxiv.org/abs/1911.08174 https://arxiv.org/abs/1911.08174
    - xvilka 5y ago
      There is also a problem of HoTT and equality reflection incompatibility[1]. [1] https://www2.mathematik.tu-darmstadt.de/~streicher/barc_corr.pdf https://www2.mathematik.tu-darmstadt.de/~streicher/barc_corr...

zozbot234 5y ago

mathlib != Lean. I'm talking about the basic logic. People will try to sell you Lean by describing its system as constructive, but if so the quotients stuff is pure breakage as the Coq folks point out. And if Lean could support classical logic without arbitrarily breaking interop for folks who want to also prove constructive statements, we might see some additions to mathlib with a closer focus on constructive math.

deadbeef57 5y ago
I agree very much that mathlib != Lean. Still, I think much of the talk about Lean will mention that mathlib is classical. It was an honest question: I don't know where Lean is sold as a constructive system. (Note, I haven't read every part of Lean's documentation or website. I might be missing something obvious here.)
foooobar 5y ago
I don't think anyone is trying to sell Lean as a constructive system. The current developers certainly don't think of it that way, further evidenced by the fact that the typical way of doing computation in Lean does not involve definitional reduction, but using `#eval` with additional low level code for performance. Proof irrelevance (and quotients) were adopted with that in mind.
Someody42 5y ago
You can absolutely do constructive things in Lean, as long as you use neither the built-in "quot" type nor the three other axioms described in the docs, and then you get a system with all the desired properties I think
- foooobar 5y ago
  Some constructivists may also take offense with proof irrelevance (and the resulting loss of normalization [1] or its incompatibility with HoTT), which you can only really avoid by avoiding Prop. [1] https://arxiv.org/abs/1911.08174 https://arxiv.org/abs/1911.08174
  - xvilka 5y ago
    There is also a problem of HoTT and equality reflection incompatibility[1]. [1] https://www2.mathematik.tu-darmstadt.de/~streicher/barc_corr.pdf https://www2.mathematik.tu-darmstadt.de/~streicher/barc_corr...