From 1b85d654ecc57b451b4b7d0a31aaa651f8fb2a41 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 21 Oct 2016 19:35:09 +0200
Subject: [PATCH] Rename rvs -> bupd (basic update), pvs -> fupd (fancy
update).
And also rename the corresponding proof mode tactics.
---
ProofMode.md | 25 ++--
_CoqProject | 2 +-
algebra/double_negation.v | 170 +++++++++++-----------
algebra/upred.v | 68 ++++-----
heap_lang/adequacy.v | 2 +-
heap_lang/heap.v | 22 +--
heap_lang/lib/barrier/proof.v | 32 ++---
heap_lang/lib/counter.v | 48 +++----
heap_lang/lib/par.v | 2 +-
heap_lang/lib/spawn.v | 14 +-
heap_lang/lib/spin_lock.v | 16 +--
heap_lang/lib/ticket_lock.v | 38 ++---
heap_lang/lifting.v | 10 +-
heap_lang/tactics.v | 2 +-
heap_lang/wp_tactics.v | 12 +-
program_logic/adequacy.v | 50 +++----
program_logic/auth.v | 18 +--
program_logic/boxes.v | 32 ++---
program_logic/cancelable_invariants.v | 4 +-
program_logic/counter_examples.v | 92 ++++++------
program_logic/ectx_lifting.v | 2 +-
program_logic/fancy_updates.v | 197 ++++++++++++++++++++++++++
program_logic/ghost_ownership.v | 14 +-
program_logic/hoare.v | 6 +-
program_logic/invariants.v | 14 +-
program_logic/lifting.v | 18 +--
program_logic/pviewshifts.v | 197 --------------------------
program_logic/sts.v | 16 +--
program_logic/thread_local.v | 8 +-
program_logic/viewshifts.v | 6 +-
program_logic/weakestpre.v | 92 ++++++------
program_logic/wsat.v | 18 +--
proofmode/class_instances.v | 40 +++---
proofmode/classes.v | 14 +-
proofmode/coq_tactics.v | 18 +--
proofmode/intro_patterns.v | 23 +--
proofmode/spec_patterns.v | 18 +--
proofmode/tactics.v | 86 +++++------
tests/atomic.v | 28 ++--
tests/barrier_client.v | 2 +-
tests/counter.v | 24 ++--
tests/heap_lang.v | 2 +-
tests/joining_existentials.v | 6 +-
tests/one_shot.v | 20 +--
44 files changed, 764 insertions(+), 764 deletions(-)
create mode 100644 program_logic/fancy_updates.v
delete mode 100644 program_logic/pviewshifts.v
diff --git a/ProofMode.md b/ProofMode.md
index c12a0b5b7..9ba06e4e2 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -5,8 +5,8 @@ Many of the tactics below apply to more goals than described in this document
since the behavior of these tactics can be tuned via instances of the type
classes in the file [proofmode/classes](proofmode/classes.v). Most notable, many
of the tactics can be applied when the to be introduced or to be eliminated
-connective appears under a later, a primitive view shift, or in the conclusion
-of a weakest precondition connective.
+connective appears under a later, an update modality, or in the conclusion of a
+weakest precondition.
Applying hypotheses and lemmas
------------------------------
@@ -124,14 +124,13 @@ Rewriting
Iris
----
-- `iVsIntro` : introduction of a raw or primitive view shift.
-- `iVs pm_trm as (x1 ... xn) "ipat"` : run a raw or primitive view shift
- `pm_trm` (if the goal permits, i.e. it is a raw or primitive view shift, or
- a weakest precondition).
+- `iUpdIntro` : introduction of an update modality.
+- `iUpd pm_trm as (x1 ... xn) "ipat"` : run an update modality `pm_trm` (if the
+ goal permits, i.e. it can be expanded to an update modality.
- `iInv N as (x1 ... xn) "ipat"` : open the invariant `N`.
- `iTimeless "H"` : strip a later of a timeless hypothesis `H` (if the goal
- permits, i.e. it is a later, True now, raw or primitive view shift, or a
- weakest precondition).
+ permits, i.e. it is a later, True now, update modality, or a weakest
+ precondition).
Miscellaneous
-------------
@@ -140,8 +139,8 @@ Miscellaneous
introduces pure connectives.
- The proof mode adds hints to the core `eauto` database so that `eauto`
automatically introduces: conjunctions and disjunctions, universal and
- existential quantifiers, implications and wand, always and later modalities,
- primitive view shifts, and pure connectives.
+ existential quantifiers, implications and wand, always, later and update
+ modalities, and pure connectives.
Selection patterns
==================
@@ -172,7 +171,7 @@ _introduction patterns_:
- `%` : move the hypothesis to the pure Coq context (anonymously).
- `# ipat` : move the hypothesis to the persistent context.
- `> ipat` : remove a later of a timeless hypothesis (if the goal permits).
-- `==> ipat` : run a view shift (if the goal permits).
+- `==> ipat` : run an update modality (if the goal permits).
Apart from this, there are the following introduction patterns that can only
appear at the top level:
@@ -183,7 +182,7 @@ appear at the top level:
- `!%` : introduce a pure goal (and leave the proof mode).
- `!#` : introduce an always modality (given that the spatial context is empty).
- `!>` : introduce a later (which strips laters from all hypotheses).
-- `!==>` : introduce a view shift.
+- `!==>` : introduce an update modality
- `/=` : perform `simpl`.
- `*` : introduce all universal quantifiers.
- `**` : introduce all universal quantifiers, as well as all arrows and wands.
@@ -224,7 +223,7 @@ _specification patterns_ to express splitting of hypotheses:
- `[-H1 ... Hn]` : negated form of the above pattern. This pattern does not
accept hypotheses prefixed with a `$`.
- `==>[H1 ... Hn]` : same as the above pattern, but can only be used if the goal
- is a primitive view shift, in which case the view shift will be kept in the
+ is an update modality, in which case the update modality will be kept in the
goal of the premise too.
- `[#]` : This pattern can be used when eliminating `P -★ Q` with `P`
persistent. Using this pattern, all hypotheses are available in the goal for
diff --git a/_CoqProject b/_CoqProject
index a38123baa..5d4efbcb4 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -69,7 +69,7 @@ program_logic/lifting.v
program_logic/invariants.v
program_logic/wsat.v
program_logic/weakestpre.v
-program_logic/pviewshifts.v
+program_logic/fancy_updates.v
program_logic/hoare.v
program_logic/viewshifts.v
program_logic/language.v
diff --git a/algebra/double_negation.v b/algebra/double_negation.v
index 0e9145c72..c3bd21a3f 100644
--- a/algebra/double_negation.v
+++ b/algebra/double_negation.v
@@ -1,7 +1,7 @@
From iris.algebra Require Import upred.
Import upred.
-(* In this file we show that the rvs can be thought of a kind of
+(* In this file we show that the bupd can be thought of a kind of
step-indexed double-negation when our meta-logic is classical *)
(* To define this, we need a way to talk about iterated later modalities: *)
@@ -12,10 +12,10 @@ Notation "â–·^ n P" := (uPred_laterN n P)
(at level 20, n at level 9, right associativity,
format "â–·^ n P") : uPred_scope.
-Definition uPred_nnvs {M} (P: uPred M) : uPred M :=
+Definition uPred_nnupd {M} (P: uPred M) : uPred M :=
∀ n, (P -★ ▷^n False) -★ ▷^n False.
-Notation "|=n=> Q" := (uPred_nnvs Q)
+Notation "|=n=> Q" := (uPred_nnupd Q)
(at level 99, Q at level 200, format "|=n=> Q") : uPred_scope.
Notation "P =n=> Q" := (P ⊢ |=n=> Q)
(at level 99, Q at level 200, only parsing) : C_scope.
@@ -27,7 +27,7 @@ Notation "P =n=★ Q" := (P -★ |=n=> Q)%I
(2) If our meta-logic is classical, then |=n=> and |=r=> are equivalent
*)
-Section rvs_nnvs.
+Section bupd_nnupd.
Context {M : ucmraT}.
Implicit Types φ : Prop.
Implicit Types P Q : uPred M.
@@ -58,40 +58,40 @@ Proof.
eapply (uPred_closed _ _ (S n)); eauto using cmra_validN_S.
Qed.
-(* It is easy to show that most of the basic properties of rvs that
- are used throughout Iris hold for nnvs.
+(* It is easy to show that most of the basic properties of bupd that
+ are used throughout Iris hold for nnupd.
In fact, the first three properties that follow hold for any
modality of the form (- -★ Q) -★ Q for arbitrary Q. The situation
- here is slightly different, because nnvs is of the form
+ here is slightly different, because nnupd is of the form
∀ n, (- -★ (Q n)) -★ (Q n), but the proofs carry over straightforwardly.
*)
-Lemma nnvs_intro P : P =n=> P.
+Lemma nnupd_intro P : P =n=> P.
Proof. apply forall_intro=>?. apply wand_intro_l, wand_elim_l. Qed.
-Lemma nnvs_mono P Q : (P ⊢ Q) → (|=n=> P) =n=> Q.
+Lemma nnupd_mono P Q : (P ⊢ Q) → (|=n=> P) =n=> Q.
Proof.
intros HPQ. apply forall_intro=>n.
apply wand_intro_l. rewrite -{1}HPQ.
- rewrite /uPred_nnvs (forall_elim n).
+ rewrite /uPred_nnupd (forall_elim n).
apply wand_elim_r.
Qed.
-Lemma nnvs_frame_r P R : (|=n=> P) ★ R =n=> P ★ R.
+Lemma nnupd_frame_r P R : (|=n=> P) ★ R =n=> P ★ R.
Proof.
apply forall_intro=>n. apply wand_intro_r.
rewrite (comm _ P) -wand_curry.
- rewrite /uPred_nnvs (forall_elim n).
+ rewrite /uPred_nnupd (forall_elim n).
by rewrite -assoc wand_elim_r wand_elim_l.
Qed.
-Lemma nnvs_ownM_updateP x (Φ : M → Prop) :
+Lemma nnupd_ownM_updateP x (Φ : M → Prop) :
x ~~>: Φ → uPred_ownM x =n=> ∃ y, ■Φ y ∧ uPred_ownM y.
Proof.
- intros Hrvs. split. rewrite /uPred_nnvs. repeat uPred.unseal.
+ intros Hbupd. split. rewrite /uPred_nnupd. repeat uPred.unseal.
intros n y ? Hown a.
red; rewrite //= => n' yf ??.
inversion Hown as (x'&Hequiv).
- edestruct (Hrvs n' (Some (x' â‹… yf))) as (y'&?&?); eauto.
+ edestruct (Hbupd n' (Some (x' â‹… yf))) as (y'&?&?); eauto.
{ by rewrite //= assoc -(dist_le _ _ _ _ Hequiv). }
case (decide (a ≤ n')).
- intros Hle Hwand.
@@ -110,18 +110,18 @@ Qed.
now over n?
*)
-Remark nnvs_trans P: (|=n=> |=n=> P) ⊢ (|=n=> P).
+Remark nnupd_trans P: (|=n=> |=n=> P) ⊢ (|=n=> P).
Proof.
- rewrite /uPred_nnvs.
+ rewrite /uPred_nnupd.
apply forall_intro=>a. apply wand_intro_l.
rewrite (forall_elim a).
- rewrite (nnvs_intro (P -★ _)).
- rewrite /uPred_nnvs.
+ rewrite (nnupd_intro (P -★ _)).
+ rewrite /uPred_nnupd.
(* Oops -- the exponents of the later modality don't match up! *)
Abort.
(* Instead, we will need to prove this in the model. We start by showing that
- nnvs is the limit of a the following sequence:
+ nnupd is the limit of a the following sequence:
(- -★ False) - ★ False,
(- -★ ▷ False) - ★ ▷ False ∧ (- -★ False) - ★ False,
@@ -129,33 +129,33 @@ Abort.
...
Then, it is easy enough to show that each of the uPreds in this sequence
- is transitive. It turns out that this implies that nnvs is transitive. *)
+ is transitive. It turns out that this implies that nnupd is transitive. *)
(* The definition of the sequence above: *)
-Fixpoint uPred_nnvs_k {M} k (P: uPred M) : uPred M :=
+Fixpoint uPred_nnupd_k {M} k (P: uPred M) : uPred M :=
((P -★ ▷^k False) -★ ▷^k False) ∧
match k with
O => True
- | S k' => uPred_nnvs_k k' P
+ | S k' => uPred_nnupd_k k' P
end.
-Notation "|=n=>_ k Q" := (uPred_nnvs_k k Q)
+Notation "|=n=>_ k Q" := (uPred_nnupd_k k Q)
(at level 99, k at level 9, Q at level 200, format "|=n=>_ k Q") : uPred_scope.
-(* One direction of the limiting process is easy -- nnvs implies nnvs_k for each k *)
-Lemma nnvs_trunc1 k P: (|=n=> P) ⊢ |=n=>_k P.
+(* One direction of the limiting process is easy -- nnupd implies nnupd_k for each k *)
+Lemma nnupd_trunc1 k P: (|=n=> P) ⊢ |=n=>_k P.
Proof.
induction k.
- - rewrite /uPred_nnvs_k /uPred_nnvs.
+ - rewrite /uPred_nnupd_k /uPred_nnupd.
rewrite (forall_elim 0) //= right_id //.
- simpl. apply and_intro; auto.
- rewrite /uPred_nnvs.
+ rewrite /uPred_nnupd.
rewrite (forall_elim (S k)) //=.
Qed.
-Lemma nnvs_k_elim n k P: n ≤ k → ((|=n=>_k P) ★ (P -★ (▷^n False)) ⊢ (▷^n False))%I.
+Lemma nnupd_k_elim n k P: n ≤ k → ((|=n=>_k P) ★ (P -★ (▷^n False)) ⊢ (▷^n False))%I.
Proof.
induction k.
- inversion 1; subst; rewrite //= ?right_id. apply wand_elim_l.
@@ -164,23 +164,23 @@ Proof.
* rewrite and_elim_r IHk //.
Qed.
-Lemma nnvs_k_unfold k P:
+Lemma nnupd_k_unfold k P:
(|=n=>_(S k) P) ⊣⊢ ((P -★ (▷^(S k) False)) -★ (▷^(S k) False)) ∧ (|=n=>_k P).
Proof. done. Qed.
-Lemma nnvs_k_unfold' k P n x:
+Lemma nnupd_k_unfold' k P n x:
(|=n=>_(S k) P)%I n x ↔ (((P -★ (▷^(S k) False)) -★ (▷^(S k) False)) ∧ (|=n=>_k P))%I n x.
Proof. done. Qed.
-Lemma nnvs_k_weaken k P: (|=n=>_(S k) P) ⊢ |=n=>_k P.
-Proof. by rewrite nnvs_k_unfold and_elim_r. Qed.
+Lemma nnupd_k_weaken k P: (|=n=>_(S k) P) ⊢ |=n=>_k P.
+Proof. by rewrite nnupd_k_unfold and_elim_r. Qed.
-(* Now we are ready to show nnvs is the limit -- ie, for each k, it is within distance k
+(* Now we are ready to show nnupd is the limit -- ie, for each k, it is within distance k
of the kth term of the sequence *)
-Lemma nnvs_nnvs_k_dist k P: (|=n=> P)%I ≡{k}≡ (|=n=>_k P)%I.
+Lemma nnupd_nnupd_k_dist k P: (|=n=> P)%I ≡{k}≡ (|=n=>_k P)%I.
split; intros n' x Hle Hx. split.
- - by apply (nnvs_trunc1 k).
+ - by apply (nnupd_trunc1 k).
- revert n' x Hle Hx; induction k; intros n' x Hle Hx;
- rewrite ?nnvs_k_unfold' /uPred_nnvs.
+ rewrite ?nnupd_k_unfold' /uPred_nnupd.
* rewrite //=. unseal.
inversion Hle; subst.
intros (HnnP&_) n k' x' ?? HPF.
@@ -199,17 +199,17 @@ Lemma nnvs_nnvs_k_dist k P: (|=n=> P)%I ≡{k}≡ (|=n=>_k P)%I.
*** intros. exfalso. assert (n ≤ k'). omega.
assert (n = S k ∨ n < S k) as [->|] by omega.
**** eapply laterN_big; eauto; unseal. eapply HnnP; eauto.
- **** move:nnvs_k_elim. unseal. intros Hnnvsk.
+ **** move:nnupd_k_elim. unseal. intros Hnnupdk.
eapply laterN_big; eauto. unseal.
- eapply (Hnnvsk n k); first omega; eauto.
+ eapply (Hnnupdk n k); first omega; eauto.
exists x, x'. split_and!; eauto. eapply uPred_closed; eauto.
eapply cmra_validN_op_l; eauto.
** intros HP. eapply IHk; auto.
move:HP. unseal. intros (?&?); naive_solver.
Qed.
-(* nnvs_k has a number of structural properties, including transitivity *)
-Lemma nnvs_k_intro k P: P ⊢ (|=n=>_k P).
+(* nnupd_k has a number of structural properties, including transitivity *)
+Lemma nnupd_k_intro k P: P ⊢ (|=n=>_k P).
Proof.
induction k; rewrite //= ?right_id.
- apply wand_intro_l. apply wand_elim_l.
@@ -217,58 +217,58 @@ Proof.
apply wand_intro_l. apply wand_elim_l.
Qed.
-Lemma nnvs_k_mono k P Q: (P ⊢ Q) → (|=n=>_k P) ⊢ (|=n=>_k Q).
+Lemma nnupd_k_mono k P Q: (P ⊢ Q) → (|=n=>_k P) ⊢ (|=n=>_k Q).
Proof.
induction k; rewrite //= ?right_id=>HPQ.
- do 2 (apply wand_mono; auto).
- apply and_mono; auto; do 2 (apply wand_mono; auto).
Qed.
-Instance nnvs_k_mono' k: Proper ((⊢) ==> (⊢)) (@uPred_nnvs_k M k).
-Proof. by intros P P' HP; apply nnvs_k_mono. Qed.
+Instance nnupd_k_mono' k: Proper ((⊢) ==> (⊢)) (@uPred_nnupd_k M k).
+Proof. by intros P P' HP; apply nnupd_k_mono. Qed.
-Instance nnvs_k_ne k n : Proper (dist n ==> dist n) (@uPred_nnvs_k M k).
+Instance nnupd_k_ne k n : Proper (dist n ==> dist n) (@uPred_nnupd_k M k).
Proof. induction k; rewrite //= ?right_id=>P P' HP; by rewrite HP. Qed.
-Lemma nnvs_k_proper k P Q: (P ⊣⊢ Q) → (|=n=>_k P) ⊣⊢ (|=n=>_k Q).
-Proof. intros HP; apply (anti_symm (⊢)); eapply nnvs_k_mono; by rewrite HP. Qed.
-Instance nnvs_k_proper' k: Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_nnvs_k M k).
-Proof. by intros P P' HP; apply nnvs_k_proper. Qed.
+Lemma nnupd_k_proper k P Q: (P ⊣⊢ Q) → (|=n=>_k P) ⊣⊢ (|=n=>_k Q).
+Proof. intros HP; apply (anti_symm (⊢)); eapply nnupd_k_mono; by rewrite HP. Qed.
+Instance nnupd_k_proper' k: Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_nnupd_k M k).
+Proof. by intros P P' HP; apply nnupd_k_proper. Qed.
-Lemma nnvs_k_trans k P: (|=n=>_k |=n=>_k P) ⊢ (|=n=>_k P).
+Lemma nnupd_k_trans k P: (|=n=>_k |=n=>_k P) ⊢ (|=n=>_k P).
Proof.
revert P.
induction k; intros P.
- rewrite //= ?right_id. apply wand_intro_l.
- rewrite {1}(nnvs_k_intro 0 (P -★ False)%I) //= ?right_id. apply wand_elim_r.
- - rewrite {2}(nnvs_k_unfold k P).
+ rewrite {1}(nnupd_k_intro 0 (P -★ False)%I) //= ?right_id. apply wand_elim_r.
+ - rewrite {2}(nnupd_k_unfold k P).
apply and_intro.
- * rewrite (nnvs_k_unfold k P). rewrite and_elim_l.
- rewrite nnvs_k_unfold. rewrite and_elim_l.
+ * rewrite (nnupd_k_unfold k P). rewrite and_elim_l.
+ rewrite nnupd_k_unfold. rewrite and_elim_l.
apply wand_intro_l.
- rewrite {1}(nnvs_k_intro (S k) (P -★ ▷^(S k) (False)%I)).
- rewrite nnvs_k_unfold and_elim_l. apply wand_elim_r.
- * do 2 rewrite nnvs_k_weaken //.
+ rewrite {1}(nnupd_k_intro (S k) (P -★ ▷^(S k) (False)%I)).
+ rewrite nnupd_k_unfold and_elim_l. apply wand_elim_r.
+ * do 2 rewrite nnupd_k_weaken //.
Qed.
-Lemma nnvs_trans P : (|=n=> |=n=> P) =n=> P.
+Lemma nnupd_trans P : (|=n=> |=n=> P) =n=> P.
Proof.
split=> n x ? Hnn.
- eapply nnvs_nnvs_k_dist in Hnn; eauto.
- eapply (nnvs_k_ne (n) n ((|=n=>_(n) P)%I)) in Hnn; eauto;
- [| symmetry; eapply nnvs_nnvs_k_dist].
- eapply nnvs_nnvs_k_dist; eauto.
- by apply nnvs_k_trans.
+ eapply nnupd_nnupd_k_dist in Hnn; eauto.
+ eapply (nnupd_k_ne (n) n ((|=n=>_(n) P)%I)) in Hnn; eauto;
+ [| symmetry; eapply nnupd_nnupd_k_dist].
+ eapply nnupd_nnupd_k_dist; eauto.
+ by apply nnupd_k_trans.
Qed.
-(* Now that we have shown nnvs has all of the desired properties of
- rvs, we go further and show it is in fact equivalent to rvs! The
- direction from rvs to nnvs is similar to the proof of
- nnvs_ownM_updateP *)
+(* Now that we have shown nnupd has all of the desired properties of
+ bupd, we go further and show it is in fact equivalent to bupd! The
+ direction from bupd to nnupd is similar to the proof of
+ nnupd_ownM_updateP *)
-Lemma rvs_nnvs P: (|=r=> P) ⊢ |=n=> P.
+Lemma bupd_nnupd P: (|=r=> P) ⊢ |=n=> P.
Proof.
- split. rewrite /uPred_nnvs. repeat uPred.unseal. intros n x ? Hrvs a.
+ split. rewrite /uPred_nnupd. repeat uPred.unseal. intros n x ? Hbupd a.
red; rewrite //= => n' yf ??.
- edestruct Hrvs as (x'&?&?); eauto.
+ edestruct Hbupd as (x'&?&?); eauto.
case (decide (a ≤ n')).
- intros Hle Hwand.
exfalso. eapply laterN_big; last (uPred.unseal; eapply (Hwand n' x')); eauto.
@@ -282,9 +282,9 @@ Qed.
(* However, the other direction seems to need a classical axiom: *)
Section classical.
Context (not_all_not_ex: ∀ (P : M → Prop), ¬ (∀ n : M, ¬ P n) → ∃ n : M, P n).
-Lemma nnvs_rvs P: (|=n=> P) ⊢ (|=r=> P).
+Lemma nnupd_bupd P: (|=n=> P) ⊢ (|=r=> P).
Proof.
- rewrite /uPred_nnvs.
+ rewrite /uPred_nnupd.
split. uPred.unseal; red; rewrite //=.
intros n x ? Hforall k yf Hle ?.
apply not_all_not_ex.
@@ -300,36 +300,36 @@ Proof.
Qed.
End classical.
-(* We might wonder whether we can prove an adequacy lemma for nnvs. We could combine
- the adequacy lemma for rvs with the previous result to get adquacy for nnvs, but
+(* We might wonder whether we can prove an adequacy lemma for nnupd. We could combine
+ the adequacy lemma for bupd with the previous result to get adquacy for nnupd, but
this would rely on the classical axiom we needed to prove the equivalence! Can
we establish adequacy without axioms? Unfortunately not, because adequacy for
- nnvs would imply double negation elimination, which is classical: *)
+ nnupd would imply double negation elimination, which is classical: *)
-Lemma nnvs_dne φ: True ⊢ (|=n=> (■(¬¬ φ → φ)): uPred M)%I.
+Lemma nnupd_dne φ: True ⊢ (|=n=> (■(¬¬ φ → φ)): uPred M)%I.
Proof.
- rewrite /uPred_nnvs. apply forall_intro=>n.
+ rewrite /uPred_nnupd. apply forall_intro=>n.
apply wand_intro_l. rewrite ?right_id.
assert (∀ φ, ¬¬¬¬φ → ¬¬φ) by naive_solver.
assert (Hdne: ¬¬ (¬¬φ → φ)) by naive_solver.
- split. unseal. intros n' ?? Hvs.
+ split. unseal. intros n' ?? Hupd.
case (decide (n' < n)).
- intros. move: laterN_small. unseal. naive_solver.
- intros. assert (n ≤ n'). omega.
- exfalso. specialize (Hvs n' ∅).
+ exfalso. specialize (Hupd n' ∅).
eapply Hdne. intros Hfal.
eapply laterN_big; eauto.
- unseal. rewrite right_id in Hvs *; naive_solver.
+ unseal. rewrite right_id in Hupd *; naive_solver.
Qed.
(* Nevertheless, we can prove a weaker form of adequacy (which is equvialent to adequacy
- under classical axioms) directly without passing through the proofs for rvs: *)
+ under classical axioms) directly without passing through the proofs for bupd: *)
Lemma adequacy_helper1 P n k x:
✓{S n + k} x → ¬¬ (Nat.iter (S n) (λ P, |=n=> ▷ P)%I P (S n + k) x)
→ ¬¬ (∃ x', ✓{n + k} (x') ∧ Nat.iter n (λ P, |=n=> ▷ P)%I P (n + k) (x')).
Proof.
revert k P x. induction n.
- - rewrite /uPred_nnvs. unseal=> k P x Hx Hf1 Hf2.
+ - rewrite /uPred_nnupd. unseal=> k P x Hx Hf1 Hf2.
eapply Hf1. intros Hf3.
eapply (laterN_big (S k) (S k)); eauto.
specialize (Hf3 (S k) (S k) ∅). rewrite right_id in Hf3 *. unseal.
@@ -373,8 +373,8 @@ Qed.
(* Open question:
- Do the basic properties of the |=r=> modality (rvs_intro, rvs_mono, rvs_trans, rvs_frame_r,
- rvs_ownM_updateP, and adequacy) uniquely characterize |=r=>?
+ Do the basic properties of the |=r=> modality (bupd_intro, bupd_mono, rvs_trans, rvs_frame_r,
+ bupd_ownM_updateP, and adequacy) uniquely characterize |=r=>?
*)
-End rvs_nnvs.
\ No newline at end of file
+End bupd_nnupd.
diff --git a/algebra/upred.v b/algebra/upred.v
index 8d8baee24..79dd89383 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -264,7 +264,7 @@ Definition uPred_cmra_valid {M A} := proj1_sig uPred_cmra_valid_aux M A.
Definition uPred_cmra_valid_eq :
@uPred_cmra_valid = @uPred_cmra_valid_def := proj2_sig uPred_cmra_valid_aux.
-Program Definition uPred_rvs_def {M} (Q : uPred M) : uPred M :=
+Program Definition uPred_bupd_def {M} (Q : uPred M) : uPred M :=
{| uPred_holds n x := ∀ k yf,
k ≤ n → ✓{k} (x ⋅ yf) → ∃ x', ✓{k} (x' ⋅ yf) ∧ Q k x' |}.
Next Obligation.
@@ -275,9 +275,9 @@ Next Obligation.
apply uPred_mono with x'; eauto using cmra_includedN_l.
Qed.
Next Obligation. naive_solver. Qed.
-Definition uPred_rvs_aux : { x | x = @uPred_rvs_def }. by eexists. Qed.
-Definition uPred_rvs {M} := proj1_sig uPred_rvs_aux M.
-Definition uPred_rvs_eq : @uPred_rvs = @uPred_rvs_def := proj2_sig uPred_rvs_aux.
+Definition uPred_bupd_aux : { x | x = @uPred_bupd_def }. by eexists. Qed.
+Definition uPred_bupd {M} := proj1_sig uPred_bupd_aux M.
+Definition uPred_bupd_eq : @uPred_bupd = @uPred_bupd_def := proj2_sig uPred_bupd_aux.
Notation "P ⊢ Q" := (uPred_entails P%I Q%I)
(at level 99, Q at level 200, right associativity) : C_scope.
@@ -310,7 +310,7 @@ Notation "â–· P" := (uPred_later P)
(at level 20, right associativity) : uPred_scope.
Infix "≡" := uPred_eq : uPred_scope.
Notation "✓ x" := (uPred_cmra_valid x) (at level 20) : uPred_scope.
-Notation "|=r=> Q" := (uPred_rvs Q)
+Notation "|=r=> Q" := (uPred_bupd Q)
(at level 99, Q at level 200, format "|=r=> Q") : uPred_scope.
Notation "P =r=> Q" := (P ⊢ |=r=> Q)
(at level 99, Q at level 200, only parsing) : C_scope.
@@ -344,7 +344,7 @@ Module uPred.
Definition unseal :=
(uPred_pure_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq,
uPred_exist_eq, uPred_eq_eq, uPred_sep_eq, uPred_wand_eq, uPred_always_eq,
- uPred_later_eq, uPred_ownM_eq, uPred_cmra_valid_eq, uPred_rvs_eq).
+ uPred_later_eq, uPred_ownM_eq, uPred_cmra_valid_eq, uPred_bupd_eq).
Ltac unseal := rewrite !unseal /=.
Section uPred_logic.
@@ -488,14 +488,14 @@ Proof.
Qed.
Global Instance cmra_valid_proper {A : cmraT} :
Proper ((≡) ==> (⊣⊢)) (@uPred_cmra_valid M A) := ne_proper _.
-Global Instance rvs_ne n : Proper (dist n ==> dist n) (@uPred_rvs M).
+Global Instance bupd_ne n : Proper (dist n ==> dist n) (@uPred_bupd M).
Proof.
intros P Q HPQ.
unseal; split=> n' x; split; intros HP k yf ??;
destruct (HP k yf) as (x'&?&?); auto;
exists x'; split; auto; apply HPQ; eauto using cmra_validN_op_l.
Qed.
-Global Instance rvs_proper : Proper ((≡) ==> (≡)) (@uPred_rvs M) := ne_proper _.
+Global Instance bupd_proper : Proper ((≡) ==> (≡)) (@uPred_bupd M) := ne_proper _.
(** Introduction and elimination rules *)
Lemma pure_intro φ P : φ → P ⊢ ■φ.
@@ -1282,21 +1282,21 @@ Lemma always_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a.
apply:always_cmra_valid_1.
Qed.
-(* Viewshifts *)
-Lemma rvs_intro P : P =r=> P.
+(* Basic update modality *)
+Lemma bupd_intro P : P =r=> P.
Proof.
unseal. split=> n x ? HP k yf ?; exists x; split; first done.
apply uPred_closed with n; eauto using cmra_validN_op_l.
Qed.
-Lemma rvs_mono P Q : (P ⊢ Q) → (|=r=> P) =r=> Q.
+Lemma bupd_mono P Q : (P ⊢ Q) → (|=r=> P) =r=> Q.
Proof.
unseal. intros HPQ; split=> n x ? HP k yf ??.
destruct (HP k yf) as (x'&?&?); eauto.
exists x'; split; eauto using uPred_in_entails, cmra_validN_op_l.
Qed.
-Lemma rvs_trans P : (|=r=> |=r=> P) =r=> P.
+Lemma bupd_trans P : (|=r=> |=r=> P) =r=> P.
Proof. unseal; split; naive_solver. Qed.
-Lemma rvs_frame_r P R : (|=r=> P) ★ R =r=> P ★ R.
+Lemma bupd_frame_r P R : (|=r=> P) ★ R =r=> P ★ R.
Proof.
unseal; split; intros n x ? (x1&x2&Hx&HP&?) k yf ??.
destruct (HP k (x2 â‹… yf)) as (x'&?&?); eauto.
@@ -1305,7 +1305,7 @@ Proof.
exists x', x2; split_and?; auto.
apply uPred_closed with n; eauto 3 using cmra_validN_op_l, cmra_validN_op_r.
Qed.
-Lemma rvs_ownM_updateP x (Φ : M → Prop) :
+Lemma bupd_ownM_updateP x (Φ : M → Prop) :
x ~~>: Φ → uPred_ownM x =r=> ∃ y, ■Φ y ∧ uPred_ownM y.
Proof.
unseal=> Hup; split=> n x2 ? [x3 Hx] k yf ??.
@@ -1316,27 +1316,27 @@ Proof.
Qed.
(** * Derived rules *)
-Global Instance rvs_mono' : Proper ((⊢) ==> (⊢)) (@uPred_rvs M).
-Proof. intros P Q; apply rvs_mono. Qed.
-Global Instance rvs_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) (@uPred_rvs M).
-Proof. intros P Q; apply rvs_mono. Qed.
-Lemma rvs_frame_l R Q : (R ★ |=r=> Q) =r=> R ★ Q.
-Proof. rewrite !(comm _ R); apply rvs_frame_r. Qed.
-Lemma rvs_wand_l P Q : (P -★ Q) ★ (|=r=> P) =r=> Q.
-Proof. by rewrite rvs_frame_l wand_elim_l. Qed.
-Lemma rvs_wand_r P Q : (|=r=> P) ★ (P -★ Q) =r=> Q.
-Proof. by rewrite rvs_frame_r wand_elim_r. Qed.
-Lemma rvs_sep P Q : (|=r=> P) ★ (|=r=> Q) =r=> P ★ Q.
-Proof. by rewrite rvs_frame_r rvs_frame_l rvs_trans. Qed.
-Lemma rvs_ownM_update x y : x ~~> y → uPred_ownM x ⊢ |=r=> uPred_ownM y.
+Global Instance bupd_mono' : Proper ((⊢) ==> (⊢)) (@uPred_bupd M).
+Proof. intros P Q; apply bupd_mono. Qed.
+Global Instance bupd_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) (@uPred_bupd M).
+Proof. intros P Q; apply bupd_mono. Qed.
+Lemma bupd_frame_l R Q : (R ★ |=r=> Q) =r=> R ★ Q.
+Proof. rewrite !(comm _ R); apply bupd_frame_r. Qed.
+Lemma bupd_wand_l P Q : (P -★ Q) ★ (|=r=> P) =r=> Q.
+Proof. by rewrite bupd_frame_l wand_elim_l. Qed.
+Lemma bupd_wand_r P Q : (|=r=> P) ★ (P -★ Q) =r=> Q.
+Proof. by rewrite bupd_frame_r wand_elim_r. Qed.
+Lemma bupd_sep P Q : (|=r=> P) ★ (|=r=> Q) =r=> P ★ Q.
+Proof. by rewrite bupd_frame_r bupd_frame_l bupd_trans. Qed.
+Lemma bupd_ownM_update x y : x ~~> y → uPred_ownM x ⊢ |=r=> uPred_ownM y.
Proof.
- intros; rewrite (rvs_ownM_updateP _ (y =)); last by apply cmra_update_updateP.
- by apply rvs_mono, exist_elim=> y'; apply pure_elim_l=> ->.
+ intros; rewrite (bupd_ownM_updateP _ (y =)); last by apply cmra_update_updateP.
+ by apply bupd_mono, exist_elim=> y'; apply pure_elim_l=> ->.
Qed.
-Lemma except_last_rvs P : ◇ (|=r=> P) ⊢ (|=r=> ◇ P).
+Lemma except_last_bupd P : ◇ (|=r=> P) ⊢ (|=r=> ◇ P).
Proof.
- rewrite /uPred_except_last. apply or_elim; auto using rvs_mono.
- by rewrite -rvs_intro -or_intro_l.
+ rewrite /uPred_except_last. apply or_elim; auto using bupd_mono.
+ by rewrite -bupd_intro -or_intro_l.
Qed.
(* Products *)
@@ -1495,8 +1495,8 @@ Proof.
cut (∀ x, ✓{n} x → Nat.iter n (λ P, |=r=> ▷ P)%I (■φ)%I n x → φ).
{ intros help H. eapply (help ∅); eauto using ucmra_unit_validN.
eapply H; try unseal; eauto using ucmra_unit_validN. }
- unseal. induction n as [|n IH]=> x Hx Hvs; auto.
- destruct (Hvs (S n) ∅) as (x'&?&?); rewrite ?right_id; auto.
+ unseal. induction n as [|n IH]=> x Hx Hupd; auto.
+ destruct (Hupd (S n) ∅) as (x'&?&?); rewrite ?right_id; auto.
eapply IH with x'; eauto using cmra_validN_S, cmra_validN_op_l.
Qed.
diff --git a/heap_lang/adequacy.v b/heap_lang/adequacy.v
index c6e482cba..5884b7818 100644
--- a/heap_lang/adequacy.v
+++ b/heap_lang/adequacy.v
@@ -20,7 +20,7 @@ Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
adequate e σ φ.
Proof.
intros Hwp; eapply (wp_adequacy Σ); iIntros (?) "Hσ".
- iVs (auth_alloc to_heap _ heapN _ σ with "[Hσ]") as (γ) "[Hh _]";[|by iNext|].
+ iUpd (auth_alloc to_heap _ heapN _ σ with "[Hσ]") as (γ) "[Hh _]";[|by iNext|].
{ exact: to_heap_valid. }
set (Hheap := HeapG _ _ _ γ).
iApply (Hwp _). by rewrite /heap_ctx.
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 5701bd313..9bf95350b 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -109,10 +109,10 @@ Section heap.
heap_ctx ★ ▷ (∀ l, l ↦ v ={E}=★ Φ (LitV (LitLoc l))) ⊢ WP Alloc e @ E {{ Φ }}.
Proof.
iIntros (<-%of_to_val ?) "[#Hinv HΦ]". rewrite /heap_ctx.
- iVs (auth_empty heap_name) as "Ha".
- iVs (auth_open with "[$Hinv $Ha]") as (σ) "(%&Hσ&Hcl)"; first done.
+ iUpd (auth_empty heap_name) as "Ha".
+ iUpd (auth_open with "[$Hinv $Ha]") as (σ) "(%&Hσ&Hcl)"; first done.
iApply wp_alloc_pst. iFrame "Hσ". iNext. iIntros (l) "[% Hσ] !==>".
- iVs ("Hcl" with "* [Hσ]") as "Ha".
+ iUpd ("Hcl" with "* [Hσ]") as "Ha".
{ iFrame. iPureIntro. rewrite to_heap_insert.
eapply alloc_singleton_local_update; by auto using lookup_to_heap_None. }
iApply "HΦ". by rewrite heap_mapsto_eq /heap_mapsto_def.
@@ -125,9 +125,9 @@ Section heap.
Proof.
iIntros (?) "[#Hinv [>Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
- iVs (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
+ iUpd (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
iApply (wp_load_pst _ σ); first eauto using heap_singleton_included.
- iIntros "{$Hσ} !> Hσ !==>". iVs ("Hcl" with "* [Hσ]") as "Ha"; first eauto.
+ iIntros "{$Hσ} !> Hσ !==>". iUpd ("Hcl" with "* [Hσ]") as "Ha"; first eauto.
by iApply "HΦ".
Qed.
@@ -138,9 +138,9 @@ Section heap.
Proof.
iIntros (<-%of_to_val ?) "[#Hinv [>Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
- iVs (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
+ iUpd (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
iApply (wp_store_pst _ σ); first eauto using heap_singleton_included.
- iIntros "{$Hσ} !> Hσ !==>". iVs ("Hcl" with "* [Hσ]") as "Ha".
+ iIntros "{$Hσ} !> Hσ !==>". iUpd ("Hcl" with "* [Hσ]") as "Ha".
{ iFrame. iPureIntro. rewrite to_heap_insert.
eapply singleton_local_update, exclusive_local_update; last done.
by eapply heap_singleton_included'. }
@@ -154,9 +154,9 @@ Section heap.
Proof.
iIntros (<-%of_to_val <-%of_to_val ??) "[#Hinv [>Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
- iVs (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
+ iUpd (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
iApply (wp_cas_fail_pst _ σ); [eauto using heap_singleton_included|done|].
- iIntros "{$Hσ} !> Hσ !==>". iVs ("Hcl" with "* [Hσ]") as "Ha"; first eauto.
+ iIntros "{$Hσ} !> Hσ !==>". iUpd ("Hcl" with "* [Hσ]") as "Ha"; first eauto.
by iApply "HΦ".
Qed.
@@ -167,9 +167,9 @@ Section heap.
Proof.
iIntros (<-%of_to_val <-%of_to_val ?) "[#Hinv [>Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
- iVs (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
+ iUpd (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
iApply (wp_cas_suc_pst _ σ); first eauto using heap_singleton_included.
- iIntros "{$Hσ} !> Hσ !==>". iVs ("Hcl" with "* [Hσ]") as "Ha".
+ iIntros "{$Hσ} !> Hσ !==>". iUpd ("Hcl" with "* [Hσ]") as "Ha".
{ iFrame. iPureIntro. rewrite to_heap_insert.
eapply singleton_local_update, exclusive_local_update; last done.
by eapply heap_singleton_included'. }
diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index 9be41c4de..d38861902 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -98,8 +98,8 @@ Proof.
iIntros (HN) "[#? HΦ]".
rewrite /newbarrier /=. wp_seq. wp_alloc l as "Hl".
iApply ("HΦ" with "==>[-]").
- iVs (saved_prop_alloc (F:=idCF) P) as (γ) "#?".
- iVs (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
+ iUpd (saved_prop_alloc (F:=idCF) P) as (γ) "#?".
+ iUpd (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
as (γ') "[#? Hγ']"; eauto.
{ iNext. rewrite /barrier_inv /=. iFrame.
iExists (const P). rewrite !big_sepS_singleton /=. eauto. }
@@ -112,7 +112,7 @@ Proof.
- iApply (sts_own_weaken with "Hγ'");
auto using sts.closed_op, i_states_closed, low_states_closed;
abstract set_solver. }
- iVsIntro. rewrite /recv /send. iSplitL "Hr".
+ iUpdIntro. rewrite /recv /send. iSplitL "Hr".
- iExists γ', P, P, γ. iFrame. auto.
- auto.
Qed.
@@ -122,10 +122,10 @@ Lemma signal_spec l P (Φ : val → iProp Σ) :
Proof.
rewrite /signal /send /barrier_ctx /=.
iIntros "(Hs&HP&HΦ)"; iDestruct "Hs" as (γ) "[#(%&Hh&Hsts) Hγ]". wp_let.
- iVs (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
+ iUpd (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
destruct p; [|done]. wp_store. iFrame "HΦ".
- iVs ("Hclose" $! (State High I) (∅ : set token) with "[-]"); last done.
+ iUpd ("Hclose" $! (State High I) (∅ : set token) with "[-]"); last done.
iSplit; [iPureIntro; by eauto using signal_step|].
iNext. rewrite {2}/barrier_inv /ress /=; iFrame "Hl".
iDestruct "Hr" as (Ψ) "[Hr Hsp]"; iExists Ψ; iFrame "Hsp".
@@ -138,14 +138,14 @@ Proof.
rename P into R; rewrite /recv /barrier_ctx.
iIntros "[Hr HΦ]"; iDestruct "Hr" as (γ P Q i) "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
iLöb as "IH". wp_rec. wp_bind (! _)%E.
- iVs (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
+ iUpd (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
wp_load. destruct p.
- - iVs ("Hclose" $! (State Low I) {[ Change i ]} with "[Hl Hr]") as "Hγ".
+ - iUpd ("Hclose" $! (State Low I) {[ Change i ]} with "[Hl Hr]") as "Hγ".
{ iSplit; first done. iNext. rewrite {2}/barrier_inv /=. by iFrame. }
iAssert (sts_ownS γ (i_states i) {[Change i]})%I with "==>[Hγ]" as "Hγ".
{ iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. }
- iVsIntro. wp_if.
+ iUpdIntro. wp_if.
iApply ("IH" with "Hγ [HQR] HΦ"). auto.
- (* a High state: the comparison succeeds, and we perform a transition and
return to the client *)
@@ -153,12 +153,12 @@ Proof.
iDestruct (big_sepS_delete _ _ i with "Hsp") as "[#HΨi Hsp]"; first done.
iAssert (▷ Ψ i ★ ▷ [★ set] j ∈ I ∖ {[i]}, Ψ j)%I with "[HΨ]" as "[HΨ HΨ']".
{ iNext. iApply (big_sepS_delete _ _ i); first done. by iApply "HΨ". }
- iVs ("Hclose" $! (State High (I ∖ {[ i ]})) (∅ : set token) with "[HΨ' Hl Hsp]").
+ iUpd ("Hclose" $! (State High (I ∖ {[ i ]})) (∅ : set token) with "[HΨ' Hl Hsp]").
{ iSplit; [iPureIntro; by eauto using wait_step|].
iNext. rewrite {2}/barrier_inv /=; iFrame "Hl". iExists Ψ; iFrame. auto. }
iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by auto.
- iVsIntro. wp_if.
- iVsIntro. iApply "HΦ". iApply "HQR". by iRewrite "Heq".
+ iUpdIntro. wp_if.
+ iUpdIntro. iApply "HΦ". iApply "HQR". by iRewrite "Heq".
Qed.
Lemma recv_split E l P1 P2 :
@@ -166,13 +166,13 @@ Lemma recv_split E l P1 P2 :
Proof.
rename P1 into R1; rename P2 into R2. rewrite {1}/recv /barrier_ctx.
iIntros (?). iDestruct 1 as (γ P Q i) "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
- iVs (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
+ iUpd (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
- iVs (saved_prop_alloc_strong (R1: ∙%CF (iProp Σ)) I) as (i1) "[% #Hi1]".
- iVs (saved_prop_alloc_strong (R2: ∙%CF (iProp Σ)) (I ∪ {[i1]}))
+ iUpd (saved_prop_alloc_strong (R1: ∙%CF (iProp Σ)) I) as (i1) "[% #Hi1]".
+ iUpd (saved_prop_alloc_strong (R2: ∙%CF (iProp Σ)) (I ∪ {[i1]}))
as (i2) "[Hi2' #Hi2]"; iDestruct "Hi2'" as %Hi2.
rewrite ->not_elem_of_union, elem_of_singleton in Hi2; destruct Hi2.
- iVs ("Hclose" $! (State p ({[i1; i2]} ∪ I ∖ {[i]}))
+ iUpd ("Hclose" $! (State p ({[i1; i2]} ∪ I ∖ {[i]}))
{[Change i1; Change i2 ]} with "[-]") as "Hγ".
{ iSplit; first by eauto using split_step.
iNext. rewrite {2}/barrier_inv /=. iFrame "Hl".
@@ -184,7 +184,7 @@ Proof.
- iApply (sts_own_weaken with "Hγ");
eauto using sts.closed_op, i_states_closed.
abstract set_solver. }
- iVsIntro; iSplitL "Hγ1"; rewrite /recv /barrier_ctx.
+ iUpdIntro; iSplitL "Hγ1"; rewrite /recv /barrier_ctx.
- iExists γ, P, R1, i1. iFrame; auto.
- iExists γ, P, R2, i2. iFrame; auto.
Qed.
diff --git a/heap_lang/lib/counter.v b/heap_lang/lib/counter.v
index 2b8c7575b..c63966215 100644
--- a/heap_lang/lib/counter.v
+++ b/heap_lang/lib/counter.v
@@ -38,10 +38,10 @@ Section mono_proof.
heap_ctx ★ (∀ l, mcounter l 0 -★ Φ #l) ⊢ WP newcounter #() {{ Φ }}.
Proof.
iIntros (?) "[#Hh HΦ]". rewrite /newcounter /=. wp_seq. wp_alloc l as "Hl".
- iVs (own_alloc (◠(O:mnat) ⋅ ◯ (O:mnat))) as (γ) "[Hγ Hγ']"; first done.
- iVs (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
+ iUpd (own_alloc (◠(O:mnat) ⋅ ◯ (O:mnat))) as (γ) "[Hγ Hγ']"; first done.
+ iUpd (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
{ iNext. iExists 0%nat. by iFrame. }
- iVsIntro. iApply "HΦ". rewrite /mcounter; eauto 10.
+ iUpdIntro. iApply "HΦ". rewrite /mcounter; eauto 10.
Qed.
Lemma inc_mono_spec l n (Φ : val → iProp Σ) :
@@ -50,22 +50,22 @@ Section mono_proof.
iIntros "[Hl HΦ]". iLöb as "IH". wp_rec.
iDestruct "Hl" as (γ) "(% & #? & #Hinv & Hγf)".
wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]" "Hclose".
- wp_load. iVs ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
- iVsIntro. wp_let. wp_op.
+ wp_load. iUpd ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
+ iUpdIntro. wp_let. wp_op.
wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]" "Hclose".
destruct (decide (c' = c)) as [->|].
- iDestruct (own_valid_2 with "[$Hγ $Hγf]")
as %[?%mnat_included _]%auth_valid_discrete_2.
- iVs (own_update_2 with "[$Hγ $Hγf]") as "[Hγ Hγf]".
+ iUpd (own_update_2 with "[$Hγ $Hγf]") as "[Hγ Hγf]".
{ apply auth_update, (mnat_local_update _ _ (S c)); auto. }
- wp_cas_suc. iVs ("Hclose" with "[Hl Hγ]") as "_".
+ wp_cas_suc. iUpd ("Hclose" with "[Hl Hγ]") as "_".
{ iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
- iVsIntro. wp_if. iApply "HΦ"; iExists γ; repeat iSplit; eauto.
+ iUpdIntro. wp_if. iApply "HΦ"; iExists γ; repeat iSplit; eauto.
iApply (own_mono with "Hγf"). apply: auth_frag_mono.
by apply mnat_included, le_n_S.
- wp_cas_fail; first (by intros [= ?%Nat2Z.inj]).
- iVs ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
- iVsIntro. wp_if. iApply ("IH" with "[Hγf] HΦ").
+ iUpd ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
+ iUpdIntro. wp_if. iApply ("IH" with "[Hγf] HΦ").
rewrite {3}/mcounter; eauto 10.
Qed.
@@ -77,9 +77,9 @@ Section mono_proof.
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
iDestruct (own_valid_2 with "[$Hγ $Hγf]")
as %[?%mnat_included _]%auth_valid_discrete_2.
- iVs (own_update_2 with "[$Hγ $Hγf]") as "[Hγ Hγf]".
+ iUpd (own_update_2 with "[$Hγ $Hγf]") as "[Hγ Hγf]".
{ apply auth_update, (mnat_local_update _ _ c); auto. }
- iVs ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
+ iUpd ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
iApply ("HΦ" with "[%]"); rewrite /mcounter; eauto 10.
Qed.
End mono_proof.
@@ -116,11 +116,11 @@ Section contrib_spec.
⊢ WP newcounter #() {{ Φ }}.
Proof.
iIntros (?) "[#Hh HΦ]". rewrite /newcounter /=. wp_seq. wp_alloc l as "Hl".
- iVs (own_alloc (â— (Some (1%Qp, O%nat)) â‹… â—¯ (Some (1%Qp, 0%nat))))
+ iUpd (own_alloc (â— (Some (1%Qp, O%nat)) â‹… â—¯ (Some (1%Qp, 0%nat))))
as (γ) "[Hγ Hγ']"; first done.
- iVs (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
+ iUpd (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
{ iNext. iExists 0%nat. by iFrame. }
- iVsIntro. iApply "HΦ". rewrite /ccounter_ctx /ccounter; eauto 10.
+ iUpdIntro. iApply "HΦ". rewrite /ccounter_ctx /ccounter; eauto 10.
Qed.
Lemma inc_contrib_spec γ l q n (Φ : val → iProp Σ) :
@@ -129,19 +129,19 @@ Section contrib_spec.
Proof.
iIntros "(#(%&?&?) & Hγf & HΦ)". iLöb as "IH". wp_rec.
wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]" "Hclose".
- wp_load. iVs ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
- iVsIntro. wp_let. wp_op.
+ wp_load. iUpd ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
+ iUpdIntro. wp_let. wp_op.
wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]" "Hclose".
destruct (decide (c' = c)) as [->|].
- - iVs (own_update_2 with "[$Hγ $Hγf]") as "[Hγ Hγf]".
+ - iUpd (own_update_2 with "[$Hγ $Hγf]") as "[Hγ Hγf]".
{ apply auth_update, option_local_update, prod_local_update_2.
apply (nat_local_update _ _ (S c) (S n)); omega. }
- wp_cas_suc. iVs ("Hclose" with "[Hl Hγ]") as "_".
+ wp_cas_suc. iUpd ("Hclose" with "[Hl Hγ]") as "_".
{ iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
- iVsIntro. wp_if. by iApply "HΦ".
+ iUpdIntro. wp_if. by iApply "HΦ".
- wp_cas_fail; first (by intros [= ?%Nat2Z.inj]).
- iVs ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
- iVsIntro. wp_if. by iApply ("IH" with "[Hγf] HΦ").
+ iUpd ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
+ iUpdIntro. wp_if. by iApply ("IH" with "[Hγf] HΦ").
Qed.
Lemma read_contrib_spec γ l q n (Φ : val → iProp Σ) :
@@ -153,7 +153,7 @@ Section contrib_spec.
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
iDestruct (own_valid_2 with "[$Hγ $Hγf]")
as %[[? ?%nat_included]%Some_pair_included_total_2 _]%auth_valid_discrete_2.
- iVs ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
+ iUpd ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
iApply ("HΦ" with "[%]"); rewrite /ccounter; eauto 10.
Qed.
@@ -165,7 +165,7 @@ Section contrib_spec.
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
iDestruct (own_valid_2 with "[$Hγ $Hγf]") as %[Hn _]%auth_valid_discrete_2.
apply (Some_included_exclusive _) in Hn as [= ->]%leibniz_equiv; last done.
- iVs ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
+ iUpd ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
by iApply "HΦ".
Qed.
End contrib_spec.
diff --git a/heap_lang/lib/par.v b/heap_lang/lib/par.v
index 1c94a2ecf..f28d65004 100644
--- a/heap_lang/lib/par.v
+++ b/heap_lang/lib/par.v
@@ -23,7 +23,7 @@ Lemma par_spec (Ψ1 Ψ2 : val → iProp Σ) e (f1 f2 : val) (Φ : val → iProp
⊢ WP par e {{ Φ }}.
Proof.
iIntros (?) "(#Hh&Hf1&Hf2&HΦ)".
- rewrite /par. wp_value. iVsIntro. wp_let. wp_proj.
+ rewrite /par. wp_value. iUpdIntro. wp_let. wp_proj.
wp_apply (spawn_spec parN); try wp_done; try solve_ndisj; iFrame "Hf1 Hh".
iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _).
iApply wp_wand_l; iFrame "Hf2"; iIntros (v) "H2". wp_let.
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index 05a045314..b5a4c2b73 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -54,11 +54,11 @@ Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) (Φ : val → iProp Σ) :
Proof.
iIntros (<-%of_to_val ?) "(#Hh & Hf & HΦ)". rewrite /spawn /=.
wp_let. wp_alloc l as "Hl". wp_let.
- iVs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
- iVs (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".
+ iUpd (own_alloc (Excl ())) as (γ) "Hγ"; first done.
+ iUpd (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".
{ iNext. iExists NONEV. iFrame; eauto. }
wp_apply wp_fork; simpl. iSplitR "Hf".
- - iVsIntro. wp_seq. iVsIntro. iApply "HΦ". rewrite /join_handle. eauto.
+ - iUpdIntro. wp_seq. iUpdIntro. iApply "HΦ". rewrite /join_handle. eauto.
- wp_bind (f _). iApply wp_wand_l. iFrame "Hf"; iIntros (v) "Hv".
iInv N as (v') "[Hl _]" "Hclose".
wp_store. iApply "Hclose". iNext. iExists (SOMEV v). iFrame. eauto.
@@ -70,11 +70,11 @@ Proof.
rewrite /join_handle; iIntros "[[% H] Hv]". iDestruct "H" as (γ) "(#?&Hγ&#?)".
iLöb as "IH". wp_rec. wp_bind (! _)%E. iInv N as (v) "[Hl Hinv]" "Hclose".
wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
- - iVs ("Hclose" with "[Hl]"); [iNext; iExists _; iFrame; eauto|].
- iVsIntro. wp_match. iApply ("IH" with "Hγ Hv").
+ - iUpd ("Hclose" with "[Hl]"); [iNext; iExists _; iFrame; eauto|].
+ iUpdIntro. wp_match. iApply ("IH" with "Hγ Hv").
- iDestruct "Hinv" as (v') "[% [HΨ|Hγ']]"; simplify_eq/=.
- + iVs ("Hclose" with "[Hl Hγ]"); [iNext; iExists _; iFrame; eauto|].
- iVsIntro. wp_match. by iApply "Hv".
+ + iUpd ("Hclose" with "[Hl Hγ]"); [iNext; iExists _; iFrame; eauto|].
+ iUpdIntro. wp_match. by iApply "Hv".
+ iCombine "Hγ" "Hγ'" as "Hγ". iDestruct (own_valid with "Hγ") as %[].
Qed.
End proof.
diff --git a/heap_lang/lib/spin_lock.v b/heap_lang/lib/spin_lock.v
index 6eb603694..7659ea312 100644
--- a/heap_lang/lib/spin_lock.v
+++ b/heap_lang/lib/spin_lock.v
@@ -51,10 +51,10 @@ Section proof.
Proof.
iIntros (?) "(#Hh & HR & HΦ)". rewrite /newlock /=.
wp_seq. wp_alloc l as "Hl".
- iVs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
- iVs (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
+ iUpd (own_alloc (Excl ())) as (γ) "Hγ"; first done.
+ iUpd (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
{ iIntros "!>". iExists false. by iFrame. }
- iVsIntro. iApply "HΦ". iExists l. eauto.
+ iUpdIntro. iApply "HΦ". iExists l. eauto.
Qed.
Lemma try_acquire_spec γ lk R (Φ: val → iProp Σ) :
@@ -63,11 +63,11 @@ Section proof.
Proof.
iIntros "[#Hl HΦ]". iDestruct "Hl" as (l) "(% & #? & % & #?)". subst.
wp_rec. iInv N as ([]) "[Hl HR]" "Hclose".
- - wp_cas_fail. iVs ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
- iVsIntro. iDestruct "HΦ" as "[_ HΦ]". iApply "HΦ".
+ - wp_cas_fail. iUpd ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
+ iUpdIntro. iDestruct "HΦ" as "[_ HΦ]". iApply "HΦ".
- wp_cas_suc. iDestruct "HR" as "[Hγ HR]".
- iVs ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
- iVsIntro. iDestruct "HΦ" as "[HΦ _]". rewrite /locked. by iApply ("HΦ" with "Hγ HR").
+ iUpd ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
+ iUpdIntro. iDestruct "HΦ" as "[HΦ _]". rewrite /locked. by iApply ("HΦ" with "Hγ HR").
Qed.
Lemma acquire_spec γ lk R (Φ : val → iProp Σ) :
@@ -75,7 +75,7 @@ Section proof.
Proof.
iIntros "[#Hl HΦ]". iLöb as "IH". wp_rec. wp_bind (try_acquire _).
iApply try_acquire_spec. iFrame "#". iSplit.
- - iIntros "Hlked HR". wp_if. iVsIntro. iApply ("HΦ" with "Hlked HR").
+ - iIntros "Hlked HR". wp_if. iUpdIntro. iApply ("HΦ" with "Hlked HR").
- wp_if. iApply ("IH" with "HΦ").
Qed.
diff --git a/heap_lang/lib/ticket_lock.v b/heap_lang/lib/ticket_lock.v
index 2858a093d..2c2deae40 100644
--- a/heap_lang/lib/ticket_lock.v
+++ b/heap_lang/lib/ticket_lock.v
@@ -80,12 +80,12 @@ Section proof.
Proof.
iIntros (HN) "(#Hh & HR & HΦ)". rewrite /newlock /=.
wp_seq. wp_alloc lo as "Hlo". wp_alloc ln as "Hln".
- iVs (own_alloc (◠(Excl' 0%nat, ∅) ⋅ ◯ (Excl' 0%nat, ∅))) as (γ) "[Hγ Hγ']".
+ iUpd (own_alloc (◠(Excl' 0%nat, ∅) ⋅ ◯ (Excl' 0%nat, ∅))) as (γ) "[Hγ Hγ']".
{ by rewrite -auth_both_op. }
- iVs (inv_alloc _ _ (lock_inv γ lo ln R) with "[-HΦ]").
+ iUpd (inv_alloc _ _ (lock_inv γ lo ln R) with "[-HΦ]").
{ iNext. rewrite /lock_inv.
iExists 0%nat, 0%nat. iFrame. iLeft. by iFrame. }
- iVsIntro. iApply ("HΦ" $! (#lo, #ln)%V γ). iExists lo, ln. eauto.
+ iUpdIntro. iApply ("HΦ" $! (#lo, #ln)%V γ). iExists lo, ln. eauto.
Qed.
Lemma wait_loop_spec γ lk x R (Φ : val → iProp Σ) :
@@ -96,16 +96,16 @@ Section proof.
iInv N as (o n) "(Hlo & Hln & Ha)" "Hclose".
wp_load. destruct (decide (x = o)) as [->|Hneq].
- iDestruct "Ha" as "[Hainv [[Ho HR] | Haown]]".
- + iVs ("Hclose" with "[Hlo Hln Hainv Ht]") as "_".
+ + iUpd ("Hclose" with "[Hlo Hln Hainv Ht]") as "_".
{ iNext. iExists o, n. iFrame. eauto. }
- iVsIntro. wp_let. wp_op=>[_|[]] //.
- wp_if. iVsIntro.
+ iUpdIntro. wp_let. wp_op=>[_|[]] //.
+ wp_if. iUpdIntro.
iApply ("HΦ" with "[-HR] HR"). rewrite /locked; eauto.
+ iDestruct (own_valid_2 with "[$Ht $Haown]") as % [_ ?%gset_disj_valid_op].
set_solver.
- - iVs ("Hclose" with "[Hlo Hln Ha]").
+ - iUpd ("Hclose" with "[Hlo Hln Ha]").
{ iNext. iExists o, n. by iFrame. }
- iVsIntro. wp_let. wp_op=>[[/Nat2Z.inj //]|?].
+ iUpdIntro. wp_let. wp_op=>[[/Nat2Z.inj //]|?].
wp_if. iApply ("IH" with "Ht"). by iExact "HΦ".
Qed.
@@ -115,28 +115,28 @@ Section proof.
iIntros "[Hl HΦ]". iDestruct "Hl" as (lo ln) "(% & #? & % & #?)".
iLöb as "IH". wp_rec. wp_bind (! _)%E. subst. wp_proj.
iInv N as (o n) "[Hlo [Hln Ha]]" "Hclose".
- wp_load. iVs ("Hclose" with "[Hlo Hln Ha]") as "_".
+ wp_load. iUpd ("Hclose" with "[Hlo Hln Ha]") as "_".
{ iNext. iExists o, n. by iFrame. }
- iVsIntro. wp_let. wp_proj. wp_op.
+ iUpdIntro. wp_let. wp_proj. wp_op.
wp_bind (CAS _ _ _).
iInv N as (o' n') "(>Hlo' & >Hln' & >Hauth & Haown)" "Hclose".
destruct (decide (#n' = #n))%V as [[= ->%Nat2Z.inj] | Hneq].
- wp_cas_suc.
- iVs (own_update with "Hauth") as "[Hauth Hofull]".
+ iUpd (own_update with "Hauth") as "[Hauth Hofull]".
{ eapply auth_update_alloc, prod_local_update_2.
eapply (gset_disj_alloc_empty_local_update _ {[ n ]}).
apply (seq_set_S_disjoint 0). }
rewrite -(seq_set_S_union_L 0).
- iVs ("Hclose" with "[Hlo' Hln' Haown Hauth]") as "_".
+ iUpd ("Hclose" with "[Hlo' Hln' Haown Hauth]") as "_".
{ iNext. iExists o', (S n).
rewrite Nat2Z.inj_succ -Z.add_1_r. by iFrame. }
- iVsIntro. wp_if.
+ iUpdIntro. wp_if.
iApply (wait_loop_spec γ (#lo, #ln)).
iFrame "HΦ". rewrite /issued; eauto 10.
- wp_cas_fail.
- iVs ("Hclose" with "[Hlo' Hln' Hauth Haown]") as "_".
+ iUpd ("Hclose" with "[Hlo' Hln' Hauth Haown]") as "_".
{ iNext. iExists o', n'. by iFrame. }
- iVsIntro. wp_if. by iApply "IH".
+ iUpdIntro. wp_if. by iApply "IH".
Qed.
Lemma release_spec γ lk R (Φ : val → iProp Σ):
@@ -150,19 +150,19 @@ Section proof.
wp_load.
iDestruct (own_valid_2 with "[$Hauth $Hγo]") as
%[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2.
- iVs ("Hclose" with "[Hlo Hln Hauth Haown]") as "_".
+ iUpd ("Hclose" with "[Hlo Hln Hauth Haown]") as "_".
{ iNext. iExists o, n. by iFrame. }
- iVsIntro. wp_op.
+ iUpdIntro. wp_op.
iInv N as (o' n') "(>Hlo & >Hln & >Hauth & Haown)" "Hclose".
wp_store.
iDestruct (own_valid_2 with "[$Hauth $Hγo]") as
%[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2.
iDestruct "Haown" as "[[Hγo' _]|?]".
{ iDestruct (own_valid_2 with "[$Hγo $Hγo']") as %[[] ?]. }
- iVs (own_update_2 with "[$Hauth $Hγo]") as "[Hauth Hγo]".
+ iUpd (own_update_2 with "[$Hauth $Hγo]") as "[Hauth Hγo]".
{ apply auth_update, prod_local_update_1.
by apply option_local_update, (exclusive_local_update _ (Excl (S o))). }
- iVs ("Hclose" with "[Hlo Hln Hauth Haown Hγo HR]") as "_"; last auto.
+ iUpd ("Hclose" with "[Hlo Hln Hauth Haown Hγo HR]") as "_"; last auto.
iNext. iExists (S o), n'.
rewrite Nat2Z.inj_succ -Z.add_1_r. iFrame. iLeft. by iFrame.
Qed.
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 7767e5ecf..a2d7729d8 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -98,7 +98,7 @@ Lemma wp_fork E e Φ :
▷ (|={E}=> Φ (LitV LitUnit)) ★ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}.
Proof.
rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) [e]) //=; eauto.
- - by rewrite later_sep -(wp_value_pvs _ _ (Lit _)) // big_sepL_singleton.
+ - by rewrite later_sep -(wp_value_fupd _ _ (Lit _)) // big_sepL_singleton.
- intros; inv_head_step; eauto.
Qed.
@@ -119,7 +119,7 @@ Lemma wp_un_op E op e v v' Φ :
▷ (|={E}=> Φ v') ⊢ WP UnOp op e @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_pure_det_head_step' (UnOp op _) (of_val v'))
- -?wp_value_pvs'; eauto.
+ -?wp_value_fupd'; eauto.
intros; inv_head_step; eauto.
Qed.
@@ -129,7 +129,7 @@ Lemma wp_bin_op E op e1 e2 v1 v2 v' Φ :
▷ (|={E}=> Φ v') ⊢ WP BinOp op e1 e2 @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_pure_det_head_step' (BinOp op _ _) (of_val v'))
- -?wp_value_pvs'; eauto.
+ -?wp_value_fupd'; eauto.
intros; inv_head_step; eauto.
Qed.
@@ -152,7 +152,7 @@ Lemma wp_fst E e1 v1 e2 Φ :
▷ (|={E}=> Φ v1) ⊢ WP Fst (Pair e1 e2) @ E {{ Φ }}.
Proof.
intros ? [v2 ?].
- rewrite -(wp_lift_pure_det_head_step' (Fst _) e1) -?wp_value_pvs; eauto.
+ rewrite -(wp_lift_pure_det_head_step' (Fst _) e1) -?wp_value_fupd; eauto.
intros; inv_head_step; eauto.
Qed.
@@ -161,7 +161,7 @@ Lemma wp_snd E e1 e2 v2 Φ :
▷ (|={E}=> Φ v2) ⊢ WP Snd (Pair e1 e2) @ E {{ Φ }}.
Proof.
intros [v1 ?] ?.
- rewrite -(wp_lift_pure_det_head_step' (Snd _) e2) -?wp_value_pvs; eauto.
+ rewrite -(wp_lift_pure_det_head_step' (Snd _) e2) -?wp_value_fupd; eauto.
intros; inv_head_step; eauto.
Qed.
diff --git a/heap_lang/tactics.v b/heap_lang/tactics.v
index dfb46f6c6..9e585b2c9 100644
--- a/heap_lang/tactics.v
+++ b/heap_lang/tactics.v
@@ -229,7 +229,7 @@ Ltac solve_atomic :=
apply W.atomic_correct; vm_compute; exact I
end.
Hint Extern 10 (language.atomic _) => solve_atomic.
-(* For the side-condition of elim_vs_pvs_wp_atomic *)
+(* For the side-condition of elim_upd_fupd_wp_atomic *)
Hint Extern 10 (language.atomic _) => solve_atomic : typeclass_instances.
(** Substitution *)
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index c4bed5297..4f7309555 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -18,12 +18,12 @@ Ltac wp_done :=
| _ => fast_done
end.
-(* sometimes, we will have to do a final view shift, so only apply
-pvs_intro if we obtain a consecutive wp *)
-Ltac wp_strip_pvs :=
+(* sometimes, we want to keep the update modality, so only apply [fupd_intro]
+if we obtain a consecutive wp *)
+Ltac wp_strip_fupd :=
lazymatch goal with
| |- _ ⊢ |={?E}=> _ =>
- etrans; [|apply pvs_intro];
+ etrans; [|apply fupd_intro];
match goal with
| |- _ ⊢ wp E _ _ => simpl
| |- _ ⊢ |={E,_}=> _ => simpl
@@ -31,7 +31,7 @@ Ltac wp_strip_pvs :=
end
end.
-Ltac wp_value_head := etrans; [|eapply wp_value_pvs; wp_done]; lazy beta.
+Ltac wp_value_head := etrans; [|eapply wp_value_fupd; wp_done]; lazy beta.
Ltac wp_strip_later := idtac. (* a hook to be redefined later *)
@@ -48,7 +48,7 @@ Ltac wp_finish := intros_revert ltac:(
| |- _ ⊢ wp ?E (Seq _ _) ?Q =>
etrans; [|eapply wp_seq; wp_done]; wp_strip_later
| |- _ ⊢ wp ?E _ ?Q => wp_value_head
- | |- _ ⊢ |={_,_}=> _ => wp_strip_pvs
+ | |- _ ⊢ |={_,_}=> _ => wp_strip_fupd
end).
Tactic Notation "wp_value" :=
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index 96377473f..af2c649d6 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -44,10 +44,10 @@ Lemma wp_step e1 σ1 e2 σ2 efs Φ :
Proof.
rewrite {1}wp_unfold /wp_pre. iIntros (Hstep) "[(Hw & HE & Hσ) [H|[_ H]]]".
{ iDestruct "H" as (v) "[% _]". apply val_stuck in Hstep; simplify_eq. }
- rewrite pvs_eq /pvs_def.
- iVs ("H" $! σ1 with "Hσ [Hw HE]") as ">(Hw & HE & _ & H)"; first by iFrame.
- iVsIntro; iNext.
- iVs ("H" $! e2 σ2 efs with "[%] [Hw HE]")
+ rewrite fupd_eq /fupd_def.
+ iUpd ("H" $! σ1 with "Hσ [Hw HE]") as ">(Hw & HE & _ & H)"; first by iFrame.
+ iUpdIntro; iNext.
+ iUpd ("H" $! e2 σ2 efs with "[%] [Hw HE]")
as ">($ & $ & $ & $)"; try iFrame; eauto.
Qed.
@@ -75,18 +75,18 @@ Proof.
revert e1 t1 t2 σ1 σ2; simpl; induction n as [|n IH]=> e1 t1 t2 σ1 σ2 /=.
{ inversion_clear 1; iIntros "?"; eauto 10. }
iIntros (Hsteps) "H". inversion_clear Hsteps as [|?? [t1' σ1']].
- iVs (wptp_step with "H") as (e1' t1'') "[% H]"; first eauto; simplify_eq.
- iVsIntro; iNext; iVs "H" as ">?". by iApply IH.
+ iUpd (wptp_step with "H") as (e1' t1'') "[% H]"; first eauto; simplify_eq.
+ iUpdIntro; iNext; iUpd "H" as ">?". by iApply IH.
Qed.
-Instance rvs_iter_mono n : Proper ((⊢) ==> (⊢)) (Nat.iter n (λ P, |=r=> ▷ P)%I).
+Instance bupd_iter_mono n : Proper ((⊢) ==> (⊢)) (Nat.iter n (λ P, |=r=> ▷ P)%I).
Proof. intros P Q HP. induction n; simpl; do 2?f_equiv; auto. Qed.
-Lemma rvs_iter_frame_l n R Q :
+Lemma bupd_iter_frame_l n R Q :
R ★ Nat.iter n (λ P, |=r=> ▷ P) Q ⊢ Nat.iter n (λ P, |=r=> ▷ P) (R ★ Q).
Proof.
induction n as [|n IH]; simpl; [done|].
- by rewrite rvs_frame_l {1}(later_intro R) -later_sep IH.
+ by rewrite bupd_frame_l {1}(later_intro R) -later_sep IH.
Qed.
Lemma wptp_result n e1 t1 v2 t2 σ1 σ2 φ :
@@ -95,10 +95,10 @@ Lemma wptp_result n e1 t1 v2 t2 σ1 σ2 φ :
Nat.iter (S (S n)) (λ P, |=r=> ▷ P) (■φ v2).
Proof.
intros. rewrite wptp_steps //.
- rewrite (Nat_iter_S_r (S n)). apply rvs_iter_mono.
+ rewrite (Nat_iter_S_r (S n)). apply bupd_iter_mono.
iDestruct 1 as (e2 t2') "(% & (Hw & HE & _) & H & _)"; simplify_eq.
- iDestruct (wp_value_inv with "H") as "H". rewrite pvs_eq /pvs_def.
- iVs ("H" with "[Hw HE]") as ">(_ & _ & $)"; iFrame; auto.
+ iDestruct (wp_value_inv with "H") as "H". rewrite fupd_eq /fupd_def.
+ iUpd ("H" with "[Hw HE]") as ">(_ & _ & $)"; iFrame; auto.
Qed.
Lemma wp_safe e σ Φ :
@@ -106,7 +106,7 @@ Lemma wp_safe e σ Φ :
Proof.
rewrite wp_unfold /wp_pre. iIntros "[(Hw&HE&Hσ) [H|[_ H]]]".
{ iDestruct "H" as (v) "[% _]"; eauto 10. }
- rewrite pvs_eq. iVs ("H" with "* Hσ [-]") as ">(?&?&%&?)"; first by iFrame.
+ rewrite fupd_eq. iUpd ("H" with "* Hσ [-]") as ">(?&?&%&?)"; first by iFrame.
eauto 10.
Qed.
@@ -115,7 +115,7 @@ Lemma wptp_safe n e1 e2 t1 t2 σ1 σ2 Φ :
world σ1 ★ WP e1 {{ Φ }} ★ wptp t1 ⊢
Nat.iter (S (S n)) (λ P, |=r=> ▷ P) (■(is_Some (to_val e2) ∨ reducible e2 σ2)).
Proof.
- intros ? He2. rewrite wptp_steps //; rewrite (Nat_iter_S_r (S n)). apply rvs_iter_mono.
+ intros ? He2. rewrite wptp_steps //; rewrite (Nat_iter_S_r (S n)). apply bupd_iter_mono.
iDestruct 1 as (e2' t2') "(% & Hw & H & Htp)"; simplify_eq.
apply elem_of_cons in He2 as [<-|?]; first (iApply wp_safe; by iFrame "Hw H").
iApply wp_safe. iFrame "Hw". by iApply (big_sepL_elem_of with "Htp").
@@ -128,11 +128,11 @@ Lemma wptp_invariance n e1 e2 t1 t2 σ1 σ2 I φ Φ :
Nat.iter (S (S n)) (λ P, |=r=> ▷ P) (■φ σ2).
Proof.
intros ? HI. rewrite wptp_steps //.
- rewrite (Nat_iter_S_r (S n)) rvs_iter_frame_l. apply rvs_iter_mono.
+ rewrite (Nat_iter_S_r (S n)) bupd_iter_frame_l. apply bupd_iter_mono.
iIntros "[HI H]".
iDestruct "H" as (e2' t2') "(% & (Hw&HE&Hσ) & _)"; subst.
- rewrite pvs_eq in HI;
- iVs (HI with "HI [Hw HE]") as "> (_ & _ & H)"; first by iFrame.
+ rewrite fupd_eq in HI;
+ iUpd (HI with "HI [Hw HE]") as "> (_ & _ & H)"; first by iFrame.
iDestruct "H" as (σ2') "[Hσf %]".
iDestruct (ownP_agree σ2 σ2' with "[-]") as %<-. by iFrame. eauto.
Qed.
@@ -145,13 +145,13 @@ Proof.
intros Hwp; split.
- intros t2 σ2 v2 [n ?]%rtc_nsteps.
eapply (adequacy (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
- rewrite Nat_iter_S. iVs (iris_alloc σ) as (?) "(?&?&?&Hσ)".
- iVsIntro. iNext. iApply wptp_result; eauto.
+ rewrite Nat_iter_S. iUpd (iris_alloc σ) as (?) "(?&?&?&Hσ)".
+ iUpdIntro. iNext. iApply wptp_result; eauto.
iFrame. iSplitL. by iApply Hwp. by iApply big_sepL_nil.
- intros t2 σ2 e2 [n ?]%rtc_nsteps ?.
eapply (adequacy (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
- rewrite Nat_iter_S. iVs (iris_alloc σ) as (?) "(Hw & HE & Hσ & Hσf)".
- iVsIntro. iNext. iApply wptp_safe; eauto.
+ rewrite Nat_iter_S. iUpd (iris_alloc σ) as (?) "(Hw & HE & Hσ & Hσf)".
+ iUpdIntro. iNext. iApply wptp_safe; eauto.
iFrame "Hw HE Hσ". iSplitL. by iApply Hwp. by iApply big_sepL_nil.
Qed.
@@ -163,8 +163,8 @@ Theorem wp_invariance Σ `{irisPreG Λ Σ} e σ1 t2 σ2 I φ Φ :
Proof.
intros Hwp HI [n ?]%rtc_nsteps.
eapply (adequacy (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
- rewrite Nat_iter_S. iVs (iris_alloc σ1) as (?) "(Hw & HE & ? & Hσ)".
- rewrite pvs_eq in Hwp.
- iVs (Hwp _ with "Hσ [Hw HE]") as ">(? & ? & ? & ?)"; first by iFrame.
- iVsIntro. iNext. iApply wptp_invariance; eauto. iFrame. by iApply big_sepL_nil.
+ rewrite Nat_iter_S. iUpd (iris_alloc σ1) as (?) "(Hw & HE & ? & Hσ)".
+ rewrite fupd_eq in Hwp.
+ iUpd (Hwp _ with "Hσ [Hw HE]") as ">(? & ? & ? & ?)"; first by iFrame.
+ iUpdIntro. iNext. iApply wptp_invariance; eauto. iFrame. by iApply big_sepL_nil.
Qed.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 81217798b..689b32079 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -94,9 +94,9 @@ Section auth.
✓ (f t) → ▷ φ t ={E}=> ∃ γ, ■(γ ∉ G) ∧ auth_ctx γ N f φ ∧ auth_own γ (f t).
Proof.
iIntros (?) "Hφ". rewrite /auth_own /auth_ctx.
- iVs (own_alloc_strong (Auth (Excl' (f t)) (f t)) G) as (γ) "[% Hγ]"; first done.
+ iUpd (own_alloc_strong (Auth (Excl' (f t)) (f t)) G) as (γ) "[% Hγ]"; first done.
iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']".
- iVs (inv_alloc N _ (auth_inv γ f φ) with "[-Hγ']") as "#?".
+ iUpd (inv_alloc N _ (auth_inv γ f φ) with "[-Hγ']") as "#?".
{ iNext. rewrite /auth_inv. iExists t. by iFrame. }
eauto.
Qed.
@@ -105,7 +105,7 @@ Section auth.
✓ (f t) → ▷ φ t ={E}=> ∃ γ, auth_ctx γ N f φ ∧ auth_own γ (f t).
Proof.
iIntros (?) "Hφ".
- iVs (auth_alloc_strong N E t ∅ with "Hφ") as (γ) "[_ ?]"; eauto.
+ iUpd (auth_alloc_strong N E t ∅ with "Hφ") as (γ) "[_ ?]"; eauto.
Qed.
Lemma auth_empty γ : True =r=> auth_own γ ∅.
@@ -118,12 +118,12 @@ Section auth.
Proof.
iIntros "(Hinv & Hγf)". rewrite /auth_inv /auth_own.
iDestruct "Hinv" as (t) "[>Hγa Hφ]".
- iVsIntro. iExists t.
+ iUpdIntro. iExists t.
iDestruct (own_valid_2 with "[$Hγa $Hγf]") as % [? ?]%auth_valid_discrete_2.
iSplit; first done. iFrame. iIntros (u b) "[% Hφ]".
- iVs (own_update_2 with "[$Hγa $Hγf]") as "[Hγa Hγf]".
+ iUpd (own_update_2 with "[$Hγa $Hγf]") as "[Hγa Hγf]".
{ eapply auth_update; eassumption. }
- iVsIntro. iFrame. iExists u. iFrame.
+ iUpdIntro. iFrame. iExists u. iFrame.
Qed.
Lemma auth_open E N γ a :
@@ -139,9 +139,9 @@ Section auth.
to unpack and repack various proofs.
TODO: Make this mostly automatic, by supporting "opening accessors
around accessors". *)
- iVs (auth_acc with "[$Hinv $Hγf]") as (t) "(?&?&HclAuth)".
- iVsIntro. iExists t. iFrame. iIntros (u b) "H".
- iVs ("HclAuth" $! u b with "H") as "(Hinv & ?)". by iVs ("Hclose" with "Hinv").
+ iUpd (auth_acc with "[$Hinv $Hγf]") as (t) "(?&?&HclAuth)".
+ iUpdIntro. iExists t. iFrame. iIntros (u b) "H".
+ iUpd ("HclAuth" $! u b with "H") as "(Hinv & ?)". by iUpd ("Hclose" with "Hinv").
Qed.
End auth.
diff --git a/program_logic/boxes.v b/program_logic/boxes.v
index 57c21b865..eedb29709 100644
--- a/program_logic/boxes.v
+++ b/program_logic/boxes.v
@@ -90,14 +90,14 @@ Lemma box_insert f P Q :
slice N γ Q ★ ▷ box N (<[γ:=false]> f) (Q ★ P).
Proof.
iDestruct 1 as (Φ) "[#HeqP Hf]".
- iVs (own_alloc_strong (â— Excl' false â‹… â—¯ Excl' false,
+ iUpd (own_alloc_strong (â— Excl' false â‹… â—¯ Excl' false,
Some (to_agree (Next (iProp_unfold Q)))) (dom _ f))
as (γ) "[Hdom Hγ]"; first done.
rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]".
iDestruct "Hdom" as % ?%not_elem_of_dom.
- iVs (inv_alloc N _ (slice_inv γ Q) with "[Hγ]") as "#Hinv".
+ iUpd (inv_alloc N _ (slice_inv γ Q) with "[Hγ]") as "#Hinv".
{ iNext. iExists false; eauto. }
- iVsIntro; iExists γ; repeat iSplit; auto.
+ iUpdIntro; iExists γ; repeat iSplit; auto.
iNext. iExists (<[γ:=Q]> Φ); iSplit.
- iNext. iRewrite "HeqP". by rewrite big_sepM_fn_insert'.
- rewrite (big_sepM_fn_insert (λ _ _ P', _ ★ _ _ P' ★ _ _ (_ _ P')))%I //.
@@ -112,7 +112,7 @@ Proof.
iIntros (?) "[#Hinv H]"; iDestruct "H" as (Φ) "[#HeqP Hf]".
iExists ([★ map] γ'↦_ ∈ delete γ f, Φ γ')%I.
iInv N as (b) "(Hγ & #HγQ &_)" "Hclose".
- iApply pvs_trans_frame; iFrame "Hclose"; iVsIntro; iNext.
+ iApply fupd_trans_frame; iFrame "Hclose"; iUpdIntro; iNext.
iDestruct (big_sepM_delete _ f _ false with "Hf")
as "[[Hγ' #[HγΦ ?]] ?]"; first done.
iDestruct (box_own_agree γ Q (Φ γ) with "[#]") as "HeqQ"; first by eauto.
@@ -132,10 +132,10 @@ Proof.
iDestruct (big_sepM_later _ f with "Hf") as "Hf".
iDestruct (big_sepM_delete _ f _ false with "Hf")
as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
- iVs (box_own_auth_update γ b' false true with "[Hγ Hγ']")
+ iUpd (box_own_auth_update γ b' false true with "[Hγ Hγ']")
as "[Hγ Hγ']"; first by iFrame.
- iVs ("Hclose" with "[Hγ HQ]"); first (iNext; iExists true; by iFrame).
- iVsIntro; iNext; iExists Φ; iSplit.
+ iUpd ("Hclose" with "[Hγ HQ]"); first (iNext; iExists true; by iFrame).
+ iUpdIntro; iNext; iExists Φ; iSplit.
- by rewrite big_sepM_insert_override.
- rewrite -insert_delete big_sepM_insert ?lookup_delete //.
iFrame; eauto.
@@ -152,9 +152,9 @@ Proof.
as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
iFrame "HQ".
- iVs (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ Hγ']"; first by iFrame.
- iVs ("Hclose" with "[Hγ]"); first (iNext; iExists false; by repeat iSplit).
- iVsIntro; iNext; iExists Φ; iSplit.
+ iUpd (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ Hγ']"; first by iFrame.
+ iUpd ("Hclose" with "[Hγ]"); first (iNext; iExists false; by repeat iSplit).
+ iUpdIntro; iNext; iExists Φ; iSplit.
- by rewrite big_sepM_insert_override.
- rewrite -insert_delete big_sepM_insert ?lookup_delete //.
iFrame; eauto.
@@ -166,11 +166,11 @@ Proof.
iExists Φ; iSplitR; first by rewrite big_sepM_fmap.
rewrite eq_iff later_iff big_sepM_later; iDestruct ("HeqP" with "HP") as "HP".
iCombine "Hf" "HP" as "Hf".
- rewrite big_sepM_fmap; iApply (pvs_big_sepM _ _ f).
+ rewrite big_sepM_fmap; iApply (fupd_big_sepM _ _ f).
iApply (big_sepM_impl _ _ f); iFrame "Hf".
iAlways; iIntros (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
iInv N as (b) "[>Hγ _]" "Hclose".
- iVs (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ $]"; first by iFrame.
+ iUpd (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ $]"; first by iFrame.
iApply "Hclose". iNext; iExists true. by iFrame.
Qed.
@@ -181,16 +181,16 @@ Proof.
iDestruct 1 as (Φ) "[#HeqP Hf]".
iAssert ([★ map] γ↦b ∈ f, ▷ Φ γ ★ box_own_auth γ (◯ Excl' false) ★
box_own_prop γ (Φ γ) ★ inv N (slice_inv γ (Φ γ)))%I with "==>[Hf]" as "[HΦ ?]".
- { iApply (pvs_big_sepM _ _ f); iApply (big_sepM_impl _ _ f); iFrame "Hf".
+ { iApply (fupd_big_sepM _ _ f); iApply (big_sepM_impl _ _ f); iFrame "Hf".
iAlways; iIntros (γ b ?) "(Hγ' & #$ & #$)".
assert (true = b) as <- by eauto.
iInv N as (b) "(>Hγ & _ & HΦ)" "Hclose".
iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
- iVs (box_own_auth_update γ true true false with "[Hγ Hγ']")
+ iUpd (box_own_auth_update γ true true false with "[Hγ Hγ']")
as "[Hγ $]"; first by iFrame.
- iVs ("Hclose" with "[Hγ]"); first (iNext; iExists false; iFrame; eauto).
+ iUpd ("Hclose" with "[Hγ]"); first (iNext; iExists false; iFrame; eauto).
by iApply "HΦ". }
- iVsIntro; iSplitL "HΦ".
+ iUpdIntro; iSplitL "HΦ".
- rewrite eq_iff later_iff big_sepM_later. by iApply "HeqP".
- iExists Φ; iSplit; by rewrite big_sepM_fmap.
Qed.
diff --git a/program_logic/cancelable_invariants.v b/program_logic/cancelable_invariants.v
index 486f22b64..8e526d1ea 100644
--- a/program_logic/cancelable_invariants.v
+++ b/program_logic/cancelable_invariants.v
@@ -47,8 +47,8 @@ Section proofs.
Lemma cinv_alloc E N P : ▷ P ={E}=> ∃ γ, cinv N γ P ★ cinv_own γ 1.
Proof.
rewrite /cinv /cinv_own. iIntros "HP".
- iVs (own_alloc 1%Qp) as (γ) "H1"; first done.
- iVs (inv_alloc N _ (P ∨ own γ 1%Qp)%I with "[HP]"); eauto.
+ iUpd (own_alloc 1%Qp) as (γ) "H1"; first done.
+ iUpd (inv_alloc N _ (P ∨ own γ 1%Qp)%I with "[HP]"); eauto.
Qed.
Lemma cinv_cancel E N γ P :
diff --git a/program_logic/counter_examples.v b/program_logic/counter_examples.v
index fe673a206..3090c8153 100644
--- a/program_logic/counter_examples.v
+++ b/program_logic/counter_examples.v
@@ -9,7 +9,7 @@ Module savedprop. Section savedprop.
Notation "¬ P" := (□ (P → False))%I : uPred_scope.
Implicit Types P : iProp.
- (* Saved Propositions and view shifts. *)
+ (** Saved Propositions and the update modality *)
Context (sprop : Type) (saved : sprop → iProp → iProp).
Hypothesis sprop_persistent : ∀ i P, PersistentP (saved i P).
Hypothesis sprop_alloc_dep :
@@ -40,9 +40,9 @@ Module savedprop. Section savedprop.
Lemma contradiction : False.
Proof.
apply (@uPred.adequacy M False 1); simpl.
- iIntros "". iVs A_alloc as (i) "#H".
+ iIntros "". iUpd A_alloc as (i) "#H".
iPoseProof (saved_NA with "H") as "HN".
- iVsIntro. iNext.
+ iUpdIntro. iNext.
iApply "HN". iApply saved_A. done.
Qed.
@@ -56,22 +56,22 @@ Module inv. Section inv.
Implicit Types P : iProp.
(** Assumptions *)
- (* We have view shifts (two classes: empty/full mask) *)
+ (** We have the update modality (two classes: empty/full mask) *)
Inductive mask := M0 | M1.
- Context (pvs : mask → iProp → iProp).
+ Context (fupd : mask → iProp → iProp).
- Hypothesis pvs_intro : ∀ E P, P ⊢ pvs E P.
- Hypothesis pvs_mono : ∀ E P Q, (P ⊢ Q) → pvs E P ⊢ pvs E Q.
- Hypothesis pvs_pvs : ∀ E P, pvs E (pvs E P) ⊢ pvs E P.
- Hypothesis pvs_frame_l : ∀ E P Q, P ★ pvs E Q ⊢ pvs E (P ★ Q).
- Hypothesis pvs_mask_mono : ∀ P, pvs M0 P ⊢ pvs M1 P.
+ Hypothesis fupd_intro : ∀ E P, P ⊢ fupd E P.
+ Hypothesis fupd_mono : ∀ E P Q, (P ⊢ Q) → fupd E P ⊢ fupd E Q.
+ Hypothesis fupd_fupd : ∀ E P, fupd E (fupd E P) ⊢ fupd E P.
+ Hypothesis fupd_frame_l : ∀ E P Q, P ★ fupd E Q ⊢ fupd E (P ★ Q).
+ Hypothesis fupd_mask_mono : ∀ P, fupd M0 P ⊢ fupd M1 P.
- (* We have invariants *)
+ (** We have invariants *)
Context (name : Type) (inv : name → iProp → iProp).
Hypothesis inv_persistent : ∀ i P, PersistentP (inv i P).
- Hypothesis inv_alloc : ∀ P, P ⊢ pvs M1 (∃ i, inv i P).
+ Hypothesis inv_alloc : ∀ P, P ⊢ fupd M1 (∃ i, inv i P).
Hypothesis inv_open :
- ∀ i P Q R, (P ★ Q ⊢ pvs M0 (P ★ R)) → (inv i P ★ Q ⊢ pvs M1 R).
+ ∀ i P Q R, (P ★ Q ⊢ fupd M0 (P ★ R)) → (inv i P ★ Q ⊢ fupd M1 R).
(* We have tokens for a little "two-state STS": [start] -> [finish].
state. [start] also asserts the exact state; it is only ever owned by the
@@ -85,47 +85,47 @@ Module inv. Section inv.
Context (gname : Type).
Context (start finished : gname → iProp).
- Hypothesis sts_alloc : True ⊢ pvs M0 (∃ γ, start γ).
- Hypotheses start_finish : ∀ γ, start γ ⊢ pvs M0 (finished γ).
+ Hypothesis sts_alloc : True ⊢ fupd M0 (∃ γ, start γ).
+ Hypotheses start_finish : ∀ γ, start γ ⊢ fupd M0 (finished γ).
Hypothesis finished_not_start : ∀ γ, start γ ★ finished γ ⊢ False.
Hypothesis finished_dup : ∀ γ, finished γ ⊢ finished γ ★ finished γ.
- (* We assume that we cannot view shift to false. *)
- Hypothesis consistency : ¬ (True ⊢ pvs M1 False).
+ (** We assume that we cannot update to false. *)
+ Hypothesis consistency : ¬ (True ⊢ fupd M1 False).
(** Some general lemmas and proof mode compatibility. *)
- Lemma inv_open' i P R : inv i P ★ (P -★ pvs M0 (P ★ pvs M1 R)) ⊢ pvs M1 R.
+ Lemma inv_open' i P R : inv i P ★ (P -★ fupd M0 (P ★ fupd M1 R)) ⊢ fupd M1 R.
Proof.
- iIntros "(#HiP & HP)". iApply pvs_pvs. iApply inv_open; last first.
+ iIntros "(#HiP & HP)". iApply fupd_fupd. iApply inv_open; last first.
{ iSplit; first done. iExact "HP". }
iIntros "(HP & HPw)". by iApply "HPw".
Qed.
- Instance pvs_mono' E : Proper ((⊢) ==> (⊢)) (pvs E).
- Proof. intros P Q ?. by apply pvs_mono. Qed.
- Instance pvs_proper E : Proper ((⊣⊢) ==> (⊣⊢)) (pvs E).
+ Instance fupd_mono' E : Proper ((⊢) ==> (⊢)) (fupd E).
+ Proof. intros P Q ?. by apply fupd_mono. Qed.
+ Instance fupd_proper E : Proper ((⊣⊢) ==> (⊣⊢)) (fupd E).
Proof.
- intros P Q; rewrite !uPred.equiv_spec=> -[??]; split; by apply pvs_mono.
+ intros P Q; rewrite !uPred.equiv_spec=> -[??]; split; by apply fupd_mono.
Qed.
- Lemma pvs_frame_r E P Q : (pvs E P ★ Q) ⊢ pvs E (P ★ Q).
- Proof. by rewrite comm pvs_frame_l comm. Qed.
+ Lemma fupd_frame_r E P Q : (fupd E P ★ Q) ⊢ fupd E (P ★ Q).
+ Proof. by rewrite comm fupd_frame_l comm. Qed.
- Global Instance elim_pvs_pvs E P Q : ElimVs (pvs E P) P (pvs E Q) (pvs E Q).
- Proof. by rewrite /ElimVs pvs_frame_r uPred.wand_elim_r pvs_pvs. Qed.
+ Global Instance elim_fupd_fupd E P Q : ElimUpd (fupd E P) P (fupd E Q) (fupd E Q).
+ Proof. by rewrite /ElimUpd fupd_frame_r uPred.wand_elim_r fupd_fupd. Qed.
- Global Instance elim_pvs0_pvs1 P Q : ElimVs (pvs M0 P) P (pvs M1 Q) (pvs M1 Q).
+ Global Instance elim_fupd0_fupd1 P Q : ElimUpd (fupd M0 P) P (fupd M1 Q) (fupd M1 Q).
Proof.
- by rewrite /ElimVs pvs_frame_r uPred.wand_elim_r pvs_mask_mono pvs_pvs.
+ by rewrite /ElimUpd fupd_frame_r uPred.wand_elim_r fupd_mask_mono fupd_fupd.
Qed.
- Global Instance exists_split_pvs0 {A} E P (Φ : A → iProp) :
- FromExist P Φ → FromExist (pvs E P) (λ a, pvs E (Φ a)).
+ Global Instance exists_split_fupd0 {A} E P (Φ : A → iProp) :
+ FromExist P Φ → FromExist (fupd E P) (λ a, fupd E (Φ a)).
Proof.
rewrite /FromExist=>HP. apply uPred.exist_elim=> a.
- apply pvs_mono. by rewrite -HP -(uPred.exist_intro a).
+ apply fupd_mono. by rewrite -HP -(uPred.exist_intro a).
Qed.
(** Now to the actual counterexample. We start with a weird form of saved propositions. *)
@@ -133,47 +133,47 @@ Module inv. Section inv.
∃ i, inv i (start γ ∨ (finished γ ★ □ P)).
Global Instance saved_persistent γ P : PersistentP (saved γ P) := _.
- Lemma saved_alloc (P : gname → iProp) : True ⊢ pvs M1 (∃ γ, saved γ (P γ)).
+ Lemma saved_alloc (P : gname → iProp) : True ⊢ fupd M1 (∃ γ, saved γ (P γ)).
Proof.
- iIntros "". iVs (sts_alloc) as (γ) "Hs".
- iVs (inv_alloc (start γ ∨ (finished γ ★ □ (P γ))) with "[Hs]") as (i) "#Hi".
+ iIntros "". iUpd (sts_alloc) as (γ) "Hs".
+ iUpd (inv_alloc (start γ ∨ (finished γ ★ □ (P γ))) with "[Hs]") as (i) "#Hi".
{ auto. }
- iApply pvs_intro. by iExists γ, i.
+ iApply fupd_intro. by iExists γ, i.
Qed.
- Lemma saved_cast γ P Q : saved γ P ★ saved γ Q ★ □ P ⊢ pvs M1 (□ Q).
+ Lemma saved_cast γ P Q : saved γ P ★ saved γ Q ★ □ P ⊢ fupd M1 (□ Q).
Proof.
iIntros "(#HsP & #HsQ & #HP)". iDestruct "HsP" as (i) "HiP".
iApply (inv_open' i). iSplit; first done.
- iIntros "HaP". iAssert (pvs M0 (finished γ)) with "[HaP]" as "==> Hf".
+ iIntros "HaP". iAssert (fupd M0 (finished γ)) with "[HaP]" as "==> Hf".
{ iDestruct "HaP" as "[Hs | [Hf _]]".
- by iApply start_finish.
- - by iApply pvs_intro. }
+ - by iApply fupd_intro. }
iDestruct (finished_dup with "Hf") as "[Hf Hf']".
- iApply pvs_intro. iSplitL "Hf'"; first by eauto.
+ iApply fupd_intro. iSplitL "Hf'"; first by eauto.
(* Step 2: Open the Q-invariant. *)
iClear (i) "HiP ". iDestruct "HsQ" as (i) "HiQ".
iApply (inv_open' i). iSplit; first done.
iIntros "[HaQ | [_ #HQ]]".
{ iExFalso. iApply finished_not_start. by iFrame. }
- iApply pvs_intro. iSplitL "Hf".
+ iApply fupd_intro. iSplitL "Hf".
{ iRight. by iFrame. }
- by iApply pvs_intro.
+ by iApply fupd_intro.
Qed.
(** And now we tie a bad knot. *)
- Notation "¬ P" := (□ (P -★ pvs M1 False))%I : uPred_scope.
+ Notation "¬ P" := (□ (P -★ fupd M1 False))%I : uPred_scope.
Definition A i : iProp := ∃ P, ¬P ★ saved i P.
Global Instance A_persistent i : PersistentP (A i) := _.
- Lemma A_alloc : True ⊢ pvs M1 (∃ i, saved i (A i)).
+ Lemma A_alloc : True ⊢ fupd M1 (∃ i, saved i (A i)).
Proof. by apply saved_alloc. Qed.
Lemma saved_NA i : saved i (A i) ⊢ ¬A i.
Proof.
iIntros "#Hi !# #HA". iPoseProof "HA" as "HA'".
iDestruct "HA'" as (P) "#[HNP Hi']".
- iVs (saved_cast i (A i) P with "[]") as "HP".
+ iUpd (saved_cast i (A i) P with "[]") as "HP".
{ eauto. }
by iApply "HNP".
Qed.
@@ -187,7 +187,7 @@ Module inv. Section inv.
Lemma contradiction : False.
Proof.
apply consistency. iIntros "".
- iVs A_alloc as (i) "#H".
+ iUpd A_alloc as (i) "#H".
iPoseProof (saved_NA with "H") as "HN".
iApply "HN". iApply saved_A. done.
Qed.
diff --git a/program_logic/ectx_lifting.v b/program_logic/ectx_lifting.v
index f0361cfa4..4349b35b9 100644
--- a/program_logic/ectx_lifting.v
+++ b/program_logic/ectx_lifting.v
@@ -23,7 +23,7 @@ Lemma wp_lift_head_step E Φ e1 :
⊢ WP e1 @ E {{ Φ }}.
Proof.
iIntros "H". iApply (wp_lift_step E); try done.
- iVs "H" as (σ1) "(%&Hσ1&Hwp)". iVsIntro. iExists σ1.
+ iUpd "H" as (σ1) "(%&Hσ1&Hwp)". iUpdIntro. iExists σ1.
iSplit; first by eauto. iFrame. iNext. iIntros (e2 σ2 efs) "[% ?]".
iApply "Hwp". by eauto.
Qed.
diff --git a/program_logic/fancy_updates.v b/program_logic/fancy_updates.v
new file mode 100644
index 000000000..874fcb5d4
--- /dev/null
+++ b/program_logic/fancy_updates.v
@@ -0,0 +1,197 @@
+From iris.program_logic Require Export iris.
+From iris.program_logic Require Import wsat.
+From iris.algebra Require Import upred_big_op gmap.
+From iris.proofmode Require Import tactics classes.
+Import uPred.
+
+Program Definition fupd_def `{irisG Λ Σ}
+ (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
+ (wsat ★ ownE E1 =r=★ ◇ (wsat ★ ownE E2 ★ P))%I.
+Definition fupd_aux : { x | x = @fupd_def }. by eexists. Qed.
+Definition fupd := proj1_sig fupd_aux.
+Definition fupd_eq : @fupd = @fupd_def := proj2_sig fupd_aux.
+Arguments fupd {_ _ _} _ _ _%I.
+Instance: Params (@fupd) 5.
+
+Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q)
+ (at level 99, E1, E2 at level 50, Q at level 200,
+ format "|={ E1 , E2 }=> Q") : uPred_scope.
+Notation "P ={ E1 , E2 }=★ Q" := (P -★ |={E1,E2}=> Q)%I
+ (at level 99, E1,E2 at level 50, Q at level 200,
+ format "P ={ E1 , E2 }=★ Q") : uPred_scope.
+Notation "P ={ E1 , E2 }=> Q" := (P ⊢ |={E1,E2}=> Q)
+ (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : C_scope.
+
+Notation "|={ E }=> Q" := (fupd E E Q)
+ (at level 99, E at level 50, Q at level 200,
+ format "|={ E }=> Q") : uPred_scope.
+Notation "P ={ E }=★ Q" := (P -★ |={E}=> Q)%I
+ (at level 99, E at level 50, Q at level 200,
+ format "P ={ E }=★ Q") : uPred_scope.
+Notation "P ={ E }=> Q" := (P ⊢ |={E}=> Q)
+ (at level 99, E at level 50, Q at level 200, only parsing) : C_scope.
+
+Notation "|={ E1 , E2 }â–·=> Q" := (|={E1,E2}=> (â–· |={E2,E1}=> Q))%I
+ (at level 99, E1, E2 at level 50, Q at level 200,
+ format "|={ E1 , E2 }â–·=> Q") : uPred_scope.
+Notation "|={ E }â–·=> Q" := (|={E,E}â–·=> Q)%I
+ (at level 99, E at level 50, Q at level 200,
+ format "|={ E }â–·=> Q") : uPred_scope.
+
+Section fupd.
+Context `{irisG Λ Σ}.
+Implicit Types P Q : iProp Σ.
+
+Global Instance fupd_ne E1 E2 n : Proper (dist n ==> dist n) (@fupd Λ Σ _ E1 E2).
+Proof. rewrite fupd_eq. solve_proper. Qed.
+Global Instance fupd_proper E1 E2 : Proper ((≡) ==> (≡)) (@fupd Λ Σ _ E1 E2).
+Proof. apply ne_proper, _. Qed.
+
+Lemma fupd_intro_mask E1 E2 P : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P.
+Proof.
+ intros (E1''&->&?)%subseteq_disjoint_union_L.
+ rewrite fupd_eq /fupd_def ownE_op //. iIntros "H ($ & $ & HE) !==>".
+ iApply except_last_intro. iIntros "[$ $] !==>" . iApply except_last_intro.
+ by iFrame.
+Qed.
+
+Lemma except_last_fupd E1 E2 P : â—‡ (|={E1,E2}=> P) ={E1,E2}=> P.
+Proof.
+ rewrite fupd_eq. iIntros "H [Hw HE]". iTimeless "H". iApply "H"; by iFrame.
+Qed.
+
+Lemma bupd_fupd E P : (|=r=> P) ={E}=> P.
+Proof.
+ rewrite fupd_eq /fupd_def. iIntros "H [$ $]"; iUpd "H".
+ iUpdIntro. by iApply except_last_intro.
+Qed.
+
+Lemma fupd_mono E1 E2 P Q : (P ⊢ Q) → (|={E1,E2}=> P) ={E1,E2}=> Q.
+Proof.
+ rewrite fupd_eq /fupd_def. iIntros (HPQ) "HP HwE".
+ rewrite -HPQ. by iApply "HP".
+Qed.
+
+Lemma fupd_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) ={E1,E3}=> P.
+Proof.
+ rewrite fupd_eq /fupd_def. iIntros "HP HwE".
+ iUpd ("HP" with "HwE") as ">(Hw & HE & HP)". iApply "HP"; by iFrame.
+Qed.
+
+Lemma fupd_mask_frame_r' E1 E2 Ef P :
+ E1 ⊥ Ef → (|={E1,E2}=> E2 ⊥ Ef → P) ={E1 ∪ Ef,E2 ∪ Ef}=> P.
+Proof.
+ intros. rewrite fupd_eq /fupd_def ownE_op //. iIntros "Hvs (Hw & HE1 &HEf)".
+ iUpd ("Hvs" with "[Hw HE1]") as ">($ & HE2 & HP)"; first by iFrame.
+ iDestruct (ownE_op' with "[HE2 HEf]") as "[? $]"; first by iFrame.
+ iUpdIntro; iApply except_last_intro. by iApply "HP".
+Qed.
+
+Lemma fupd_frame_r E1 E2 P Q : (|={E1,E2}=> P) ★ Q ={E1,E2}=> P ★ Q.
+Proof. rewrite fupd_eq /fupd_def. by iIntros "[HwP $]". Qed.
+
+(** * Derived rules *)
+Global Instance fupd_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (@fupd Λ Σ _ E1 E2).
+Proof. intros P Q; apply fupd_mono. Qed.
+Global Instance fupd_flip_mono' E1 E2 :
+ Proper (flip (⊢) ==> flip (⊢)) (@fupd Λ Σ _ E1 E2).
+Proof. intros P Q; apply fupd_mono. Qed.
+
+Lemma fupd_intro E P : P ={E}=> P.
+Proof. iIntros "HP". by iApply bupd_fupd. Qed.
+Lemma fupd_intro_mask' E1 E2 : E2 ⊆ E1 → True ⊢ |={E1,E2}=> |={E2,E1}=> True.
+Proof. exact: fupd_intro_mask. Qed.
+Lemma fupd_except_last E1 E2 P : (|={E1,E2}=> â—‡ P) ={E1,E2}=> P.
+Proof. by rewrite {1}(fupd_intro E2 P) except_last_fupd fupd_trans. Qed.
+
+Lemma fupd_frame_l E1 E2 P Q : (P ★ |={E1,E2}=> Q) ={E1,E2}=> P ★ Q.
+Proof. rewrite !(comm _ P); apply fupd_frame_r. Qed.
+Lemma fupd_wand_l E1 E2 P Q : (P -★ Q) ★ (|={E1,E2}=> P) ={E1,E2}=> Q.
+Proof. by rewrite fupd_frame_l wand_elim_l. Qed.
+Lemma fupd_wand_r E1 E2 P Q : (|={E1,E2}=> P) ★ (P -★ Q) ={E1,E2}=> Q.
+Proof. by rewrite fupd_frame_r wand_elim_r. Qed.
+
+Lemma fupd_trans_frame E1 E2 E3 P Q :
+ ((Q ={E2,E3}=★ True) ★ |={E1,E2}=> (Q ★ P)) ={E1,E3}=> P.
+Proof.
+ rewrite fupd_frame_l assoc -(comm _ Q) wand_elim_r.
+ by rewrite fupd_frame_r left_id fupd_trans.
+Qed.
+
+Lemma fupd_mask_frame_r E1 E2 Ef P :
+ E1 ⊥ Ef → (|={E1,E2}=> P) ={E1 ∪ Ef,E2 ∪ Ef}=> P.
+Proof.
+ iIntros (?) "H". iApply fupd_mask_frame_r'; auto.
+ iApply fupd_wand_r; iFrame "H"; eauto.
+Qed.
+Lemma fupd_mask_mono E1 E2 P : E1 ⊆ E2 → (|={E1}=> P) ={E2}=> P.
+Proof.
+ intros (Ef&->&?)%subseteq_disjoint_union_L. by apply fupd_mask_frame_r.
+Qed.
+
+Lemma fupd_sep E P Q : (|={E}=> P) ★ (|={E}=> Q) ={E}=> P ★ Q.
+Proof. by rewrite fupd_frame_r fupd_frame_l fupd_trans. Qed.
+Lemma fupd_big_sepM `{Countable K} {A} E (Φ : K → A → iProp Σ) (m : gmap K A) :
+ ([★ map] k↦x ∈ m, |={E}=> Φ k x) ={E}=> [★ map] k↦x ∈ m, Φ k x.
+Proof.
+ apply (big_opM_forall (λ P Q, P ={E}=> Q)); auto using fupd_intro.
+ intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
+Qed.
+Lemma fupd_big_sepS `{Countable A} E (Φ : A → iProp Σ) X :
+ ([★ set] x ∈ X, |={E}=> Φ x) ={E}=> [★ set] x ∈ X, Φ x.
+Proof.
+ apply (big_opS_forall (λ P Q, P ={E}=> Q)); auto using fupd_intro.
+ intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
+Qed.
+End fupd.
+
+(** Proofmode class instances *)
+Section proofmode_classes.
+ Context `{irisG Λ Σ}.
+ Implicit Types P Q : iProp Σ.
+
+ Global Instance from_pure_fupd E P φ : FromPure P φ → FromPure (|={E}=> P) φ.
+ Proof. rewrite /FromPure. intros <-. apply fupd_intro. Qed.
+
+ Global Instance from_assumption_fupd E p P Q :
+ FromAssumption p P (|=r=> Q) → FromAssumption p P (|={E}=> Q)%I.
+ Proof. rewrite /FromAssumption=>->. apply bupd_fupd. Qed.
+
+ Global Instance into_wand_fupd E1 E2 R P Q :
+ IntoWand R P Q → IntoWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
+ Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite fupd_wand_r. Qed.
+
+ Global Instance from_sep_fupd E P Q1 Q2 :
+ FromSep P Q1 Q2 → FromSep (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
+ Proof. rewrite /FromSep=><-. apply fupd_sep. Qed.
+
+ Global Instance or_split_fupd E1 E2 P Q1 Q2 :
+ FromOr P Q1 Q2 → FromOr (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2).
+ Proof. rewrite /FromOr=><-. apply or_elim; apply fupd_mono; auto with I. Qed.
+
+ Global Instance exists_split_fupd {A} E1 E2 P (Φ : A → iProp Σ) :
+ FromExist P Φ → FromExist (|={E1,E2}=> P) (λ a, |={E1,E2}=> Φ a)%I.
+ Proof.
+ rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
+ Qed.
+
+ Global Instance frame_fupd E1 E2 R P Q :
+ Frame R P Q → Frame R (|={E1,E2}=> P) (|={E1,E2}=> Q).
+ Proof. rewrite /Frame=><-. by rewrite fupd_frame_l. Qed.
+
+ Global Instance is_except_last_fupd E1 E2 P : IsExceptLast (|={E1,E2}=> P).
+ Proof. by rewrite /IsExceptLast except_last_fupd. Qed.
+
+ Global Instance from_upd_fupd E P : FromUpd (|={E}=> P) P.
+ Proof. by rewrite /FromUpd -bupd_fupd. Qed.
+
+ Global Instance elim_upd_bupd_fupd E1 E2 P Q :
+ ElimUpd (|=r=> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q).
+ Proof. by rewrite /ElimUpd (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans. Qed.
+ Global Instance elim_upd_fupd_fupd E1 E2 E3 P Q :
+ ElimUpd (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
+ Proof. by rewrite /ElimUpd fupd_frame_r wand_elim_r fupd_trans. Qed.
+End proofmode_classes.
+
+Hint Extern 2 (coq_tactics.of_envs _ ⊢ _) =>
+ match goal with |- _ ⊢ |={_}=> _ => iUpdIntro end.
diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index dc9840967..334465548 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -89,9 +89,9 @@ Lemma own_alloc_strong a (G : gset gname) :
✓ a → True =r=> ∃ γ, ■(γ ∉ G) ∧ own γ a.
Proof.
intros Ha.
- rewrite -(rvs_mono (∃ m, ■(∃ γ, γ ∉ G ∧ m = iRes_singleton γ a) ∧ uPred_ownM m)%I).
+ rewrite -(bupd_mono (∃ m, ■(∃ γ, γ ∉ G ∧ m = iRes_singleton γ a) ∧ uPred_ownM m)%I).
- rewrite ownM_empty.
- eapply rvs_ownM_updateP, (iprod_singleton_updateP_empty (inG_id i));
+ eapply bupd_ownM_updateP, (iprod_singleton_updateP_empty (inG_id i));
first (eapply alloc_updateP_strong', cmra_transport_valid, Ha);
naive_solver.
- apply exist_elim=>m; apply pure_elim_l=>-[γ [Hfresh ->]].
@@ -100,15 +100,15 @@ Qed.
Lemma own_alloc a : ✓ a → True =r=> ∃ γ, own γ a.
Proof.
intros Ha. rewrite (own_alloc_strong a ∅) //; [].
- apply rvs_mono, exist_mono=>?. eauto with I.
+ apply bupd_mono, exist_mono=>?. eauto with I.
Qed.
(** ** Frame preserving updates *)
Lemma own_updateP P γ a : a ~~>: P → own γ a =r=> ∃ a', ■P a' ∧ own γ a'.
Proof.
intros Ha. rewrite !own_eq.
- rewrite -(rvs_mono (∃ m, ■(∃ a', m = iRes_singleton γ a' ∧ P a') ∧ uPred_ownM m)%I).
- - eapply rvs_ownM_updateP, iprod_singleton_updateP;
+ rewrite -(bupd_mono (∃ m, ■(∃ a', m = iRes_singleton γ a' ∧ P a') ∧ uPred_ownM m)%I).
+ - eapply bupd_ownM_updateP, iprod_singleton_updateP;
first by (eapply singleton_updateP', cmra_transport_updateP', Ha).
naive_solver.
- apply exist_elim=>m; apply pure_elim_l=>-[a' [-> HP]].
@@ -118,7 +118,7 @@ Qed.
Lemma own_update γ a a' : a ~~> a' → own γ a =r=> own γ a'.
Proof.
intros; rewrite (own_updateP (a' =)); last by apply cmra_update_updateP.
- by apply rvs_mono, exist_elim=> a''; apply pure_elim_l=> ->.
+ by apply bupd_mono, exist_elim=> a''; apply pure_elim_l=> ->.
Qed.
Lemma own_update_2 γ a1 a2 a' :
a1 ⋅ a2 ~~> a' → own γ a1 ★ own γ a2 =r=> own γ a'.
@@ -141,7 +141,7 @@ Arguments own_update_3 {_ _} [_] _ _ _ _ _ _.
Lemma own_empty `{inG Σ (A:ucmraT)} γ : True =r=> own γ ∅.
Proof.
rewrite ownM_empty !own_eq /own_def.
- apply rvs_ownM_update, iprod_singleton_update_empty.
+ apply bupd_ownM_update, iprod_singleton_update_empty.
apply (alloc_unit_singleton_update (cmra_transport inG_prf ∅)); last done.
- apply cmra_transport_valid, ucmra_unit_valid.
- intros x; destruct inG_prf. by rewrite left_id.
diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index 3b978b9f3..5b079dfb6 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -62,8 +62,8 @@ Lemma ht_vs E P P' Φ Φ' e :
(P ={E}=> P') ∧ {{ P' }} e @ E {{ Φ' }} ∧ (∀ v, Φ' v ={E}=> Φ v)
⊢ {{ P }} e @ E {{ Φ }}.
Proof.
- iIntros "(#Hvs & #Hwp & #HΦ) !# HP". iVs ("Hvs" with "HP") as "HP".
- iApply wp_pvs; iApply wp_wand_r; iSplitL; [by iApply "Hwp"|].
+ iIntros "(#Hvs & #Hwp & #HΦ) !# HP". iUpd ("Hvs" with "HP") as "HP".
+ iApply wp_fupd; iApply wp_wand_r; iSplitL; [by iApply "Hwp"|].
iIntros (v) "Hv". by iApply "HΦ".
Qed.
@@ -73,7 +73,7 @@ Lemma ht_atomic E1 E2 P P' Φ Φ' e :
⊢ {{ P }} e @ E1 {{ Φ }}.
Proof.
iIntros (?) "(#Hvs & #Hwp & #HΦ) !# HP". iApply (wp_atomic _ E2); auto.
- iVs ("Hvs" with "HP") as "HP". iVsIntro.
+ iUpd ("Hvs" with "HP") as "HP". iUpdIntro.
iApply wp_wand_r; iSplitL; [by iApply "Hwp"|].
iIntros (v) "Hv". by iApply "HΦ".
Qed.
diff --git a/program_logic/invariants.v b/program_logic/invariants.v
index 8fe284f24..8749825a3 100644
--- a/program_logic/invariants.v
+++ b/program_logic/invariants.v
@@ -1,4 +1,4 @@
-From iris.program_logic Require Export pviewshifts.
+From iris.program_logic Require Export fancy_updates.
From iris.program_logic Require Export namespaces.
From iris.program_logic Require Import wsat.
From iris.algebra Require Import gmap.
@@ -31,8 +31,8 @@ Proof. rewrite inv_eq /inv; apply _. Qed.
Lemma inv_alloc N E P : â–· P ={E}=> inv N P.
Proof.
- rewrite inv_eq /inv_def pvs_eq /pvs_def. iIntros "HP [Hw $]".
- iVs (ownI_alloc (∈ nclose N) P with "[HP Hw]") as (i) "(% & $ & ?)"; auto.
+ rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros "HP [Hw $]".
+ iUpd (ownI_alloc (∈ nclose N) P with "[HP Hw]") as (i) "(% & $ & ?)"; auto.
- intros Ef. exists (coPpick (nclose N ∖ coPset.of_gset Ef)).
rewrite -coPset.elem_of_of_gset comm -elem_of_difference.
apply coPpick_elem_of=> Hfin.
@@ -45,11 +45,11 @@ Qed.
Lemma inv_open E N P :
nclose N ⊆ E → inv N P ={E,E∖N}=> ▷ P ★ (▷ P ={E∖N,E}=★ True).
Proof.
- rewrite inv_eq /inv_def pvs_eq /pvs_def; iDestruct 1 as (i) "[Hi #HiP]".
+ rewrite inv_eq /inv_def fupd_eq /fupd_def; iDestruct 1 as (i) "[Hi #HiP]".
iDestruct "Hi" as % ?%elem_of_subseteq_singleton.
rewrite {1 4}(union_difference_L (nclose N) E) // ownE_op; last set_solver.
rewrite {1 5}(union_difference_L {[ i ]} (nclose N)) // ownE_op; last set_solver.
- iIntros "(Hw & [HE $] & $)"; iVsIntro; iApply except_last_intro.
+ iIntros "(Hw & [HE $] & $)"; iUpdIntro; iApply except_last_intro.
iDestruct (ownI_open i P with "[Hw HE]") as "($ & $ & HD)"; first by iFrame.
iIntros "HP [Hw $] !==>"; iApply except_last_intro. iApply ownI_close; by iFrame.
Qed.
@@ -57,7 +57,7 @@ Qed.
Lemma inv_open_timeless E N P `{!TimelessP P} :
nclose N ⊆ E → inv N P ={E,E∖N}=> P ★ (P ={E∖N,E}=★ True).
Proof.
- iIntros (?) "Hinv". iVs (inv_open with "Hinv") as "[>HP Hclose]"; auto.
+ iIntros (?) "Hinv". iUpd (inv_open with "Hinv") as "[>HP Hclose]"; auto.
iIntros "!==> {$HP} HP". iApply "Hclose"; auto.
Qed.
End inv.
@@ -66,7 +66,7 @@ Tactic Notation "iInvCore" constr(N) "as" tactic(tac) constr(Hclose) :=
let Htmp := iFresh in
let patback := intro_pat.parse_one Hclose in
let pat := constr:(IList [[IName Htmp; patback]]) in
- iVs (inv_open _ N with "[#]") as pat;
+ iUpd (inv_open _ N with "[#]") as pat;
[idtac|iAssumption || fail "iInv: invariant" N "not found"|idtac];
[solve_ndisj || match goal with |- ?P => fail "iInv: cannot solve" P end
|tac Htmp].
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index 1eb1c336b..9cf5f0ae6 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -19,13 +19,13 @@ Lemma wp_lift_step E Φ e1 :
Proof.
iIntros "H". rewrite wp_unfold /wp_pre.
destruct (to_val e1) as [v|] eqn:EQe1.
- - iLeft. iExists v. iSplit. done. iVs "H" as (σ1) "[% _]".
+ - iLeft. iExists v. iSplit. done. iUpd "H" as (σ1) "[% _]".
by erewrite reducible_not_val in EQe1.
- iRight; iSplit; eauto.
- iIntros (σ1) "Hσ". iVs "H" as (σ1') "(% & >Hσf & H)".
+ iIntros (σ1) "Hσ". iUpd "H" as (σ1') "(% & >Hσf & H)".
iDestruct (ownP_agree σ1 σ1' with "[-]") as %<-; first by iFrame.
- iVsIntro; iSplit; [done|]; iNext; iIntros (e2 σ2 efs Hstep).
- iVs (ownP_update σ1 σ2 with "[-H]") as "[$ ?]"; first by iFrame.
+ iUpdIntro; iSplit; [done|]; iNext; iIntros (e2 σ2 efs Hstep).
+ iUpd (ownP_update σ1 σ2 with "[-H]") as "[$ ?]"; first by iFrame.
iApply "H"; eauto.
Qed.
@@ -38,10 +38,10 @@ Lemma wp_lift_pure_step `{Inhabited (state Λ)} E Φ e1 :
Proof.
iIntros (Hsafe Hstep) "H". rewrite wp_unfold /wp_pre; iRight; iSplit; auto.
{ iPureIntro. eapply reducible_not_val, (Hsafe inhabitant). }
- iIntros (σ1) "Hσ". iVs (pvs_intro_mask' E ∅) as "Hclose"; first set_solver.
- iVsIntro. iSplit; [done|]; iNext; iIntros (e2 σ2 efs ?).
+ iIntros (σ1) "Hσ". iUpd (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
+ iUpdIntro. iSplit; [done|]; iNext; iIntros (e2 σ2 efs ?).
destruct (Hstep σ1 e2 σ2 efs); auto; subst.
- iVs "Hclose"; iVsIntro. iFrame "Hσ". iApply "H"; auto.
+ iUpd "Hclose"; iUpdIntro. iFrame "Hσ". iApply "H"; auto.
Qed.
(** Derived lifting lemmas. *)
@@ -53,12 +53,12 @@ Lemma wp_lift_atomic_step {E Φ} e1 σ1 :
⊢ WP e1 @ E {{ Φ }}.
Proof.
iIntros (Hatomic ?) "[Hσ H]". iApply (wp_lift_step E _ e1).
- iVs (pvs_intro_mask' E ∅) as "Hclose"; first set_solver. iVsIntro.
+ iUpd (fupd_intro_mask' E ∅) as "Hclose"; first set_solver. iUpdIntro.
iExists σ1. iFrame "Hσ"; iSplit; eauto.
iNext; iIntros (e2 σ2 efs) "[% Hσ]".
edestruct (Hatomic σ1 e2 σ2 efs) as [v2 <-%of_to_val]; eauto.
iDestruct ("H" $! v2 σ2 efs with "[Hσ]") as "[HΦ $]"; first by eauto.
- iVs "Hclose". iVs "HΦ". iApply wp_value; auto using to_of_val.
+ iUpd "Hclose". iUpd "HΦ". iApply wp_value; auto using to_of_val.
Qed.
Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 efs :
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
deleted file mode 100644
index 945213d41..000000000
--- a/program_logic/pviewshifts.v
+++ /dev/null
@@ -1,197 +0,0 @@
-From iris.program_logic Require Export iris.
-From iris.program_logic Require Import wsat.
-From iris.algebra Require Import upred_big_op gmap.
-From iris.proofmode Require Import tactics classes.
-Import uPred.
-
-Program Definition pvs_def `{irisG Λ Σ}
- (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
- (wsat ★ ownE E1 =r=★ ◇ (wsat ★ ownE E2 ★ P))%I.
-Definition pvs_aux : { x | x = @pvs_def }. by eexists. Qed.
-Definition pvs := proj1_sig pvs_aux.
-Definition pvs_eq : @pvs = @pvs_def := proj2_sig pvs_aux.
-Arguments pvs {_ _ _} _ _ _%I.
-Instance: Params (@pvs) 5.
-
-Notation "|={ E1 , E2 }=> Q" := (pvs E1 E2 Q)
- (at level 99, E1, E2 at level 50, Q at level 200,
- format "|={ E1 , E2 }=> Q") : uPred_scope.
-Notation "P ={ E1 , E2 }=★ Q" := (P -★ |={E1,E2}=> Q)%I
- (at level 99, E1,E2 at level 50, Q at level 200,
- format "P ={ E1 , E2 }=★ Q") : uPred_scope.
-Notation "P ={ E1 , E2 }=> Q" := (P ⊢ |={E1,E2}=> Q)
- (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : C_scope.
-
-Notation "|={ E }=> Q" := (pvs E E Q)
- (at level 99, E at level 50, Q at level 200,
- format "|={ E }=> Q") : uPred_scope.
-Notation "P ={ E }=★ Q" := (P -★ |={E}=> Q)%I
- (at level 99, E at level 50, Q at level 200,
- format "P ={ E }=★ Q") : uPred_scope.
-Notation "P ={ E }=> Q" := (P ⊢ |={E}=> Q)
- (at level 99, E at level 50, Q at level 200, only parsing) : C_scope.
-
-Notation "|={ E1 , E2 }â–·=> Q" := (|={E1,E2}=> (â–· |={E2,E1}=> Q))%I
- (at level 99, E1, E2 at level 50, Q at level 200,
- format "|={ E1 , E2 }â–·=> Q") : uPred_scope.
-Notation "|={ E }â–·=> Q" := (|={E,E}â–·=> Q)%I
- (at level 99, E at level 50, Q at level 200,
- format "|={ E }â–·=> Q") : uPred_scope.
-
-Section pvs.
-Context `{irisG Λ Σ}.
-Implicit Types P Q : iProp Σ.
-
-Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Λ Σ _ E1 E2).
-Proof. rewrite pvs_eq. solve_proper. Qed.
-Global Instance pvs_proper E1 E2 : Proper ((≡) ==> (≡)) (@pvs Λ Σ _ E1 E2).
-Proof. apply ne_proper, _. Qed.
-
-Lemma pvs_intro_mask E1 E2 P : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P.
-Proof.
- intros (E1''&->&?)%subseteq_disjoint_union_L.
- rewrite pvs_eq /pvs_def ownE_op //. iIntros "H ($ & $ & HE) !==>".
- iApply except_last_intro. iIntros "[$ $] !==>" . iApply except_last_intro.
- by iFrame.
-Qed.
-
-Lemma except_last_pvs E1 E2 P : â—‡ (|={E1,E2}=> P) ={E1,E2}=> P.
-Proof.
- rewrite pvs_eq. iIntros "H [Hw HE]". iTimeless "H". iApply "H"; by iFrame.
-Qed.
-
-Lemma rvs_pvs E P : (|=r=> P) ={E}=> P.
-Proof.
- rewrite pvs_eq /pvs_def. iIntros "H [$ $]"; iVs "H".
- iVsIntro. by iApply except_last_intro.
-Qed.
-
-Lemma pvs_mono E1 E2 P Q : (P ⊢ Q) → (|={E1,E2}=> P) ={E1,E2}=> Q.
-Proof.
- rewrite pvs_eq /pvs_def. iIntros (HPQ) "HP HwE".
- rewrite -HPQ. by iApply "HP".
-Qed.
-
-Lemma pvs_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) ={E1,E3}=> P.
-Proof.
- rewrite pvs_eq /pvs_def. iIntros "HP HwE".
- iVs ("HP" with "HwE") as ">(Hw & HE & HP)". iApply "HP"; by iFrame.
-Qed.
-
-Lemma pvs_mask_frame_r' E1 E2 Ef P :
- E1 ⊥ Ef → (|={E1,E2}=> E2 ⊥ Ef → P) ={E1 ∪ Ef,E2 ∪ Ef}=> P.
-Proof.
- intros. rewrite pvs_eq /pvs_def ownE_op //. iIntros "Hvs (Hw & HE1 &HEf)".
- iVs ("Hvs" with "[Hw HE1]") as ">($ & HE2 & HP)"; first by iFrame.
- iDestruct (ownE_op' with "[HE2 HEf]") as "[? $]"; first by iFrame.
- iVsIntro; iApply except_last_intro. by iApply "HP".
-Qed.
-
-Lemma pvs_frame_r E1 E2 P Q : (|={E1,E2}=> P) ★ Q ={E1,E2}=> P ★ Q.
-Proof. rewrite pvs_eq /pvs_def. by iIntros "[HwP $]". Qed.
-
-(** * Derived rules *)
-Global Instance pvs_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (@pvs Λ Σ _ E1 E2).
-Proof. intros P Q; apply pvs_mono. Qed.
-Global Instance pvs_flip_mono' E1 E2 :
- Proper (flip (⊢) ==> flip (⊢)) (@pvs Λ Σ _ E1 E2).
-Proof. intros P Q; apply pvs_mono. Qed.
-
-Lemma pvs_intro E P : P ={E}=> P.
-Proof. iIntros "HP". by iApply rvs_pvs. Qed.
-Lemma pvs_intro_mask' E1 E2 : E2 ⊆ E1 → True ⊢ |={E1,E2}=> |={E2,E1}=> True.
-Proof. exact: pvs_intro_mask. Qed.
-Lemma pvs_except_last E1 E2 P : (|={E1,E2}=> â—‡ P) ={E1,E2}=> P.
-Proof. by rewrite {1}(pvs_intro E2 P) except_last_pvs pvs_trans. Qed.
-
-Lemma pvs_frame_l E1 E2 P Q : (P ★ |={E1,E2}=> Q) ={E1,E2}=> P ★ Q.
-Proof. rewrite !(comm _ P); apply pvs_frame_r. Qed.
-Lemma pvs_wand_l E1 E2 P Q : (P -★ Q) ★ (|={E1,E2}=> P) ={E1,E2}=> Q.
-Proof. by rewrite pvs_frame_l wand_elim_l. Qed.
-Lemma pvs_wand_r E1 E2 P Q : (|={E1,E2}=> P) ★ (P -★ Q) ={E1,E2}=> Q.
-Proof. by rewrite pvs_frame_r wand_elim_r. Qed.
-
-Lemma pvs_trans_frame E1 E2 E3 P Q :
- ((Q ={E2,E3}=★ True) ★ |={E1,E2}=> (Q ★ P)) ={E1,E3}=> P.
-Proof.
- rewrite pvs_frame_l assoc -(comm _ Q) wand_elim_r.
- by rewrite pvs_frame_r left_id pvs_trans.
-Qed.
-
-Lemma pvs_mask_frame_r E1 E2 Ef P :
- E1 ⊥ Ef → (|={E1,E2}=> P) ={E1 ∪ Ef,E2 ∪ Ef}=> P.
-Proof.
- iIntros (?) "H". iApply pvs_mask_frame_r'; auto.
- iApply pvs_wand_r; iFrame "H"; eauto.
-Qed.
-Lemma pvs_mask_mono E1 E2 P : E1 ⊆ E2 → (|={E1}=> P) ={E2}=> P.
-Proof.
- intros (Ef&->&?)%subseteq_disjoint_union_L. by apply pvs_mask_frame_r.
-Qed.
-
-Lemma pvs_sep E P Q : (|={E}=> P) ★ (|={E}=> Q) ={E}=> P ★ Q.
-Proof. by rewrite pvs_frame_r pvs_frame_l pvs_trans. Qed.
-Lemma pvs_big_sepM `{Countable K} {A} E (Φ : K → A → iProp Σ) (m : gmap K A) :
- ([★ map] k↦x ∈ m, |={E}=> Φ k x) ={E}=> [★ map] k↦x ∈ m, Φ k x.
-Proof.
- apply (big_opM_forall (λ P Q, P ={E}=> Q)); auto using pvs_intro.
- intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -pvs_sep.
-Qed.
-Lemma pvs_big_sepS `{Countable A} E (Φ : A → iProp Σ) X :
- ([★ set] x ∈ X, |={E}=> Φ x) ={E}=> [★ set] x ∈ X, Φ x.
-Proof.
- apply (big_opS_forall (λ P Q, P ={E}=> Q)); auto using pvs_intro.
- intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -pvs_sep.
-Qed.
-End pvs.
-
-(** Proofmode class instances *)
-Section proofmode_classes.
- Context `{irisG Λ Σ}.
- Implicit Types P Q : iProp Σ.
-
- Global Instance from_pure_pvs E P φ : FromPure P φ → FromPure (|={E}=> P) φ.
- Proof. rewrite /FromPure. intros <-. apply pvs_intro. Qed.
-
- Global Instance from_assumption_pvs E p P Q :
- FromAssumption p P (|=r=> Q) → FromAssumption p P (|={E}=> Q)%I.
- Proof. rewrite /FromAssumption=>->. apply rvs_pvs. Qed.
-
- Global Instance into_wand_pvs E1 E2 R P Q :
- IntoWand R P Q → IntoWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
- Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite pvs_wand_r. Qed.
-
- Global Instance from_sep_pvs E P Q1 Q2 :
- FromSep P Q1 Q2 → FromSep (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
- Proof. rewrite /FromSep=><-. apply pvs_sep. Qed.
-
- Global Instance or_split_pvs E1 E2 P Q1 Q2 :
- FromOr P Q1 Q2 → FromOr (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2).
- Proof. rewrite /FromOr=><-. apply or_elim; apply pvs_mono; auto with I. Qed.
-
- Global Instance exists_split_pvs {A} E1 E2 P (Φ : A → iProp Σ) :
- FromExist P Φ → FromExist (|={E1,E2}=> P) (λ a, |={E1,E2}=> Φ a)%I.
- Proof.
- rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
- Qed.
-
- Global Instance frame_pvs E1 E2 R P Q :
- Frame R P Q → Frame R (|={E1,E2}=> P) (|={E1,E2}=> Q).
- Proof. rewrite /Frame=><-. by rewrite pvs_frame_l. Qed.
-
- Global Instance is_except_last_pvs E1 E2 P : IsExceptLast (|={E1,E2}=> P).
- Proof. by rewrite /IsExceptLast except_last_pvs. Qed.
-
- Global Instance from_vs_pvs E P : FromVs (|={E}=> P) P.
- Proof. by rewrite /FromVs -rvs_pvs. Qed.
-
- Global Instance elim_vs_rvs_pvs E1 E2 P Q :
- ElimVs (|=r=> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q).
- Proof. by rewrite /ElimVs (rvs_pvs E1) pvs_frame_r wand_elim_r pvs_trans. Qed.
- Global Instance elim_vs_pvs_pvs E1 E2 E3 P Q :
- ElimVs (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
- Proof. by rewrite /ElimVs pvs_frame_r wand_elim_r pvs_trans. Qed.
-End proofmode_classes.
-
-Hint Extern 2 (coq_tactics.of_envs _ ⊢ _) =>
- match goal with |- _ ⊢ |={_}=> _ => iVsIntro end.
diff --git a/program_logic/sts.v b/program_logic/sts.v
index 06c1f37ad..8b8ac1701 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -85,10 +85,10 @@ Section sts.
▷ φ s ={E}=> ∃ γ, sts_ctx γ N φ ∧ sts_own γ s (⊤ ∖ sts.tok s).
Proof.
iIntros "Hφ". rewrite /sts_ctx /sts_own.
- iVs (own_alloc (sts_auth s (⊤ ∖ sts.tok s))) as (γ) "Hγ".
+ iUpd (own_alloc (sts_auth s (⊤ ∖ sts.tok s))) as (γ) "Hγ".
{ apply sts_auth_valid; set_solver. }
iExists γ; iRevert "Hγ"; rewrite -sts_op_auth_frag_up; iIntros "[Hγ $]".
- iVs (inv_alloc N _ (sts_inv γ φ) with "[Hφ Hγ]") as "#?"; auto.
+ iUpd (inv_alloc N _ (sts_inv γ φ) with "[Hφ Hγ]") as "#?"; auto.
rewrite /sts_inv. iNext. iExists s. by iFrame.
Qed.
@@ -103,11 +103,11 @@ Section sts.
assert (s ∈ S) by eauto using sts_auth_frag_valid_inv.
assert (✓ sts_frag S T) as [??] by eauto using cmra_valid_op_r.
rewrite sts_op_auth_frag //.
- iVsIntro; iExists s; iSplit; [done|]; iFrame "Hφ".
+ iUpdIntro; iExists s; iSplit; [done|]; iFrame "Hφ".
iIntros (s' T') "[% Hφ]".
- iVs (own_update with "Hγ") as "Hγ"; first eauto using sts_update_auth.
+ iUpd (own_update with "Hγ") as "Hγ"; first eauto using sts_update_auth.
iRevert "Hγ"; rewrite -sts_op_auth_frag_up; iIntros "[Hγ $]".
- iVsIntro. iNext. iExists s'; by iFrame.
+ iUpdIntro. iNext. iExists s'; by iFrame.
Qed.
Lemma sts_acc E γ s0 T :
@@ -129,9 +129,9 @@ Section sts.
to unpack and repack various proofs.
TODO: Make this mostly automatic, by supporting "opening accessors
around accessors". *)
- iVs (sts_accS with "[Hinv Hγf]") as (s) "(?&?& HclSts)"; first by iFrame.
- iVsIntro. iExists s. iFrame. iIntros (s' T') "H".
- iVs ("HclSts" $! s' T' with "H") as "(Hinv & ?)". by iVs ("Hclose" with "Hinv").
+ iUpd (sts_accS with "[Hinv Hγf]") as (s) "(?&?& HclSts)"; first by iFrame.
+ iUpdIntro. iExists s. iFrame. iIntros (s' T') "H".
+ iUpd ("HclSts" $! s' T' with "H") as "(Hinv & ?)". by iUpd ("Hclose" with "Hinv").
Qed.
Lemma sts_open E N γ s0 T :
diff --git a/program_logic/thread_local.v b/program_logic/thread_local.v
index 5be913c45..0d7ccc359 100644
--- a/program_logic/thread_local.v
+++ b/program_logic/thread_local.v
@@ -54,8 +54,8 @@ Section proofs.
Lemma tl_inv_alloc tid E N P : â–· P ={E}=> tl_inv tid N P.
Proof.
iIntros "HP".
- iVs (own_empty (A:=prodUR coPset_disjUR (gset_disjUR positive)) tid) as "Hempty".
- iVs (own_updateP with "Hempty") as ([m1 m2]) "[Hm Hown]".
+ iUpd (own_empty (A:=prodUR coPset_disjUR (gset_disjUR positive)) tid) as "Hempty".
+ iUpd (own_updateP with "Hempty") as ([m1 m2]) "[Hm Hown]".
{ apply prod_updateP'. apply cmra_updateP_id, (reflexivity (R:=eq)).
apply (gset_disj_alloc_empty_updateP_strong' (λ i, i ∈ nclose N)).
intros Ef. exists (coPpick (nclose N ∖ coPset.of_gset Ef)).
@@ -65,7 +65,7 @@ Section proofs.
apply of_gset_finite. }
simpl. iDestruct "Hm" as %(<- & i & -> & ?).
rewrite /tl_inv.
- iVs (inv_alloc tlN with "[-]"); last (iVsIntro; iExists i; eauto).
+ iUpd (inv_alloc tlN with "[-]"); last (iUpdIntro; iExists i; eauto).
iNext. iLeft. by iFrame.
Qed.
@@ -80,7 +80,7 @@ Section proofs.
rewrite {1 5}(union_difference_L {[i]} (nclose N)) ?tl_own_union; [|set_solver..].
iDestruct "Htoks" as "[[Htoki $] $]".
iInv tlN as "[[$ >Hdis]|>Htoki2]" "Hclose".
- - iVs ("Hclose" with "[Htoki]") as "_"; first auto.
+ - iUpd ("Hclose" with "[Htoki]") as "_"; first auto.
iIntros "!==>[HP $]".
iInv tlN as "[[_ >Hdis2]|>Hitok]" "Hclose".
+ iCombine "Hdis" "Hdis2" as "Hdis".
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index e975a02de..3688fc337 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -47,7 +47,7 @@ Lemma vs_transitive E1 E2 E3 P Q R :
(P ={E1,E2}=> Q) ∧ (Q ={E2,E3}=> R) ⊢ P ={E1,E3}=> R.
Proof.
iIntros "#[HvsP HvsQ] !# HP".
- iVs ("HvsP" with "HP") as "HQ". by iApply "HvsQ".
+ iUpd ("HvsP" with "HP") as "HQ". by iApply "HvsQ".
Qed.
Lemma vs_reflexive E P : P ={E}=> P.
@@ -65,14 +65,14 @@ Proof. iIntros "#Hvs !# [HP $]". by iApply "Hvs". Qed.
Lemma vs_mask_frame_r E1 E2 Ef P Q :
E1 ⊥ Ef → (P ={E1,E2}=> Q) ⊢ P ={E1 ∪ Ef,E2 ∪ Ef}=> Q.
Proof.
- iIntros (?) "#Hvs !# HP". iApply pvs_mask_frame_r; auto. by iApply "Hvs".
+ iIntros (?) "#Hvs !# HP". iApply fupd_mask_frame_r; auto. by iApply "Hvs".
Qed.
Lemma vs_inv N E P Q R :
nclose N ⊆ E → inv N R ★ (▷ R ★ P ={E ∖ nclose N}=> ▷ R ★ Q) ⊢ P ={E}=> Q.
Proof.
iIntros (?) "#[? Hvs] !# HP". iInv N as "HR" "Hclose".
- iVs ("Hvs" with "[HR HP]") as "[? $]"; first by iFrame.
+ iUpd ("Hvs" with "[HR HP]") as "[? $]"; first by iFrame.
by iApply "Hclose".
Qed.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 9890456f7..9c0f14e08 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -1,4 +1,4 @@
-From iris.program_logic Require Export pviewshifts.
+From iris.program_logic Require Export fancy_updates.
From iris.program_logic Require Import wsat.
From iris.algebra Require Import upred_big_op.
From iris.prelude Require Export coPset.
@@ -21,9 +21,9 @@ Local Instance wp_pre_contractive `{irisG Λ Σ} : Contractive wp_pre.
Proof.
rewrite /wp_pre=> n wp wp' Hwp E e1 Φ.
apply or_ne, and_ne, forall_ne; auto=> σ1; apply wand_ne; auto.
- apply pvs_ne, sep_ne, later_contractive; auto=> i ?.
+ apply fupd_ne, sep_ne, later_contractive; auto=> i ?.
apply forall_ne=> e2; apply forall_ne=> σ2; apply forall_ne=> efs.
- apply wand_ne, pvs_ne, sep_ne, sep_ne; auto; first by apply Hwp.
+ apply wand_ne, fupd_ne, sep_ne, sep_ne; auto; first by apply Hwp.
apply big_opL_ne=> ? ef. by apply Hwp.
Qed.
@@ -66,9 +66,9 @@ Proof.
revert e. induction (lt_wf n) as [n _ IH]=> e Φ Ψ HΦ.
rewrite !wp_unfold /wp_pre. apply or_ne, and_ne; auto; first solve_proper.
apply forall_ne=> σ1.
- apply wand_ne, pvs_ne, sep_ne, later_contractive; auto=> i ?.
+ apply wand_ne, fupd_ne, sep_ne, later_contractive; auto=> i ?.
apply forall_ne=> e2; apply forall_ne=> σ2; apply forall_ne=> ef.
- apply wand_ne, pvs_ne, sep_ne, sep_ne; auto.
+ apply wand_ne, fupd_ne, sep_ne, sep_ne; auto.
apply IH; [done|]=> v. eapply dist_le; eauto with omega.
Qed.
Global Instance wp_proper E e :
@@ -94,25 +94,25 @@ Proof.
iIntros (?) "[HΦ H]". iLöb as "IH" forall (e). rewrite !wp_unfold /wp_pre.
iDestruct "H" as "[Hv|[% H]]"; [iLeft|iRight].
{ iDestruct "Hv" as (v) "[% Hv]". iExists v; iSplit; first done.
- iApply ("HΦ" with "==>[-]"). by iApply (pvs_mask_mono E1 _). }
+ iApply ("HΦ" with "==>[-]"). by iApply (fupd_mask_mono E1 _). }
iSplit; [done|]; iIntros (σ1) "Hσ".
- iVs (pvs_intro_mask' E2 E1) as "Hclose"; first done.
- iVs ("H" $! σ1 with "Hσ") as "[$ H]".
- iVsIntro. iNext. iIntros (e2 σ2 efs Hstep).
- iVs ("H" $! _ σ2 efs with "[#]") as "($ & H & $)"; auto.
- iVs "Hclose" as "_". by iApply ("IH" with "HΦ").
+ iUpd (fupd_intro_mask' E2 E1) as "Hclose"; first done.
+ iUpd ("H" $! σ1 with "Hσ") as "[$ H]".
+ iUpdIntro. iNext. iIntros (e2 σ2 efs Hstep).
+ iUpd ("H" $! _ σ2 efs with "[#]") as "($ & H & $)"; auto.
+ iUpd "Hclose" as "_". by iApply ("IH" with "HΦ").
Qed.
-Lemma pvs_wp E e Φ : (|={E}=> WP e @ E {{ Φ }}) ⊢ WP e @ E {{ Φ }}.
+Lemma fupd_wp E e Φ : (|={E}=> WP e @ E {{ Φ }}) ⊢ WP e @ E {{ Φ }}.
Proof.
rewrite wp_unfold /wp_pre. iIntros "H". destruct (to_val e) as [v|] eqn:?.
{ iLeft. iExists v; iSplit; first done.
- by iVs "H" as "[H|[% ?]]"; [iDestruct "H" as (v') "[% ?]"|]; simplify_eq. }
+ by iUpd "H" as "[H|[% ?]]"; [iDestruct "H" as (v') "[% ?]"|]; simplify_eq. }
iRight; iSplit; [done|]; iIntros (σ1) "Hσ1".
- iVs "H" as "[H|[% H]]"; last by iApply "H".
+ iUpd "H" as "[H|[% H]]"; last by iApply "H".
iDestruct "H" as (v') "[% ?]"; simplify_eq.
Qed.
-Lemma wp_pvs E e Φ : WP e @ E {{ v, |={E}=> Φ v }} ⊢ WP e @ E {{ Φ }}.
+Lemma wp_fupd E e Φ : WP e @ E {{ v, |={E}=> Φ v }} ⊢ WP e @ E {{ Φ }}.
Proof. iIntros "H". iApply (wp_strong_mono E); try iFrame; auto. Qed.
Lemma wp_atomic E1 E2 e Φ :
@@ -120,16 +120,16 @@ Lemma wp_atomic E1 E2 e Φ :
(|={E1,E2}=> WP e @ E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ E1 {{ Φ }}.
Proof.
iIntros (Hatomic) "H". destruct (to_val e) as [v|] eqn:He.
- { apply of_to_val in He as <-. iApply wp_pvs. iApply wp_value'.
- iVs "H". by iVs (wp_value_inv with "H"). }
+ { apply of_to_val in He as <-. iApply wp_fupd. iApply wp_value'.
+ iUpd "H". by iUpd (wp_value_inv with "H"). }
setoid_rewrite wp_unfold; rewrite /wp_pre. iRight; iSplit; auto.
- iIntros (σ1) "Hσ". iVs "H" as "[H|[_ H]]".
+ iIntros (σ1) "Hσ". iUpd "H" as "[H|[_ H]]".
{ iDestruct "H" as (v') "[% ?]"; simplify_eq. }
- iVs ("H" $! σ1 with "Hσ") as "[$ H]".
- iVsIntro. iNext. iIntros (e2 σ2 efs Hstep).
+ iUpd ("H" $! σ1 with "Hσ") as "[$ H]".
+ iUpdIntro. iNext. iIntros (e2 σ2 efs Hstep).
destruct (Hatomic _ _ _ _ Hstep) as [v <-%of_to_val].
- iVs ("H" $! _ σ2 efs with "[#]") as "($ & H & $)"; auto.
- iVs (wp_value_inv with "H") as "==> H". by iApply wp_value'.
+ iUpd ("H" $! _ σ2 efs with "[#]") as "($ & H & $)"; auto.
+ iUpd (wp_value_inv with "H") as "==> H". by iApply wp_value'.
Qed.
Lemma wp_frame_step_l E1 E2 e Φ R :
@@ -139,10 +139,10 @@ Proof.
rewrite !wp_unfold /wp_pre. iIntros (??) "[HR [Hv|[_ H]]]".
{ iDestruct "Hv" as (v) "[% Hv]"; simplify_eq. }
iRight; iSplit; [done|]. iIntros (σ1) "Hσ".
- iVs "HR". iVs ("H" $! _ with "Hσ") as "[$ H]".
- iVsIntro; iNext; iIntros (e2 σ2 efs Hstep).
- iVs ("H" $! e2 σ2 efs with "[%]") as "($ & H & $)"; auto.
- iVs "HR". iVsIntro. iApply (wp_strong_mono E2 _ _ Φ); try iFrame; eauto.
+ iUpd "HR". iUpd ("H" $! _ with "Hσ") as "[$ H]".
+ iUpdIntro; iNext; iIntros (e2 σ2 efs Hstep).
+ iUpd ("H" $! e2 σ2 efs with "[%]") as "($ & H & $)"; auto.
+ iUpd "HR". iUpdIntro. iApply (wp_strong_mono E2 _ _ Φ); try iFrame; eauto.
Qed.
Lemma wp_bind K `{!LanguageCtx Λ K} E e Φ :
@@ -151,14 +151,14 @@ Proof.
iIntros "H". iLöb as "IH" forall (E e Φ). rewrite wp_unfold /wp_pre.
iDestruct "H" as "[Hv|[% H]]".
{ iDestruct "Hv" as (v) "[Hev Hv]"; iDestruct "Hev" as % <-%of_to_val.
- by iApply pvs_wp. }
+ by iApply fupd_wp. }
rewrite wp_unfold /wp_pre. iRight; iSplit; eauto using fill_not_val.
- iIntros (σ1) "Hσ". iVs ("H" $! _ with "Hσ") as "[% H]".
- iVsIntro; iSplit.
+ iIntros (σ1) "Hσ". iUpd ("H" $! _ with "Hσ") as "[% H]".
+ iUpdIntro; iSplit.
{ iPureIntro. unfold reducible in *. naive_solver eauto using fill_step. }
iNext; iIntros (e2 σ2 efs Hstep).
destruct (fill_step_inv e σ1 e2 σ2 efs) as (e2'&->&?); auto.
- iVs ("H" $! e2' σ2 efs with "[%]") as "($ & H & $)"; auto.
+ iUpd ("H" $! e2' σ2 efs with "[%]") as "($ & H & $)"; auto.
by iApply "IH".
Qed.
@@ -176,11 +176,11 @@ Proof. by intros Φ Φ' ?; apply wp_mono. Qed.
Lemma wp_value E Φ e v : to_val e = Some v → Φ v ⊢ WP e @ E {{ Φ }}.
Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value'. Qed.
-Lemma wp_value_pvs' E Φ v : (|={E}=> Φ v) ⊢ WP of_val v @ E {{ Φ }}.
-Proof. intros. by rewrite -wp_pvs -wp_value'. Qed.
-Lemma wp_value_pvs E Φ e v :
+Lemma wp_value_fupd' E Φ v : (|={E}=> Φ v) ⊢ WP of_val v @ E {{ Φ }}.
+Proof. intros. by rewrite -wp_fupd -wp_value'. Qed.
+Lemma wp_value_fupd E Φ e v :
to_val e = Some v → (|={E}=> Φ v) ⊢ WP e @ E {{ Φ }}.
-Proof. intros. rewrite -wp_pvs -wp_value //. Qed.
+Proof. intros. rewrite -wp_fupd -wp_value //. Qed.
Lemma wp_frame_l E e Φ R : R ★ WP e @ E {{ Φ }} ⊢ WP e @ E {{ v, R ★ Φ v }}.
Proof. iIntros "[??]". iApply (wp_strong_mono E E _ Φ); try iFrame; eauto. Qed.
@@ -223,20 +223,20 @@ Section proofmode_classes.
Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.
Global Instance is_except_last_wp E e Φ : IsExceptLast (WP e @ E {{ Φ }}).
- Proof. by rewrite /IsExceptLast -{2}pvs_wp -except_last_pvs -pvs_intro. Qed.
+ Proof. by rewrite /IsExceptLast -{2}fupd_wp -except_last_fupd -fupd_intro. Qed.
- Global Instance elim_vs_rvs_wp E e P Φ :
- ElimVs (|=r=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
- Proof. by rewrite /ElimVs (rvs_pvs E) pvs_frame_r wand_elim_r pvs_wp. Qed.
+ Global Instance elim_upd_bupd_wp E e P Φ :
+ ElimUpd (|=r=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
+ Proof. by rewrite /ElimUpd (bupd_fupd E) fupd_frame_r wand_elim_r fupd_wp. Qed.
- Global Instance elim_vs_pvs_wp E e P Φ :
- ElimVs (|={E}=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
- Proof. by rewrite /ElimVs pvs_frame_r wand_elim_r pvs_wp. Qed.
+ Global Instance elim_upd_fupd_wp E e P Φ :
+ ElimUpd (|={E}=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
+ Proof. by rewrite /ElimUpd fupd_frame_r wand_elim_r fupd_wp. Qed.
- (* lower precedence, if possible, it should always pick elim_vs_pvs_wp *)
- Global Instance elim_vs_pvs_wp_atomic E1 E2 e P Φ :
+ (* lower precedence, if possible, it should always pick elim_upd_fupd_wp *)
+ Global Instance elim_upd_fupd_wp_atomic E1 E2 e P Φ :
atomic e →
- ElimVs (|={E1,E2}=> P) P
- (WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
- Proof. intros. by rewrite /ElimVs pvs_frame_r wand_elim_r wp_atomic. Qed.
+ ElimUpd (|={E1,E2}=> P) P
+ (WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
+ Proof. intros. by rewrite /ElimUpd fupd_frame_r wand_elim_r wp_atomic. Qed.
End proofmode_classes.
diff --git a/program_logic/wsat.v b/program_logic/wsat.v
index 6f3c7fa9b..0351fc5bf 100644
--- a/program_logic/wsat.v
+++ b/program_logic/wsat.v
@@ -45,11 +45,11 @@ Lemma iris_alloc `{irisPreG Λ Σ} σ :
True =r=> ∃ _ : irisG Λ Σ, wsat ★ ownE ⊤ ★ ownP_auth σ ★ ownP σ.
Proof.
iIntros.
- iVs (own_alloc (◠(Excl' σ) ⋅ ◯ (Excl' σ))) as (γσ) "[Hσ Hσ']"; first done.
- iVs (own_alloc (◠(∅ : gmap _ _))) as (γI) "HI"; first done.
- iVs (own_alloc (CoPset ⊤)) as (γE) "HE"; first done.
- iVs (own_alloc (GSet ∅)) as (γD) "HD"; first done.
- iVsIntro; iExists (IrisG _ _ _ γσ γI γE γD).
+ iUpd (own_alloc (◠(Excl' σ) ⋅ ◯ (Excl' σ))) as (γσ) "[Hσ Hσ']"; first done.
+ iUpd (own_alloc (◠(∅ : gmap _ _))) as (γI) "HI"; first done.
+ iUpd (own_alloc (CoPset ⊤)) as (γE) "HE"; first done.
+ iUpd (own_alloc (GSet ∅)) as (γD) "HD"; first done.
+ iUpdIntro; iExists (IrisG _ _ _ γσ γI γE γD).
rewrite /wsat /ownE /ownP_auth /ownP; iFrame.
iExists ∅. rewrite fmap_empty big_sepM_empty. by iFrame.
Qed.
@@ -154,17 +154,17 @@ Lemma ownI_alloc φ P :
wsat ★ ▷ P =r=> ∃ i, ■(φ i) ★ wsat ★ ownI i P.
Proof.
iIntros (Hfresh) "[Hw HP]". iDestruct "Hw" as (I) "[? HI]".
- iVs (own_empty (A:=gset_disjUR positive) disabled_name) as "HE".
- iVs (own_updateP with "HE") as "HE".
+ iUpd (own_empty (A:=gset_disjUR positive) disabled_name) as "HE".
+ iUpd (own_updateP with "HE") as "HE".
{ apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None ∧ φ i)).
intros E. destruct (Hfresh (E ∪ dom _ I))
as (i & [? HIi%not_elem_of_dom]%not_elem_of_union & ?); eauto. }
iDestruct "HE" as (X) "[Hi HE]"; iDestruct "Hi" as %(i & -> & HIi & ?).
- iVs (own_update with "Hw") as "[Hw HiP]".
+ iUpd (own_update with "Hw") as "[Hw HiP]".
{ eapply auth_update_alloc,
(alloc_singleton_local_update _ i (invariant_unfold P)); last done.
by rewrite /= lookup_fmap HIi. }
- iVsIntro; iExists i; iSplit; [done|]. rewrite /ownI; iFrame "HiP".
+ iUpdIntro; iExists i; iSplit; [done|]. rewrite /ownI; iFrame "HiP".
iExists (<[i:=P]>I); iSplitL "Hw".
{ by rewrite fmap_insert insert_singleton_op ?lookup_fmap ?HIi. }
iApply (big_sepM_insert _ I); first done.
diff --git a/proofmode/class_instances.v b/proofmode/class_instances.v
index 47277f8bb..e7781a3fe 100644
--- a/proofmode/class_instances.v
+++ b/proofmode/class_instances.v
@@ -15,9 +15,9 @@ Proof. rewrite /FromAssumption=><-. by rewrite always_elim. Qed.
Global Instance from_assumption_always_r P Q :
FromAssumption true P Q → FromAssumption true P (□ Q).
Proof. rewrite /FromAssumption=><-. by rewrite always_always. Qed.
-Global Instance from_assumption_rvs p P Q :
+Global Instance from_assumption_bupd p P Q :
FromAssumption p P Q → FromAssumption p P (|=r=> Q)%I.
-Proof. rewrite /FromAssumption=>->. apply rvs_intro. Qed.
+Proof. rewrite /FromAssumption=>->. apply bupd_intro. Qed.
(* IntoPure *)
Global Instance into_pure_pure φ : @IntoPure M (■φ) φ.
@@ -40,8 +40,8 @@ Proof.
rewrite /FromPure. eapply pure_elim; [done|]=> ?.
rewrite -cmra_valid_intro //. auto with I.
Qed.
-Global Instance from_pure_rvs P φ : FromPure P φ → FromPure (|=r=> P) φ.
-Proof. rewrite /FromPure=> ->. apply rvs_intro. Qed.
+Global Instance from_pure_bupd P φ : FromPure P φ → FromPure (|=r=> P) φ.
+Proof. rewrite /FromPure=> ->. apply bupd_intro. Qed.
(* IntoPersistentP *)
Global Instance into_persistentP_always_trans P Q :
@@ -109,9 +109,9 @@ Global Instance into_wand_iff_r P Q : IntoWand (P ↔ Q) Q P.
Proof. apply and_elim_r', impl_wand. Qed.
Global Instance into_wand_always R P Q : IntoWand R P Q → IntoWand (□ R) P Q.
Proof. rewrite /IntoWand=> ->. apply always_elim. Qed.
-Global Instance into_wand_rvs R P Q :
+Global Instance into_wand_bupd R P Q :
IntoWand R P Q → IntoWand R (|=r=> P) (|=r=> Q) | 100.
-Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite rvs_wand_r. Qed.
+Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite bupd_wand_r. Qed.
(* FromAnd *)
Global Instance from_and_and P1 P2 : FromAnd (P1 ∧ P2) P1 P2.
@@ -142,9 +142,9 @@ Proof. rewrite /FromSep=> <-. by rewrite always_sep. Qed.
Global Instance from_sep_later P Q1 Q2 :
FromSep P Q1 Q2 → FromSep (▷ P) (▷ Q1) (▷ Q2).
Proof. rewrite /FromSep=> <-. by rewrite later_sep. Qed.
-Global Instance from_sep_rvs P Q1 Q2 :
+Global Instance from_sep_bupd P Q1 Q2 :
FromSep P Q1 Q2 → FromSep (|=r=> P) (|=r=> Q1) (|=r=> Q2).
-Proof. rewrite /FromSep=><-. apply rvs_sep. Qed.
+Proof. rewrite /FromSep=><-. apply bupd_sep. Qed.
Global Instance from_sep_big_sepM
`{Countable K} {A} (Φ Ψ1 Ψ2 : K → A → uPred M) m :
@@ -317,15 +317,15 @@ Global Instance frame_forall {A} R (Φ Ψ : A → uPred M) :
(∀ a, Frame R (Φ a) (Ψ a)) → Frame R (∀ x, Φ x) (∀ x, Ψ x).
Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
-Global Instance frame_rvs R P Q : Frame R P Q → Frame R (|=r=> P) (|=r=> Q).
-Proof. rewrite /Frame=><-. by rewrite rvs_frame_l. Qed.
+Global Instance frame_bupd R P Q : Frame R P Q → Frame R (|=r=> P) (|=r=> Q).
+Proof. rewrite /Frame=><-. by rewrite bupd_frame_l. Qed.
(* FromOr *)
Global Instance from_or_or P1 P2 : FromOr (P1 ∨ P2) P1 P2.
Proof. done. Qed.
-Global Instance from_or_rvs P Q1 Q2 :
+Global Instance from_or_bupd P Q1 Q2 :
FromOr P Q1 Q2 → FromOr (|=r=> P) (|=r=> Q1) (|=r=> Q2).
-Proof. rewrite /FromOr=><-. apply or_elim; apply rvs_mono; auto with I. Qed.
+Proof. rewrite /FromOr=><-. apply or_elim; apply bupd_mono; auto with I. Qed.
(* IntoOr *)
Global Instance into_or_or P Q : IntoOr (P ∨ Q) P Q.
@@ -337,7 +337,7 @@ Proof. rewrite /IntoOr=>->. by rewrite later_or. Qed.
(* FromExist *)
Global Instance from_exist_exist {A} (Φ : A → uPred M): FromExist (∃ a, Φ a) Φ.
Proof. done. Qed.
-Global Instance from_exist_rvs {A} P (Φ : A → uPred M) :
+Global Instance from_exist_bupd {A} P (Φ : A → uPred M) :
FromExist P Φ → FromExist (|=r=> P) (λ a, |=r=> Φ a)%I.
Proof.
rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
@@ -367,17 +367,17 @@ Global Instance is_except_last_except_last P : IsExceptLast (â—‡ P).
Proof. by rewrite /IsExceptLast except_last_idemp. Qed.
Global Instance is_except_last_later P : IsExceptLast (â–· P).
Proof. by rewrite /IsExceptLast except_last_later. Qed.
-Global Instance is_except_last_rvs P : IsExceptLast P → IsExceptLast (|=r=> P).
+Global Instance is_except_last_bupd P : IsExceptLast P → IsExceptLast (|=r=> P).
Proof.
rewrite /IsExceptLast=> HP.
- by rewrite -{2}HP -(except_last_idemp P) -except_last_rvs -(except_last_intro P).
+ by rewrite -{2}HP -(except_last_idemp P) -except_last_bupd -(except_last_intro P).
Qed.
-(* FromViewShift *)
-Global Instance from_vs_rvs P : FromVs (|=r=> P) P.
+(* FromUpd *)
+Global Instance from_upd_bupd P : FromUpd (|=r=> P) P.
Proof. done. Qed.
-(* ElimViewShift *)
-Global Instance elim_vs_rvs_rvs P Q : ElimVs (|=r=> P) P (|=r=> Q) (|=r=> Q).
-Proof. by rewrite /ElimVs rvs_frame_r wand_elim_r rvs_trans. Qed.
+(* ElimVs *)
+Global Instance elim_upd_bupd_bupd P Q : ElimUpd (|=r=> P) P (|=r=> Q) (|=r=> Q).
+Proof. by rewrite /ElimUpd bupd_frame_r wand_elim_r bupd_trans. Qed.
End classes.
diff --git a/proofmode/classes.v b/proofmode/classes.v
index 224b1e483..3b9958f51 100644
--- a/proofmode/classes.v
+++ b/proofmode/classes.v
@@ -68,13 +68,13 @@ Global Arguments into_except_last : clear implicits.
Class IsExceptLast (Q : uPred M) := is_except_last : ◇ Q ⊢ Q.
Global Arguments is_except_last : clear implicits.
-Class FromVs (P Q : uPred M) := from_vs : (|=r=> Q) ⊢ P.
-Global Arguments from_vs : clear implicits.
+Class FromUpd (P Q : uPred M) := from_upd : (|=r=> Q) ⊢ P.
+Global Arguments from_upd : clear implicits.
-Class ElimVs (P P' : uPred M) (Q Q' : uPred M) :=
- elim_vs : P ★ (P' -★ Q') ⊢ Q.
-Global Arguments elim_vs _ _ _ _ {_}.
+Class ElimUpd (P P' : uPred M) (Q Q' : uPred M) :=
+ elim_upd : P ★ (P' -★ Q') ⊢ Q.
+Global Arguments elim_upd _ _ _ _ {_}.
-Lemma elim_vs_dummy P Q : ElimVs P P Q Q.
-Proof. by rewrite /ElimVs wand_elim_r. Qed.
+Lemma elim_upd_dummy P Q : ElimUpd P P Q Q.
+Proof. by rewrite /ElimUpd wand_elim_r. Qed.
End classes.
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 4c270ef40..ffe86380c 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -533,7 +533,7 @@ Qed.
Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js R P1 P2 P1' Q :
envs_lookup_delete j Δ = Some (q, R, Δ') →
- IntoWand R P1 P2 → ElimVs P1' P1 Q Q →
+ IntoWand R P1 P2 → ElimUpd P1' P1 Q Q →
('(Δ1,Δ2) ↠envs_split lr js Δ';
Δ2' ↠envs_app false (Esnoc Enil j P2) Δ2;
Some (Δ1,Δ2')) = Some (Δ1,Δ2') → (* does not preserve position of [j] *)
@@ -545,7 +545,7 @@ Proof.
rewrite envs_lookup_sound // envs_split_sound //.
rewrite (envs_app_sound Δ2) //; simpl.
rewrite right_id (into_wand R) HP1 assoc -(comm _ P1') -assoc.
- rewrite -(elim_vs P1' P1 Q Q). apply sep_mono_r, wand_intro_l.
+ rewrite -(elim_upd P1' P1 Q Q). apply sep_mono_r, wand_intro_l.
by rewrite always_if_elim assoc !wand_elim_r.
Qed.
@@ -607,7 +607,7 @@ Proof.
Qed.
Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P P' Q :
- ElimVs P' P Q Q →
+ ElimUpd P' P Q Q →
envs_split lr js Δ = Some (Δ1,Δ2) →
envs_app false (Esnoc Enil j P) Δ2 = Some Δ2' →
(Δ1 ⊢ P') → (Δ2' ⊢ Q) → Δ ⊢ Q.
@@ -828,17 +828,17 @@ Proof.
rewrite envs_simple_replace_sound' //; simpl. by rewrite right_id wand_elim_r.
Qed.
-(** * Viewshifts *)
-Lemma tac_vs_intro Δ P Q : FromVs P Q → (Δ ⊢ Q) → Δ ⊢ P.
-Proof. rewrite /FromVs. intros <- ->. apply rvs_intro. Qed.
+(** * Update modality *)
+Lemma tac_upd_intro Δ P Q : FromUpd P Q → (Δ ⊢ Q) → Δ ⊢ P.
+Proof. rewrite /FromUpd. intros <- ->. apply bupd_intro. Qed.
-Lemma tac_vs_elim Δ Δ' i p P' P Q Q' :
+Lemma tac_upd_elim Δ Δ' i p P' P Q Q' :
envs_lookup i Δ = Some (p, P) →
- ElimVs P P' Q Q' →
+ ElimUpd P P' Q Q' →
envs_replace i p false (Esnoc Enil i P') Δ = Some Δ' →
(Δ' ⊢ Q') → Δ ⊢ Q.
Proof.
intros ??? HΔ. rewrite envs_replace_sound //; simpl.
- rewrite right_id HΔ always_if_elim. by apply elim_vs.
+ rewrite right_id HΔ always_if_elim. by apply elim_upd.
Qed.
End tactics.
diff --git a/proofmode/intro_patterns.v b/proofmode/intro_patterns.v
index f2feecb44..f7f4d711b 100644
--- a/proofmode/intro_patterns.v
+++ b/proofmode/intro_patterns.v
@@ -9,11 +9,11 @@ Inductive intro_pat :=
| IPureElim : intro_pat
| IAlwaysElim : intro_pat → intro_pat
| ILaterElim : intro_pat → intro_pat
- | IVsElim : intro_pat → intro_pat
+ | IUpdElim : intro_pat → intro_pat
| IPureIntro : intro_pat
| IAlwaysIntro : intro_pat
| ILaterIntro : intro_pat
- | IVsIntro : intro_pat
+ | IUpdIntro : intro_pat
| ISimpl : intro_pat
| IForall : intro_pat
| IAll : intro_pat
@@ -43,11 +43,11 @@ Inductive token :=
| TPureElim : token
| TAlwaysElim : token
| TLaterElim : token
- | TVsElim : token
+ | TUpdElim : token
| TPureIntro : token
| TAlwaysIntro : token
| TLaterIntro : token
- | TVsIntro : token
+ | TUpdIntro : token
| TSimpl : token
| TForall : token
| TAll : token
@@ -73,12 +73,12 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
| String "#" s => tokenize_go s (TAlwaysElim :: cons_name kn k) ""
| String ">" s => tokenize_go s (TLaterElim :: cons_name kn k) ""
| String "=" (String "=" (String ">" s)) =>
- tokenize_go s (TVsElim :: cons_name kn k) ""
+ tokenize_go s (TUpdElim :: cons_name kn k) ""
| String "!" (String "%" s) => tokenize_go s (TPureIntro :: cons_name kn k) ""
| String "!" (String "#" s) => tokenize_go s (TAlwaysIntro :: cons_name kn k) ""
| String "!" (String ">" s) => tokenize_go s (TLaterIntro :: cons_name kn k) ""
| String "!" (String "=" (String "=" (String ">" s))) =>
- tokenize_go s (TVsIntro :: cons_name kn k) ""
+ tokenize_go s (TUpdIntro :: cons_name kn k) ""
| String "{" s => tokenize_go s (TClearL :: cons_name kn k) ""
| String "}" s => tokenize_go s (TClearR :: cons_name kn k) ""
| String "/" (String "=" s) => tokenize_go s (TSimpl :: cons_name kn k) ""
@@ -96,7 +96,7 @@ Inductive stack_item :=
| SAmp : stack_item
| SAlwaysElim : stack_item
| SLaterElim : stack_item
- | SVsElim : stack_item.
+ | SUpdElim : stack_item.
Notation stack := (list stack_item).
Fixpoint close_list (k : stack)
@@ -108,7 +108,8 @@ Fixpoint close_list (k : stack)
'(p,ps) ↠maybe2 (::) ps; close_list k (IAlwaysElim p :: ps) pss
| SLaterElim :: k =>
'(p,ps) ↠maybe2 (::) ps; close_list k (ILaterElim p :: ps) pss
- | SVsElim :: k => '(p,ps) ↠maybe2 (::) ps; close_list k (IVsElim p :: ps) pss
+ | SUpdElim :: k =>
+ '(p,ps) ↠maybe2 (::) ps; close_list k (IUpdElim p :: ps) pss
| SBar :: k => close_list k [] (ps :: pss)
| _ => None
end.
@@ -132,7 +133,7 @@ Fixpoint close_conj_list (k : stack)
| SPat pat :: k => guard (cur = None); close_conj_list k (Some pat) ps
| SAlwaysElim :: k => p ↠cur; close_conj_list k (Some (IAlwaysElim p)) ps
| SLaterElim :: k => p ↠cur; close_conj_list k (Some (ILaterElim p)) ps
- | SVsElim :: k => p ↠cur; close_conj_list k (Some (IVsElim p)) ps
+ | SUpdElim :: k => p ↠cur; close_conj_list k (Some (IUpdElim p)) ps
| SAmp :: k => p ↠cur; close_conj_list k None (p :: ps)
| _ => None
end.
@@ -153,11 +154,11 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
| TPureElim :: ts => parse_go ts (SPat IPureElim :: k)
| TAlwaysElim :: ts => parse_go ts (SAlwaysElim :: k)
| TLaterElim :: ts => parse_go ts (SLaterElim :: k)
- | TVsElim :: ts => parse_go ts (SVsElim :: k)
+ | TUpdElim :: ts => parse_go ts (SUpdElim :: k)
| TPureIntro :: ts => parse_go ts (SPat IPureIntro :: k)
| TAlwaysIntro :: ts => parse_go ts (SPat IAlwaysIntro :: k)
| TLaterIntro :: ts => parse_go ts (SPat ILaterIntro :: k)
- | TVsIntro :: ts => parse_go ts (SPat IVsIntro :: k)
+ | TUpdIntro :: ts => parse_go ts (SPat IUpdIntro :: k)
| TSimpl :: ts => parse_go ts (SPat ISimpl :: k)
| TAll :: ts => parse_go ts (SPat IAll :: k)
| TForall :: ts => parse_go ts (SPat IForall :: k)
diff --git a/proofmode/spec_patterns.v b/proofmode/spec_patterns.v
index 9c53823de..6be7eafce 100644
--- a/proofmode/spec_patterns.v
+++ b/proofmode/spec_patterns.v
@@ -1,7 +1,7 @@
From iris.prelude Require Export strings.
Record spec_goal := SpecGoal {
- spec_goal_vs : bool;
+ spec_goal_update : bool;
spec_goal_negate : bool;
spec_goal_frame : list string;
spec_goal_hyps : list string
@@ -23,7 +23,7 @@ Inductive token :=
| TPersistent : token
| TPure : token
| TForall : token
- | TVs : token
+ | TUpd : token
| TFrame : token.
Fixpoint cons_name (kn : string) (k : list token) : list token :=
@@ -38,7 +38,7 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
| String "#" s => tokenize_go s (TPersistent :: cons_name kn k) ""
| String "%" s => tokenize_go s (TPure :: cons_name kn k) ""
| String "*" s => tokenize_go s (TForall :: cons_name kn k) ""
- | String "=" (String "=" (String ">" s)) => tokenize_go s (TVs :: cons_name kn k) ""
+ | String "=" (String "=" (String ">" s)) => tokenize_go s (TUpd :: cons_name kn k) ""
| String "$" s => tokenize_go s (TFrame :: cons_name kn k) ""
| String a s => tokenize_go s k (String a kn)
end.
@@ -55,8 +55,8 @@ Fixpoint parse_go (ts : list token) (k : list spec_pat) : option (list spec_pat)
| TBracketL :: TPersistent :: TBracketR :: ts => parse_go ts (SGoalPersistent :: k)
| TBracketL :: TPure :: TBracketR :: ts => parse_go ts (SGoalPure :: k)
| TBracketL :: ts => parse_goal ts (SpecGoal false false [] []) k
- | TVs :: TBracketL :: ts => parse_goal ts (SpecGoal true false [] []) k
- | TVs :: ts => parse_go ts (SGoal (SpecGoal true true [] []) :: k)
+ | TUpd :: TBracketL :: ts => parse_goal ts (SpecGoal true false [] []) k
+ | TUpd :: ts => parse_go ts (SGoal (SpecGoal true true [] []) :: k)
| TForall :: ts => parse_go ts (SForall :: k)
| _ => None
end
@@ -65,17 +65,17 @@ with parse_goal (ts : list token) (g : spec_goal)
match ts with
| TMinus :: ts =>
guard (¬spec_goal_negate g ∧ spec_goal_frame g = [] ∧ spec_goal_hyps g = []);
- parse_goal ts (SpecGoal (spec_goal_vs g) true
+ parse_goal ts (SpecGoal (spec_goal_update g) true
(spec_goal_frame g) (spec_goal_hyps g)) k
| TName s :: ts =>
- parse_goal ts (SpecGoal (spec_goal_vs g) (spec_goal_negate g)
+ parse_goal ts (SpecGoal (spec_goal_update g) (spec_goal_negate g)
(spec_goal_frame g) (s :: spec_goal_hyps g)) k
| TFrame :: TName s :: ts =>
guard (¬spec_goal_negate g);
- parse_goal ts (SpecGoal (spec_goal_vs g) (spec_goal_negate g)
+ parse_goal ts (SpecGoal (spec_goal_update g) (spec_goal_negate g)
(s :: spec_goal_frame g) (spec_goal_hyps g)) k
| TBracketR :: ts =>
- parse_go ts (SGoal (SpecGoal (spec_goal_vs g) (spec_goal_negate g)
+ parse_go ts (SGoal (SpecGoal (spec_goal_update g) (spec_goal_negate g)
(reverse (spec_goal_frame g)) (reverse (spec_goal_hyps g))) :: k)
| _ => None
end.
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 9941b50ef..59177425f 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -312,8 +312,8 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
[env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
|solve_to_wand H1
|match vs with
- | false => apply elim_vs_dummy
- | true => apply _ || fail "iSpecialize: cannot generate view shifted goal"
+ | false => apply elim_upd_dummy
+ | true => apply _ || fail "iSpecialize: goal not an update modality"
end
|env_cbv; reflexivity || fail "iSpecialize:" Hs "not found"
|iFrame Hs_frame (*goal*)
@@ -619,19 +619,19 @@ Tactic Notation "iTimeless" constr(H) :=
apply _ || fail "iTimeless: cannot turn" P "into â—‡"
|env_cbv; reflexivity|].
-(** * View shifts *)
-Tactic Notation "iVsIntro" :=
- eapply tac_vs_intro;
- [let P := match goal with |- FromVs ?P _ => P end in
- apply _ || fail "iVsIntro:" P "not a view shift"|].
-
-Tactic Notation "iVsCore" constr(H) :=
- eapply tac_vs_elim with _ H _ _ _ _;
- [env_cbv; reflexivity || fail "iVs:" H "not found"
- |let P := match goal with |- ElimVs ?P _ _ _ => P end in
- let Q := match goal with |- ElimVs _ _ ?Q _ => Q end in
- apply _ || fail "iVs: cannot run" P "in" Q
- "because the goal or hypothesis is not a view shift"
+(** * Update modality *)
+Tactic Notation "iUpdIntro" :=
+ eapply tac_upd_intro;
+ [let P := match goal with |- FromUpd ?P _ => P end in
+ apply _ || fail "iUpdIntro:" P "not an update modality"|].
+
+Tactic Notation "iUpdCore" constr(H) :=
+ eapply tac_upd_elim with _ H _ _ _ _;
+ [env_cbv; reflexivity || fail "iUpd:" H "not found"
+ |let P := match goal with |- ElimUpd ?P _ _ _ => P end in
+ let Q := match goal with |- ElimUpd _ _ ?Q _ => Q end in
+ apply _ || fail "iUpd: cannot run" P "in" Q
+ "because the goal or hypothesis is not an update modality"
|env_cbv; reflexivity|].
(** * Basic destruct tactic *)
@@ -651,7 +651,7 @@ Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
| IPureElim => iPure Hz as ?
| IAlwaysElim ?pat => iPersistent Hz; go Hz pat
| ILaterElim ?pat => iTimeless Hz; go Hz pat
- | IVsElim ?pat => iVsCore Hz; go Hz pat
+ | IUpdElim ?pat => iUpdCore Hz; go Hz pat
| _ => fail "iDestruct:" pat "invalid"
end
in let pat := intro_pat.parse_one pat in go H pat.
@@ -750,7 +750,7 @@ Tactic Notation "iIntros" constr(pat) :=
| IPureIntro :: ?pats => iPureIntro; go pats
| IAlwaysIntro :: ?pats => iAlways; go pats
| ILaterIntro :: ?pats => iNext; go pats
- | IVsIntro :: ?pats => iVsIntro; go pats
+ | IUpdIntro :: ?pats => iUpdIntro; go pats
| ISimpl :: ?pats => simpl; go pats
| IForall :: ?pats => repeat iIntroForall; go pats
| IAll :: ?pats => repeat (iIntroForall || iIntro); go pats
@@ -1099,8 +1099,8 @@ Tactic Notation "iAssertCore" open_constr(Q) "with" constr(Hs) "as" tactic(tac)
| [SGoal (SpecGoal ?vs ?lr ?Hs_frame ?Hs)] =>
eapply tac_assert with _ _ _ lr (Hs_frame ++ Hs) H Q _;
[match vs with
- | false => apply elim_vs_dummy
- | true => apply _ || fail "iAssert: cannot generate view shifted goal"
+ | false => apply elim_upd_dummy
+ | true => apply _ || fail "iAssert: goal not an update modality"
end
|env_cbv; reflexivity || fail "iAssert:" Hs "not found"
|env_cbv; reflexivity
@@ -1163,50 +1163,50 @@ Ltac iSimplifyEq := repeat (
iMatchGoal ltac:(fun H P => match P with (_ = _)%I => iDestruct H as %? end)
|| simplify_eq/=).
-(** * View shifts *)
-Tactic Notation "iVs" open_constr(lem) :=
- iDestructCore lem as false (fun H => iVsCore H).
-Tactic Notation "iVs" open_constr(lem) "as" constr(pat) :=
- iDestructCore lem as false (fun H => iVsCore H; last iDestructHyp H as pat).
-Tactic Notation "iVs" open_constr(lem) "as" "(" simple_intropattern(x1) ")"
+(** * Update modality *)
+Tactic Notation "iUpd" open_constr(lem) :=
+ iDestructCore lem as false (fun H => iUpdCore H).
+Tactic Notation "iUpd" open_constr(lem) "as" constr(pat) :=
+ iDestructCore lem as false (fun H => iUpdCore H; last iDestructHyp H as pat).
+Tactic Notation "iUpd" open_constr(lem) "as" "(" simple_intropattern(x1) ")"
constr(pat) :=
- iDestructCore lem as false (fun H => iVsCore H; last iDestructHyp H as ( x1 ) pat).
-Tactic Notation "iVs" open_constr(lem) "as" "(" simple_intropattern(x1)
+ iDestructCore lem as false (fun H => iUpdCore H; last iDestructHyp H as ( x1 ) pat).
+Tactic Notation "iUpd" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) ")" constr(pat) :=
- iDestructCore lem as false (fun H => iVsCore H; last iDestructHyp H as ( x1 x2 ) pat).
-Tactic Notation "iVs" open_constr(lem) "as" "(" simple_intropattern(x1)
+ iDestructCore lem as false (fun H => iUpdCore H; last iDestructHyp H as ( x1 x2 ) pat).
+Tactic Notation "iUpd" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
- iDestructCore lem as false (fun H => iVsCore H; last iDestructHyp H as ( x1 x2 x3 ) pat).
-Tactic Notation "iVs" open_constr(lem) "as" "(" simple_intropattern(x1)
+ iDestructCore lem as false (fun H => iUpdCore H; last iDestructHyp H as ( x1 x2 x3 ) pat).
+Tactic Notation "iUpd" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
constr(pat) :=
iDestructCore lem as false (fun H =>
- iVsCore H; last iDestructHyp H as ( x1 x2 x3 x4 ) pat).
-Tactic Notation "iVs" open_constr(lem) "as" "(" simple_intropattern(x1)
+ iUpdCore H; last iDestructHyp H as ( x1 x2 x3 x4 ) pat).
+Tactic Notation "iUpd" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) ")" constr(pat) :=
iDestructCore lem as false (fun H =>
- iVsCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 ) pat).
-Tactic Notation "iVs" open_constr(lem) "as" "(" simple_intropattern(x1)
+ iUpdCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 ) pat).
+Tactic Notation "iUpd" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
iDestructCore lem as false (fun H =>
- iVsCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 x6 ) pat).
-Tactic Notation "iVs" open_constr(lem) "as" "(" simple_intropattern(x1)
+ iUpdCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 x6 ) pat).
+Tactic Notation "iUpd" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
constr(pat) :=
iDestructCore lem as false (fun H =>
- iVsCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
-Tactic Notation "iVs" open_constr(lem) "as" "(" simple_intropattern(x1)
+ iUpdCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
+Tactic Notation "iUpd" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) ")" constr(pat) :=
iDestructCore lem as false (fun H =>
- iVsCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
+ iUpdCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
-Tactic Notation "iVs" open_constr(lem) "as" "%" simple_intropattern(pat) :=
- iDestructCore lem as false (fun H => iVsCore H; iPure H as pat).
+Tactic Notation "iUpd" open_constr(lem) "as" "%" simple_intropattern(pat) :=
+ iDestructCore lem as false (fun H => iUpdCore H; iPure H as pat).
(* Make sure that by and done solve trivial things in proof mode *)
Hint Extern 0 (of_envs _ ⊢ _) => by iPureIntro.
@@ -1223,7 +1223,7 @@ Hint Extern 1 (of_envs _ ⊢ _) =>
| |- _ ⊢ ▷ _ => iNext
| |- _ ⊢ □ _ => iClear "*"; iAlways
| |- _ ⊢ ∃ _, _ => iExists _
- | |- _ ⊢ |=r=> _ => iVsIntro
+ | |- _ ⊢ |=r=> _ => iUpdIntro
end.
Hint Extern 1 (of_envs _ ⊢ _) =>
match goal with |- _ ⊢ (_ ∨ _)%I => iLeft end.
diff --git a/tests/atomic.v b/tests/atomic.v
index 37cee397c..251f033f7 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -1,4 +1,4 @@
-From iris.program_logic Require Export hoare weakestpre pviewshifts.
+From iris.program_logic Require Export hoare weakestpre.
From iris.algebra Require Import upred_big_op.
From iris.prelude Require Export coPset.
From iris.proofmode Require Import tactics.
@@ -75,22 +75,22 @@ Section incr.
iIntros "!# HP".
wp_rec.
wp_bind (! _)%E.
- iVs ("Hvs" with "HP") as (x) "[Hl [Hvs' _]]".
+ iUpd ("Hvs" with "HP") as (x) "[Hl [Hvs' _]]".
wp_load.
- iVs ("Hvs'" with "Hl") as "HP".
- iVsIntro. wp_let. wp_bind (CAS _ _ _). wp_op.
- iVs ("Hvs" with "HP") as (x') "[Hl Hvs']".
+ iUpd ("Hvs'" with "Hl") as "HP".
+ iUpdIntro. wp_let. wp_bind (CAS _ _ _). wp_op.
+ iUpd ("Hvs" with "HP") as (x') "[Hl Hvs']".
destruct (decide (x = x')).
- subst.
iDestruct "Hvs'" as "[_ Hvs']".
iSpecialize ("Hvs'" $! #x').
wp_cas_suc.
- iVs ("Hvs'" with "[Hl]") as "HQ"; first by iFrame.
- iVsIntro. wp_if. iVsIntro. by iExists x'.
+ iUpd ("Hvs'" with "[Hl]") as "HQ"; first by iFrame.
+ iUpdIntro. wp_if. iUpdIntro. by iExists x'.
- iDestruct "Hvs'" as "[Hvs' _]".
wp_cas_fail.
- iVs ("Hvs'" with "[Hl]") as "HP"; first by iFrame.
- iVsIntro. wp_if. by iApply "IH".
+ iUpd ("Hvs'" with "[Hl]") as "HP"; first by iFrame.
+ iUpdIntro. wp_if. by iApply "IH".
Qed.
End incr.
@@ -112,7 +112,7 @@ Section user.
rewrite /incr_2.
wp_let.
wp_alloc l as "Hl".
- iVs (inv_alloc N _ (∃x':Z, l ↦ #x')%I with "[Hl]") as "#?"; first eauto.
+ iUpd (inv_alloc N _ (∃x':Z, l ↦ #x')%I with "[Hl]") as "#?"; first eauto.
wp_let.
wp_bind (_ || _)%E.
iApply (wp_par (λ _, True%I) (λ _, True%I)).
@@ -125,15 +125,15 @@ Section user.
(* open the invariant *)
iInv N as (x') ">Hl'" "Hclose".
(* mask magic *)
- iVs (pvs_intro_mask' _ heapN) as "Hclose'".
+ iUpd (fupd_intro_mask' _ heapN) as "Hclose'".
{ apply ndisj_subseteq_difference; auto. }
- iVsIntro. iExists x'. iFrame "Hl'". iSplit.
+ iUpdIntro. iExists x'. iFrame "Hl'". iSplit.
+ (* provide a way to rollback *)
iIntros "Hl'".
- iVs "Hclose'". iVs ("Hclose" with "[Hl']"); eauto.
+ iUpd "Hclose'". iUpd ("Hclose" with "[Hl']"); eauto.
+ (* provide a way to commit *)
iIntros (v) "[Heq Hl']".
- iVs "Hclose'". iVs ("Hclose" with "[Hl']"); eauto.
+ iUpd "Hclose'". iUpd ("Hclose" with "[Hl']"); eauto.
- iDestruct "Hincr" as "#HIncr".
iSplitL; [|iSplitL]; try (iApply wp_wand_r;iSplitL; [by iApply "HIncr"|auto]).
iIntros (v1 v2) "_ !>".
diff --git a/tests/barrier_client.v b/tests/barrier_client.v
index abbfe8cbf..8fab9362d 100644
--- a/tests/barrier_client.v
+++ b/tests/barrier_client.v
@@ -49,7 +49,7 @@ Section client.
iSplitL; [|by iIntros (_ _) "_ !>"].
iDestruct (recv_weaken with "[] Hr") as "Hr".
{ iIntros "Hy". by iApply (y_inv_split with "Hy"). }
- iVs (recv_split with "Hr") as "[H1 H2]"; first done.
+ iUpd (recv_split with "Hr") as "[H1 H2]"; first done.
iApply (wp_par (λ _, True%I) (λ _, True%I)). iFrame "Hh".
iSplitL "H1"; [|iSplitL "H2"; [|by iIntros (_ _) "_ !>"]];
iApply worker_safe; by iSplit.
diff --git a/tests/counter.v b/tests/counter.v
index 92d7c61c2..935e1e136 100644
--- a/tests/counter.v
+++ b/tests/counter.v
@@ -95,11 +95,11 @@ Lemma newcounter_spec N :
heap_ctx ⊢ {{ True }} newcounter #() {{ v, ∃ l, v = #l ∧ C l 0 }}.
Proof.
iIntros (?) "#Hh !# _ /=". rewrite /newcounter /=. wp_seq. wp_alloc l as "Hl".
- iVs (own_alloc (Auth 0)) as (γ) "Hγ"; first done.
+ iUpd (own_alloc (Auth 0)) as (γ) "Hγ"; first done.
rewrite (auth_frag_op 0 0) //; iDestruct "Hγ" as "[Hγ Hγf]".
- iVs (inv_alloc N _ (I γ l) with "[Hl Hγ]") as "#?".
+ iUpd (inv_alloc N _ (I γ l) with "[Hl Hγ]") as "#?".
{ iIntros "!>". iExists 0%nat. by iFrame. }
- iVsIntro. rewrite /C; eauto 10.
+ iUpdIntro. rewrite /C; eauto 10.
Qed.
Lemma inc_spec l n :
@@ -108,20 +108,20 @@ Proof.
iIntros "!# Hl /=". iLöb as "IH". wp_rec.
iDestruct "Hl" as (N γ) "(% & #Hh & #Hinv & Hγf)".
wp_bind (! _)%E; iInv N as (c) "[Hl Hγ]" "Hclose".
- wp_load. iVs ("Hclose" with "[Hl Hγ]"); [iNext; iExists c; by iFrame|].
- iVsIntro. wp_let. wp_op.
+ wp_load. iUpd ("Hclose" with "[Hl Hγ]"); [iNext; iExists c; by iFrame|].
+ iUpdIntro. wp_let. wp_op.
wp_bind (CAS _ _ _). iInv N as (c') ">[Hl Hγ]" "Hclose".
destruct (decide (c' = c)) as [->|].
- iCombine "Hγ" "Hγf" as "Hγ".
iDestruct (own_valid with "Hγ") as %?%auth_frag_valid; rewrite -auth_frag_op //.
- iVs (own_update with "Hγ") as "Hγ"; first apply M_update.
+ iUpd (own_update with "Hγ") as "Hγ"; first apply M_update.
rewrite (auth_frag_op (S n) (S c)); last lia; iDestruct "Hγ" as "[Hγ Hγf]".
- wp_cas_suc. iVs ("Hclose" with "[Hl Hγ]").
+ wp_cas_suc. iUpd ("Hclose" with "[Hl Hγ]").
{ iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
- iVsIntro. wp_if. iVsIntro; rewrite {3}/C; eauto 10.
+ iUpdIntro. wp_if. iUpdIntro; rewrite {3}/C; eauto 10.
- wp_cas_fail; first (intros [=]; abstract omega).
- iVs ("Hclose" with "[Hl Hγ]"); [iNext; iExists c'; by iFrame|].
- iVsIntro. wp_if. iApply ("IH" with "[Hγf]"). rewrite {3}/C; eauto 10.
+ iUpd ("Hclose" with "[Hl Hγ]"); [iNext; iExists c'; by iFrame|].
+ iUpdIntro. wp_if. iApply ("IH" with "[Hγf]"). rewrite {3}/C; eauto 10.
Qed.
Lemma read_spec l n :
@@ -132,7 +132,7 @@ Proof.
iDestruct (own_valid γ (Frag n ⋅ Auth c) with "[-]") as % ?%auth_frag_valid.
{ iApply own_op. by iFrame. }
rewrite (auth_frag_op c c); last lia; iDestruct "Hγ" as "[Hγ Hγf']".
- iVs ("Hclose" with "[Hl Hγ]"); [iNext; iExists c; by iFrame|].
- iVsIntro; rewrite /C; eauto 10 with omega.
+ iUpd ("Hclose" with "[Hl Hγ]"); [iNext; iExists c; by iFrame|].
+ iUpdIntro; rewrite /C; eauto 10 with omega.
Qed.
End proof.
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index bccc4848c..d18943ad0 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -47,7 +47,7 @@ Section LiftingTests.
iIntros (Hn) "HΦ". iLöb as "IH" forall (n1 Hn).
wp_rec. wp_let. wp_op. wp_let. wp_op=> ?; wp_if.
- iApply ("IH" with "[%] HΦ"). omega.
- - iApply pvs_intro. by assert (n1 = n2 - 1) as -> by omega.
+ - iApply fupd_intro. by assert (n1 = n2 - 1) as -> by omega.
Qed.
Lemma Pred_spec n E Φ : ▷ Φ #(n - 1) ⊢ WP Pred #n @ E {{ Φ }}.
diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index 3aa32e4ff..dc693644d 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -75,7 +75,7 @@ Lemma client_spec_new eM eW1 eW2 `{!Closed [] eM, !Closed [] eW1, !Closed [] eW2
⊢ WP client eM eW1 eW2 {{ _, ∃ γ, barrier_res γ Ψ }}.
Proof.
iIntros (HN) "/= (#Hh&HP&#He&#He1&#He2)"; rewrite /client.
- iVs (own_alloc (Pending : one_shotR Σ F)) as (γ) "Hγ"; first done.
+ iUpd (own_alloc (Pending : one_shotR Σ F)) as (γ) "Hγ"; first done.
wp_apply (newbarrier_spec N (barrier_res γ Φ)); auto.
iFrame "Hh". iIntros (l) "[Hr Hs]".
set (workers_post (v : val) := (barrier_res γ Ψ1 ★ barrier_res γ Ψ2)%I).
@@ -83,12 +83,12 @@ Proof.
iSplitL "HP Hs Hγ"; [|iSplitL "Hr"].
- wp_bind eM. iApply wp_wand_l; iSplitR "HP"; [|by iApply "He"].
iIntros (v) "HP"; iDestruct "HP" as (x) "HP". wp_let.
- iVs (own_update with "Hγ") as "Hx".
+ iUpd (own_update with "Hγ") as "Hx".
{ by apply (cmra_update_exclusive (Shot x)). }
iApply signal_spec; iFrame "Hs"; iSplit; last done.
iExists x; auto.
- iDestruct (recv_weaken with "[] Hr") as "Hr"; first by iApply P_res_split.
- iVs (recv_split with "Hr") as "[H1 H2]"; first done.
+ iUpd (recv_split with "Hr") as "[H1 H2]"; first done.
wp_apply (wp_par (λ _, barrier_res γ Ψ1)%I
(λ _, barrier_res γ Ψ2)%I); iFrame "Hh".
iSplitL "H1"; [|iSplitL "H2"].
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 1bf218843..1f95e9060 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -43,17 +43,17 @@ Lemma wp_one_shot (Φ : val → iProp Σ) :
Proof.
iIntros "[#? Hf] /=".
rewrite /one_shot_example /=. wp_seq. wp_alloc l as "Hl". wp_let.
- iVs (own_alloc Pending) as (γ) "Hγ"; first done.
- iVs (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN".
+ iUpd (own_alloc Pending) as (γ) "Hγ"; first done.
+ iUpd (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN".
{ iNext. iLeft. by iSplitL "Hl". }
- iVsIntro. iApply "Hf"; iSplit.
+ iUpdIntro. iApply "Hf"; iSplit.
- iIntros (n) "!#". wp_let.
iInv N as ">[[Hl Hγ]|H]" "Hclose"; last iDestruct "H" as (m) "[Hl Hγ]".
- + wp_cas_suc. iVs (own_update with "Hγ") as "Hγ".
+ + wp_cas_suc. iUpd (own_update with "Hγ") as "Hγ".
{ by apply cmra_update_exclusive with (y:=Shot n). }
- iVs ("Hclose" with "[-]"); last eauto.
+ iUpd ("Hclose" with "[-]"); last eauto.
iNext; iRight; iExists n; by iFrame.
- + wp_cas_fail. iVs ("Hclose" with "[-]"); last eauto.
+ + wp_cas_fail. iUpd ("Hclose" with "[-]"); last eauto.
rewrite /one_shot_inv; eauto 10.
- iIntros "!#". wp_seq. wp_bind (! _)%E.
iInv N as ">Hγ" "Hclose".
@@ -68,8 +68,8 @@ Proof.
{ iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as (m) "[% ?]"; subst.
+ iSplit. iLeft; by iSplitL "Hl". eauto.
+ iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
- iVs ("Hclose" with "[Hinv]") as "_"; eauto; iVsIntro.
- wp_let. iVsIntro. iIntros "!#". wp_seq.
+ iUpd ("Hclose" with "[Hinv]") as "_"; eauto; iUpdIntro.
+ wp_let. iUpdIntro. iIntros "!#". wp_seq.
iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']"; subst.
{ by wp_match. }
wp_match. wp_bind (! _)%E.
@@ -78,9 +78,9 @@ Proof.
wp_load.
iCombine "Hγ" "Hγ'" as "Hγ".
iDestruct (own_valid with "Hγ") as %[=->]%dec_agree_op_inv.
- iVs ("Hclose" with "[Hl]") as "_".
+ iUpd ("Hclose" with "[Hl]") as "_".
{ iNext; iRight; by eauto. }
- iVsIntro. wp_match. iApply wp_assert. wp_op=>?; simplify_eq/=; eauto.
+ iUpdIntro. wp_match. iApply wp_assert. wp_op=>?; simplify_eq/=; eauto.
Qed.
Lemma ht_one_shot (Φ : val → iProp Σ) :
--
GitLab