Alternative definition of basic updates.

_CoqProject

@@ -52,6 +52,7 @@ theories/base_logic/bi.v
 theories/base_logic/derived.v
 theories/base_logic/proofmode.v
 theories/base_logic/base_logic.v
+theories/base_logic/bupd_alt.v
 theories/base_logic/lib/iprop.v
 theories/base_logic/lib/own.v
 theories/base_logic/lib/saved_prop.v

theories/base_logic/bupd_alt.v

+From iris.base_logic Require Export base_logic.
+From iris.proofmode Require Import tactics.
+
+(** This file contains an alternative version of basic updates, that is
+expression in terms of just the plain modality [■]. *)
+Definition bupd_alt `{BiPlainly PROP} (P : PROP) : PROP :=
+  (∀ R, (P -∗ ■ R) -∗ ■ R)%I.
+
+(** This definition is stated for any BI with a plain modality. The above
+definition is akin to the continuation monad, where one should think of [■ R]
+being the final result that one wants to get out of the basic update in the end
+of the day (via [bupd_alt (■ P) ⊢ ■ P]).
+
+We show that:
+
+1. [bupd_alt] enjoys the usual rules of the basic update modality.
+2. [bupd_alt] entails any other modality that enjoys the laws of a basic update
+   modality (see [bupd_bupd_alt]).
+3. The ordinary basic update modality [|==>] on [uPred] entails [bupd_alt]
+   (see [bupd_alt_bupd]). This result is proven in the model of [uPred].
+
+The first two points are shown for any BI with a plain modality. *)
+
+Section bupd_alt.
+  Context `{BiPlainly PROP}.
+  Implicit Types P Q R : PROP.
+  Notation bupd_alt := (@bupd_alt PROP _).
+
+  Global Instance bupd_alt_ne : NonExpansive bupd_alt.
+  Proof. solve_proper. Qed.
+  Global Instance bupd_alt_proper : Proper ((≡) ==> (≡)) bupd_alt.
+  Proof. solve_proper. Qed.
+  Global Instance bupd_alt_mono' : Proper ((⊢) ==> (⊢)) bupd_alt.
+  Proof. solve_proper. Qed.
+  Global Instance bupd_alt_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) bupd_alt.
+  Proof. solve_proper. Qed.
+
+  (** The laws of the basic update modality hold *)
+  Lemma bupd_alt_intro P : P ⊢ bupd_alt P.
+  Proof. iIntros "HP" (R) "H". by iApply "H". Qed.
+  Lemma bupd_alt_mono P Q : (P ⊢ Q) → bupd_alt P ⊢ bupd_alt Q.
+  Proof. by intros ->. Qed.
+  Lemma bupd_alt_trans P : bupd_alt (bupd_alt P) ⊢ bupd_alt P.
+  Proof. iIntros "HP" (R) "H". iApply "HP". iIntros "HP". by iApply "HP". Qed.
+  Lemma bupd_alt_frame_r P Q : bupd_alt P ∗ Q ⊢ bupd_alt (P ∗ Q).
+  Proof.
+    iIntros "[HP HQ]" (R) "H". iApply "HP". iIntros "HP". iApply ("H" with "[$]").
+  Qed.
+  Lemma bupd_alt_plainly P : bupd_alt (■ P) ⊢ ■ P.
+  Proof. iIntros "H". iApply ("H" $! P with "[]"); auto. Qed.
+
+  (** Any modality conforming with [BiBUpdPlainly] entails the alternative
+  definition *)
+  Lemma bupd_bupd_alt `{!BiBUpd PROP, BiBUpdPlainly PROP} P : (|==> P) ⊢ bupd_alt P.
+  Proof. iIntros "HP" (R) "H". by iMod ("H" with "HP") as "?". Qed.
+
+  (** We get the usual rule for frame preserving updates if we have an [own]
+  connective satisfying the following rule w.r.t. interaction with plainly. *)
+  Context {M : ucmraT} (own : M → PROP).
+  Context (own_updateP_plainly : ∀ x Φ R,
+    x ~~>: Φ →
+    own x ∗ (∀ y, ⌜Φ y⌝ -∗ own y -∗ ■ R) ⊢ ■ R).
+
+  Lemma own_updateP x (Φ : M → Prop) :
+    x ~~>: Φ → own x ⊢ bupd_alt (∃ y, ⌜Φ y⌝ ∧ own y).
+  Proof.
+    iIntros (Hup) "Hx"; iIntros (R) "H".
+    iApply (own_updateP_plainly with "[$Hx H]"); first done.
+    iIntros (y ?) "Hy". iApply "H"; auto.
+  Qed.
+End bupd_alt.
+
+(** The alternative definition entails the ordinary basic update *)
+Lemma bupd_alt_bupd {M} (P : uPred M) : bupd_alt P ⊢ |==> P.
+Proof.
+  rewrite /bupd_alt. uPred.unseal; split=> n x Hx H k y ? Hxy.
+  unshelve refine (H {| uPred_holds k _ :=
+    ∃ x' : M, ✓{k} (x' ⋅ y) ∧ P k x' |} k y _ _ _).
+  - intros n1 n2 x1 x2 (z&?&?) _ ?.
+    eauto using cmra_validN_le, uPred_mono.
+  - done.
+  - done.
+  - intros k' z ?? HP. exists z. by rewrite (comm op).
+Qed.
+
+Lemma bupd_alt_bupd_iff {M} (P : uPred M) : bupd_alt P ⊣⊢ |==> P.
+Proof. apply (anti_symm _). apply bupd_alt_bupd. apply bupd_bupd_alt. Qed.
+
+(** The law about the interaction between [uPred_ownM] and plainly holds. *)
+Lemma ownM_updateP {M : ucmraT} x (Φ : M → Prop) (R : uPred M) :
+  x ~~>: Φ →
+  uPred_ownM x ∗ (∀ y, ⌜Φ y⌝ -∗ uPred_ownM y -∗ ■ R) ⊢ ■ R.
+Proof.
+  uPred.unseal=> Hup; split; intros n z Hv (?&z2&?&[z1 ?]&HR); ofe_subst.
+  destruct (Hup n (Some (z1 ⋅ z2))) as (y&?&?); simpl in *.
+  { by rewrite assoc. }
+  refine (HR y n z1 _ _ _ n y _ _ _); auto.
+  - rewrite comm. by eapply cmra_validN_op_r.
+  - by rewrite (comm _ _ y) (comm _ z2).
+  - apply (reflexivity (R:=includedN _)).
+Qed.