proposition: Lemma cinterp_cexec: forall n c s s', cinterp n c s = Some s' -> cexec s c s'.
proof: Proof. induction n as [ | n]; simpl; intros. - discriminate. - destruct c. + inversion H; apply cexec_skip. + inversion H; apply cexec_assign. + destruct (cinterp n c1 s) as [s1|] eqn:C1; try discriminate. simpl in H. apply cexec_seq with s1; auto. + apply cexec_ifthenelse; auto. + destruct (beval b s) eqn:B. * destruct (cinterp n c s) as [s1|] eqn:C1; try discriminate. simpl in H. apply cexec_while_loop with s1; auto. * inversion H; subst; apply cexec_while_done; auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP Compil) Coq(Classical Description)