proposition: Theorem ceval_step_more: forall i1 i2 st st' c, i1 <= i2 -> ceval_step st c i1 = Some st' -> ceval_step st c i2 = Some st'.
proof: Proof. induction i1 as [|i1']; intros i2 st st' c Hle Hceval. - simpl in Hceval. inversion Hceval. - destruct i2 as [|i2']. inversion Hle. assert (Hle': i1' <= i2') by omega. destruct c. + simpl in Hceval. inversion Hceval. reflexivity. + simpl in Hceval. inversion Hceval. reflexivity. + simpl in Hceval. simpl. destruct (ceval_step st c1 i1') eqn:Heqst1'o. * apply (IHi1' i2') in Heqst1'o; try assumption. rewrite Heqst1'o. simpl. simpl in Hceval. apply (IHi1' i2') in Hceval; try assumption. * inversion Hceval. + simpl in Hceval. simpl. destruct (beval st b); apply (IHi1' i2') in Hceval; assumption. + simpl in Hceval. simpl. destruct (beval st b); try assumption. destruct (ceval_step st c i1') eqn: Heqst1'o. * apply (IHi1' i2') in Heqst1'o; try assumption. rewrite -> Heqst1'o. simpl. simpl in Hceval. apply (IHi1' i2') in Hceval; try assumption. * simpl in Hceval. inversion Hceval. Qed.
imports: Coq.omega.Omega Coq.Arith.Arith Imp Maps