proposition: Lemma simulate_step : forall D h e s h' e' s' , machine_step D (h,e,s) = TakeStep _ (h',e',s') -> scoped_conf D (h,e,s) -> decode (h,e,s) = decode (h',e',s') \/ step (decode (h,e,s)) (decode (h',e',s')).
proof: Proof. intros D h e s h' e' s' STEP SCOPE. inversion SCOPE; subst; clear SCOPE. simpl in *. destruct (isVal e) eqn:?. destruct s. - inversion STEP. - destruct f eqn:?. + destruct e eqn:?; try solve [inversion STEP]. right. destruct AtomSetProperties.In_dec. * destruct atom_fresh. inversion STEP; subst; clear STEP. simpl in *; autorewrite with lngen in *. rewrite combine. rewrite apply_stack_fresh_eq; auto; try fsetdec. apply apply_stack_cong. simpl. assert (x <> x0) by fsetdec. rewrite <- swap_spec; auto; try fsetdec. rewrite (subst_exp_spec _ _ x). autorewrite with lngen; auto with lngen. default_simp. rewrite subst_exp_fresh_eq; autorewrite with lngen; auto. apply step_beta; auto with lngen. rewrite <- apply_heap_abs. eapply apply_heap_lc. auto with lngen. rewrite H4. fsetdec. * inversion STEP; subst; clear STEP; simpl in *; rewrite combine; rewrite apply_stack_fresh_eq; auto; try fsetdec. apply apply_stack_cong; autorewrite with lngen in *; simpl. rewrite subst_exp_spec. rewrite apply_heap_open; auto with lngen. apply step_beta; auto with lngen. rewrite <- apply_heap_abs. eapply apply_heap_lc. auto with lngen. - destruct e eqn:?; try solve [inversion STEP]. + destruct (get x h) eqn:?; inversion STEP; subst; clear STEP. left. f_equal. apply apply_heap_get with (D:= D); auto. + inversion STEP; subst; clear STEP. left. simpl. rewrite apply_heap_app. auto. Qed.
imports: String Metalib.Metatheory Stlc.Nominal Stlc.Lemmas