Homework: Software foundations

Software foundations is a good introductory text to using Coq. For 6.826 we will use a few chapters to get you ready for the 6.826 labs. To do these exercises, you will have to first install Coq and then download the source code for Software Foundations, which contains the Coq files for the exercises.

For this homework you should do:

• All of the exercises in the Poly chapter except for "Additional Exercises".
• All of the exercises in the Tactics chapter except for "Additional Exercises".
• All of the exercises in the Logic chapter except for "tr_rev_correct" and "Classical vs. Constructive Logic".

You don't have to submit your solutions and you won't be graded on them; but, if you are unfamiliar with Coq, you better do these exercises.