Remove basic updates from the Iris model, and define them using plainly.
In this MR, I define basic updates as:
|==> P := (∀ R, (P -∗ ■ R) -∗ ■ R)
This is the continuation monad, where one should think of
■ R being the final result that one wants to get out of the soundness theorem. The proposition
R needs to be plain (i.e. wrapped in
■) because we can only get resource independent propositions out of the soundness theorem.
From this definitions, we can prove all laws of basic updates, apart from those related to frame preserving updates. For that, we need the following primitive rule:
x ~~>: Φ → uPred_ownM x ∗ (∀ y, ⌜Φ y⌝ -∗ uPred_ownM y -∗ ■ R) ⊢ ■ R.
This rule could be read as: If we want to prove the final result while owning
x, we could also prove it while owning any
y to which we could do a frame preserving update.
So, in total, this gets rid of 1 primitive connective (
|==>) and 5 primitive
rules (those of
|==>), which is replaced by one new primitive rule.