More principled set of axioms for fancy updates and plainly
This MR proposes a new set of axioms for the BiFUpdPlainly
interface, namely:
fupd_plainly_mask_empty E (P : PROP) :
(|={E,∅}=> ■ P) ⊢ |={E}=> P;
fupd_plainly_frame_r E (P R : PROP) :
(R ={E}=∗ ■ P) ∗ R ⊢ |={E}=> P ∗ R;
fupd_plainly_later E (P : PROP) :
(▷ |={E}=> ■ P) ⊢ |={E}=> ▷ ◇ P;
fupd_plainly_forall_2 E {A} (Φ : A → PROP) :
(∀ x, |={E}=> ■ Φ x) ⊢ |={E}=> ∀ x, Φ x
Contrary to what we had before, I think these axioms are more principled: all of these axioms do exactly one thing, which I believe can be explained.
-
fupd_plainly_mask_empty
: When proving a fancy update of a plain proposition, you can also prove it while being allowed to open all invariants. -
fupd_plainly_frame_r
: A stronger version of the usual framing rule. The difference is that you get the frameR
back for proving the remaining proposition, which should be plain to make that possible. -
fupd_plainly_later
: Laters commute with fancy updates over plain propositions. -
fupd_plainly_forall_2
: Forall quantifiers commute with fancy updates over plain propositions.
This merge request closes #164 (closed).
Note that the result in !183 (closed) follows from the new laws. We can show that universal quantifiers commute with step-taking fancy updates, using just the above laws.
As part of this MR I also ported the adequacy proof of total weakest preconditions to the new style.
I directly took the liberty to clean up some of the derived results about the interaction between fancy updates and the plain modality.