Commit a5771292 authored by Robbert's avatar Robbert

Merge branch 'robbert/bupd_alt' into 'master'

Alternative definition of the basic update modality

See merge request !211
parents f5d03e25 ebb452d3
......@@ -52,7 +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/double_negation.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
......
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.
This diff is collapsed.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment