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. Proof Compil.compile_com_correct_terminating. Lemma compile_com_productive: forall c s, cexecinf s c -> forall C pc σ, code_at C pc (compile_com c) -> exists c' pc' s', plus (transition C) (pc, σ, s) (pc', σ, s') /\ cexecinf s' c' /\ code_at C pc' (compile_com c'). Proof. induction c; intros s EXEC C pc σ CODEAT; inversion EXEC; subst; clear EXEC; simpl in CODEAT. - eapply IHc1; eauto with code. - edestruct IHc2 as (c' & pc' & s'' & PLUS & EXEC' & CODEAT'); eauto with code. exists c', pc', s''; split; auto. eapply star_plus_trans. eapply compile_com_correct_terminating; eauto with code. exact PLUS. - set (code1 := compile_com c1) in *. set (code2 := compile_com c2) in *. set (codeb := compile_bexp b 0 (codelen code1 + 1)) in *. destruct (beval b s) eqn:B. + edestruct IHc1 as (c' & pc' & s' & PLUS & EXEC' & CODEAT'); eauto with code. exists c', pc', s'; split; auto. eapply star_plus_trans. eapply compile_bexp_correct with (b := b); eauto with code. fold codeb. rewrite B. autorewrite with code. eexact PLUS. + edestruct IHc2 as (c' & pc' & s' & PLUS & EXEC' & CODEAT'); eauto with code. exists c', pc', s'; split; auto. eapply star_plus_trans. eapply compile_bexp_correct with (b := b); eauto with code. fold codeb. rewrite B. autorewrite with code. eexact PLUS. - edestruct IHc as (c' & pc' & s' & PLUS & EXEC' & CODEAT'); eauto with code. exists c', pc', s'; split; auto. eapply star_plus_trans. eapply compile_bexp_correct with (b := b); eauto with code. rewrite H2. autorewrite with code. eexact PLUS. - exists (WHILE b c), pc, s'; split; auto. eapply star_plus_trans. eapply compile_bexp_correct with (b := b); eauto with code. rewrite H1. autorewrite with code. eapply star_plus_trans. eapply compile_com_correct_terminating; eauto with code. apply plus_one. eapply trans_branch. eauto with code. lia. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP Compil) Coq(Classical Description)