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 frame R 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.

changed the description

added 4 commits

• 66483b1d - 1 commit from branch master
• 2318a964 - A more principled set of axioms for fupd+plainly.
• a3032864 - Allow introduction of `∀` under `|={E}=>` in case the predicate is plain.
• 871156f6 - Adapt adequacy of total weakest preconditions to use adequacy of fupd.

Compare with previous version

cc @amintimany @jtassaro

mentioned in issue #164 (closed)

I like the direction this is taking. :) Could you add these intuitive explanations that you gave here, to the sources as comments right next to these axioms? However, I first have some questions because I could not follow all of them. ;)

Laters commute with fancy updates over plain propositions.

Well, not quite. You get an except-0. Not too surprising because of the except-0 in the definition of fancy updates, but still -- maybe say "Laters almost commute" or so?

A stronger version of the usual framing rule. The difference is that you get the frame R back for proving the remaining proposition, which should be plain to make that possible.

Uh, how's that anything like framing?^^ To me this looks more like our "when a wand concludes in sth. persistent you can keep the premise", just with s/wand/fancy update/ and s/persistent/pure/. Which is nice! I just don't see the relation to framing here, so I also think the same is not chosen well.

fupd_plainly_frame_r also looks a bit like a "commuting out" property to me, and the thing that commutes with the update is R -* _.

Could you add these intuitive explanations that you gave here

Will do, once we settle on them :).

maybe say "Laters almost commute" or so?

Sure, I will also point out that it's "almost" due to the ◇.

Uh, how's that anything like framing?

Visually they are quite the same:

fupd_frame_r E1 E2 P R : (|={E1,E2}=> P) ∗ R ={E1,E2}=∗ P ∗ R.
fupd_plainly_frame_r E P R : (R ={E}=∗ ■ P) ∗ R ⊢ |={E}=> P ∗ R;

The R disappears out of the fancy update, but the difference is that you get it back.

I'm open to other names/descriptions.

Nice! I'm in favor of merging this. One suggested extension: Right now you have

   Lemma step_fupd_plain_forall E1 E2 {A} (Φ : A → PROP) `{!∀ x, Plain (Φ x)} :
      E2 ⊆ E1 →
      (|={E1,E2}▷=> ∀ x, Φ x) ⊣⊢ (∀ x, |={E1,E2}▷=> Φ x).

You can also derive something similar for the non-step taking version:

    Lemma fupd_plain_forall_partial E1 E2 {A} (Φ : A → PROP) `{!∀ x, Plain (Φ x)} :
      E2 ⊆ E1 →
      (|={E1,E2}=> ∀ x, Φ x) ⊣⊢ (∀ x, |={E1,E2}=> Φ x).

I have the following proof:

    Lemma fupd_plain_mask_mono E1 E2 P `{!Plain P} :
      E2 ⊆ E1 → (|={E1}=> P) ⊢ |={E1,E2}=> P.
    Proof.
      intros ?. rewrite -(fupd_trans E1 E1 E2). f_equiv.
      rewrite {1}(fupd_intro_mask E1 E2 P) //.
      trans (|={E1,E2}=> |={E2,E2}=> P)%I; last by apply fupd_trans.
      f_equiv. by apply fupd_plain_mask.
    Qed.
    Lemma fupd_plain_forall_partial E1 E2 {A} (Φ : A → PROP) `{!∀ x, Plain (Φ x)} :
      E2 ⊆ E1 →
      (|={E1,E2}=> ∀ x, Φ x) ⊣⊢ (∀ x, |={E1,E2}=> Φ x).
    Proof.
      intros.
      apply (anti_symm _).
      { apply forall_intro=> x. by rewrite (forall_elim x). }
      trans (∀ x, |={E1}=> Φ x)%I.
      { apply forall_mono=> x. by rewrite fupd_plain_mask. }
      rewrite fupd_plain_forall_2. eapply fupd_plain_mask_mono; eauto. apply _.
    Qed.

(There must be a way to simplify this.) Then perhaps consider adding typeclass instances for introducing the quantifiers when it's |={E,∅}=> and |={E,∅}=▷>, since these are the ones that also come up in the new style of adequacy proofs?

Thanks @jtassaro I will include your suggestions into the MR.

@robbertkrebbers What about my parallel with (P -* <pers> Q) * P |- <pers> Q * P? To be that makes way more sense than "framing where you get it back". I still don't know what you mean by "getting it back", and we never called the law I just mentioned "framing" either. "Framing" is all about cancellation, and you are not cancelling anything here, I find it just confusing.

mentioned in merge request !183 (closed)

@robbertkrebbers What about my parallel with (P -* <pers> Q) * P |- <pers> Q * P

Do we have that rule? What is its name?

I just took at look at how these rules work out for non-affine logics. And came to the following conclusions:

• From the rules we have now (and I believe also from what we had before) we can prove True ={E}=∗ emp. So these rules will not be inhabited for any sensible non-affine logic.
• No version of these rules will hold in Iron. There we define Iron fancy updates in terms of Iris fancy updates by threading through a piece of ghost state that's existentially quantified in the conclusion of the fancy update. So, even if we would use the version with ■ modalities in both the premise and conclusion, or with the Plain condition, it will not hold.

That said, right now we don't have any non-affine logic for which the interaction between fancy updates and plainly matters. For the case of the ordered RA model we have no idea how basic updates will even work out. So, I propose we do one of the following things:

1. Leave the rules the way they are now, and put a comment in the file that the BiFUpdPlainly is only usable for affine logics.
2. Make the above more formal, by adding a field BiAffine to BiFUpdPlainly.
3. Change it to the version that also has a ■ in the conclusion. This version may hold for some non-affine logics, but we don't know since we don't have any such logics yet. As a consequence, all rules that are stated in terms of the Plain class also need that proposition to be Absorbing.

added 6 commits

• 7cbc3abe - Prove `E2 ⊆ E1 → P ={E1,E2}=∗ P`.
• 79e1fd5c - A more principled set of axioms for fupd+plainly.
• 8fd28250 - Comment about BiFUpdPlainly and affine BIs.
• f3949c8e - Document new fupd+plainly laws.
• 788b1b90 - Allow introduction of `∀` under `|={E1,E2}=>` in case the predicate is plain.
• 1979df48 - Adapt adequacy of total weakest preconditions to use adequacy of fupd.

Compare with previous version

I've updated the MR:

• Joe's suggestion has been included (more derived rules for ∀, and instruct the proofmode to automatically use those).
• Ralf's suggestion to include the intuitive descriptions of the axioms.
• Included a proof that True ={E}=∗ emp, and inserted a remark that the BiFUpdPlainly is only usable for affine logics.

TODO:

• Sort of if any of the other options from https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/184#note_31461 are preferred.
• A better name/description for fupd_plainly_frame_r.

added 7 commits

• 1979df48...c148ac4d - 2 commits from branch master
• 8d0bb046 - A more principled set of axioms for fupd+plainly.
• 6fb61ba5 - Comment about BiFUpdPlainly and affine BIs.
• 73c7fb5b - Document new fupd+plainly laws.
• 33627058 - Allow introduction of `∀` under `|={E1,E2}=>` in case the predicate is plain.
• 6730b277 - Adapt adequacy of total weakest preconditions to use adequacy of fupd.

Compare with previous version

added 1 commit

• a0fb9914 - New lemma `step_fupdN_wand`, and use instead of `step_fupdN_mono`.

Compare with previous version

mentioned in merge request !182 (merged)

Do we have that rule? What is its name?

It's a principle we use a lot and the proof mode knows how to exploit it. You brought it up yourself recently when we talked about linear logic vs BI, citing own_valid as one common use.

I haven't found it among our derived rules, but that seems like an oversight?