7 ms·

Basically it turned out that theoretical undecidability did not matter in practice, because Scholze mathematics relies so little on definitional equality. We pr

Basically it turned out that theoretical undecidability did not matter in practice, because Scholze mathematics relies so little on definitional equality. We prove theorems with `simp` not `refl`. Pierre-Marie Pédrot is quoted above as saying that various design decisions are "breaking everything around", but we don't care that our `refl` is slightly broken because it is regarded as quite a low-level tool for the tasks (eg proving theorems of Clausen and Scholze) that we are actually interested in, and I believe our interests contrast quite a lot with the things that Pédrot is interested in.

kmill 5y ago
And in "Lean style", refl proofs are a bit distasteful from a software engineering point of view because they pierce through the API of a mathematical object. (In the language of OOP, it can break encapsulation.) It tends to be a good idea to give some definition, then prove a bunch of lemmas that characterize the object, and finally forget the definition.
bryan0 5y ago
Can you explain to a non-mathematician how you can prove anything without refl (which I assume is the statement “x=x is true”) ?
- digama0 5y ago
  The jargon is a bit confusing sometimes. In Lean, "refl" does a whole lot more than prove x=x. It is of course available if you want to prove x=x, but the real power of "refl" is that it also proves x=y where x and y are definitionally equal. Or at least that's the idea; it turns out that lean's definitional equality relation is not decidable so sometimes it will fail to work even when x and y are defeq, and this is the theoretically distasteful aspect that came up on the linked Coq issue. In practice, the theoretical undecidability issue never happens, however there is a related problem where depending on what is unfolded a proof by "refl" can take seconds to minutes, and if alternative external proof-checkers don't follow exactly the same unfolding heuristics it can turn a seconds long proof into a thousand-year goose chase. By comparison, methods like "simp" have much more controllable performance because they actually produce a proof term, so they tend to be preferable.
  - bryan0 5y ago
    Thanks for the explanation. Is the defeq undecidability a bug of Lean that should be fixed in the future? Or is it an intentional design decision for it to function properly for other types of proofs?
    - Jweb_Guru 5y ago
      I am quite confident that the developers of lean consider it a feature (or at least, not a bug). Though I'm also not sure why they are building on a complex metatheory like CiC if they are willing to accept undecidable typechecking since you can simplify a lot of things if you give that up.
      - foooobar 5y ago
        What simplifications do you have in mind? I think one of the reasons is that Lean's approximation of defeq still works well enough in practice. As mentioned by others, you never really run into the kind of counter examples that break theoretical properties, but instead into examples where checking defeq is inacceptably slow, which remains an issue even when defeq is decidable. From my understanding CiC is used because it allows using a unified language for proofs, specifications, programs and types, which greatly simplifies the system. For example, in Lean 4, more or less the entire system is built on the same core term language: Proofs, propositions / specifications, programs, tactics (i.e. meta programs), the output of tactics and even Lean 4 itself are all written in that same language, even if they don't always use the same method of computation. In my eyes, for the purposes of writing and checking proofs, CiC is quite complex; but if you want to capture all of the above and have them all checked by the same kernel, CiC seems like a fairly minimal metatheory to do so, even with undecidable type checking.
        Jweb_Guru 5y ago
        For example, if you are willing to accept undecidable typechecking, you can define inductive types in a much simpler theory (inductive types and dependent pattern matching are by far the most complex parts of CiC): https://homepage.cs.uiowa.edu/~astump/papers/from-realizability-to-induction-aaron-stump.pdf https://homepage.cs.uiowa.edu/~astump/papers/from-realizabil... . There are a few other examples but this is the one that immediately sprung to mind. The complexity of CiC is very much about decidable typechecking, it's not fundamental to writing a sound dependently typed proof assistant. And anyone who has actually worked on a kernel for CiC knows that while it is "minimal" compared to what people want to do with it, no efficient kernel is nearly as minimal as something like λP2 with dependent intersections.

kmill 5y ago

And in "Lean style", refl proofs are a bit distasteful from a software engineering point of view because they pierce through the API of a mathematical object. (In the language of OOP, it can break encapsulation.) It tends to be a good idea to give some definition, then prove a bunch of lemmas that characterize the object, and finally forget the definition.

bryan0 5y ago

Can you explain to a non-mathematician how you can prove anything without refl (which I assume is the statement “x=x is true”) ?

digama0 5y ago
The jargon is a bit confusing sometimes. In Lean, "refl" does a whole lot more than prove x=x. It is of course available if you want to prove x=x, but the real power of "refl" is that it also proves x=y where x and y are definitionally equal. Or at least that's the idea; it turns out that lean's definitional equality relation is not decidable so sometimes it will fail to work even when x and y are defeq, and this is the theoretically distasteful aspect that came up on the linked Coq issue. In practice, the theoretical undecidability issue never happens, however there is a related problem where depending on what is unfolded a proof by "refl" can take seconds to minutes, and if alternative external proof-checkers don't follow exactly the same unfolding heuristics it can turn a seconds long proof into a thousand-year goose chase. By comparison, methods like "simp" have much more controllable performance because they actually produce a proof term, so they tend to be preferable.
- bryan0 5y ago
  Thanks for the explanation. Is the defeq undecidability a bug of Lean that should be fixed in the future? Or is it an intentional design decision for it to function properly for other types of proofs?
  - Jweb_Guru 5y ago
    I am quite confident that the developers of lean consider it a feature (or at least, not a bug). Though I'm also not sure why they are building on a complex metatheory like CiC if they are willing to accept undecidable typechecking since you can simplify a lot of things if you give that up.
    - foooobar 5y ago
      What simplifications do you have in mind? I think one of the reasons is that Lean's approximation of defeq still works well enough in practice. As mentioned by others, you never really run into the kind of counter examples that break theoretical properties, but instead into examples where checking defeq is inacceptably slow, which remains an issue even when defeq is decidable. From my understanding CiC is used because it allows using a unified language for proofs, specifications, programs and types, which greatly simplifies the system. For example, in Lean 4, more or less the entire system is built on the same core term language: Proofs, propositions / specifications, programs, tactics (i.e. meta programs), the output of tactics and even Lean 4 itself are all written in that same language, even if they don't always use the same method of computation. In my eyes, for the purposes of writing and checking proofs, CiC is quite complex; but if you want to capture all of the above and have them all checked by the same kernel, CiC seems like a fairly minimal metatheory to do so, even with undecidable type checking.
      - Jweb_Guru 5y ago
        For example, if you are willing to accept undecidable typechecking, you can define inductive types in a much simpler theory (inductive types and dependent pattern matching are by far the most complex parts of CiC): https://homepage.cs.uiowa.edu/~astump/papers/from-realizability-to-induction-aaron-stump.pdf https://homepage.cs.uiowa.edu/~astump/papers/from-realizabil... . There are a few other examples but this is the one that immediately sprung to mind. The complexity of CiC is very much about decidable typechecking, it's not fundamental to writing a sound dependently typed proof assistant. And anyone who has actually worked on a kernel for CiC knows that while it is "minimal" compared to what people want to do with it, no efficient kernel is nearly as minimal as something like λP2 with dependent intersections.