proposition: Lemma compile_com_correct_terminating: forall s c s', cexec s c s' -> forall C pc σ, code_at C pc (compile_com c) -> transitions C (pc, σ, s) (pc + codelen (compile_com c), σ, s').
proof: Proof. induction 1; cbn; intros. - autorewrite with code. apply star_refl. - eapply star_trans. apply compile_aexp_correct with (a := a). eauto with code. apply star_one. autorewrite with code. apply trans_setvar. eauto with code. - eapply star_trans. apply IHcexec1. eauto with code. autorewrite with code. apply IHcexec2. eauto with code. - set (code1 := compile_com c1) in *. set (code2 := compile_com c2) in *. set (codeb := compile_bexp b 0 (codelen code1 + 1)) in *. eapply star_trans. apply compile_bexp_correct with (b := b). eauto with code. fold codeb. destruct (beval b s); autorewrite with code. + eapply star_trans. apply IHcexec. eauto with code. fold code1. apply star_one. apply trans_branch with (d := codelen code2). eauto with code. lia. + replace (pc + codelen codeb + codelen code1 + codelen code2 + 1) with (pc + codelen codeb + codelen code1 + 1 + codelen code2) by lia. apply IHcexec. eauto with code. - set (code_body := compile_com c) in *. set (code_branch := compile_bexp b 0 (codelen code_body + 1)) in *. set (d := - (codelen code_branch + codelen code_body + 1)) in *. eapply star_trans. apply compile_bexp_correct with (b := b). eauto with code. rewrite H. fold code_branch. autorewrite with code. apply star_refl. - set (code_body := compile_com c) in *. set (code_branch := compile_bexp b 0 (codelen code_body + 1)) in *. set (d := - (codelen code_branch + codelen code_body + 1)) in *. eapply star_trans. apply compile_bexp_correct with (b := b). eauto with code. rewrite H. fold code_branch. autorewrite with code. eapply star_trans. apply IHcexec1. eauto with code. eapply star_trans. apply star_one. apply trans_branch with (d := d). eauto with code. eauto. replace (pc + codelen code_branch + codelen code_body + 1 + d) with pc by lia. replace (pc + codelen code_branch + codelen code_body + 1) with (pc + codelen (compile_com (WHILE b c))) by (cbn; autorewrite with code; auto). apply IHcexec2. auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences IMP Simulation)