Homework 1

1. Install Coq 8.16.1 on your computer (see the installation notes).
2. Download Basics.v, Induction.v, and Lists.v.
3. You may use any interactive development environment for Coq: CoqIDE, VSCode, or Proof General. The rest of these instructions assume you're using CoqIDE.
4. Change the navigation shortcut from <ctrl><alt> to <ctrl> and change the font to Lucida Sans Unicode.
5. Using coqide, interactively step through the first few definitions and/or proofs in Basics.v.
6. Compile Basics.v to produce Basics.vo. You can do this either via the Compile/Compile-Buffer menu tab, or using the coqc command in the shell.
7. Check that your compile worked by using coqide to step through the first command of Induction.v, the line "Require Export Basics."
8. Fill in the proofs in Basics.v, at each place marked "Exercise". Add a README comment at the top describing who you helped (or got help from), and what kind of help.
9. Upload your Basics.v file at right.
10. Fill in the proofs in Induction.v, and Lists.v at each place marked "Exercise", and upload those.
    
11. If you got help from other than the teaching assistants or the professor, add a README comment at the top of Basics.v describing who you helped (or got help from), and what kind of help (and re-upload Basics).