You will have an easier time if you define a function to test for constants, like so:

Definition as_const (e: expr) : option nat :=
  match e with
  | Const n => Some n
  | _ => None
  end.

Otherwise, goals will get very large.

In the proof of opt_constprop_sound, or more likely the strengthened version of it, you will probably find the following lemma useful:

Lemma includes_remove_add (consts v: valuation) x n:
  consts $<= v ->
  consts $- x $<= v $+ (x, n).

In the implementation of read_only, you can use if x ==v x0 then true else false to get a Boolean indicating whether two variables are equal.

Programs in this section can get pretty big — consider adding intermediate definitions and proving lemmas about them. For example, I used this:

Definition loop1 x body :=
  body;; x <- x - 1.

Lemma opt_unroll_decr : forall {phi v v' x body n},
    eval phi v (loop1 x body) v' ->
    read_only body x = true ->
    v $? x = Some n ->
    v' $? x = Some (n - 1).

The key difficulty in this problem is connecting the unrolled loop body to the original loop body. Because of the way EvalWhileTrue and EvalWhileFalse are defined, regular induction gives you two cases: one where the loop exits immediately and one where it runs n + 1 times.

Instead, you want to think about three cases: the loops exits immediately, the loop runs a single time, and the loop runs n + 2 times. The key is to make a lemma that mentions both of these cases at once. Let's look at a concrete example:

Fixpoint even (n: nat) :=
  match n with
  | 0 => True
  | 1 => False
  | S (S n) => even n
  end.

Lemma even_sum : forall x y, even x -> even y -> even (x + y).
Proof.
  induction x; intros.
  - simpl. assumption.
  - destruct x.
Abort.

This proof is stuck: intuitively, IH steps one step forward, and we want to take two steps at once.

The trick is to generalize the lemma to assert two "levels":

Lemma even_sum : forall x y,
    (even x -> even y -> even (x + y)) /\
    (even (S x) -> even y -> even (S x + y)).
Proof.
  induction x; intros.
  - destruct y; firstorder.
  - firstorder.
Qed.

What does that mean for this exercise? Chances are you'll probably come up with a lemma that looks like this at some point:

Lemma opt_unroll_template_sound : forall phi v v' x body n,
    n mod 2 = 0 ->
    v $? x = Some n ->
    read_only body x = true ->
    eval phi v (while x loop (loop1 x body) done) v' ->
    eval phi v (while x loop (loop1 x body);; (loop1 x body) done) v'.

… but it won't work by induction. No, what you need is this, which will work by induction:

Lemma opt_unroll_template_mx_sound : forall phi v v' x body n,
    v $? x = Some n ->
    read_only body x = true ->
    eval phi v (while x loop (loop1 x body) done) v' ->
    eval phi v (if n mod 2 =? 0 then
                while x loop (loop1 x body);; (loop1 x body) done
            else
                (loop1 x body);;
                while x loop (loop1 x body);; (loop1 x body) done) v'.

One last trick: this form with an if is essentially a partially evaluated version of the full loop-unrolling template, with the “fixup” phase at the beginning. In other words, you can prove the following theorem:

Lemma opt_unroll_eqn {phi v v' body x}:
let n := match v $? x with Some n => n | None => 0 end in
eval phi v (if n mod 2 =? 0 then
            while x loop (loop1 x body);; (loop1 x body) done
            else
            (loop1 x body);;
            while x loop (loop1 x body);; (loop1 x body) done) v' ->
eval phi v (when (x mod 2) then loop1 x body else Skip done;;
            while x loop (loop1 x body);; (loop1 x body) done) v'.