bupd_alt.v 4.17 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101
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.