coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: mechvel AT scico.botik.ru
- To: Jason Gross <jasongross9 AT gmail.com>
- Cc: coq-club <coq-club AT inria.fr>, agda-list <agda AT lists.chalmers.se>, coq+miscellaneous AT discoursemail.com, lean-user <lean-user AT googlegroups.com>
- Subject: Re: [Coq-Club] [Agda] Why dependent type theory?
- Date: Wed, 04 Mar 2020 01:14:14 +0300
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mechvel AT scico.botik.ru; spf=Pass smtp.mailfrom=mechvel AT scico.botik.ru; spf=None smtp.helo=postmaster AT mail.botik.ru
- Ironport-phdr: 9a23:ki+1aBDyu//C0SKpuvCHUyQJP3N1i/DPJgcQr6AfoPdwSPv9psbcNUDSrc9gkEXOFd2Cra4d16yP6/6rADFRqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAi5oAnLq8UanYpvJqksxhbJpnZDZvhby35vKV+PkBnw4du98oR++CpKofIh8MBAUaT+f6smSLFTESorPWMo6sD1rBfPVQSA6GcSXWUQiRpIHhPK7ArmUZfrsyv1rfRy1S+HNsDrV780WDCi76B2SB/0jSoMKjA0/H3LhsF2kalWuwyqqQBhzIHIYYGVLPt+cb3bfdMGXmpKQ8JdWzVcDo+gc4cDCuwMNvtaoYbgvVsDtRSxChWjCu3hyjFGmGL40q800+oiHgDJ0hctH84MvXTWsNn5KL0fXf6zwaLVzTvDdfRW2TLl5YjNbB8uvfGMXaxufsrV0kQvDB/KjlSMpoziJT+azeMNs3Sa7+pjT+6vkXMnpgdsqTas3schko3Ei4IPxlzZ6yl0xJw5KcC2RUN5e9KoDZpduiCCO4ZyQs4uWXxktDg+x7EcpJK2cioHxI46yxPbdvCKdZWD7Aj5W+aLOzh4gWpoeLKhiBa29kit0uj8WdO10FZOtCZKid7MtmwM1xzQ8MSHUOZ98l+g2TaJyQ/T9vlJLEQ0mKbBNpIt3Lo9moAOvUnNHCL6glj6ga6Xe0k8/+in8eXnYrHopp+GMI90jxnzMqEwlcOjAeQ4LBYBX2yA9OSnyLLj/FH2QLJQgvItlanZrJHaJccBqq6jHg9Zypwj5AqnDze6zNQYmmEKI05CeBKeloTmJ1XOIO3jAvqkmFStkDJrx+jcMbH7A5XNKGLDkLb7crpn5U5c0ll78dcKxZtPDbdJD+j0QVS54N7RFRg/PBaz2P22INp434IaH2mIB/nKHrnVtAqN6+kvPeSITJQeuT36bfIi+//ty2UkygxVRrWgwZZCMCPwJf9hOUjMJCO02o5cQ1dPhRI3SanRsHPHUTNXYC/vDac15zV9AoW6DISFXJ3/2OXQjhf+JYVfYyV9Mn7JFH7pc4ueXPJVNnCJKc5qlXoOUqSgSMk7yEP37VOo+/9cNuPRvxYgm9f7ztEsub/InhA58np+CNic0CeXUjMskw==
On 2020-03-03 22:43, Jason Gross wrote:
I'm in the process of writing my thesis on proof assistant performance
bottlenecks (with a focus on Coq), and there's a large class of
performance bottlenecks that come from (mis)using the power of
dependent types. So in writing the introduction, I want to provide
some justification for the design decision of using dependent types,
rather than, say, set theory or classical logic (as in, e.g.,
Isabelle/HOL). And the only reasons I can come up with are "it's fun"
and "lots of people do it"
So I'm asking these mailing lists: why do we base proof assistants on
dependent type theory? What are the trade-offs involved?
I'm interested both in explanations and arguments given on list, as
well as in references to papers that discuss these sorts of choices.
For example, mathematicians write:
"In any field F there is an inversion operation for a nonzero elements:
inv : F\{0} -> F
".
With dependent types, the type of inv is expressed as
(x : F) -> x /= 0# -> F
This type depends on the value x, and this value can change during some computation.
And I do not know how to express as a type this mathematical notion.
There are many such examples.
Also dependent types are good for constructive proofs.
For example, consider a theorem
"For any prime number p there exists a prime q greater than p".
With dependent types, we prove a stronger statement:
"This provided below algorithm A takes any prime number p and returns a prime q greater than p".
If one cannot invent a constructive proof, but can prove the thing in a classical logic,
then one can add the postulate of excluded third and write a classical proof in Agda.
Regards,
------
Sergei
- Re: [Coq-Club] Why dependent type theory?, (continued)
- Re: [Coq-Club] Why dependent type theory?, Pierre Courtieu, 03/04/2020
- Re: [Coq-Club] Why dependent type theory?, Pierre-Marie Pédrot, 03/04/2020
- Re: [Coq-Club] Why dependent type theory?, Jesper Cockx, 03/03/2020
- Re: [Coq-Club] Why dependent type theory?, Ralf Jung, 03/04/2020
- Re: [Coq-Club] Why dependent type theory?, Jesper Cockx, 03/04/2020
- Re: [Coq-Club] Why dependent type theory?, Ralf Jung, 03/04/2020
- Re: [Coq-Club] Why dependent type theory?, Jesper Cockx, 03/04/2020
- Re: [Coq-Club] Why dependent type theory?, Ralf Jung, 03/04/2020
- Re: [Coq-Club] Why dependent type theory?, Christian Doczkal, 03/03/2020
- Re: [Coq-Club] Why dependent type theory?, Ken Kubota, 03/03/2020
- Re: [Coq-Club] Why dependent type theory?, jonikelee AT gmail.com, 03/03/2020
- Re: [Coq-Club] Why dependent type theory?, Daniel Schepler, 03/03/2020
- Re: [Coq-Club] [Agda] Why dependent type theory?, mechvel, 03/03/2020
- Re: [Coq-Club] [Agda] Why dependent type theory?, Steven Shaw, 03/03/2020
- Re: [Coq-Club] [Agda] Why dependent type theory?, Steven Shaw, 03/03/2020
- Re: [Coq-Club] [Agda] Why dependent type theory?, Martin Escardo, 03/03/2020
- Re: [Coq-Club] [Agda] Why dependent type theory?, Sylvain Boulmé, 03/04/2020
- Re: [Coq-Club] [Agda] Why dependent type theory?, Kevin Buzzard, 03/05/2020
- Re: [Coq-Club] [lean-user] Re: [Agda] Why dependent type theory?, Bas Spitters, 03/08/2020
- Re: [Coq-Club] [Agda] [lean-user] Re: Why dependent type theory?, Thorsten Altenkirch, 03/12/2020
- Re: [Coq-Club] [Agda] [lean-user] Re: Why dependent type theory?, Mario Carneiro, 03/13/2020
- Re: [Coq-Club] [Agda] [lean-user] Re: Why dependent type theory?, Kevin Buzzard, 03/13/2020
- Message not available
- Message not available
- Re: [Coq-Club] [Agda] [lean-user] Re: Why dependent type theory?, Bas Spitters, 03/17/2020
- Message not available
- Re: [Coq-Club] [Agda] [lean-user] Re: Why dependent type theory?, Thorsten Altenkirch, 03/12/2020
- Re: [Coq-Club] [lean-user] Re: [Agda] Why dependent type theory?, Bas Spitters, 03/08/2020
Archive powered by MHonArc 2.6.18.