proposition: Lemma transitions_smart_Ibranch: forall C pc d pc' σ s, code_at C pc (smart_Ibranch d) -> pc' = pc + codelen (smart_Ibranch d) + d -> transitions C (pc, σ, s) (pc', σ, s).
proof: Proof. unfold smart_Ibranch; intros. Abort. Inductive compile_cont (C: code): cont -> Z -> Prop := | ccont_stop: forall pc, instr_at C pc = Some Ihalt -> compile_cont C Kstop pc | ccont_seq: forall c k pc pc', code_at C pc (compile_com c) -> pc' = pc + codelen (compile_com c) -> compile_cont C k pc' -> compile_cont C (Kseq c k) pc | ccont_while: forall b c k pc d pc' pc'', instr_at C pc = Some(Ibranch d) -> pc' = pc + 1 + d -> code_at C pc' (compile_com (WHILE b c)) -> pc'' = pc' + codelen (compile_com (WHILE b c)) -> compile_cont C k pc'' -> compile_cont C (Kwhile b c k) pc | ccont_branch: forall d k pc pc', instr_at C pc = Some(Ibranch d) -> pc' = pc + 1 + d -> compile_cont C k pc' -> compile_cont C k pc. Inductive match_config (C: code): com * cont * store -> config -> Prop := | match_config_intro: forall c k st pc, code_at C pc (compile_com c) -> compile_cont C k (pc + codelen (compile_com c)) -> match_config C (c, k, st) (pc, nil, st). Fixpoint com_size (c: com) : nat := match c with | SKIP => 1%nat | ASSIGN x a => 1%nat | SEQ c1 c2 => (com_size c1 + com_size c2 + 1)%nat | IFTHENELSE b c1 c2 => (com_size c1 + com_size c2 + 1)%nat | WHILE b c1 => (com_size c1 + 1)%nat end. Remark com_size_nonzero: forall c, (com_size c > 0)%nat. Proof. induction c; cbn; lia. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences IMP Simulation)