Volume 6
Separation Logic Foundations
Hints and Solutions to Exercises
<<< Previous exercise
All exercises
Next exercise >>>
Solution for Affine.NewTriples.wp_haffine_pre
introv HA. xchange (>> wp_frame t H Q). unfold wp. intros s M. applys eval_conseq M. intros r. xchange* (>> himpl_hgc_r H). xchange hstar_hgc_hgc. xsimpl. Qed.
Click on the 'Next' button to reveal the proof step by step.
Prev
Next
Full
Please provide feedback
If you did need a hint to complete the exercise, your feedback would be very useful to improve the course.
Please write below a sentence or two. Do not hesitate to copy-paste the proof script that you had reached.
By submitting, you agree to share your text anonymously, under the Creative Common copyleft licence (CC-Zero).
Please type the result of 32+32:
