proposition: Lemma simulation_step: forall C impconf1 impconf2, step impconf1 impconf2 -> forall machconf1, match_config C impconf1 machconf1 -> exists machconf2, (plus (transition C) machconf1 machconf2 \/ (star (transition C) machconf1 machconf2 /\ (measure impconf2 < measure impconf1)%nat)) /\ match_config C impconf2 machconf2.
proof: Proof. destruct 1; intros machconf1 MATCH; inversion MATCH; clear MATCH; subst; cbn in *. - econstructor; split. + left. eapply plus_right. eapply compile_aexp_correct; eauto with code. eapply trans_setvar; eauto with code. + autorewrite with code in *. apply match_config_skip. auto. - econstructor; split. + right; split. apply star_refl. lia. + autorewrite with code in *. constructor. eauto with code. eapply ccont_seq; eauto with code. - set (code1 := compile_com c1) in *. set (codeb := compile_bexp b 0 (codelen code1 + 1)) in *. set (code2 := compile_com c2) in *. autorewrite with code in *. econstructor; split. + right; split. apply compile_bexp_correct with (b := b). eauto with code. destruct (beval b s); lia. + fold codeb. destruct (beval b s). * autorewrite with code. constructor. eauto with code. eapply ccont_branch. eauto with code. eauto. fold code1. replace (pc + codelen codeb + codelen code1 + 1 + codelen code2) with (pc + codelen codeb + codelen code1 + codelen code2 + 1) by lia. auto. * autorewrite with code. constructor. eauto with code. auto. fold code2. replace (pc + codelen codeb + codelen code1 + 1 + codelen code2) with (pc + codelen codeb + codelen code1 + codelen code2 + 1) by lia. auto. - set (codec := compile_com c) in *. set (codeb := compile_bexp b 0 (codelen codec + 1)) in *. econstructor; split. + right; split. apply compile_bexp_correct with (b := b). eauto with code. assert (com_size c > 0)%nat by apply com_size_nonzero. lia. + rewrite H. fold codeb. autorewrite with code in *. apply match_config_skip. auto. - set (codec := compile_com c) in *. set (codeb := compile_bexp b 0 (codelen codec + 1)) in *. econstructor; split. + right; split. apply compile_bexp_correct with (b := b). eauto with code. lia. + rewrite H. fold codeb. autorewrite with code in *. constructor. eauto with code. eapply ccont_while with (pc' := pc). eauto with code. fold codec. lia. auto. cbn. fold codec; fold codeb. eauto. autorewrite with code. auto. - autorewrite with code in *. edestruct compile_cont_Kseq_inv as (pc' & X & Y & Z). eauto. econstructor; split. + right; split. eauto. lia. + constructor; auto. - autorewrite with code in *. edestruct compile_cont_Kwhile_inv as (pc' & X & Y & Z). eauto. econstructor; split. + left. eauto. + constructor; auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences IMP Simulation)