coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Exercises on dependent type proofs?

From: Siddharth Bhat <siddu.druid AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Exercises on dependent type proofs?
Date: Wed, 17 Jan 2018 14:53:22 +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-f173.google.com
Ironport-phdr: 9a23:3ImdXh1+i+Y0fmlXsmDT+DRfVm0co7zxezQtwd8Zse0WLPad9pjvdHbS+e9qxAeQG9mDsrQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPfglEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLnhycJOTA6/m/KlMJ/kLlWrwi9qxFl2YPYfJ2ZOfh4c6jAfd0aX21BXsNJWiJcA4OzcpYAD+obMuZCs4n9p0YFoAa+BQa2GOPk1zhFhmT33aInzushDBvK0xE6H9ITsXTbsc74NKgXUe+vzanIyS/PYO9R2Tf48YXFdA0qr/KUXb9ob8bd1U0iGxnGg1iQs4DpIS2Z2vgXv2SG7edtW+SigHM9pQ5ruDig3MIsh5HJho0LzlDE8j10wIMvKt25TE53eMekEJhMuy2DOYt6X8EvTm9ytCY1zb0GvpG7fCwUx5g92xHfbPmHf5CJ4hLlSumRPS91iGx5dL+7nRq/8kitxvfiWsWqzFpGtDdJn9vCu3wV0hzc8MmHSv9z/ke73jaP0hje6vpFIU8piKXbNoQtzaMqlpoOsETMAzT7mErzjKCMd0Uk/vKk5PjgYrXjvpOcLZN7ihniMqQyncyyGfg3Mg8XX2SC5eu80KDj8lbiTbVRjvw2l7HZv4rAKcQaoK65GQ5V3Zw55xaxFTf1mOgfyHIANRdOfA+Np4nvIVDHZv7iXtmlhFH5qzZny/DPJKHhSr/NJ2SLxKzgcbpgrUJG1Qs/5d9a7pNQTLoGJaSgCQfKqNXEA0phYESPyOH9BYAlj9JMaSe0GqacdZjqnxqN7+MrLfOLYdZM6jn4IvkhofXpiC1gwANPTeySxZISLUuAMLF+OUzAOCjjh94AFSEBuQ9sFLW32m3HaiZaYjOJZ4x55jw/D9j4X4LKR4Tomb/ZmSniQcYQaWdBBVSBV3zvctfcVg==

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