Assignment 08_19

[alkaza]

The proof of Lemma constfold_0plus_sound should be somewhat similar to Lemma optimize_0plus_bexp_sound of the Assignment 08_18. But it appears that it is not. Could you please explain to me why in Lemma optimize_0plus_bexp_sound in Case "::=" we can apply optimize_0plus_aexp_sound. to solve the subgoal aequiv a (optimize_0plus_aexp a), but in Lemma constfold_0plus_sound, this approach doesn't work on the same case's subgoal aequiv a (optimize_0plus_aexp (fold_constants_aexp a)). How do I get fold_constants out of my way? Could you give me any hint on how to move from there?

[alkaza]

I feel I should use Theorem fold_constants_aexp_sound but I don't know how...

[jaewooklee93]

Well.. Actually that exercise is the easiest one which can be solved by few tactics. Since we proved the correctness of two optimizations, and fold_constants is a composite of those two, the correctness of fold_constants also follows.

[alkaza]

I don't understand :(

[alkaza]

So, I get to here:

2 subgoal
c : com
st : state
st' : state
H : c / st || st'
______________________________________(1/2)
optimize_0plus_com (constfold_0plus c) / st || st'
______________________________________(2/2)
c / st || st'

Then what can I do?

[jaewooklee93]

I mean, we proved the following at the previous exercise. For all c, (1) c and (constfold_0plus c) are equivalent. (2) c and (optimize_0plus_com c) are equivalent

Thus, we can draw the conclusion using the transitivity of cequiv, c and (optimize_0plus_com (constfold_0plus c)) are equivalent.

Thus, you don't need to unfold cequiv, and you can apply trans_cequiv just after doing unfold ctrans_sound.

[AdamBJ]

I can't get trans_cequiv working right. Still stuck on the plus case. Given that this homework can't be handed in anymore, would you consider posting your solution?

[jaewooklee93]

Sure.

Lemma constfold_0plus_sound:
  ctrans_sound constfold_0plus.
Proof.
  intros c.
  apply trans_cequiv with (fold_constants_com c).
  apply fold_constants_com_sound.
  apply optimize_0plus_com_sound.
Qed.

[AdamBJ]

Wow, you weren't kidding that it was a simple answer!

[AdamBJ]

Thanks for the help

[jaewooklee93]

Also, we learned much more automation recently. Thus, even single line solution can be.

Hint Unfold ctrans_sound.
Hint Resolve trans_cequiv fold_constants_com_sound optimize_0plus_com_sound.

Lemma constfold_0plus_sound:
  ctrans_sound constfold_0plus.
Proof with eauto.
  unfold constfold_0plus...
Qed.