Solution for Repr.triple_mlength'
Lemma triple_acclength : forall L c p n,
triple (acclength c p)
(MList L p \* c ~~> n)
(fun u => (c ~~> (n + length L)) \* (MList L p)).
Proof using.
intros. gen p n. induction_wf IH: list_sub L.
xwp. xapp. xchange MList_if. xif; intros C; case_if; xpull.
{ intros x q L' ->. xapp. xapp. xapp. xchange <- MList_cons. xsimpl.
{ rew_list*. math. } }
{ intros ->. xval. xsimpl. { rew_list*. math. } { xchange* <- MList_nil. } }
Qed.
xwp. xapp. intros c. xapp triple_acclength. xapp. xsimpl. { math. }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
