Nothing beside the earlier lectures at this summer school. You might want to review files `Semantics.v` and `Compiler.v` from Xavier Leroy's lectures!

directory `auto` of `dsss17` repository

Add `do..while` to Imp and extend our automated compiler proofs from class to accommodate it.
Directory `auto` now contains the end-product code from class.
This exercise is about modifying files there to extend with new features, which includes a component of understanding how things work now.
These files continue further along than we were able to get to in class, though you're free to stop your extension process at any point in the sequence from file `Semantics.v` to file `Compiler.v`.
The starting point would be editing `SF/lf/Imp.v` to add the language feature.

Alternatively, go back and add more automation to all the homework you've done so far at this summer school!

code posted after class

Implement a reflective procedure for normalizing systems of linear equations over rational numbers. In particular, the tactic should identify all hypotheses that are linear equations over rationals where the equation righthand sides are constants. It should normalize each hypothesis to have a lefthand side that is a sum of products of constants and variables, with no variable appearing multiple times. Then, your tactic should add together all of these equations to form a single new equation, possibly clearing the original equations. Some coefficients may cancel in the addition, reducing the number of variables that appear.

To work with rational numbers, import module `QArith` and use `Local Open Scope Q_scope.`.
All of the usual arithmetic operator notations will then work with rationals, and there are shorthands for constants 0 and 1.
Other rationals must be written as `num # den` for numerator `num` and denominator `den`.
Use the infix operator `==` in place of `=`, to deal with different ways of expressing the same number as a fraction.

For instance, a theorem and proof like this one should work with your tactic (called `reifyContext` here):

Theorem t2 : forall x y z, (2 # 1) * (x - (3 # 2) * y) == 15 # 1 -> z + (8 # 1) * x == 20 # 1 -> (-6 # 2) × y + (10 # 1) * x + z == 35 # 1. Proof. intros; reifyContext; assumption. Qed.The effect of calling

More on this theme is found in Adam's books *Certified Programming with Dependent Types*, for general Coq strategies; and *Formal Reasoning About Programs*, for applications to semantics and program proof.