Solution for Repr.triple_mrev
Lemma triple_mrev_aux : forall L1 L2 p1 p2,
triple (mrev_aux p1 p2)
(MList L1 p1 \* MList L2 p2)
(funloc q => MList (rev L2 ++ L1) q).
Proof using.
intros. gen p1 p2 L1. induction_wf IH: list_sub L2. intros.
xwp. xapp. xchange (MList_if p2). xif; intros C; case_if; xpull.
{ intros ->. xval. rew_list. xsimpl*. }
{ intros x p2' L2' ->. xapp. xapp. xchange <- MList_cons.
xapp. intros q. rew_list. xsimpl*. }
Qed.
xwp. xchanges* <- (MList_nil null). xapp triple_mrev_aux.
intros q. rew_list. xsimpl*.
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
