- Project 3 Extension
- Mystery tactics
- Crypto theory
- Project 3 is posted
- Runtime Checks to Type Checks
- Dependent Register File
- Bounded register file
- Array model from class
- distr_rev
- Eval on theorems

Blog

A couple of hints on the proof for `distr_rev`

in your current project. First, it goes largely the same way that the examples we did in class do. Start with induction and look for lemmas that can help get rid of proof goals. Second, you may need lemmas for both the base case and inductive cases. Your mileage may vary, but my proof worked out that way. Finally, try rewriting with your inductive hypothesis *before* starting your lemma proofs. Sometimes rewriting will result in a simpler lemma.

Do not forget `simpl`

before diving into an auxilliary lemma.

Do go back and check your lemma statements. I had difficulty proving one that was clearly false because of a simple typo.

Bottom line is that this proof goes just like the one in class with only one or two small twists.