DeepSpec Summer School, July 13-28, 2017

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 reifyContext is to replace the two hypotheses with one that matches the conclusion exactly. (The individual coefficients just happen to add up that way.)

demos using Bedrock, Fiat, and Kami

none