coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Théo Zimmermann <theo.zimmermann AT ens.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Lean Theorem Prover
- Date: Thu, 25 Feb 2016 11:45:32 +0000
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=theo.zimmermann AT ens.fr; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f41.google.com
- Ironport-phdr: 9a23:SqneEBLJrPnHenUcjtmcpTZWNBhigK39O0sv0rFitYgULv3xwZ3uMQTl6Ol3ixeRBMOAu60C1bKd6PmocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWC0ILpj6vpotX6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD86Fpy8kVWqLjOq88ULZwDTI8Mmlz6te4mwPESF6z5vobZVcXlx9FGQ3M6heyCovxvyy8pOt43SSAOMTwS5g5Xy/k4b09G0ygszsOKzNsqDKfscd3lq8O+B8=
Hi Freek,
Lean has two modes: one standard and one "HoTT". The standard one has proof irrelevance built-in, indeed, but the HoTT one has not, of course. Leonardo de Moura claims that Lean would make it possible to add new modes, if a new logic became of much interest for experimentation.
As for bridging the gap between automated theorem proving and interactive theorem proving, this is a long term goal. Leonardo de Moura comes from the world of automated theorem proving so has probably some interesting plans on how to do so.Lean has two modes: one standard and one "HoTT". The standard one has proof irrelevance built-in, indeed, but the HoTT one has not, of course. Leonardo de Moura claims that Lean would make it possible to add new modes, if a new logic became of much interest for experimentation.
Le jeu. 25 févr. 2016 à 12:01, Freek Wiedijk <freek AT cs.ru.nl> a écrit :
Hi Jonathan,
>It looks eerily similar to Coq.
I also is quite different from Coq in some respects.
It is implemented in C++, not in ML. It has proof
irrelevance, function extensionality, classical logic, even
a choice operator as part of the standard setup (exactly
which of those are hardwired in, and which ones are just
conventionally available in the library, I don't know.)
It has been explicitly designed to be useful for HoTT (how
that can be true in conjunction with the previous sentence, I
don't know :-)) The type theory is simpler: they don't have
"match" in the foundations, but instead work with recursors,
and they don't have universe cumulativity.
Jeremy Avigad is one of the people behind Lean. He comes
from an Isabelle background. I can imagine Lean will feel
more familiar to Isabelle people than Coq does.
Freek
- [Coq-Club] Lean Theorem Prover, Saulo Araujo, 02/25/2016
- Re: [Coq-Club] Lean Theorem Prover, Jonathan Leivent, 02/25/2016
- RE: [Coq-Club] Lean Theorem Prover, Soegtrop, Michael, 02/25/2016
- Re: [Coq-Club] Lean Theorem Prover, Benjamin Pierce, 02/25/2016
- RE: [Coq-Club] Lean Theorem Prover, Soegtrop, Michael, 02/25/2016
- Re: [Coq-Club] Lean Theorem Prover, Benjamin Pierce, 02/25/2016
- Re: [Coq-Club] Lean Theorem Prover, Freek Wiedijk, 02/25/2016
- Re: [Coq-Club] Lean Theorem Prover, Théo Zimmermann, 02/25/2016
- Re: [Coq-Club] Lean Theorem Prover, Bas Spitters, 02/25/2016
- Re: [Coq-Club] Lean Theorem Prover, roux cody, 02/25/2016
- Re: [Coq-Club] Lean Theorem Prover, Clément Pit--Claudel, 02/25/2016
- Re: [Coq-Club] Lean Theorem Prover, Clément Pit--Claudel, 02/25/2016
- Re: [Coq-Club] Lean Theorem Prover, Jonathan Leivent, 02/25/2016
- Re: [Coq-Club] Lean Theorem Prover, roux cody, 02/25/2016
- Re: [Coq-Club] Lean Theorem Prover, John Wiegley, 02/25/2016
- RE: [Coq-Club] Lean Theorem Prover, Soegtrop, Michael, 02/25/2016
- Re: [Coq-Club] Lean Theorem Prover, Daniel Schepler, 02/25/2016
- Re: [Coq-Club] Lean Theorem Prover, Abhishek Anand, 02/25/2016
- Re: [Coq-Club] Lean Theorem Prover, Daniel Schepler, 02/26/2016
- Re: [Coq-Club] Lean Theorem Prover, roux cody, 02/26/2016
- Re: [Coq-Club] Lean Theorem Prover, Daniel Schepler, 02/26/2016
- Re: [Coq-Club] Lean Theorem Prover, Abhishek Anand, 02/25/2016
- Re: [Coq-Club] Lean Theorem Prover, Jonathan Leivent, 02/25/2016
Archive powered by MHonArc 2.6.18.