proposition: Lemma step_star_correct_gen s s' k k' l l' : step_star (s, k) l' (s', k') -> reify (denote_continuation M k) (s, l) = reify (denote_continuation M k') (s', l++l').
proof: Proof. intro Hstep_star. remember (s, k) as sk eqn: Heq. remember (s', k') as sk' eqn: Heq'. revert s s' k k' l Heq Heq'. induction Hstep_star as [ s | (s, k) (s', k') (s'', k'') l' Hstep Hstep_star IH | (s, k) (s', k') (s'', k'') t l' Hstep Hstep_star IH ]; intros s1 s2 k1 k2 l1 Heq1 Heq2. - rewrite cats0. by move: Heq2; rewrite Heq1 => -[<- <-]. - move: Heq1 Heq2 => [<- <-] [<- <-]. apply step_None_correct with (l := l1) in Hstep. rewrite Hstep. apply IH; reflexivity. - move: Heq1 Heq2 => [<- <-] [<- <-]. apply step_Some_correct with (l := []) in Hstep. rewrite <- cats0 at 1. rewrite denote_continuation_prefix_independent; [ | now exists k ]. rewrite -> Hstep, (IH _ s'' _ k''); [ | reflexivity | reflexivity ]. cbn. rewrite denote_continuation_prefix_independent; [ reflexivity | ]. now eexists. Qed.
imports: Eqdep JMeq List ssreflect mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) hierarchy monad_lib state_lib trace_lib monad_model