proposition: Lemma cexec_f_sound: forall fuel s c s', cexec_f fuel s c = Some s' -> cexec s c s'.
proof: Proof. induction fuel as [ | fuel ]; cbn; intros. - discriminate. - destruct c. Abort. Lemma cexec_f_complete: forall s c s', cexec s c s' -> exists fuel1, forall fuel, (fuel >= fuel1)%nat -> cexec_f fuel s c = Some s'. Proof. induction 1. Abort. Inductive cont : Type := | Kstop | Kseq (c: com) (k: cont) | Kwhile (b: bexp) (c: com) (k: cont). Fixpoint apply_cont (k: cont) (c: com) : com := match k with | Kstop => c | Kseq c1 k1 => apply_cont k1 (SEQ c c1) | Kwhile b1 c1 k1 => apply_cont k1 (SEQ c (WHILE b1 c1)) end. Inductive step: com * cont * store -> com * cont * store -> Prop := | step_assign: forall x a k s, step (ASSIGN x a, k, s) (SKIP, k, update x (aeval a s) s) | step_seq: forall c1 c2 s k, step (SEQ c1 c2, k, s) (c1, Kseq c2 k, s) | step_ifthenelse: forall b c1 c2 k s, step (IFTHENELSE b c1 c2, k, s) ((if beval b s then c1 else c2), k, s) | step_while_done: forall b c k s, beval b s = false -> step (WHILE b c, k, s) (SKIP, k, s) | step_while_loop: forall b c k s, beval b s = true -> step (WHILE b c, k, s) (c, Kwhile b c k, s) | step_skip_seq: forall c k s, step (SKIP, Kseq c k, s) (c, k, s) | step_skip_while: forall b c k s, step (SKIP, Kwhile b c k, s) (WHILE b c, k, s). Definition kterminates (s: store) (c: com) (s': store) : Prop := star step (c, Kstop, s) (SKIP, Kstop, s'). Definition kdiverges (s: store) (c: com) : Prop := infseq step (c, Kstop, s). Inductive match_conf : com * cont * store -> com * store -> Prop := | match_conf_intro: forall c k s c', c' = apply_cont k c -> match_conf (c, k, s) (c', s). Fixpoint num_seq (c: com) : nat := match c with | SEQ c1 c2 => S (num_seq c1) | _ => O end. Definition kmeasure (C: com * cont * store) : nat := let '(c, k, s) := C in num_seq c. Remark red_apply_cont: forall k c1 s1 c2 s2, red (c1, s1) (c2, s2) -> red (apply_cont k c1, s1) (apply_cont k c2, s2). Proof. induction k; intros; simpl; eauto using red_seq_step. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences Simulation)