proposition: Lemma match_initial_configs: forall c s, match_config (compile_program c) (c, Kstop, s) (0, nil, s).
proof: Proof. intros. set (C := compile_program c). assert (code_at C 0 (compile_com c ++ Ihalt :: nil)). { replace C with (nil ++ (compile_com c ++ Ihalt :: nil) ++ nil). constructor; auto. rewrite app_nil_r; auto. } constructor. - eauto with code. - apply ccont_stop. eauto with code. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences IMP Simulation)