6 ms·

Coq is a Lean Typechecker

91 points by palmskog 7y ago

perthmad 7y ago
This particular feat was triggered by Kevin Buzzard's unsubstantiated claim that "Lean was better than Coq" as a foundation for mathematics, because it had built-in quotient types. The work described above precisely shows that such types can be encoded as well using features shipped with the vanilla Coq distro. See https://sympa.inria.fr/sympa/arc/coq-club/2020-01/msg00006.html https://sympa.inria.fr/sympa/arc/coq-club/2020-01/msg00006.h....
- jmgrosen 7y ago
  My understanding is that this shows how vanilla Coq still can’t encode quotients well. This project relies on a PR [0] that breaks term normalization, which makes it highly unlikely it will be merged. My understanding is that Lean’s implementation of quotients also breaks normalization, but they don’t care as much about that as Coq devs do. [0]: https://github.com/coq/coq/pull/10390#issuecomment-554316311 https://github.com/coq/coq/pull/10390#issuecomment-554316311
  - SkySkimmer 7y ago
    The normalization issue is not about quotients at all. It's https://arxiv.org/abs/1911.08174 https://arxiv.org/abs/1911.08174 "Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality"
    - jmgrosen 7y ago
      Well, I will defer to your judgment! I’m by no means a type theory person. My understanding was that these features are how quotients are managed to be implemented. But perhaps that is wrong.
LemonAndroid 7y ago
Why isn't good stuff like this not more upvoted, but Ross Ulbricht post are simply deleted while I can't delete my comments from 2012 (accname: mkorfmann). Cheerio and you're fun at parties Paul, enjoy that Gin Fizz
zozbot234 7y ago
Very nice work. This kind of embedding (a direct equivalent to "transpiling" for code) is quite common in the formal methods community; for example, Freek Wiedijk has shown a similar embedding of HOL Light https://www.cs.ru.nl/~freek/notes/index.html https://www.cs.ru.nl/~freek/notes/index.html into Coq.
- xvilka 7y ago
  There is also a Dedukti[1][2] project that can load the logic from many different systems, including Coq[3]. [1] https://deducteam.github.io/ https://deducteam.github.io/ [2] https://github.com/Deducteam/ https://github.com/Deducteam/ [3] https://github.com/Deducteam/CoqInE https://github.com/Deducteam/CoqInE
- perthmad 7y ago
  You can actually do much better than mere embeddings. Using program translations similar to what Haskell users routinely perform when using the do-notation for monads, you can actually extend your type theory with new reasoning principles. See for instance the parametric exceptional theory [1], which adds well-behaved exceptions and allows to extend Coq with the independence of premises, i.e. (¬A → ∃n:ℕ. P n) → ∃n:ℕ. (¬A → P n). [1] https://hal.inria.fr/hal-01840643/document https://hal.inria.fr/hal-01840643/document
spidermango 7y ago
How do you pronounce Coq?
- optimiz3 7y ago
  Rooster synonym (see their icon).
- deleted 7y ago
  [deleted]
- wk_end 7y ago
  The correct French pronunciation would be something close to English "coke" but with a shorter 'o' sound.
  - harperlee 7y ago
    I don't think this is correct - coq does not have a /u/ sound in /cok/ but coke is pronounced /couk/ (sorry for the completely unortodox phonetic language).
    - yesenadam 7y ago
      >coke is pronounced /couk/ Well, it entirely depends where you live. The GP's comment make perfect sense where I am, and seem a good explanation, but sure, depends on how you pronounce 'coke'!
- sls 7y ago
  https://forvo.com/word/coq/#fr https://forvo.com/word/coq/#fr
- wyldfire 7y ago
  'Coq' (cock/rooster) in this case is the same as the 'Coq' in "Coq au vin" which is a dish some English speakers might be familiar with.
- rburhum 7y ago
  Not trying to be childish, but let's be honest, this is a horrible name if you are not a native english speaker. I just hear giggles every time somebody mentions this name...
jnordwick 7y ago
These guys shouldn't be supported. Tech already has enough issues with sexism and female participation. This doesn't help the situation at all. I expressed the same opinion last time, and will flag this all day long.
- deleted 7y ago
  [deleted]
Ericson2314 7y ago
The more powerful our languages get and more robust our programs written in them get (those go hand in hand), the easier it will be to compile languages from one language to another without compromising code quality or legibility. I hope this will lead to a new golden age of programming and PL research where more software is not "trapped" in the language and era it is first developed, and we aren't constantly bouncing between the extremes of endlessly accumulating tech debt or naively rewriting.
- firethief 7y ago
  > The more powerful our languages get[...], the easier it will be to compile languages from one language to another I'm not sure about this. Don't languages get their power from restrictions and opinionatedness, that create a fundamental impedance mismatch between any languages that aren't redundant? You can do anything the processor can do in assembly, and the unstructured mass is about as powerful as muscle with no bone. But maybe I'm reading "powerful" too positively. As languages get kitchen-sinky, as JavaScript/C++/Java are with reckless abandon, it will be easier to use them as translation targets (and harder to reason about the results). But won't kitchen-sinky languages eventually give way to languages that haven't yet had time to tie themselves in knots, as C++ (which finished the kitchen and is now putting a second sink in the bathroom) is losing ground to Rust (which only just bolted on async), in an endless cycle of collapse and renewal?

91 points by palmskog 7y ago

This particular feat was triggered by Kevin Buzzard's unsubstantiated claim that "Lean was better than Coq" as a foundation for mathematics, because it had built-in quotient types. The work described above precisely shows that such types can be encoded as well using features shipped with the vanilla Coq distro. See https://sympa.inria.fr/sympa/arc/coq-club/2020-01/msg00006.html https://sympa.inria.fr/sympa/arc/coq-club/2020-01/msg00006.h....

jmgrosen 7y ago
My understanding is that this shows how vanilla Coq still can’t encode quotients well. This project relies on a PR [0] that breaks term normalization, which makes it highly unlikely it will be merged. My understanding is that Lean’s implementation of quotients also breaks normalization, but they don’t care as much about that as Coq devs do. [0]: https://github.com/coq/coq/pull/10390#issuecomment-554316311 https://github.com/coq/coq/pull/10390#issuecomment-554316311
- SkySkimmer 7y ago
  The normalization issue is not about quotients at all. It's https://arxiv.org/abs/1911.08174 https://arxiv.org/abs/1911.08174 "Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality"
  - jmgrosen 7y ago
    Well, I will defer to your judgment! I’m by no means a type theory person. My understanding was that these features are how quotients are managed to be implemented. But perhaps that is wrong.

LemonAndroid 7y ago

Why isn't good stuff like this not more upvoted, but Ross Ulbricht post are simply deleted while I can't delete my comments from 2012 (accname: mkorfmann). Cheerio and you're fun at parties Paul, enjoy that Gin Fizz

zozbot234 7y ago

Very nice work. This kind of embedding (a direct equivalent to "transpiling" for code) is quite common in the formal methods community; for example, Freek Wiedijk has shown a similar embedding of HOL Light https://www.cs.ru.nl/~freek/notes/index.html https://www.cs.ru.nl/~freek/notes/index.html into Coq.

xvilka 7y ago
There is also a Dedukti[1][2] project that can load the logic from many different systems, including Coq[3]. [1] https://deducteam.github.io/ https://deducteam.github.io/ [2] https://github.com/Deducteam/ https://github.com/Deducteam/ [3] https://github.com/Deducteam/CoqInE https://github.com/Deducteam/CoqInE
perthmad 7y ago
You can actually do much better than mere embeddings. Using program translations similar to what Haskell users routinely perform when using the do-notation for monads, you can actually extend your type theory with new reasoning principles. See for instance the parametric exceptional theory [1], which adds well-behaved exceptions and allows to extend Coq with the independence of premises, i.e. (¬A → ∃n:ℕ. P n) → ∃n:ℕ. (¬A → P n). [1] https://hal.inria.fr/hal-01840643/document https://hal.inria.fr/hal-01840643/document

spidermango 7y ago

How do you pronounce Coq?

optimiz3 7y ago
Rooster synonym (see their icon).
deleted 7y ago
[deleted]
wk_end 7y ago
The correct French pronunciation would be something close to English "coke" but with a shorter 'o' sound.
- harperlee 7y ago
  I don't think this is correct - coq does not have a /u/ sound in /cok/ but coke is pronounced /couk/ (sorry for the completely unortodox phonetic language).
  - yesenadam 7y ago
    >coke is pronounced /couk/ Well, it entirely depends where you live. The GP's comment make perfect sense where I am, and seem a good explanation, but sure, depends on how you pronounce 'coke'!
sls 7y ago
https://forvo.com/word/coq/#fr https://forvo.com/word/coq/#fr
wyldfire 7y ago
'Coq' (cock/rooster) in this case is the same as the 'Coq' in "Coq au vin" which is a dish some English speakers might be familiar with.
rburhum 7y ago
Not trying to be childish, but let's be honest, this is a horrible name if you are not a native english speaker. I just hear giggles every time somebody mentions this name...

jnordwick 7y ago

These guys shouldn't be supported. Tech already has enough issues with sexism and female participation. This doesn't help the situation at all. I expressed the same opinion last time, and will flag this all day long.

deleted 7y ago
[deleted]

Ericson2314 7y ago

The more powerful our languages get and more robust our programs written in them get (those go hand in hand), the easier it will be to compile languages from one language to another without compromising code quality or legibility. I hope this will lead to a new golden age of programming and PL research where more software is not "trapped" in the language and era it is first developed, and we aren't constantly bouncing between the extremes of endlessly accumulating tech debt or naively rewriting.

firethief 7y ago
> The more powerful our languages get[...], the easier it will be to compile languages from one language to another I'm not sure about this. Don't languages get their power from restrictions and opinionatedness, that create a fundamental impedance mismatch between any languages that aren't redundant? You can do anything the processor can do in assembly, and the unstructured mass is about as powerful as muscle with no bone. But maybe I'm reading "powerful" too positively. As languages get kitchen-sinky, as JavaScript/C++/Java are with reckless abandon, it will be easier to use them as translation targets (and harder to reason about the results). But won't kitchen-sinky languages eventually give way to languages that haven't yet had time to tie themselves in knots, as C++ (which finished the kitchen and is now putting a second sink in the bathroom) is losing ground to Rust (which only just bolted on async), in an endless cycle of collapse and renewal?