proposition: Theorem ceval_step__ceval: forall c st st', (exists i, ceval_step st c i = Some st') -> st =[ c ]=> st'.
proof: Proof. intros c st st' H. inversion H as [i E]. clear H. generalize dependent st'. generalize dependent st. generalize dependent c. induction i as [| i' ]. - intros c st st' H. discriminate H. - intros c st st' H. destruct c; simpl in H; inversion H; subst; clear H. + apply E_Skip. + apply E_Asgn. reflexivity. + destruct (ceval_step st c1 i') eqn:Heqr1. * apply E_Seq with s. apply IHi'. rewrite Heqr1. reflexivity. apply IHi'. assumption. * discriminate H1. + destruct (beval st b) eqn:Heqr. * apply E_IfTrue. rewrite Heqr. reflexivity. apply IHi'. assumption. * apply E_IfFalse. rewrite Heqr. reflexivity. apply IHi'. assumption. + destruct (beval st b) eqn :Heqr. * destruct (ceval_step st c i') eqn:Heqr1. { apply E_WhileTrue with s. rewrite Heqr. reflexivity. apply IHi'. rewrite Heqr1. reflexivity. apply IHi'. assumption. } { discriminate H1. } * injection H1 as H2. rewrite <- H2. apply E_WhileFalse. apply Heqr. Qed.
imports: Coq(Lia) Coq(Arith.Arith) Coq(Arith.PeanoNat) Coq(Arith.EqNat) LF(Imp Maps)