Project 0 - Building IMP

The objective of this project is to build a platform for proving properties about IMP programs while getting more familiar with Rocq. Most of the project is available in our class materials and has been presented in class. However, I find it a useful exercise to clean things up and put them in a usable form.

1. Encode an abstract syntax for IMP. Your definition should include all the basic IMP constructs plus division and a for loop.
2. Create functional definitions for aeval and beval.
3. Create relational definitions for aevalR, bevalR and cevalR.
4. Prove that aeval and beval are correct with respect to aevalR and bevalR. Explore how you might account for error cases such as division by 0 and negative subtraction.

Note that the proving part of this homework is not prescriptive in that I am more interested in your exploration than in seeing any specific solution.