Notes on Homework 1

Import and Export statements. Near the top of Induction.v, there is the statement

Require Export Basics.

This Export statement (and the similar Import statement) reads a ".vo" file, in this case Basics.vo. You create this by compiling Basics.v, either using the coqc program, or inside CoqIDE while visiting Basics.v, using the Compile/Compile-Buffer menu tab.

If you are using VSCode, see here for compilation instructions.

It will suffice to compile the Basics.v that we gave you originally; when Induction imports Basics, it doesn't care whether the theorems were admitted or proved. When we grade your homework, we will always use the Basics.vo that we build from the original Basics.v.

The "Check" button.

The Basics.v file that we give you compiles successfully in Coq, although of course many results are "Admitted." The Basics.v file you submit must compile successfully in Coq, or you will get no credit.

The button labeled "Check All Submitted Files" will tell you,

First, whether your file compiles successfully in Coq.
Second, where are all the results that are still Admitted. You won't get credit for those results, of course, but they won't prevent you from getting credit for the ones you do prove (or define).
In addition, for the first few assignments you must not use the "auto" tactic; the "Check" program will notice those too.
Third, whether all the statements of the theorems (and types of the definitions) are what they should be. You should rarely have a problem with this unless for some reason you edit the statement of a theorem to be proved.

One of the proofs in Basics.v is "Write an informal proof of ...". If you forget to do this one, the "Check" program won't notice that for you!

The "Check" program does not determine your grade! It just helps you make sure you've completed all the relevant tasks. Your proofs will be graded for correctness (which is mostly handled automatically) and style: The clarity of your presentation, the clarity of your induction hypotheses, and so on. In the first homework there's not much room for you to be creative, but that will change as your proofs grow more sophisticated.

All of this applies to the .v files in future homeworks.

Fonts in the "Check" window

If the font is so big in the Check window that you're scrolling around too much, you may want to change your browser's font in the Check window.

Note on dependent files:

In checking your Induction.v file (and for the "Check All Submitted Files" button), our check-scripts import the original unmodified version of Basics.v, not whatever version you submitted in the last homework.