coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Exercises on dependent type proofs?

From: Siddharth Bhat <siddu.druid AT gmail.com>
To: Adam Chlipala <adamc AT csail.mit.edu>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Exercises on dependent type proofs?
Date: Wed, 17 Jan 2018 16:54:46 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=siddu.druid AT gmail.com; spf=Pass smtp.mailfrom=siddu.druid AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f178.google.com
Ironport-phdr: 9a23:EJe2qhDVi7eJ5zbV3CD6UyQJP3N1i/DPJgcQr6AfoPdwSPv9rsbcNUDSrc9gkEXOFd2Cra4c0qyO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUmTaxe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Qiqp4bt1RxD0iScHLz85/3/Risxsl6JQvRatqwViz4LIfI2ZMfxzdb7fc9wHX2pMRsleVyJDDY28YYUBDPcPM/hEoITmvVQCsQGzCBOwCO/zyDJFgGL9060g0+QmFAHLxBEuH9MTv3vJrNX6Lr0SUfy1zKLV0DjDb+lZ2Svg44XPaRAhoOyDUq9tccbL1EYvDR7FjlSNpoH+MDOV0/4Cs2mf7+Z6Se2vjGsnphh3rzOyxckskpHEipwJxl3A7yl0w4Y4KcemREJlfdKoCoZcuiOZOoZwX8gsWXtnuDwgxb0DoZO7fDYFyJAgxxPHbvyIaYmI4hb6WOaIIjd0mGtpeLyiixuw8kWs0OL8Vs6z0FZFqipKjMPAuWwK1xzW8sSHS/198Vm92TuXyQzf9uVJLVo3mKfbMZIt3KA8moYJvUjeHCL7m136jKqMeUUl/uio5f7nYrLjppKELI90ixzxPbkzmsClHOs4KBUOX2mG9umn273j+Ff2QLROjvEsjqbZt5XaKdwBpqGlGw9Vzpoj6xGnAji619QYhGALI05BeBKalIfkIErOIfD9DfenmVugijZrx/bcPr3gGJrBNHbDkK2yNYp6vmdQwQ975tBb5opdDrhJdPv/U0r6nNfDBx49dQm136DqBMgrha0EXmfaOa6VPKPbq0OIrsgvKvXEMJQUtDrgbfQ/+v/ipXA8kF4ZO6Ku2M1EOziDAv16LhDBMjLXidAbHDJP51JmFb24uBi5STdWIk2Kcec57zA/BpihCN6aFI+oib2Fmiy8G88PPzwUOhW3CX7tMr68dbIUcivLe51ulzUFUf6qTIpzjUjz5j+/8KJuK6/vwgNdtZ/n04IrtejalBV37D8sSsrEjDHLQGZzkWcFATQx2fInrA==

For context, I was hoping for things like small libraries to.. proof fix? Or things of that nature. Some real world experience on this stuff.

Cheers,
Siddharth

On Wed 17 Jan, 2018, 22:19 Siddharth Bhat, <siddu.druid AT gmail.com> wrote:

Ah no. I haven't seen that. Will solve :)
Once that's done, any other recommendations?

Thanks,
Siddharth

On Wed 17 Jan, 2018, 21:45 Adam Chlipala, <adamc AT csail.mit.edu> wrote:

Glad to hear you are getting some mileage out of CPDT!

There is an exercises page on the CPDT web site. Did you check it out? (I couldn't claim it's nearly as well-synchronized with the content as are SF's exercises.)

On 01/17/2018 09:53 AM, Siddharth Bhat wrote:

Hello all,

I've been solving software foundations, and while it's very satisfying, it doesn't show off much of the dependent typed abilities of coq (at least, so far)

CPDT has the opposite problem; it explains very well, but I could find no exercises!

Does anyone have some "recommended exercises" that are paced as well as the SF ones are?

Thanks for everyone who helped in writing both the books, they're amazing!

Cheers

Siddharth

--

Sending this from my phone, please excuse any typos!

--
Sending this from my phone, please excuse any typos!

Sending this from my phone, please excuse any typos!

[Coq-Club] Exercises on dependent type proofs?, Siddharth Bhat, 01/17/2018
- Re: [Coq-Club] Exercises on dependent type proofs?, Adam Chlipala, 01/17/2018
  - Re: [Coq-Club] Exercises on dependent type proofs?, Siddharth Bhat, 01/17/2018
    - Re: [Coq-Club] Exercises on dependent type proofs?, Siddharth Bhat, 01/17/2018