proposition: Lemma denote_prefix_independent A (m : M A) : stateTrace_sub m -> forall s l1 l2, reify m (s, l1 ++ l2) = let res := reify m (s, l2) in match res with | None => None | Some res => Some (res.1, (res.2.1, l1 ++ res.2.2)) end.
proof: Proof. intros [ p Hp ] s l1 l2. subst m. elim: p s l1 l2 => /= {A} [A a|A B p1 IH1 p2 IH2|A b p1 IH1 p2 IH2| n p IHp|fuel c p IHp||s'|t] s l1 l2. - by rewrite !reifyret. - rewrite [in LHS]reifybind [in LHS]IH1. rewrite [in RHS]reifybind. case: (reify (denote M _ p1) (s, l2)) => [[a' [s' l']] | ] /=. + by rewrite IH2. + reflexivity. - by case: ifPn => _; [rewrite IH1|rewrite IH2]. - revert s l2. induction n as [ | n' IH ]; intros s l2. + by rewrite !reifyret. + do 2 rewrite reifybind. rewrite {}IHp. case_eq (reify (denote M _ p) (s, l2)). * intros (a, (s0, l0)) Hp. exact: IH. * reflexivity. - revert s l2. induction fuel as [ | fuel' IH ]; intros s l2. + by rewrite !reifyret. + do 2 rewrite reifybind reifystget. cbn. destruct (c s). * do 2 rewrite reifybind. rewrite IHp. clear IHp. case_eq (reify (denote M _ p) (s, l2)). -- intros (a, (s0, l0)) Hp. exact: IH. -- reflexivity. * by rewrite !reifyret. - by rewrite !reifystget. - by rewrite !reifystput. - by rewrite !reifystmark rcons_cat. Qed.
imports: Eqdep JMeq List ssreflect mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) hierarchy monad_lib state_lib trace_lib monad_model