Separation Logic Foundations

Separation Logic Foundations

Hints and Solutions to Exercises

<<< Previous exercise

Next exercise >>>

Solution for Wand.Hwand.hwand_inv

introv M2 M1 D. unfolds hwand. lets (H0&M3): hexists_inv M2. lets (h0&h3&P1&P3&D'&U): hstar_inv M3. lets (P4&E3): hpure_inv P3. subst h2 h3. rewrite union_empty_r in *. applys P4. applys* hstar_intro. Qed.

Click on the 'Next' button to reveal the proof step by step.

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: