Tip 1

Think carefully on what you want to be doing induction on: commands, or proofs of eval? In many cases both are possible, but not always: theorems that require reasoning about equivalences between loops will typically not be provable by induction on a command.

Tip 2

Do not assume that all lemmas are directly provable as stated: you will often need intermediate lemmas. For example, for eval_deterministic, you will likely want to prove a variant with premises reordered to get a stronger induction hypothesis. For opt_constprop_sound, you'll want to make a generalized version with an arbitrary consts set instead of $0.

Tip 3

Automation can help with many of the proofs in this exercise. The tactics eval_intro may be convenient building blocks to use in your own tactics.

To detect an arbitrary match from Ltac, use match ?x with _ => _ end.

Tip 4

Coq's standard library contains many lemmas — you do not need to prove everything from first principles! Among other lemmas, our solution uses the following, which get automatically picked up by autorewrite with core in *:

Local Hint Rewrite Nat.mul_0_r Nat.div_1_r Nat.add_0_r.
Local Hint Rewrite <- Nat.ones_equiv.
Local Hint Rewrite Nat.mul_1_r Nat.shiftl_mul_pow2 Nat.shiftr_div_pow2 Nat.land_ones.

As always, use Search to find relevant lemmas.

Tip 5

Beware of issues with operator precedence: (n - 1) mod 2 is not the same as n - 1 mod 2.