proposition: Lemma compile_aexp_correct: forall C s a pc σ, code_at C pc (compile_aexp a) -> transitions C (pc, σ, s) (pc + codelen (compile_aexp a), aeval a s :: σ, s).
proof: Proof. induction a; simpl; intros. - apply star_one. apply trans_const. eauto with code. - apply star_one. apply trans_var. eauto with code. - eapply star_trans. apply IHa1. eauto with code. eapply star_trans. apply IHa2. eauto with code. apply star_one. autorewrite with code. apply trans_add. eauto with code. - eapply star_trans. apply IHa1. eauto with code. eapply star_trans. apply IHa2. eauto with code. eapply star_trans. apply star_one. apply trans_opp. eauto with code. apply star_one. replace (aeval a1 s - aeval a2 s) with (aeval a1 s + (- aeval a2 s)) by lia. autorewrite with code. apply trans_add. eauto with code. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences IMP Simulation)