Skip to content

GitLab

Open
Created by Ralf Jung@jungOwner

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.

Edited by Ralf Jung