proposition: Lemma denote_prefix_preserved A (m : M A) : stateTrace_sub m -> forall s s' l1 l a, reify m (s, l1) = Some (a, (s', l)) -> exists l2, l = l1 ++ l2.
proof: Proof. case=> p <-{m}. 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' l1 l a' Heq. - exists []. rewrite cats0. by move: Heq; rewrite reifyret => -[]. - rewrite reifybind in Heq. case_eq (reify (denote M _ p) (s, l1)). + intros (a, (s0, l0)) Hp. rewrite Hp in Heq. move/IHp : Hp => [l2 Hp]. move/IHg : Heq => [l2' Heq]. exists (l2 ++ l2'). by rewrite Heq Hp catA. + intro Hp. rewrite Hp in Heq. discriminate Heq. - destruct b; [ eapply IHp1 | eapply IHp2 ]; exact Heq. - revert s l1 Heq. induction n as [ | n' IH ]; intros s l1 Heq. + exists []. rewrite cats0. by move: Heq; rewrite reifyret => -[]. + rewrite reifybind in Heq. case_eq (reify (denote M _ p) (s, l1)). * intros (a, (s0, l0)) Hp. move: (IHp _ _ _ _ _ Hp) => [l2 ?]. subst l0. rewrite Hp in Heq. move: (IH _ _ Heq) => [l3 ?]. exists (l2 ++ l3). by rewrite catA. * intro Hp. rewrite Hp in Heq. discriminate Heq. - revert s l1 Heq. induction fuel as [ | fuel' IH ]; intros s l1 Heq. + exists []. rewrite cats0. by move: Heq; rewrite reifyret => -[]. + rewrite reifybind reifystget in Heq. simpl in Heq. destruct (c s). * rewrite reifybind in Heq. case_eq (reify (denote M _ p) (s, l1)). -- intros (a ,(s0, l0)) Hp. move: (IHp _ _ _ _ _ Hp) => [l2 ?]. subst l0. rewrite Hp in Heq. move: (IH _ _ Heq) => [l3 ?]. exists (l2 ++ l3). by rewrite catA. -- intro Hp. rewrite Hp in Heq. discriminate Heq. * exists []. rewrite cats0. by move: Heq; rewrite reifyret => -[]. - exists []. rewrite cats0. by move: Heq; rewrite reifystget => -[]. - exists []. rewrite cats0. by move: Heq; rewrite reifystput => -[]. - exists [t]. by move: Heq; rewrite reifystmark -cats1 => -[]. Qed.
imports: Eqdep JMeq List ssreflect mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) hierarchy monad_lib state_lib trace_lib monad_model