Solution for Repr.triple_mtreesum
Lemma triple_treeacc : forall T c p m,
triple (treeacc c p)
(MTree T p \* c ~~> m)
(fun u => (c ~~> (m + treesum T)) \* (MTree T p)).
Proof using.
intros. gen p m. induction_wf IH: tree_sub T.
xwp. xapp. xchange MTree_if. xif; intros C; case_if; xpull.
{ intros n p1 p2 T1 T2 ->. xapp. xapp. xapp. xapp.
xapp. xapp. { constructors. } xapp. xapp. { constructors. }
xsimpl. math. xchange <- MTree_Node. }
{ intros ->. xval. xsimpl. { simpl. math. } { xchange* <- MTree_Leaf. } }
Qed.
xwp. xapp. intros c. xapp triple_treeacc. xapp. xsimpl. { math. }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
