4 ms·

It's because the mathlib authors don't really care about being constructive and frequently use things like choice/LEM, in contrast to Coq/math-comp. If there's

It's because the mathlib authors don't really care about being constructive and frequently use things like choice/LEM, in contrast to Coq/math-comp. If there's a constructive and non-constructive version of something, the mathlib people will use whatever's easier or nicer to work with. There's some info here about how Lean does realizability with pervasive use of choice: https://github.com/coq/coq/issues/10871#issuecomment-546641216 https://github.com/coq/coq/issues/10871#issuecomment-5466412...

tlringer 6y ago
That makes sense! I just wish discussion on this end would stay nuanced: In that case Lean has great library support for classical mathematics. This is an important distinction because it is something that the authors of other constructive proof assistants can focus on if they want to reach more mathematicians.
kmill 6y ago
Sort of the official policy is that inside proofs (i.e., terms of types in Prop) constructibility doesn't matter, but inside definitions (i.e., terms of types in Type 0 and above) try to be constructive. For example, it is ok to define a function constructively but with a nonconstructive proof of termination. LEM is used everywhere because it's actually a theorem. It follows from functional extentionality and the existence of quotient types. https://github.com/leanprover/lean/blob/master/library/init/classical.lean#L69 https://github.com/leanprover/lean/blob/master/library/init/... The axiom of choice is an actual axiom, and it too ends up being used everywhere, but mostly to introduce decidable instances to permit things like double negation elimination inside proofs. An illustration: [1] introduces these instances to the file and [2] implicitly uses the instance. [1] https://github.com/leanprover-community/mathlib/blob/master/src/logic/basic.lean#L22 https://github.com/leanprover-community/mathlib/blob/master/... [2] https://github.com/leanprover-community/mathlib/blob/master/src/logic/basic.lean#L260 https://github.com/leanprover-community/mathlib/blob/master/...
- tlringer 6y ago
  It is my understanding that functional extensionality in Lean itself follows from the axiom propositional extensionality, so in that sense LEM is still a consequence of an axiom. The core theory of Lean is constructive.
  - kmill 6y ago
    I'm not an expert on the foundations of Lean, but I do know that funext in the source code follows only from the axioms of quotient types and the eliminator for equality. There are a number of axioms that are implicit in the type checker itself, so you might say that proof irrelevance is built-in in that way. Propositional extensionality (propext) is that propositions that imply each other are equal, and that's an axiom in the library, but funext does not depend on propext.
    - kmill 6y ago
      Correcting my non-expert inaccuracies in this thread: I just learned that Diaconescu's theorem depends on the axiom of choice, which I'd missed even though I'd glanced at the code for classical.em a few times. So, LEM definitely depends on the axiom of choice in Lean.
- zozbot234 6y ago
  LEM and double-negation elimination is very poor style from a constructive POV, though. If you need to prove something non-constructively, just stick to the negative fragment.
  - kmill 6y ago
    I think your comment illustrates a difference in cultures -- mathematicians generally don't care about whether it's bad style in the constructive POV. Sure, you can 'just' stick to the negative fragment, but that 'just' is sweeping a lot of questions of ergonomics under the rug. One thing that attracted me to Lean was that I could formalize mathematics as I knew it, more or less, and there was a vibrant community with a fairly well developed library of basic classical mathematics. I'm not saying these concerns about constructibility aren't unimportant. I do appreciate both POVs. I just don't think it's something you have to force mathematicians to worry about if all they're interested in is formalizing their math on a computer. Something that's interesting about Lean is that double-negation elimination is used in Prop but not generally in Type and above. You have to explicitly reach for the axiom of choice if you want to "construct" a term of a type that isn't empty.

tlringer 6y ago

That makes sense! I just wish discussion on this end would stay nuanced: In that case Lean has great library support for classical mathematics. This is an important distinction because it is something that the authors of other constructive proof assistants can focus on if they want to reach more mathematicians.

kmill 6y ago

Sort of the official policy is that inside proofs (i.e., terms of types in Prop) constructibility doesn't matter, but inside definitions (i.e., terms of types in Type 0 and above) try to be constructive. For example, it is ok to define a function constructively but with a nonconstructive proof of termination. LEM is used everywhere because it's actually a theorem. It follows from functional extentionality and the existence of quotient types. https://github.com/leanprover/lean/blob/master/library/init/classical.lean#L69 https://github.com/leanprover/lean/blob/master/library/init/... The axiom of choice is an actual axiom, and it too ends up being used everywhere, but mostly to introduce decidable instances to permit things like double negation elimination inside proofs. An illustration: [1] introduces these instances to the file and [2] implicitly uses the instance. [1] https://github.com/leanprover-community/mathlib/blob/master/src/logic/basic.lean#L22 https://github.com/leanprover-community/mathlib/blob/master/... [2] https://github.com/leanprover-community/mathlib/blob/master/src/logic/basic.lean#L260 https://github.com/leanprover-community/mathlib/blob/master/...

tlringer 6y ago
It is my understanding that functional extensionality in Lean itself follows from the axiom propositional extensionality, so in that sense LEM is still a consequence of an axiom. The core theory of Lean is constructive.
- kmill 6y ago
  I'm not an expert on the foundations of Lean, but I do know that funext in the source code follows only from the axioms of quotient types and the eliminator for equality. There are a number of axioms that are implicit in the type checker itself, so you might say that proof irrelevance is built-in in that way. Propositional extensionality (propext) is that propositions that imply each other are equal, and that's an axiom in the library, but funext does not depend on propext.
  - kmill 6y ago
    Correcting my non-expert inaccuracies in this thread: I just learned that Diaconescu's theorem depends on the axiom of choice, which I'd missed even though I'd glanced at the code for classical.em a few times. So, LEM definitely depends on the axiom of choice in Lean.
zozbot234 6y ago
LEM and double-negation elimination is very poor style from a constructive POV, though. If you need to prove something non-constructively, just stick to the negative fragment.
- kmill 6y ago
  I think your comment illustrates a difference in cultures -- mathematicians generally don't care about whether it's bad style in the constructive POV. Sure, you can 'just' stick to the negative fragment, but that 'just' is sweeping a lot of questions of ergonomics under the rug. One thing that attracted me to Lean was that I could formalize mathematics as I knew it, more or less, and there was a vibrant community with a fairly well developed library of basic classical mathematics. I'm not saying these concerns about constructibility aren't unimportant. I do appreciate both POVs. I just don't think it's something you have to force mathematicians to worry about if all they're interested in is formalizing their math on a computer. Something that's interesting about Lean is that double-negation elimination is used in Prop but not generally in Type and above. You have to explicitly reach for the axiom of choice if you want to "construct" a term of a type that isn't empty.