proposition: Lemma compile_bexp_correct: forall C s b d1 d0 pc σ, code_at C pc (compile_bexp b d1 d0) -> transitions C (pc, σ, s) (pc + codelen (compile_bexp b d1 d0) + (if beval b s then d1 else d0), σ, s).
proof: Proof. induction b; cbn; intros. - destruct (d1 =? 0) eqn:Z. + assert (d1 = 0) by (apply Z.eqb_eq; auto). subst d1. autorewrite with code. apply star_refl. + apply star_one. apply trans_branch with (d := d1). eauto with code. auto. - destruct (d0 =? 0) eqn:Z. + assert (d0 = 0) by (apply Z.eqb_eq; auto). subst d0. autorewrite with code. apply star_refl. + apply star_one. apply trans_branch with (d := d0). eauto with code. auto. - eapply star_trans. apply compile_aexp_correct with (a := a1). eauto with code. eapply star_trans. apply compile_aexp_correct with (a := a2). eauto with code. apply star_one. apply trans_beq with (d1 := d1) (d0 := d0). eauto with code. autorewrite with code. auto. - eapply star_trans. apply compile_aexp_correct with (a := a1). eauto with code. eapply star_trans. apply compile_aexp_correct with (a := a2). eauto with code. apply star_one. apply trans_ble with (d1 := d1) (d0 := d0). eauto with code. autorewrite with code. auto. - replace (if negb (beval b s) then d1 else d0) with (if beval b s then d0 else d1). apply IHb. auto. destruct (beval b s); auto. - set (code2 := compile_bexp b2 d1 d0) in *. set (code1 := compile_bexp b1 0 (codelen code2 + d0)) in *. eapply star_trans. apply IHb1. eauto with code. fold code1. destruct (beval b1 s); cbn. + autorewrite with code. apply IHb2. eauto with code. + autorewrite with code. apply star_refl. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences IMP Simulation)