proposition: Lemma step_None_correct s s' k k' l : step (s, k) None (s', k') -> reify (denote_continuation M k) (s, l) = reify (denote_continuation M k') (s', l).
proof: Proof. intro Hstep. remember (s, k) as sk eqn: Heq. remember None as o eqn: Heqo. remember (s', k') as sk' eqn: Heq'. revert s s' k k' l Heq Heq' Heqo. induction Hstep as [ s A a f | s A B p f g | s A p1 p2 k | s A p1 p2 k | s p k | s n p k | fuel s c p k Htrue | fuel s c p k Hfalse | s c p k | s f | s s' f | s t f ]; intros s1 s2 k1 k2 l [= Hs1 Hk1] [= Hs2 Hk2] Heqo. - subst s1 k1 s2 k2. by rewrite /= reifybind reifyret. - subst s1 k1 s2 k2. cbn. by rewrite bindA. - subst s1 s2 k1 k2. reflexivity. - subst s1 s2 k1 k2. reflexivity. - subst. cbn. rewrite bindretf. reflexivity. - subst. cbn. rewrite bindA. reflexivity. - subst. cbn. rewrite bindA reifybind reifystget Htrue bindA. reflexivity. - subst. cbn. rewrite bindA reifybind reifystget Hfalse bindretf. reflexivity. - subst. cbn. rewrite bindretf. reflexivity. - subst s1 k1 s2 k2. by rewrite /= reifybind reifystget. - subst s1 k1 s2 k2. by rewrite /= reifybind reifystput. - discriminate Heqo. Qed.
imports: Eqdep JMeq List ssreflect mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) hierarchy monad_lib state_lib trace_lib monad_model