The one place for your designs
To enable design management, you'll need to meet the requirements. If you need help, reach out to our support team for assistance.
iAssert without any spatial assumptions should produce a persistent result
The following proof script should work:
Lemma test_persistent_assert `{!BiBUpd PROP} P :
□ P -∗ □ |==> P.
Proof.
iIntros "#HP".
iAssert (|==> P)%I as "#HPupd". (* FAIL! *)
{ iIntros "!> !> !>". done. }
iAssumption.
Qed.It currently fails because the update is not persistent -- however, this is an iAssert which is not provided any spatial assertions, so whatever it produces can always be put into the persistent context.