coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Adam Chlipala <adamc AT csail.mit.edu>
To: Siddharth Bhat <siddu.druid AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Exercises on dependent type proofs?
Date: Wed, 17 Jan 2018 11:15:46 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=adamc AT csail.mit.edu; spf=Pass smtp.mailfrom=adamc AT csail.mit.edu; spf=None smtp.helo=postmaster AT outgoing-stata.csail.mit.edu
Ironport-phdr: 9a23:RfW7mBY+pZUCb9UvMmHUObn/LSx+4OfEezUN459isYplN5qZoMi8bnLW6fgltlLVR4KTs6sC17KP9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCagbb9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjAk7m/XhMx+gqFVrh2vqBNwwZLbbZqPO/ZiZK7QZ88WSGRDU8tXSidPApm8b4wKD+cZIetXspPyp14TphagBQmsAOLvyidSiX/yx6IxzuMsHhvb0wM6GtIBrG/Zo8nuNKgIUOC1yLPEzTDCb/NKwzvy9pXHcg04rPyKQLl+ctLRxFEyGw/bjVics4LoMy+P2ugTqWSX8fdsWf63h2MmtQ19uCWjy8MyhoXTmI4Z0E3I+Ct2zYszONa2UlR0YcS+H5tVryyaN5V5QsclQ2xwvyY616EGuZG8fCgLzpQnyAfTa+ebc4eS/hLsTvydLitjhH1/ebK/gwy+8U2hyu3gTMW7zktFrjddntnNsHACyQDT59CaRvdj/UqtwziC2xzJ5u1aO0w4i7fXJ4I5zr41jJUTsEDDHiHsmEXxia+bbl8r9fWy5OTifrrrvYOTN5RuhQH/NqQigMm/AeUkMgQUQWeU5Pm82KX5/ULlWLVKkuE2kq7BvZ/GIsQbv7e1DBNR0oY+8BmyFCym0dQdnXkfNl1JYhOHj47zO1HPOv/0F/m/g07/2AtsksvHMrHhC4/RLjDpkL79NeJm6kJQ1Uw/181e67pbD7gAJLT4XUqn5/LCCRpsGgC9xq7MCNF8zooaUCrbC6OQNaj6ukSB5+ZpJuiQIoIZpWCueLAe+/fygCphyhcmdq6z0M5PMSHqLrFdO0ycJEHUrJIEGGYOsBA5SbW32laZWD9XIXOzQ+Qx6ixpUdv6X7eGfZikhfm65An+BodfPz0UAUuFEHOucoSYHfoAdXDKe5Izonk/TbGkDrQZ+1SuuQv9kOI1KffI9SoZs52mz8R8++SVngo79DgyCsWBlWyBUjMskw==

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!

[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