4 ms·

> You might be confused by the fact that Lean's definitional equality is not decidable, but that doesn't mean it isn't sound. Nobody has ever found a proof of `

by xvilka 5y ago

> You might be confused by the fact that Lean's definitional equality is not decidable, but that doesn't mean it isn't sound. Nobody has ever found a proof of `false` so far in Lean 3. You are right, my bad. Taking my words back on that. A bit more details from the Pierre-Marie Pédrot: > Lean does not escape this limitation, as it defines the equality type inductively as in Coq. Rather, in a mastermind PR campaign, they successfully convinced non-experts of type theory that they could give them quotient types without breaking everything around. > The first thing they do is to axiomatize quotient types, which is somewhat fine and can be done the same in Coq. As any use of axioms, this breaks canonicity, meaning your computations may get stuck on some opaque term. (While slightly cumbersome, axiomatizing quotients already solves 99,9% of the problems of the working mathematician). > Now, were they do evil things that would make decent type theorists shake in terror, they add a definitional reduction rule over the quotient induction principle. We could do the same in the Coq kernel, but there is a very good reason not to do this. Namely, this definitional rule breaks subject reduction, which is a property deemed more important than loss of canonicity. > In Lean, you can write a term t : A where t reduces to u, but u doesn't have type A (or equivalently may not typecheck at all). This is BAD for a flurry of reasons, mark my words. Reinstating it while keeping quotients requires an undecidable type checking algorithm, which is another can of worms you don't want to wander into. The same kind of trouble arises from similar Lean extensions like choice.

deadbeef57 5y ago
Ok, no worries. I understand that from a theoretical point it's not so nice that defeq is not decidable. But frankly I don't care. Because in practice, I don't know of any example where someone was bitten by this. It only shows up in contrived examples. And even if you have some practical example where lean gets stuck on A = B, it will probably be very easy to find a C so that lean gets unstuck on A = C = B. [Edit, this comment only replies to the first paragraph of parent. I wrote it before parent was edited.]
- xvilka 5y ago
  By the way, just for the record, I like many aspects of the new Lean 4 design and wish the project luck. They really aim for better maintainability and user experience. It is nice to see them taking best solutions from other programming languages and frameworks.
deadbeef57 5y ago
> Lean does not escape this limitation, as it defines the equality type inductively as in Coq. Rather, in a mastermind PR campaign, they successfully convinced non-experts of type theory that they could give them quotient types without breaking everything around. This is not the first time that I hear someone from the Coq community talk about Lean and its "mastermind PR campaign". To me it comes across in a denigrating way, and frankly I'm a bit sick of it. Working mathematicians are usually not experts of type theory. Yes. But they aren't stupid either. Why does the Lean community have such a large number of mathematician users? Why did it successfully formalize the main technical result of Peter Scholze's challenge in less than 6 months? Is this all because of a "mastermind PR campaign" selling mathematicians snake oil? There has been some strong disagreements and even mud slinging between the Coq and Lean communities in the past. But I thought that axe was buried. I would like to move on. I'm fine with people finding the foundations of Lean ugly, distasteful, improper, or whatever. But please stop the insults.
- zozbot234 5y ago
  The Coq folks tend to focus on constructivity, and Lean gets sold as a constructive system but then you get this weird axiomatised-quotients stuff that's the farthest thing from constructivity. I can see how they might find that kind of thing highly frustrating. It might not show up as a problem if you only ever care about classical stuff, but there are arguably better ways of doing purely classical mathematics that don't arbitrarily break interoperability w/ the constructive world.
  - deadbeef57 5y ago
    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.
chriswarbo 5y ago
I haven't used quotients (or Lean), but I've certainly encountered subject reduction problems in Coq when using coinduction, so this sounds a tad hypocritical. It's certainly good to avoid breaking subject reduction even more though ;)
- xvilka 5y ago
  There's ongoing work[1] on fixing that. Also let's see how migrating setoids to cubical type theory might fix more issues for Coq. Will they follow the Arend[2] path? That remains to be seen. [1] https://github.com/coq/coq/pull/10764 https://github.com/coq/coq/pull/10764 [2] https://arend-lang.github.io/about/arend-features https://arend-lang.github.io/about/arend-features
- Jweb_Guru 5y ago
  Pierre Pedrot has been very vocal in his belief that broken SR from coinductive types is a serious problem with Coq that needs to be fixed. This is quite different from introducing stuff that deliberately breaks it.
deleted 5y ago
[deleted]

by xvilka 5y ago

deadbeef57 5y ago

Ok, no worries. I understand that from a theoretical point it's not so nice that defeq is not decidable. But frankly I don't care. Because in practice, I don't know of any example where someone was bitten by this. It only shows up in contrived examples. And even if you have some practical example where lean gets stuck on A = B, it will probably be very easy to find a C so that lean gets unstuck on A = C = B. [Edit, this comment only replies to the first paragraph of parent. I wrote it before parent was edited.]

xvilka 5y ago
By the way, just for the record, I like many aspects of the new Lean 4 design and wish the project luck. They really aim for better maintainability and user experience. It is nice to see them taking best solutions from other programming languages and frameworks.

deadbeef57 5y ago

> Lean does not escape this limitation, as it defines the equality type inductively as in Coq. Rather, in a mastermind PR campaign, they successfully convinced non-experts of type theory that they could give them quotient types without breaking everything around. This is not the first time that I hear someone from the Coq community talk about Lean and its "mastermind PR campaign". To me it comes across in a denigrating way, and frankly I'm a bit sick of it. Working mathematicians are usually not experts of type theory. Yes. But they aren't stupid either. Why does the Lean community have such a large number of mathematician users? Why did it successfully formalize the main technical result of Peter Scholze's challenge in less than 6 months? Is this all because of a "mastermind PR campaign" selling mathematicians snake oil? There has been some strong disagreements and even mud slinging between the Coq and Lean communities in the past. But I thought that axe was buried. I would like to move on. I'm fine with people finding the foundations of Lean ugly, distasteful, improper, or whatever. But please stop the insults.

zozbot234 5y ago
The Coq folks tend to focus on constructivity, and Lean gets sold as a constructive system but then you get this weird axiomatised-quotients stuff that's the farthest thing from constructivity. I can see how they might find that kind of thing highly frustrating. It might not show up as a problem if you only ever care about classical stuff, but there are arguably better ways of doing purely classical mathematics that don't arbitrarily break interoperability w/ the constructive world.
- deadbeef57 5y ago
  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.

chriswarbo 5y ago

I haven't used quotients (or Lean), but I've certainly encountered subject reduction problems in Coq when using coinduction, so this sounds a tad hypocritical. It's certainly good to avoid breaking subject reduction even more though ;)

xvilka 5y ago
There's ongoing work[1] on fixing that. Also let's see how migrating setoids to cubical type theory might fix more issues for Coq. Will they follow the Arend[2] path? That remains to be seen. [1] https://github.com/coq/coq/pull/10764 https://github.com/coq/coq/pull/10764 [2] https://arend-lang.github.io/about/arend-features https://arend-lang.github.io/about/arend-features
Jweb_Guru 5y ago
Pierre Pedrot has been very vocal in his belief that broken SR from coinductive types is a serious problem with Coq that needs to be fixed. This is quite different from introducing stuff that deliberately breaks it.

deleted 5y ago

[deleted]