proposition: Lemma step_star_complete_gen (s s' : S) (A : Type) (a : A) (p : program A) (l1 l2 : list T) f : reify (denote M _ p) (s, l1) = Some (a, (s', l1 ++ l2)) -> step_star (s, p `; f) l2 (s', f a).
proof: Proof. revert s s' a l1 l2 f. induction p as [ A a | A B p IHp g IHg | A b p1 IHp1 p2 IHp2 | n p IHp | fuel c p IHp | | s0' | t ]; cbn; intros s s' a' l1 l2 f Heq. - rewrite reifyret in Heq. injection Heq; clear Heq; intros; subst a' s'. replace l2 with (@nil T) by (revert l2 H; induction l1; [ tauto | intros ? [=]; firstorder ]). eapply ss_step_None; [ apply s_ret | apply ss_refl ]. - eapply ss_step_None. + apply s_bind. + move: Heq. rewrite reifybind. case_eq (reify (denote M _ p) (s, l1)). intros (a, (s0, l0)) Hp Heq. move: (denote_prefix_preserved ltac:(now eexists) Hp) => [l3 Hl3]. rewrite Hl3 in Hp. apply IHp with (f := (fun a => g a `; f)) in Hp. clear IHp. move: (denote_prefix_preserved ltac:(now eexists) Heq) => [l4 Hl4]. rewrite Hl4 in Heq. apply IHg with (f := f) in Heq. clear IHg. subst l0. replace l2 with (l3 ++ l4) by (induction l1; cbn in Hl4; [ congruence | injection Hl4; tauto ]). eapply step_star_transitive. * exact Hp. * exact Heq. * discriminate. - destruct b; [ eapply ss_step_None; [ apply s_cond_true | apply IHp1 with (l1 := l1); exact Heq ] | eapply ss_step_None; [ apply s_cond_false | apply IHp2 with (l1 := l1); exact Heq ] ]. - revert s l1 l2 Heq. induction n as [ | n' IHn ]; intros s l1 l2 Heq. + rewrite reifyret in Heq. injection Heq; clear Heq; intros; subst a' s'. replace l2 with (@nil T) by (revert l2 H; induction l1; [ tauto | intros ? [=]; firstorder ]). eapply ss_step_None; [ apply s_repeat_O | apply ss_refl ]. + rewrite reifybind in Heq. case_eq (reify (denote M _ p) (s, l1)). * intros (a, (s0, l0)) Hp. rewrite Hp in Heq. move: (denote_prefix_preserved ltac:(now eexists) Hp) => [l3 Hl3]. rewrite Hl3 {l0 Hl3} in Hp, Heq. specialize (IHp _ _ _ _ _ (fun _ => p_repeat n' p `; f) Hp). assert (Heq': reify (denote M _ (p_repeat n' p)) (s0, l1 ++ l3) = Some (a', (s', l1 ++ l2))) by apply Heq. move: (denote_prefix_preserved ltac:(now eexists) Heq') => [l4 Hl4]. rewrite Hl4 in Heq. eapply ss_step_None; [ apply s_repeat_S | ]. have -> : l2 = l3 ++ l4. by move/(congr1 (drop (size l1))) : Hl4; rewrite -catA ?drop_size_cat. eapply step_star_transitive; [ eexact IHp | eapply IHn; eexact Heq ]. * intro Hp. rewrite Hp in Heq. discriminate. - revert s l1 l2 Heq. induction fuel as [ | fuel' IHn ]; intros s l1 l2 Heq. + rewrite reifyret in Heq. injection Heq; clear Heq; intros; subst a' s'. replace l2 with (@nil T) by (revert l2 H; induction l1; [ tauto | intros ? [=]; firstorder ]). eapply ss_step_None; [ apply s_while_broke | apply ss_refl ]. + rewrite reifybind reifystget in Heq. cbn in Heq. case_eq (c s); [ intro Htrue | intro Hfalse ]. * rewrite Htrue reifybind in Heq. case_eq (reify (denote M _ p) (s, l1)). -- intros (a, (s0, l0)) Hp. rewrite Hp in Heq. move: (denote_prefix_preserved ltac:(now eexists) Hp) => [l3 Hl3]. rewrite Hl3 {l0 Hl3} in Hp, Heq. specialize (IHp _ _ _ _ _ (fun _ => p_while fuel' c p `; f) Hp). assert (Heq': reify (denote M _ (p_while fuel' c p)) (s0, l1 ++ l3) = Some (a', (s', l1 ++ l2))) by apply Heq. move: (denote_prefix_preserved ltac:(now eexists) Heq') => [l4 Hl4]. rewrite Hl4 in Heq. eapply ss_step_None; [ apply s_while_true; exact Htrue | ]. have -> : l2 = l3 ++ l4. by move/(congr1 (drop (size l1))) : Hl4; rewrite -catA ?drop_size_cat. eapply step_star_transitive; [ eexact IHp | eapply IHn; eexact Heq ]. -- intro Hp. rewrite Hp in Heq. discriminate. * move: Heq; rewrite Hfalse reifyret. move=> [<- <-] /(congr1 (drop (size l1))). rewrite drop_size_cat // drop_size => <-. eapply ss_step_None; [ apply s_while_false; exact Hfalse | apply ss_refl ]. - move: Heq; rewrite reifystget. move=> [<- <-] /(congr1 (drop (size l1))). rewrite drop_size_cat // drop_size => <-. eapply ss_step_None; [ apply s_get | apply ss_refl ]. - move: Heq; rewrite reifystput. move=> [<- <-] /(congr1 (drop (size l1))). rewrite drop_size_cat // drop_size => <-. eapply ss_step_None; [ apply s_put | apply ss_refl ]. - move: Heq; rewrite reifystmark. move=> [<- <-] /(congr1 (drop (size l1))). rewrite drop_size_cat // drop_rcons // drop_size => <-. eapply ss_step_Some; [ apply s_mark | apply ss_refl ]. Qed.
imports: Eqdep JMeq List ssreflect mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) hierarchy monad_lib state_lib trace_lib monad_model