Complete this form and hit the "Save Changes" button!
No ratings
Are you sure you want to delete this code? Please type DELETE in the box below to confirm.
Are you sure you want to verify this code?
Are you sure you want to publish this code?
Are you sure you want to unpublish this code?
Are you sure you want to autogenerate the summary + description for this code?
xxxxxxxxxx
Require Export P09.
(** **** Exercise: 3 stars (fold_constants_com_sound) *)
(** Complete the [WHILE] case of the following proof. *)
Theorem fold_constants_com_sound :
ctrans_sound fold_constants_com.
Proof.
unfold ctrans_sound. intros c.
induction c; simpl.
- (* SKIP *) apply refl_cequiv.
- (* ::= *) apply CAss_congruence.
apply fold_constants_aexp_sound.
- (* ;; *) apply CSeq_congruence; assumption.
- (* IFB *)
assert (bequiv b (fold_constants_bexp b)). {
apply fold_constants_bexp_sound. }
destruct (fold_constants_bexp b) eqn:Heqb;
try (apply CIf_congruence; assumption).
(** (If the optimization doesn't eliminate the if, then the
result is easy to prove from the IH and
[fold_constants_bexp_sound].) *)
+ (* b always true *)
apply trans_cequiv with c1; try assumption.
apply IFB_true; assumption.
+ (* b always false *)
apply trans_cequiv with c2; try assumption.
apply IFB_false; assumption.
- (* WHILE *)
exact FILL_IN_HERE.
Qed.
