diff --git a/ProofMode.md b/ProofMode.md
index 9ba06e4e214906b2adb218b9dc8af99243f23841..c8748778fa6a7e2a2e8cf814ce43b9a76516f5b3 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -98,8 +98,19 @@ Separating logic specific tactics
- `iCombine "H1" "H2" as "H"` : turns `H1 : P1` and `H2 : P2` into
`H : P1 ★ P2`.
+Modalities
+----------
+
+- `iModIntro` : introduction of a modality that is an instance of the
+ `IntoModal` type class. Instances include: later, except 0, basic update and
+ fancy update.
+- `iMod pm_trm as (x1 ... xn) "ipat"` : eliminate a modality `pm_trm` that is
+ an instance of the `ElimModal` type class. Instances include: later, except 0,
+ basic update and fancy update.
+
The later modality
------------------
+
- `iNext` : introduce a later by stripping laters from all hypotheses.
- `iLöb as "IH" forall (x1 ... xn)` : perform Löb induction by generating a
hypothesis `IH : â–· goal`. The tactic generalizes over the Coq level variables
@@ -108,6 +119,7 @@ The later modality
Induction
---------
+
- `iInduction x as cpat "IH" forall (x1 ... xn) "selpat"` : perform induction on
the Coq term `x`. The Coq introduction pattern is used to name the introduced
variables. The induction hypotheses are inserted into the persistent context
@@ -124,13 +136,8 @@ Rewriting
Iris
----
-- `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, update modality, or a weakest
- precondition).
+- `iInv N as (x1 ... xn) "ipat" "Hclose"` : open the invariant `N`, the update
+ for closing the invariant is put in a hypothesis named `Hclose`.
Miscellaneous
-------------
@@ -170,8 +177,7 @@ _introduction patterns_:
- `[]` : false elimination.
- `%` : 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 an update modality (if the goal permits).
+- `> ipat` : eliminate a modality (if the goal permits).
Apart from this, there are the following introduction patterns that can only
appear at the top level:
@@ -181,8 +187,7 @@ appear at the top level:
previous pattern, e.g., `{$H1 H2 $H3}`).
- `!%` : 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 an update modality
+- `!>` : introduce a modality.
- `/=` : perform `simpl`.
- `*` : introduce all universal quantifiers.
- `**` : introduce all universal quantifiers, as well as all arrows and wands.
@@ -222,9 +227,9 @@ _specification patterns_ to express splitting of hypotheses:
framed in the generated goal.
- `[-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 an update modality, in which case the update modality will be kept in the
- goal of the premise too.
+- `>[H1 ... Hn]` : same as the above pattern, but can only be used if the goal
+ is a modality, in which case the modality will be kept in the generated goal
+ for the premise will be wrapped into the modality.
- `[#]` : This pattern can be used when eliminating `P -★ Q` with `P`
persistent. Using this pattern, all hypotheses are available in the goal for
`P`, as well the remaining goal.
diff --git a/heap_lang/adequacy.v b/heap_lang/adequacy.v
index 5884b78184ffde603c49a74b1a1c2f0db71b06b8..b71175c1f0b7659bc48e9da821804058daf6ed6f 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σ".
- iUpd (auth_alloc to_heap _ heapN _ σ with "[Hσ]") as (γ) "[Hh _]";[|by iNext|].
+ iMod (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 6cc7e17833cb208baa868ad9f30dfbfc1b09ab26..d0f0c872acd742b37d2e70b3dbfd0d4b23bb0aee 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.
- 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σ] !==>".
- iUpd ("Hcl" with "* [Hσ]") as "Ha".
+ iMod (auth_empty heap_name) as "Ha".
+ iMod (auth_open with "[$Hinv $Ha]") as (σ) "(%&Hσ&Hcl)"; first done.
+ iApply wp_alloc_pst. iFrame "Hσ". iNext. iIntros (l) "[% Hσ] !>".
+ iMod ("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,10 +125,10 @@ Section heap.
Proof.
iIntros (?) "[#Hinv [>Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
- iUpd (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
+ iMod (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
iApply (wp_load_pst _ σ); first eauto using heap_singleton_included.
- iIntros "{$Hσ} !> Hσ !==>". iUpd ("Hcl" with "* [Hσ]") as "Ha"; first eauto.
- by iApply "HΦ".
+ iIntros "{$Hσ}"; iNext; iIntros "Hσ !>".
+ iMod ("Hcl" with "* [Hσ]") as "Ha"; first eauto. by iApply "HΦ".
Qed.
Lemma wp_store E l v' e v Φ :
@@ -138,9 +138,9 @@ Section heap.
Proof.
iIntros (<-%of_to_val ?) "[#Hinv [>Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
- iUpd (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
+ iMod (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
iApply (wp_store_pst _ σ); first eauto using heap_singleton_included.
- iIntros "{$Hσ} !> Hσ !==>". iUpd ("Hcl" with "* [Hσ]") as "Ha".
+ iIntros "{$Hσ}"; iNext; iIntros "Hσ !>". iMod ("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,10 +154,10 @@ Section heap.
Proof.
iIntros (<-%of_to_val <-%of_to_val ??) "[#Hinv [>Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
- iUpd (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
+ iMod (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
iApply (wp_cas_fail_pst _ σ); [eauto using heap_singleton_included|done|].
- iIntros "{$Hσ} !> Hσ !==>". iUpd ("Hcl" with "* [Hσ]") as "Ha"; first eauto.
- by iApply "HΦ".
+ iIntros "{$Hσ}"; iNext; iIntros "Hσ !>".
+ iMod ("Hcl" with "* [Hσ]") as "Ha"; first eauto. by iApply "HΦ".
Qed.
Lemma wp_cas_suc E l e1 v1 e2 v2 Φ :
@@ -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.
- iUpd (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
+ iMod (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
iApply (wp_cas_suc_pst _ σ); first eauto using heap_singleton_included.
- iIntros "{$Hσ} !> Hσ !==>". iUpd ("Hcl" with "* [Hσ]") as "Ha".
+ iIntros "{$Hσ}"; iNext; iIntros "Hσ !>". iMod ("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 a9b9db7fba3185f14f3398659a9b2aaede55a4d8..71cb6ffd07bd5cf7baba339ece79808dfd0eb316 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -97,22 +97,22 @@ Lemma newbarrier_spec (P : iProp Σ) (Φ : val → iProp Σ) :
Proof.
iIntros (HN) "[#? HΦ]".
rewrite /newbarrier /=. wp_seq. wp_alloc l as "Hl".
- iApply ("HΦ" with "==>[-]").
- iUpd (saved_prop_alloc (F:=idCF) P) as (γ) "#?".
- iUpd (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
+ iApply ("HΦ" with ">[-]").
+ iMod (saved_prop_alloc (F:=idCF) P) as (γ) "#?".
+ iMod (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. }
iAssert (barrier_ctx γ' l P)%I as "#?".
{ rewrite /barrier_ctx. by repeat iSplit. }
iAssert (sts_ownS γ' (i_states γ) {[Change γ]}
- ★ sts_ownS γ' low_states {[Send]})%I with "==>[-]" as "[Hr Hs]".
+ ★ sts_ownS γ' low_states {[Send]})%I with ">[-]" as "[Hr Hs]".
{ iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
- set_solver.
- iApply (sts_own_weaken with "Hγ'");
auto using sts.closed_op, i_states_closed, low_states_closed;
abstract set_solver. }
- iUpdIntro. rewrite /recv /send. iSplitL "Hr".
+ iModIntro. rewrite /recv /send. iSplitL "Hr".
- iExists γ', P, P, γ. iFrame. auto.
- auto.
Qed.
@@ -122,14 +122,14 @@ 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.
- iUpd (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
+ iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
destruct p; [|done]. wp_store. iFrame "HΦ".
- iUpd ("Hclose" $! (State High I) (∅ : set token) with "[-]"); last done.
+ iMod ("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".
- iIntros "!> _"; by iApply "Hr".
+ iNext. iIntros "_"; by iApply "Hr".
Qed.
Lemma wait_spec l P (Φ : val → iProp Σ) :
@@ -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.
- iUpd (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
+ iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
wp_load. destruct p.
- - iUpd ("Hclose" $! (State Low I) {[ Change i ]} with "[Hl Hr]") as "Hγ".
+ - iMod ("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γ".
+ iAssert (sts_ownS γ (i_states i) {[Change i]})%I with ">[Hγ]" as "Hγ".
{ iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. }
- iUpdIntro. wp_if.
+ iModIntro. 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Ψ". }
- iUpd ("Hclose" $! (State High (I ∖ {[ i ]})) (∅ : set token) with "[HΨ' Hl Hsp]").
+ iMod ("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.
- iUpdIntro. wp_if.
- iUpdIntro. iApply "HΦ". iApply "HQR". by iRewrite "Heq".
+ iModIntro. wp_if.
+ iModIntro. iApply "HΦ". iApply "HQR". by iRewrite "Heq".
Qed.
Lemma recv_split E l P1 P2 :
@@ -166,25 +166,25 @@ 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)".
- iUpd (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
+ iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
- iUpd (saved_prop_alloc_strong (R1: ∙%CF (iProp Σ)) I) as (i1) "[% #Hi1]".
- iUpd (saved_prop_alloc_strong (R2: ∙%CF (iProp Σ)) (I ∪ {[i1]}))
+ iMod (saved_prop_alloc_strong (R1: ∙%CF (iProp Σ)) I) as (i1) "[% #Hi1]".
+ iMod (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.
- iUpd ("Hclose" $! (State p ({[i1; i2]} ∪ I ∖ {[i]}))
+ iMod ("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".
iApply (ress_split _ _ _ Q R1 R2); eauto. iFrame; auto. }
iAssert (sts_ownS γ (i_states i1) {[Change i1]}
- ★ sts_ownS γ (i_states i2) {[Change i2]})%I with "==>[-]" as "[Hγ1 Hγ2]".
+ ★ sts_ownS γ (i_states i2) {[Change i2]})%I with ">[-]" as "[Hγ1 Hγ2]".
{ iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
- abstract set_solver.
- iApply (sts_own_weaken with "Hγ");
eauto using sts.closed_op, i_states_closed.
abstract set_solver. }
- iUpdIntro; iSplitL "Hγ1"; rewrite /recv /barrier_ctx.
+ iModIntro; iSplitL "Hγ1"; rewrite /recv /barrier_ctx.
- iExists γ, P, R1, i1. iFrame; auto.
- iExists γ, P, R2, i2. iFrame; auto.
Qed.
@@ -194,7 +194,7 @@ Proof.
rewrite /recv.
iIntros "HP HP1"; iDestruct "HP1" as (γ P Q i) "(#Hctx&Hγ&Hi&HP1)".
iExists γ, P, Q, i. iFrame "Hctx Hγ Hi".
- iIntros "!> HQ". by iApply "HP"; iApply "HP1".
+ iNext. iIntros "HQ". by iApply "HP"; iApply "HP1".
Qed.
Lemma recv_mono l P1 P2 : (P1 ⊢ P2) → recv l P1 ⊢ recv l P2.
diff --git a/heap_lang/lib/counter.v b/heap_lang/lib/counter.v
index c63966215d072f6bfe2c92fc2c14dda1e7ae940c..cbc8d7cc1a406dac24be2cb44f8dd0bfcfb00e52 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".
- iUpd (own_alloc (◠(O:mnat) ⋅ ◯ (O:mnat))) as (γ) "[Hγ Hγ']"; first done.
- iUpd (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
+ iMod (own_alloc (◠(O:mnat) ⋅ ◯ (O:mnat))) as (γ) "[Hγ Hγ']"; first done.
+ iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
{ iNext. iExists 0%nat. by iFrame. }
- iUpdIntro. iApply "HΦ". rewrite /mcounter; eauto 10.
+ iModIntro. 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. iUpd ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
- iUpdIntro. wp_let. wp_op.
+ wp_load. iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
+ iModIntro. 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.
- iUpd (own_update_2 with "[$Hγ $Hγf]") as "[Hγ Hγf]".
+ iMod (own_update_2 with "[$Hγ $Hγf]") as "[Hγ Hγf]".
{ apply auth_update, (mnat_local_update _ _ (S c)); auto. }
- wp_cas_suc. iUpd ("Hclose" with "[Hl Hγ]") as "_".
+ wp_cas_suc. iMod ("Hclose" with "[Hl Hγ]") as "_".
{ iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
- iUpdIntro. wp_if. iApply "HΦ"; iExists γ; repeat iSplit; eauto.
+ iModIntro. 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]).
- iUpd ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
- iUpdIntro. wp_if. iApply ("IH" with "[Hγf] HΦ").
+ iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
+ iModIntro. 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.
- iUpd (own_update_2 with "[$Hγ $Hγf]") as "[Hγ Hγf]".
+ iMod (own_update_2 with "[$Hγ $Hγf]") as "[Hγ Hγf]".
{ apply auth_update, (mnat_local_update _ _ c); auto. }
- iUpd ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
+ iMod ("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".
- iUpd (own_alloc (â— (Some (1%Qp, O%nat)) â‹… â—¯ (Some (1%Qp, 0%nat))))
+ iMod (own_alloc (â— (Some (1%Qp, O%nat)) â‹… â—¯ (Some (1%Qp, 0%nat))))
as (γ) "[Hγ Hγ']"; first done.
- iUpd (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
+ iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
{ iNext. iExists 0%nat. by iFrame. }
- iUpdIntro. iApply "HΦ". rewrite /ccounter_ctx /ccounter; eauto 10.
+ iModIntro. 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. iUpd ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
- iUpdIntro. wp_let. wp_op.
+ wp_load. iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
+ iModIntro. wp_let. wp_op.
wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]" "Hclose".
destruct (decide (c' = c)) as [->|].
- - iUpd (own_update_2 with "[$Hγ $Hγf]") as "[Hγ Hγf]".
+ - iMod (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. iUpd ("Hclose" with "[Hl Hγ]") as "_".
+ wp_cas_suc. iMod ("Hclose" with "[Hl Hγ]") as "_".
{ iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
- iUpdIntro. wp_if. by iApply "HΦ".
+ iModIntro. wp_if. by iApply "HΦ".
- wp_cas_fail; first (by intros [= ?%Nat2Z.inj]).
- iUpd ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
- iUpdIntro. wp_if. by iApply ("IH" with "[Hγf] HΦ").
+ iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
+ iModIntro. 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.
- iUpd ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
+ iMod ("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.
- iUpd ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
+ iMod ("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 f28d650048a6879768eb2d0534e5702afb0a1cb1..7477d396cb97b5c618f8f9c941b242a9a5c75279 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. iUpdIntro. wp_let. wp_proj.
+ rewrite /par. wp_value. iModIntro. 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 b5a4c2b736d60073032f0e3343d8e818456a1d1d..435ed807349bc4d15ddffaff2d00c5506fec3195 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.
- iUpd (own_alloc (Excl ())) as (γ) "Hγ"; first done.
- iUpd (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".
+ iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
+ iMod (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".
{ iNext. iExists NONEV. iFrame; eauto. }
wp_apply wp_fork; simpl. iSplitR "Hf".
- - iUpdIntro. wp_seq. iUpdIntro. iApply "HΦ". rewrite /join_handle. eauto.
+ - iModIntro. wp_seq. iModIntro. 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.
- - iUpd ("Hclose" with "[Hl]"); [iNext; iExists _; iFrame; eauto|].
- iUpdIntro. wp_match. iApply ("IH" with "Hγ Hv").
+ - iMod ("Hclose" with "[Hl]"); [iNext; iExists _; iFrame; eauto|].
+ iModIntro. wp_match. iApply ("IH" with "Hγ Hv").
- iDestruct "Hinv" as (v') "[% [HΨ|Hγ']]"; simplify_eq/=.
- + iUpd ("Hclose" with "[Hl Hγ]"); [iNext; iExists _; iFrame; eauto|].
- iUpdIntro. wp_match. by iApply "Hv".
+ + iMod ("Hclose" with "[Hl Hγ]"); [iNext; iExists _; iFrame; eauto|].
+ iModIntro. 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 7659ea3128df2a9b4146e94319927c9ab635ff7d..21bedd2cdbd5058324e8831e4f368f64d6f576b3 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".
- iUpd (own_alloc (Excl ())) as (γ) "Hγ"; first done.
- iUpd (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
+ iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
+ iMod (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
{ iIntros "!>". iExists false. by iFrame. }
- iUpdIntro. iApply "HΦ". iExists l. eauto.
+ iModIntro. 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. iUpd ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
- iUpdIntro. iDestruct "HΦ" as "[_ HΦ]". iApply "HΦ".
+ - wp_cas_fail. iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
+ iModIntro. iDestruct "HΦ" as "[_ HΦ]". iApply "HΦ".
- wp_cas_suc. iDestruct "HR" as "[Hγ HR]".
- iUpd ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
- iUpdIntro. iDestruct "HΦ" as "[HΦ _]". rewrite /locked. by iApply ("HΦ" with "Hγ HR").
+ iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
+ iModIntro. 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. iUpdIntro. iApply ("HΦ" with "Hlked HR").
+ - iIntros "Hlked HR". wp_if. iModIntro. 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 2c2deae40a66170ebd3296c947c23cc7d5d63a8f..6bda146dae67c747dcee2990f58a0e866e7c6aae 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".
- iUpd (own_alloc (◠(Excl' 0%nat, ∅) ⋅ ◯ (Excl' 0%nat, ∅))) as (γ) "[Hγ Hγ']".
+ iMod (own_alloc (◠(Excl' 0%nat, ∅) ⋅ ◯ (Excl' 0%nat, ∅))) as (γ) "[Hγ Hγ']".
{ by rewrite -auth_both_op. }
- iUpd (inv_alloc _ _ (lock_inv γ lo ln R) with "[-HΦ]").
+ iMod (inv_alloc _ _ (lock_inv γ lo ln R) with "[-HΦ]").
{ iNext. rewrite /lock_inv.
iExists 0%nat, 0%nat. iFrame. iLeft. by iFrame. }
- iUpdIntro. iApply ("HΦ" $! (#lo, #ln)%V γ). iExists lo, ln. eauto.
+ iModIntro. 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]]".
- + iUpd ("Hclose" with "[Hlo Hln Hainv Ht]") as "_".
+ + iMod ("Hclose" with "[Hlo Hln Hainv Ht]") as "_".
{ iNext. iExists o, n. iFrame. eauto. }
- iUpdIntro. wp_let. wp_op=>[_|[]] //.
- wp_if. iUpdIntro.
+ iModIntro. wp_let. wp_op=>[_|[]] //.
+ wp_if. iModIntro.
iApply ("HΦ" with "[-HR] HR"). rewrite /locked; eauto.
+ iDestruct (own_valid_2 with "[$Ht $Haown]") as % [_ ?%gset_disj_valid_op].
set_solver.
- - iUpd ("Hclose" with "[Hlo Hln Ha]").
+ - iMod ("Hclose" with "[Hlo Hln Ha]").
{ iNext. iExists o, n. by iFrame. }
- iUpdIntro. wp_let. wp_op=>[[/Nat2Z.inj //]|?].
+ iModIntro. 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. iUpd ("Hclose" with "[Hlo Hln Ha]") as "_".
+ wp_load. iMod ("Hclose" with "[Hlo Hln Ha]") as "_".
{ iNext. iExists o, n. by iFrame. }
- iUpdIntro. wp_let. wp_proj. wp_op.
+ iModIntro. 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.
- iUpd (own_update with "Hauth") as "[Hauth Hofull]".
+ iMod (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).
- iUpd ("Hclose" with "[Hlo' Hln' Haown Hauth]") as "_".
+ iMod ("Hclose" with "[Hlo' Hln' Haown Hauth]") as "_".
{ iNext. iExists o', (S n).
rewrite Nat2Z.inj_succ -Z.add_1_r. by iFrame. }
- iUpdIntro. wp_if.
+ iModIntro. wp_if.
iApply (wait_loop_spec γ (#lo, #ln)).
iFrame "HΦ". rewrite /issued; eauto 10.
- wp_cas_fail.
- iUpd ("Hclose" with "[Hlo' Hln' Hauth Haown]") as "_".
+ iMod ("Hclose" with "[Hlo' Hln' Hauth Haown]") as "_".
{ iNext. iExists o', n'. by iFrame. }
- iUpdIntro. wp_if. by iApply "IH".
+ iModIntro. 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.
- iUpd ("Hclose" with "[Hlo Hln Hauth Haown]") as "_".
+ iMod ("Hclose" with "[Hlo Hln Hauth Haown]") as "_".
{ iNext. iExists o, n. by iFrame. }
- iUpdIntro. wp_op.
+ iModIntro. 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 %[[] ?]. }
- iUpd (own_update_2 with "[$Hauth $Hγo]") as "[Hauth Hγo]".
+ iMod (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))). }
- iUpd ("Hclose" with "[Hlo Hln Hauth Haown Hγo HR]") as "_"; last auto.
+ iMod ("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/program_logic/adequacy.v b/program_logic/adequacy.v
index de9d3c55b0b7c17d2cb853a5d19e51f0ab321483..0da50c86363f671b645eddc6747089731ab68bb9 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -46,9 +46,9 @@ 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 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]")
+ iMod ("H" $! σ1 with "Hσ [Hw HE]") as ">(Hw & HE & _ & H)"; first by iFrame.
+ iModIntro; iNext.
+ iMod ("H" $! e2 σ2 efs with "[%] [Hw HE]")
as ">($ & $ & $ & $)"; try iFrame; eauto.
Qed.
@@ -76,8 +76,8 @@ 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']].
- iUpd (wptp_step with "H") as (e1' t1'') "[% H]"; first eauto; simplify_eq.
- iUpdIntro; iNext; iUpd "H" as ">?". by iApply IH.
+ iMod (wptp_step with "H") as (e1' t1'') "[% H]"; first eauto; simplify_eq.
+ iModIntro; iNext; iMod "H" as ">?". by iApply IH.
Qed.
Instance bupd_iter_mono n : Proper ((⊢) ==> (⊢)) (Nat.iter n (λ P, |==> ▷ P)%I).
@@ -99,7 +99,7 @@ Proof.
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 fupd_eq /fupd_def.
- iUpd ("H" with "[Hw HE]") as ">(_ & _ & $)"; iFrame; auto.
+ iMod ("H" with "[Hw HE]") as ">(_ & _ & $)"; iFrame; auto.
Qed.
Lemma wp_safe e σ Φ :
@@ -107,7 +107,7 @@ Lemma wp_safe e σ Φ :
Proof.
rewrite wp_unfold /wp_pre. iIntros "[(Hw&HE&Hσ) [H|[_ H]]]".
{ iDestruct "H" as (v) "[% _]"; eauto 10. }
- rewrite fupd_eq. iUpd ("H" with "* Hσ [-]") as ">(?&?&%&?)"; first by iFrame.
+ rewrite fupd_eq. iMod ("H" with "* Hσ [-]") as ">(?&?&%&?)"; first by iFrame.
eauto 10.
Qed.
@@ -133,7 +133,7 @@ Proof.
iIntros "[HI H]".
iDestruct "H" as (e2' t2') "(% & (Hw&HE&Hσ) & _)"; subst.
rewrite fupd_eq in HI;
- iUpd (HI with "HI [Hw HE]") as "> (_ & _ & H)"; first by iFrame.
+ iMod (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.
@@ -146,13 +146,13 @@ Proof.
intros Hwp; split.
- intros t2 σ2 v2 [n ?]%rtc_nsteps.
eapply (soundness (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
- rewrite Nat_iter_S. iUpd (iris_alloc σ) as (?) "(?&?&?&Hσ)".
- iUpdIntro. iNext. iApply wptp_result; eauto.
+ rewrite Nat_iter_S. iMod (iris_alloc σ) as (?) "(?&?&?&Hσ)".
+ iModIntro. iNext. iApply wptp_result; eauto.
iFrame. iSplitL. by iApply Hwp. by iApply big_sepL_nil.
- intros t2 σ2 e2 [n ?]%rtc_nsteps ?.
eapply (soundness (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
- rewrite Nat_iter_S. iUpd (iris_alloc σ) as (?) "(Hw & HE & Hσ & Hσf)".
- iUpdIntro. iNext. iApply wptp_safe; eauto.
+ rewrite Nat_iter_S. iMod (iris_alloc σ) as (?) "(Hw & HE & Hσ & Hσf)".
+ iModIntro. iNext. iApply wptp_safe; eauto.
iFrame "Hw HE Hσ". iSplitL. by iApply Hwp. by iApply big_sepL_nil.
Qed.
@@ -164,8 +164,8 @@ Theorem wp_invariance Σ `{irisPreG Λ Σ} e σ1 t2 σ2 I φ Φ :
Proof.
intros Hwp HI [n ?]%rtc_nsteps.
eapply (soundness (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
- rewrite Nat_iter_S. iUpd (iris_alloc σ1) as (?) "(Hw & HE & ? & Hσ)".
+ rewrite Nat_iter_S. iMod (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.
+ iMod (Hwp _ with "Hσ [Hw HE]") as ">(? & ? & ? & ?)"; first by iFrame.
+ iModIntro. 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 28d2f6c8321f896e265b0456ff4be5b38909185e..7c2d805297984fe443433be68e8639b3f4546351 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -95,9 +95,9 @@ Section auth.
✓ (f t) → ▷ φ t ={E}=★ ∃ γ, ■(γ ∉ G) ∧ auth_ctx γ N f φ ∧ auth_own γ (f t).
Proof.
iIntros (?) "Hφ". rewrite /auth_own /auth_ctx.
- iUpd (own_alloc_strong (Auth (Excl' (f t)) (f t)) G) as (γ) "[% Hγ]"; first done.
+ iMod (own_alloc_strong (Auth (Excl' (f t)) (f t)) G) as (γ) "[% Hγ]"; first done.
iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']".
- iUpd (inv_alloc N _ (auth_inv γ f φ) with "[-Hγ']") as "#?".
+ iMod (inv_alloc N _ (auth_inv γ f φ) with "[-Hγ']") as "#?".
{ iNext. rewrite /auth_inv. iExists t. by iFrame. }
eauto.
Qed.
@@ -106,7 +106,7 @@ Section auth.
✓ (f t) → ▷ φ t ={E}=★ ∃ γ, auth_ctx γ N f φ ∧ auth_own γ (f t).
Proof.
iIntros (?) "Hφ".
- iUpd (auth_alloc_strong N E t ∅ with "Hφ") as (γ) "[_ ?]"; eauto.
+ iMod (auth_alloc_strong N E t ∅ with "Hφ") as (γ) "[_ ?]"; eauto.
Qed.
Lemma auth_empty γ : True ==★ auth_own γ ∅.
@@ -119,12 +119,12 @@ Section auth.
Proof.
iIntros "(Hinv & Hγf)". rewrite /auth_inv /auth_own.
iDestruct "Hinv" as (t) "[>Hγa Hφ]".
- iUpdIntro. iExists t.
+ iModIntro. iExists t.
iDestruct (own_valid_2 with "[$Hγa $Hγf]") as % [? ?]%auth_valid_discrete_2.
iSplit; first done. iFrame. iIntros (u b) "[% Hφ]".
- iUpd (own_update_2 with "[$Hγa $Hγf]") as "[Hγa Hγf]".
+ iMod (own_update_2 with "[$Hγa $Hγf]") as "[Hγa Hγf]".
{ eapply auth_update; eassumption. }
- iUpdIntro. iFrame. iExists u. iFrame.
+ iModIntro. iFrame. iExists u. iFrame.
Qed.
Lemma auth_open E N γ a :
@@ -140,9 +140,9 @@ Section auth.
to unpack and repack various proofs.
TODO: Make this mostly automatic, by supporting "opening accessors
around accessors". *)
- 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").
+ iMod (auth_acc with "[$Hinv $Hγf]") as (t) "(?&?&HclAuth)".
+ iModIntro. iExists t. iFrame. iIntros (u b) "H".
+ iMod ("HclAuth" $! u b with "H") as "(Hinv & ?)". by iMod ("Hclose" with "Hinv").
Qed.
End auth.
diff --git a/program_logic/boxes.v b/program_logic/boxes.v
index afba03c55e0d7181ebe48d6bd17ebf4f3b04d716..e2abbd055e972bc9eac6e223cee3db8e47acdaa8 100644
--- a/program_logic/boxes.v
+++ b/program_logic/boxes.v
@@ -75,7 +75,7 @@ Lemma box_own_agree γ Q1 Q2 :
Proof.
rewrite /box_own_prop own_valid_2 prod_validI /= and_elim_r.
rewrite option_validI /= agree_validI agree_equivI later_equivI /=.
- iIntros "#HQ !>". rewrite -{2}(iProp_fold_unfold Q1).
+ iIntros "#HQ". iNext. rewrite -{2}(iProp_fold_unfold Q1).
iRewrite "HQ". by rewrite iProp_fold_unfold.
Qed.
@@ -91,14 +91,14 @@ Lemma box_insert f P Q :
slice N γ Q ★ ▷ box N (<[γ:=false]> f) (Q ★ P).
Proof.
iDestruct 1 as (Φ) "[#HeqP Hf]".
- iUpd (own_alloc_strong (â— Excl' false â‹… â—¯ Excl' false,
+ iMod (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.
- iUpd (inv_alloc N _ (slice_inv γ Q) with "[Hγ]") as "#Hinv".
+ iMod (inv_alloc N _ (slice_inv γ Q) with "[Hγ]") as "#Hinv".
{ iNext. iExists false; eauto. }
- iUpdIntro; iExists γ; repeat iSplit; auto.
+ iModIntro; 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 //.
@@ -113,7 +113,7 @@ Proof.
iIntros (?) "[#Hinv H]"; iDestruct "H" as (Φ) "[#HeqP Hf]".
iExists ([★ map] γ'↦_ ∈ delete γ f, Φ γ')%I.
iInv N as (b) "(Hγ & #HγQ &_)" "Hclose".
- iApply fupd_trans_frame; iFrame "Hclose"; iUpdIntro; iNext.
+ iApply fupd_trans_frame; iFrame "Hclose"; iModIntro; 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.
@@ -133,10 +133,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.
- iUpd (box_own_auth_update γ b' false true with "[Hγ Hγ']")
+ iMod (box_own_auth_update γ b' false true with "[Hγ Hγ']")
as "[Hγ Hγ']"; first by iFrame.
- iUpd ("Hclose" with "[Hγ HQ]"); first (iNext; iExists true; by iFrame).
- iUpdIntro; iNext; iExists Φ; iSplit.
+ iMod ("Hclose" with "[Hγ HQ]"); first (iNext; iExists true; by iFrame).
+ iModIntro; iNext; iExists Φ; iSplit.
- by rewrite big_sepM_insert_override.
- rewrite -insert_delete big_sepM_insert ?lookup_delete //.
iFrame; eauto.
@@ -153,9 +153,9 @@ Proof.
as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
iFrame "HQ".
- 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.
+ iMod (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ Hγ']"; first by iFrame.
+ iMod ("Hclose" with "[Hγ]"); first (iNext; iExists false; by repeat iSplit).
+ iModIntro; iNext; iExists Φ; iSplit.
- by rewrite big_sepM_insert_override.
- rewrite -insert_delete big_sepM_insert ?lookup_delete //.
iFrame; eauto.
@@ -171,7 +171,7 @@ Proof.
iApply (big_sepM_impl _ _ f); iFrame "Hf".
iAlways; iIntros (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
iInv N as (b) "[>Hγ _]" "Hclose".
- iUpd (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ $]"; first by iFrame.
+ iMod (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ $]"; first by iFrame.
iApply "Hclose". iNext; iExists true. by iFrame.
Qed.
@@ -181,17 +181,17 @@ Lemma box_empty_all f P Q :
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Φ ?]".
+ box_own_prop γ (Φ γ) ★ inv N (slice_inv γ (Φ γ)))%I with ">[Hf]" as "[HΦ ?]".
{ 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.
- iUpd (box_own_auth_update γ true true false with "[Hγ Hγ']")
+ iMod (box_own_auth_update γ true true false with "[Hγ Hγ']")
as "[Hγ $]"; first by iFrame.
- iUpd ("Hclose" with "[Hγ]"); first (iNext; iExists false; iFrame; eauto).
+ iMod ("Hclose" with "[Hγ]"); first (iNext; iExists false; iFrame; eauto).
by iApply "HΦ". }
- iUpdIntro; iSplitL "HΦ".
+ iModIntro; 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 22f68d06d87c912579b84624b10ec814b911bb9d..5f7b0796304abf8b7972e830df16b937abdcd731 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".
- iUpd (own_alloc 1%Qp) as (γ) "H1"; first done.
- iUpd (inv_alloc N _ (P ∨ own γ 1%Qp)%I with "[HP]"); eauto.
+ iMod (own_alloc 1%Qp) as (γ) "H1"; first done.
+ iMod (inv_alloc N _ (P ∨ own γ 1%Qp)%I with "[HP]"); eauto.
Qed.
Lemma cinv_cancel E N γ P :
@@ -65,7 +65,7 @@ Section proofs.
Proof.
rewrite /cinv. iIntros (?) "#Hinv Hγ".
iInv N as "[$|>Hγ']" "Hclose".
- - iIntros "!==> {$Hγ} HP". iApply "Hclose"; eauto.
+ - iIntros "!> {$Hγ} HP". iApply "Hclose"; eauto.
- iDestruct (cinv_own_1_l with "[Hγ Hγ']") as %[]. by iFrame.
Qed.
End proofs.
diff --git a/program_logic/counter_examples.v b/program_logic/counter_examples.v
index ec7d171e56f979a071e2cc859c5154ea15eafcc3..5ea06663330915152d6f25361124af35384fff25 100644
--- a/program_logic/counter_examples.v
+++ b/program_logic/counter_examples.v
@@ -40,9 +40,9 @@ Module savedprop. Section savedprop.
Lemma contradiction : False.
Proof.
apply (@soundness M False 1); simpl.
- iIntros "". iUpd A_alloc as (i) "#H".
+ iIntros "". iMod A_alloc as (i) "#H".
iPoseProof (saved_NA with "H") as "HN".
- iUpdIntro. iNext.
+ iModIntro. iNext.
iApply "HN". iApply saved_A. done.
Qed.
@@ -113,12 +113,12 @@ Module inv. Section inv.
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_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_fupd_fupd E P Q : ElimModal (fupd E P) P (fupd E Q) (fupd E Q).
+ Proof. by rewrite /ElimModal fupd_frame_r uPred.wand_elim_r fupd_fupd. Qed.
- Global Instance elim_fupd0_fupd1 P Q : ElimUpd (fupd M0 P) P (fupd M1 Q) (fupd M1 Q).
+ Global Instance elim_fupd0_fupd1 P Q : ElimModal (fupd M0 P) P (fupd M1 Q) (fupd M1 Q).
Proof.
- by rewrite /ElimUpd fupd_frame_r uPred.wand_elim_r fupd_mask_mono fupd_fupd.
+ by rewrite /ElimModal fupd_frame_r uPred.wand_elim_r fupd_mask_mono fupd_fupd.
Qed.
Global Instance exists_split_fupd0 {A} E P (Φ : A → iProp) :
@@ -135,8 +135,8 @@ Module inv. Section inv.
Lemma saved_alloc (P : gname → iProp) : True ⊢ fupd M1 (∃ γ, saved γ (P γ)).
Proof.
- iIntros "". iUpd (sts_alloc) as (γ) "Hs".
- iUpd (inv_alloc (start γ ∨ (finished γ ★ □ (P γ))) with "[Hs]") as (i) "#Hi".
+ iIntros "". iMod (sts_alloc) as (γ) "Hs".
+ iMod (inv_alloc (start γ ∨ (finished γ ★ □ (P γ))) with "[Hs]") as (i) "#Hi".
{ auto. }
iApply fupd_intro. by iExists γ, i.
Qed.
@@ -145,7 +145,7 @@ Module inv. Section inv.
Proof.
iIntros "(#HsP & #HsQ & #HP)". iDestruct "HsP" as (i) "HiP".
iApply (inv_open' i). iSplit; first done.
- iIntros "HaP". iAssert (fupd 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 fupd_intro. }
@@ -173,7 +173,7 @@ Module inv. Section inv.
Proof.
iIntros "#Hi !# #HA". iPoseProof "HA" as "HA'".
iDestruct "HA'" as (P) "#[HNP Hi']".
- iUpd (saved_cast i (A i) P with "[]") as "HP".
+ iMod (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 "".
- iUpd A_alloc as (i) "#H".
+ iMod 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 4349b35b9a83b2041005d2b78926ca1540852ea3..9ec7f68782c3cb03ced8d5feb06144c2be18127b 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.
- iUpd "H" as (σ1) "(%&Hσ1&Hwp)". iUpdIntro. iExists σ1.
+ iMod "H" as (σ1) "(%&Hσ1&Hwp)". iModIntro. 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
index 14f8e54f791cab14f9239f6695a4ef5bc4f88e67..4c21e0ee95f88eea522b8307162c5d9ec7320664 100644
--- a/program_logic/fancy_updates.v
+++ b/program_logic/fancy_updates.v
@@ -51,20 +51,20 @@ 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_0_intro. iIntros "[$ $] !==>" . iApply except_0_intro.
+ rewrite fupd_eq /fupd_def ownE_op //. iIntros "H ($ & $ & HE) !>".
+ iApply except_0_intro. iIntros "[$ $] !>" . iApply except_0_intro.
by iFrame.
Qed.
Lemma except_0_fupd E1 E2 P : ◇ (|={E1,E2}=> P) ={E1,E2}=★ P.
Proof.
- rewrite fupd_eq. iIntros "H [Hw HE]". iTimeless "H". iApply "H"; by iFrame.
+ rewrite fupd_eq. iIntros "H [Hw HE]". iMod "H". iApply "H"; by iFrame.
Qed.
Lemma bupd_fupd E P : (|==> P) ={E}=★ P.
Proof.
- rewrite fupd_eq /fupd_def. iIntros "H [$ $]"; iUpd "H".
- iUpdIntro. by iApply except_0_intro.
+ rewrite fupd_eq /fupd_def. iIntros "H [$ $]"; iMod "H".
+ iModIntro. by iApply except_0_intro.
Qed.
Lemma fupd_mono E1 E2 P Q : (P ⊢ Q) → (|={E1,E2}=> P) ={E1,E2}=★ Q.
@@ -76,16 +76,16 @@ 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.
+ iMod ("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.
+ iMod ("Hvs" with "[Hw HE1]") as ">($ & HE2 & HP)"; first by iFrame.
iDestruct (ownE_op' with "[HE2 HEf]") as "[? $]"; first by iFrame.
- iUpdIntro; iApply except_0_intro. by iApply "HP".
+ iModIntro; iApply except_0_intro. by iApply "HP".
Qed.
Lemma fupd_frame_r E1 E2 P Q : (|={E1,E2}=> P) ★ Q ={E1,E2}=★ P ★ Q.
@@ -183,16 +183,18 @@ Section proofmode_classes.
Global Instance is_except_0_fupd E1 E2 P : IsExcept0 (|={E1,E2}=> P).
Proof. by rewrite /IsExcept0 except_0_fupd. Qed.
- Global Instance from_upd_fupd E P : FromUpd (|={E}=> P) P.
- Proof. by rewrite /FromUpd -bupd_fupd. Qed.
+ Global Instance into_modal_fupd E P : IntoModal P (|={E}=> P).
+ Proof. rewrite /IntoModal. apply fupd_intro. Qed.
- Global Instance elim_upd_bupd_fupd E1 E2 P Q :
- ElimUpd (|==> 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.
+ Global Instance elim_modal_bupd_fupd E1 E2 P Q :
+ ElimModal (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q).
+ Proof.
+ by rewrite /ElimModal (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans.
+ Qed.
+ Global Instance elim_modal_fupd_fupd E1 E2 E3 P Q :
+ ElimModal (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
+ Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_trans. Qed.
End proofmode_classes.
Hint Extern 2 (coq_tactics.of_envs _ ⊢ _) =>
- match goal with |- _ ⊢ |={_}=> _ => iUpdIntro end.
+ match goal with |- _ ⊢ |={_}=> _ => iModIntro end.
diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index 5b079dfb6e54a0299562959bc6c0eff48d577ed8..30250418794f31a8554b4abc67c5cf0a26e0e13e 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -62,7 +62,7 @@ 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". iUpd ("Hvs" with "HP") as "HP".
+ iIntros "(#Hvs & #Hwp & #HΦ) !# HP". iMod ("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.
- iUpd ("Hvs" with "HP") as "HP". iUpdIntro.
+ iMod ("Hvs" with "HP") as "HP". iModIntro.
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 9f76aaf775956adf6cde10b5458bbdb5214091da..d303886fbe626b295595e0968cafde24df00f559 100644
--- a/program_logic/invariants.v
+++ b/program_logic/invariants.v
@@ -32,7 +32,7 @@ Proof. rewrite inv_eq /inv; apply _. Qed.
Lemma inv_alloc N E P : ▷ P ={E}=★ inv N P.
Proof.
rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros "HP [Hw $]".
- iUpd (ownI_alloc (∈ nclose N) P with "[HP Hw]") as (i) "(% & $ & ?)"; auto.
+ iMod (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.
@@ -49,16 +49,16 @@ Proof.
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 $] & $)"; iUpdIntro; iApply except_0_intro.
+ iIntros "(Hw & [HE $] & $)"; iModIntro; iApply except_0_intro.
iDestruct (ownI_open i P with "[Hw HE]") as "($ & $ & HD)"; first by iFrame.
- iIntros "HP [Hw $] !==>"; iApply except_0_intro. iApply ownI_close; by iFrame.
+ iIntros "HP [Hw $] !> !>". iApply ownI_close; by iFrame.
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". iUpd (inv_open with "Hinv") as "[>HP Hclose]"; auto.
- iIntros "!==> {$HP} HP". iApply "Hclose"; auto.
+ iIntros (?) "Hinv". iMod (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
- iUpd (inv_open _ N with "[#]") as pat;
+ iMod (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 41025033312e617227f58a0a9fac466d74b4ece5..adad69e3166b214297925901e3fc022bd15be188 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. iUpd "H" as (σ1) "[% _]".
+ - iLeft. iExists v. iSplit. done. iMod "H" as (σ1) "[% _]".
by erewrite reducible_not_val in EQe1.
- iRight; iSplit; eauto.
- iIntros (σ1) "Hσ". iUpd "H" as (σ1') "(% & >Hσf & H)".
+ iIntros (σ1) "Hσ". iMod "H" as (σ1') "(% & >Hσf & H)".
iDestruct (ownP_agree σ1 σ1' with "[-]") as %<-; first by iFrame.
- iUpdIntro; iSplit; [done|]; iNext; iIntros (e2 σ2 efs Hstep).
- iUpd (ownP_update σ1 σ2 with "[-H]") as "[$ ?]"; first by iFrame.
+ iModIntro; iSplit; [done|]; iNext; iIntros (e2 σ2 efs Hstep).
+ iMod (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σ". iUpd (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
- iUpdIntro. iSplit; [done|]; iNext; iIntros (e2 σ2 efs ?).
+ iIntros (σ1) "Hσ". iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
+ iModIntro. iSplit; [done|]; iNext; iIntros (e2 σ2 efs ?).
destruct (Hstep σ1 e2 σ2 efs); auto; subst.
- iUpd "Hclose"; iUpdIntro. iFrame "Hσ". iApply "H"; auto.
+ iMod "Hclose"; iModIntro. 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).
- iUpd (fupd_intro_mask' E ∅) as "Hclose"; first set_solver. iUpdIntro.
+ iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver. iModIntro.
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.
- iUpd "Hclose". iUpd "HΦ". iApply wp_value; auto using to_of_val.
+ iMod "Hclose". iMod "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/sts.v b/program_logic/sts.v
index a6861685aca2252155617b78443988a10d5a1ebe..862d3a5c0836878df5d73d8e53cbcc21d04063bf 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.
- iUpd (own_alloc (sts_auth s (⊤ ∖ sts.tok s))) as (γ) "Hγ".
+ iMod (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γ $]".
- iUpd (inv_alloc N _ (sts_inv γ φ) with "[Hφ Hγ]") as "#?"; auto.
+ iMod (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 //.
- iUpdIntro; iExists s; iSplit; [done|]; iFrame "Hφ".
+ iModIntro; iExists s; iSplit; [done|]; iFrame "Hφ".
iIntros (s' T') "[% Hφ]".
- iUpd (own_update with "Hγ") as "Hγ"; first eauto using sts_update_auth.
+ iMod (own_update with "Hγ") as "Hγ"; first eauto using sts_update_auth.
iRevert "Hγ"; rewrite -sts_op_auth_frag_up; iIntros "[Hγ $]".
- iUpdIntro. iNext. iExists s'; by iFrame.
+ iModIntro. 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". *)
- 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").
+ iMod (sts_accS with "[Hinv Hγf]") as (s) "(?&?& HclSts)"; first by iFrame.
+ iModIntro. iExists s. iFrame. iIntros (s' T') "H".
+ iMod ("HclSts" $! s' T' with "H") as "(Hinv & ?)". by iMod ("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 7f389847c6b54a70ad71a0663be52de1d489e901..78c8a0bd6ccc573c5ceb2735fdbaf66a663723f0 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".
- iUpd (own_empty (A:=prodUR coPset_disjUR (gset_disjUR positive)) tid) as "Hempty".
- iUpd (own_updateP with "Hempty") as ([m1 m2]) "[Hm Hown]".
+ iMod (own_empty (A:=prodUR coPset_disjUR (gset_disjUR positive)) tid) as "Hempty".
+ iMod (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.
- iUpd (inv_alloc tlN with "[-]"); last (iUpdIntro; iExists i; eauto).
+ iMod (inv_alloc tlN with "[-]"); last (iModIntro; iExists i; eauto).
iNext. iLeft. by iFrame.
Qed.
@@ -80,8 +80,8 @@ 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".
- - iUpd ("Hclose" with "[Htoki]") as "_"; first auto.
- iIntros "!==>[HP $]".
+ - iMod ("Hclose" with "[Htoki]") as "_"; first auto.
+ iIntros "!> [HP $]".
iInv tlN as "[[_ >Hdis2]|>Hitok]" "Hclose".
+ iCombine "Hdis" "Hdis2" as "Hdis".
iDestruct (own_valid with "Hdis") as %[_ Hval%gset_disj_valid_op].
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index defadd5c1b797331b57e6fdeb999c60d28795b6f..d1cdf24f4d8a4537172243f773fcf3d1925708e9 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -54,7 +54,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".
- iUpd ("HvsP" with "HP") as "HQ". by iApply "HvsQ".
+ iMod ("HvsP" with "HP") as "HQ". by iApply "HvsQ".
Qed.
Lemma vs_reflexive E P : P ={E}=> P.
@@ -79,7 +79,7 @@ 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".
- iUpd ("Hvs" with "[HR HP]") as "[? $]"; first by iFrame.
+ iMod ("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 2bdd6f6583d5e5d798ee28c87901a0faacfaf60d..791eab9f05e7a97e4de36d0b1aa6c09fdffcb03c 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -94,22 +94,22 @@ 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 (fupd_mask_mono E1 _). }
+ iApply ("HΦ" with ">[-]"). by iApply (fupd_mask_mono E1 _). }
iSplit; [done|]; iIntros (σ1) "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Φ").
+ iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
+ iMod ("H" $! σ1 with "Hσ") as "[$ H]".
+ iModIntro. iNext. iIntros (e2 σ2 efs Hstep).
+ iMod ("H" $! _ σ2 efs with "[#]") as "($ & H & $)"; auto.
+ iMod "Hclose" as "_". by iApply ("IH" with "HΦ").
Qed.
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 iUpd "H" as "[H|[% ?]]"; [iDestruct "H" as (v') "[% ?]"|]; simplify_eq. }
+ by iMod "H" as "[H|[% ?]]"; [iDestruct "H" as (v') "[% ?]"|]; simplify_eq. }
iRight; iSplit; [done|]; iIntros (σ1) "Hσ1".
- iUpd "H" as "[H|[% H]]"; last by iApply "H".
+ iMod "H" as "[H|[% H]]"; last by iApply "H".
iDestruct "H" as (v') "[% ?]"; simplify_eq.
Qed.
Lemma wp_fupd E e Φ : WP e @ E {{ v, |={E}=> Φ v }} ⊢ WP e @ E {{ Φ }}.
@@ -121,15 +121,15 @@ Lemma wp_atomic E1 E2 e Φ :
Proof.
iIntros (Hatomic) "H". destruct (to_val e) as [v|] eqn:He.
{ apply of_to_val in He as <-. iApply wp_fupd. iApply wp_value'.
- iUpd "H". by iUpd (wp_value_inv with "H"). }
+ iMod "H". by iMod (wp_value_inv with "H"). }
setoid_rewrite wp_unfold; rewrite /wp_pre. iRight; iSplit; auto.
- iIntros (σ1) "Hσ". iUpd "H" as "[H|[_ H]]".
+ iIntros (σ1) "Hσ". iMod "H" as "[H|[_ H]]".
{ iDestruct "H" as (v') "[% ?]"; simplify_eq. }
- iUpd ("H" $! σ1 with "Hσ") as "[$ H]".
- iUpdIntro. iNext. iIntros (e2 σ2 efs Hstep).
+ iMod ("H" $! σ1 with "Hσ") as "[$ H]".
+ iModIntro. iNext. iIntros (e2 σ2 efs Hstep).
destruct (Hatomic _ _ _ _ Hstep) as [v <-%of_to_val].
- iUpd ("H" $! _ σ2 efs with "[#]") as "($ & H & $)"; auto.
- iUpd (wp_value_inv with "H") as "==> H". by iApply wp_value'.
+ iMod ("H" $! _ σ2 efs with "[#]") as "($ & H & $)"; auto.
+ iMod (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σ".
- 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.
+ iMod "HR". iMod ("H" $! _ with "Hσ") as "[$ H]".
+ iModIntro; iNext; iIntros (e2 σ2 efs Hstep).
+ iMod ("H" $! e2 σ2 efs with "[%]") as "($ & H & $)"; auto.
+ iMod "HR". iModIntro. iApply (wp_strong_mono E2 _ _ Φ); try iFrame; eauto.
Qed.
Lemma wp_bind K `{!LanguageCtx Λ K} E e Φ :
@@ -153,12 +153,12 @@ Proof.
{ iDestruct "Hv" as (v) "[Hev Hv]"; iDestruct "Hev" as % <-%of_to_val.
by iApply fupd_wp. }
rewrite wp_unfold /wp_pre. iRight; iSplit; eauto using fill_not_val.
- iIntros (σ1) "Hσ". iUpd ("H" $! _ with "Hσ") as "[% H]".
- iUpdIntro; iSplit.
+ iIntros (σ1) "Hσ". iMod ("H" $! _ with "Hσ") as "[% H]".
+ iModIntro; 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.
- iUpd ("H" $! e2' σ2 efs with "[%]") as "($ & H & $)"; auto.
+ iMod ("H" $! e2' σ2 efs with "[%]") as "($ & H & $)"; auto.
by iApply "IH".
Qed.
@@ -225,18 +225,18 @@ Section proofmode_classes.
Global Instance is_except_0_wp E e Φ : IsExcept0 (WP e @ E {{ Φ }}).
Proof. by rewrite /IsExcept0 -{2}fupd_wp -except_0_fupd -fupd_intro. Qed.
- Global Instance elim_upd_bupd_wp E e P Φ :
- ElimUpd (|==> 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_modal_bupd_wp E e P Φ :
+ ElimModal (|==> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
+ Proof. by rewrite /ElimModal (bupd_fupd E) fupd_frame_r wand_elim_r fupd_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.
+ Global Instance elim_modal_fupd_wp E e P Φ :
+ ElimModal (|={E}=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
+ Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_wp. Qed.
(* lower precedence, if possible, it should always pick elim_upd_fupd_wp *)
- Global Instance elim_upd_fupd_wp_atomic E1 E2 e P Φ :
+ Global Instance elim_modal_fupd_wp_atomic E1 E2 e P Φ :
atomic e →
- ElimUpd (|={E1,E2}=> P) P
+ ElimModal (|={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.
+ Proof. intros. by rewrite /ElimModal 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 3315aa66830fd16ae666fd078c1edfa6b80c4bd2..d10e72dea41913b0c5a5cc38ac68a8a017fc897a 100644
--- a/program_logic/wsat.v
+++ b/program_logic/wsat.v
@@ -46,11 +46,11 @@ Lemma iris_alloc `{irisPreG Λ Σ} σ :
True ==★ ∃ _ : irisG Λ Σ, wsat ★ ownE ⊤ ★ ownP_auth σ ★ ownP σ.
Proof.
iIntros.
- 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).
+ iMod (own_alloc (◠(Excl' σ) ⋅ ◯ (Excl' σ))) as (γσ) "[Hσ Hσ']"; first done.
+ iMod (own_alloc (◠(∅ : gmap _ _))) as (γI) "HI"; first done.
+ iMod (own_alloc (CoPset ⊤)) as (γE) "HE"; first done.
+ iMod (own_alloc (GSet ∅)) as (γD) "HD"; first done.
+ iModIntro; iExists (IrisG _ _ _ γσ γI γE γD).
rewrite /wsat /ownE /ownP_auth /ownP; iFrame.
iExists ∅. rewrite fmap_empty big_sepM_empty. by iFrame.
Qed.
@@ -155,17 +155,17 @@ Lemma ownI_alloc φ P :
wsat ★ ▷ P ==★ ∃ i, ■(φ i) ★ wsat ★ ownI i P.
Proof.
iIntros (Hfresh) "[Hw HP]". iDestruct "Hw" as (I) "[? HI]".
- iUpd (own_empty (A:=gset_disjUR positive) disabled_name) as "HE".
- iUpd (own_updateP with "HE") as "HE".
+ iMod (own_empty (A:=gset_disjUR positive) disabled_name) as "HE".
+ iMod (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 & ?).
- iUpd (own_update with "Hw") as "[Hw HiP]".
+ iMod (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. }
- iUpdIntro; iExists i; iSplit; [done|]. rewrite /ownI; iFrame "HiP".
+ iModIntro; 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 19f5d49cd38eeb5d47a87cc95601682bd1ca06b2..85add1c7132a0cba555c11a1a7f60d2ed71e2e13 100644
--- a/proofmode/class_instances.v
+++ b/proofmode/class_instances.v
@@ -357,13 +357,30 @@ Global Instance into_exist_always {A} P (Φ : A → uPred M) :
IntoExist P Φ → IntoExist (□ P) (λ a, □ (Φ a))%I.
Proof. rewrite /IntoExist=> HP. by rewrite HP always_exist. Qed.
-(* IntoExcept0 *)
-Global Instance into_except_0_except_0 P : IntoExcept0 (â—‡ P) P.
-Proof. done. Qed.
-Global Instance into_except_0_timeless P : TimelessP P → IntoExcept0 (▷ P) P.
-Proof. done. Qed.
+(* IntoModal *)
+Global Instance into_modal_later P : IntoModal P (â–· P).
+Proof. apply later_intro. Qed.
+Global Instance into_modal_bupd P : IntoModal P (|==> P).
+Proof. apply bupd_intro. Qed.
+Global Instance into_modal_except_0 P : IntoModal P (â—‡ P).
+Proof. apply except_0_intro. Qed.
+
+(* ElimModal *)
+Global Instance elim_modal_bupd P Q : ElimModal (|==> P) P (|==> Q) (|==> Q).
+Proof. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_trans. Qed.
+
+Global Instance elim_modal_except_0 P Q : IsExcept0 Q → ElimModal (◇ P) P Q Q.
+Proof.
+ intros. rewrite /ElimModal (except_0_intro (_ -★ _)).
+ by rewrite -except_0_sep wand_elim_r.
+Qed.
+Global Instance elim_modal_timeless_bupd P Q :
+ TimelessP P → IsExcept0 Q → ElimModal (▷ P) P Q Q.
+Proof.
+ intros. rewrite /ElimModal (except_0_intro (_ -★ _)) (timelessP P).
+ by rewrite -except_0_sep wand_elim_r.
+Qed.
-(* IsExcept0 *)
Global Instance is_except_0_except_0 P : IsExcept0 (â—‡ P).
Proof. by rewrite /IsExcept0 except_0_idemp. Qed.
Global Instance is_except_0_later P : IsExcept0 (â–· P).
@@ -373,12 +390,4 @@ Proof.
rewrite /IsExcept0=> HP.
by rewrite -{2}HP -(except_0_idemp P) -except_0_bupd -(except_0_intro P).
Qed.
-
-(* FromUpd *)
-Global Instance from_upd_bupd P : FromUpd (|==> P) P.
-Proof. done. Qed.
-
-(* ElimVs *)
-Global Instance elim_upd_bupd_bupd P Q : ElimUpd (|==> P) P (|==> Q) (|==> 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 fae732c160a9d9ff2f2f55455f6e88130b1ccad4..e40a68362c76c0bdd34b335b7de2bad6bd1456a2 100644
--- a/proofmode/classes.v
+++ b/proofmode/classes.v
@@ -62,19 +62,16 @@ Class IntoExist {A} (P : uPred M) (Φ : A → uPred M) :=
into_exist : P ⊢ ∃ x, Φ x.
Global Arguments into_exist {_} _ _ {_}.
-Class IntoExcept0 (P Q : uPred M) := into_except_0 : P ⊢ ◇ Q.
-Global Arguments into_except_0 : clear implicits.
+Class IntoModal (P Q : uPred M) := into_modal : P ⊢ Q.
+Global Arguments into_modal : clear implicits.
-Class IsExcept0 (Q : uPred M) := is_except_0 : ◇ Q ⊢ Q.
-Global Arguments is_except_0 : clear implicits.
-
-Class FromUpd (P Q : uPred M) := from_upd : (|==> Q) ⊢ P.
-Global Arguments from_upd : clear implicits.
+Class ElimModal (P P' : uPred M) (Q Q' : uPred M) :=
+ elim_modal : P ★ (P' -★ Q') ⊢ Q.
+Global Arguments elim_modal _ _ _ _ {_}.
-Class ElimUpd (P P' : uPred M) (Q Q' : uPred M) :=
- elim_upd : P ★ (P' -★ Q') ⊢ Q.
-Global Arguments elim_upd _ _ _ _ {_}.
+Lemma elim_modal_dummy P Q : ElimModal P P Q Q.
+Proof. by rewrite /ElimModal wand_elim_r. Qed.
-Lemma elim_upd_dummy P Q : ElimUpd P P Q Q.
-Proof. by rewrite /ElimUpd wand_elim_r. Qed.
+Class IsExcept0 (Q : uPred M) := is_except_0 : ◇ Q ⊢ Q.
+Global Arguments is_except_0 : clear implicits.
End classes.
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index a3bc5266817a0a149ecc47bc2258fb941efa86d9..f55b0e46e997ae55f057540078c33ed6261b2f7a 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -445,17 +445,6 @@ Proof.
by rewrite right_id always_and_sep_l' wand_elim_r HQ.
Qed.
-Lemma tac_timeless Δ Δ' i p P P' Q :
- IsExcept0 Q →
- envs_lookup i Δ = Some (p, P) → IntoExcept0 P P' →
- envs_simple_replace i p (Esnoc Enil i P') Δ = Some Δ' →
- (Δ' ⊢ Q) → Δ ⊢ Q.
-Proof.
- intros ???? HQ. rewrite envs_simple_replace_sound //; simpl.
- rewrite right_id HQ -{2}(is_except_0 Q).
- by rewrite (into_except_0 P) -except_0_always_if except_0_frame_r wand_elim_r.
-Qed.
-
(** * Always *)
Lemma tac_always_intro Δ Q : env_spatial_is_nil Δ = true → (Δ ⊢ Q) → Δ ⊢ □ Q.
Proof. intros. by apply (always_intro _ _). Qed.
@@ -533,7 +522,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 → ElimUpd P1' P1 Q Q →
+ IntoWand R P1 P2 → ElimModal 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 +534,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_upd P1' P1 Q Q). apply sep_mono_r, wand_intro_l.
+ rewrite -(elim_modal P1' P1 Q Q). apply sep_mono_r, wand_intro_l.
by rewrite always_if_elim assoc !wand_elim_r.
Qed.
@@ -607,7 +596,7 @@ Proof.
Qed.
Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P P' Q :
- ElimUpd P' P Q Q →
+ ElimModal 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 +817,17 @@ Proof.
rewrite envs_simple_replace_sound' //; simpl. by rewrite right_id wand_elim_r.
Qed.
-(** * Update modality *)
-Lemma tac_upd_intro Δ P Q : FromUpd P Q → (Δ ⊢ Q) → Δ ⊢ P.
-Proof. rewrite /FromUpd. intros <- ->. apply bupd_intro. Qed.
+(** * Modalities *)
+Lemma tac_modal_intro Δ P Q : IntoModal Q P → (Δ ⊢ Q) → Δ ⊢ P.
+Proof. rewrite /IntoModal. by intros <- ->. Qed.
-Lemma tac_upd_elim Δ Δ' i p P' P Q Q' :
+Lemma tac_modal_elim Δ Δ' i p P' P Q Q' :
envs_lookup i Δ = Some (p, P) →
- ElimUpd P P' Q Q' →
+ ElimModal 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_upd.
+ rewrite right_id HΔ always_if_elim. by apply elim_modal.
Qed.
End tactics.
diff --git a/proofmode/intro_patterns.v b/proofmode/intro_patterns.v
index f7f4d711bbc8f247492dcc761824fe40a4ccfd88..bbb58d62aee652748fb81cdc917a3f2dde76d4bd 100644
--- a/proofmode/intro_patterns.v
+++ b/proofmode/intro_patterns.v
@@ -8,12 +8,10 @@ Inductive intro_pat :=
| IList : list (list intro_pat) → intro_pat
| IPureElim : intro_pat
| IAlwaysElim : intro_pat → intro_pat
- | ILaterElim : intro_pat → intro_pat
- | IUpdElim : intro_pat → intro_pat
+ | IModalElim : intro_pat → intro_pat
| IPureIntro : intro_pat
| IAlwaysIntro : intro_pat
- | ILaterIntro : intro_pat
- | IUpdIntro : intro_pat
+ | IModalIntro : intro_pat
| ISimpl : intro_pat
| IForall : intro_pat
| IAll : intro_pat
@@ -23,7 +21,6 @@ Fixpoint intro_pat_persistent (p : intro_pat) :=
match p with
| IPureElim => true
| IAlwaysElim _ => true
- | ILaterElim p => intro_pat_persistent p
| IList pps => forallb (forallb intro_pat_persistent) pps
| _ => false
end.
@@ -42,12 +39,10 @@ Inductive token :=
| TParenR : token
| TPureElim : token
| TAlwaysElim : token
- | TLaterElim : token
- | TUpdElim : token
+ | TModalElim : token
| TPureIntro : token
| TAlwaysIntro : token
- | TLaterIntro : token
- | TUpdIntro : token
+ | TModalIntro : token
| TSimpl : token
| TForall : token
| TAll : token
@@ -71,14 +66,10 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
| String "&" s => tokenize_go s (TAmp :: cons_name kn k) ""
| String "%" s => tokenize_go s (TPureElim :: cons_name kn k) ""
| 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 (TUpdElim :: cons_name kn k) ""
+ | String ">" s => tokenize_go s (TModalElim :: 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 (TUpdIntro :: cons_name kn k) ""
+ | String "!" (String ">" s) => tokenize_go s (TModalIntro :: 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) ""
@@ -95,8 +86,7 @@ Inductive stack_item :=
| SBar : stack_item
| SAmp : stack_item
| SAlwaysElim : stack_item
- | SLaterElim : stack_item
- | SUpdElim : stack_item.
+ | SModalElim : stack_item.
Notation stack := (list stack_item).
Fixpoint close_list (k : stack)
@@ -106,10 +96,8 @@ Fixpoint close_list (k : stack)
| SPat pat :: k => close_list k (pat :: ps) pss
| SAlwaysElim :: k =>
'(p,ps) ↠maybe2 (::) ps; close_list k (IAlwaysElim p :: ps) pss
- | SLaterElim :: k =>
- '(p,ps) ↠maybe2 (::) ps; close_list k (ILaterElim p :: ps) pss
- | SUpdElim :: k =>
- '(p,ps) ↠maybe2 (::) ps; close_list k (IUpdElim p :: ps) pss
+ | SModalElim :: k =>
+ '(p,ps) ↠maybe2 (::) ps; close_list k (IModalElim p :: ps) pss
| SBar :: k => close_list k [] (ps :: pss)
| _ => None
end.
@@ -132,8 +120,7 @@ Fixpoint close_conj_list (k : stack)
Some (SPat (big_conj ps) :: k)
| 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
- | SUpdElim :: k => p ↠cur; close_conj_list k (Some (IUpdElim p)) ps
+ | SModalElim :: k => p ↠cur; close_conj_list k (Some (IModalElim p)) ps
| SAmp :: k => p ↠cur; close_conj_list k None (p :: ps)
| _ => None
end.
@@ -153,12 +140,10 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
| TParenR :: ts => close_conj_list k None [] ≫= parse_go ts
| TPureElim :: ts => parse_go ts (SPat IPureElim :: k)
| TAlwaysElim :: ts => parse_go ts (SAlwaysElim :: k)
- | TLaterElim :: ts => parse_go ts (SLaterElim :: k)
- | TUpdElim :: ts => parse_go ts (SUpdElim :: k)
+ | TModalElim :: ts => parse_go ts (SModalElim :: 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)
- | TUpdIntro :: ts => parse_go ts (SPat IUpdIntro :: k)
+ | TModalIntro :: ts => parse_go ts (SPat IModalIntro :: 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 6be7eafce7c817fc96c2a7a30893371af653234f..eb9e9dc3b0eb072ab2d64445553b7d4fbbb0dd5e 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_update : bool;
+ spec_goal_modal : 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
- | TUpd : token
+ | TModal : 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 (TUpd :: cons_name kn k) ""
+ | String ">" s => tokenize_go s (TModal :: 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
- | TUpd :: TBracketL :: ts => parse_goal ts (SpecGoal true false [] []) k
- | TUpd :: ts => parse_go ts (SGoal (SpecGoal true true [] []) :: k)
+ | TModal :: TBracketL :: ts => parse_goal ts (SpecGoal true false [] []) k
+ | TModal :: 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_update g) true
+ parse_goal ts (SpecGoal (spec_goal_modal g) true
(spec_goal_frame g) (spec_goal_hyps g)) k
| TName s :: ts =>
- parse_goal ts (SpecGoal (spec_goal_update g) (spec_goal_negate g)
+ parse_goal ts (SpecGoal (spec_goal_modal 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_update g) (spec_goal_negate g)
+ parse_goal ts (SpecGoal (spec_goal_modal g) (spec_goal_negate g)
(s :: spec_goal_frame g) (spec_goal_hyps g)) k
| TBracketR :: ts =>
- parse_go ts (SGoal (SpecGoal (spec_goal_update g) (spec_goal_negate g)
+ parse_go ts (SGoal (SpecGoal (spec_goal_modal 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 047d9bb86cfc4102e5802252a5b8fe969d8c1124..1f449b36ab698c6e6ff65dde25d9188ec635e860 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -307,13 +307,13 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
|env_cbv; reflexivity
|(*goal*)
|go H1 pats]
- | SGoal (SpecGoal ?vs ?lr ?Hs_frame ?Hs) :: ?pats =>
+ | SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs) :: ?pats =>
eapply tac_specialize_assert with _ _ _ H1 _ lr (Hs_frame ++ Hs) _ _ _ _;
[env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
|solve_to_wand H1
- |match vs with
- | false => apply elim_upd_dummy
- | true => apply _ || fail "iSpecialize: goal not an update modality"
+ |match m with
+ | false => apply elim_modal_dummy
+ | true => apply _ || fail "iSpecialize: goal not a modality"
end
|env_cbv; reflexivity || fail "iSpecialize:" Hs "not found"
|iFrame Hs_frame (*goal*)
@@ -610,28 +610,18 @@ Tactic Notation "iNext":=
|let P := match goal with |- FromLater ?P _ => P end in
apply _ || fail "iNext:" P "does not contain laters"|].
-Tactic Notation "iTimeless" constr(H) :=
- eapply tac_timeless with _ H _ _ _;
- [let Q := match goal with |- IsExcept0 ?Q => Q end in
- apply _ || fail "iTimeless: cannot remove later when goal is" Q
- |env_cbv; reflexivity || fail "iTimeless:" H "not found"
- |let P := match goal with |- IntoExcept0 ?P _ => P end in
- apply _ || fail "iTimeless: cannot turn" P "into â—‡"
- |env_cbv; reflexivity|].
-
(** * 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"
+Tactic Notation "iModIntro" :=
+ eapply tac_modal_intro;
+ [let P := match goal with |- IntoModal _ ?P => P end in
+ apply _ || fail "iModIntro:" P "not a modality"|].
+
+Tactic Notation "iModCore" constr(H) :=
+ eapply tac_modal_elim with _ H _ _ _ _;
+ [env_cbv; reflexivity || fail "iMod:" H "not found"
+ |let P := match goal with |- ElimModal ?P _ _ _ => P end in
+ let Q := match goal with |- ElimModal _ _ ?Q _ => Q end in
+ apply _ || fail "iMod: cannot eliminate modality " P "in" Q
|env_cbv; reflexivity|].
(** * Basic destruct tactic *)
@@ -650,8 +640,7 @@ Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
| IList [[?pat1];[?pat2]] => iOrDestruct Hz as Hz Hz; [go Hz pat1|go Hz pat2]
| IPureElim => iPure Hz as ?
| IAlwaysElim ?pat => iPersistent Hz; go Hz pat
- | ILaterElim ?pat => iTimeless Hz; go Hz pat
- | IUpdElim ?pat => iUpdCore Hz; go Hz pat
+ | IModalElim ?pat => iModCore Hz; go Hz pat
| _ => fail "iDestruct:" pat "invalid"
end
in let pat := intro_pat.parse_one pat in go H pat.
@@ -749,8 +738,7 @@ Tactic Notation "iIntros" constr(pat) :=
| IName ?H :: ?pats => iIntro H; go pats
| IPureIntro :: ?pats => iPureIntro; go pats
| IAlwaysIntro :: ?pats => iAlways; go pats
- | ILaterIntro :: ?pats => iNext; go pats
- | IUpdIntro :: ?pats => iUpdIntro; go pats
+ | IModalIntro :: ?pats => iModIntro; go pats
| ISimpl :: ?pats => simpl; go pats
| IForall :: ?pats => repeat iIntroForall; go pats
| IAll :: ?pats => repeat (iIntroForall || iIntro); go pats
@@ -1096,11 +1084,11 @@ Tactic Notation "iAssertCore" open_constr(Q) "with" constr(Hs) "as" tactic(tac)
|(*goal*)
|apply _ || fail "iAssert:" Q "not persistent"
|tac H]
- | [SGoal (SpecGoal ?vs ?lr ?Hs_frame ?Hs)] =>
+ | [SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs)] =>
eapply tac_assert with _ _ _ lr (Hs_frame ++ Hs) H Q _;
- [match vs with
- | false => apply elim_upd_dummy
- | true => apply _ || fail "iAssert: goal not an update modality"
+ [match m with
+ | false => apply elim_modal_dummy
+ | true => apply _ || fail "iAssert: goal not a modality"
end
|env_cbv; reflexivity || fail "iAssert:" Hs "not found"
|env_cbv; reflexivity
@@ -1164,49 +1152,49 @@ Ltac iSimplifyEq := repeat (
|| simplify_eq/=).
(** * 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) ")"
+Tactic Notation "iMod" open_constr(lem) :=
+ iDestructCore lem as false (fun H => iModCore H).
+Tactic Notation "iMod" open_constr(lem) "as" constr(pat) :=
+ iDestructCore lem as false (fun H => iModCore H; last iDestructHyp H as pat).
+Tactic Notation "iMod" open_constr(lem) "as" "(" simple_intropattern(x1) ")"
constr(pat) :=
- iDestructCore lem as false (fun H => iUpdCore H; last iDestructHyp H as ( x1 ) pat).
-Tactic Notation "iUpd" open_constr(lem) "as" "(" simple_intropattern(x1)
+ iDestructCore lem as false (fun H => iModCore H; last iDestructHyp H as ( x1 ) pat).
+Tactic Notation "iMod" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) ")" constr(pat) :=
- 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)
+ iDestructCore lem as false (fun H => iModCore H; last iDestructHyp H as ( x1 x2 ) pat).
+Tactic Notation "iMod" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
- 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)
+ iDestructCore lem as false (fun H => iModCore H; last iDestructHyp H as ( x1 x2 x3 ) pat).
+Tactic Notation "iMod" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
constr(pat) :=
iDestructCore lem as false (fun H =>
- iUpdCore H; last iDestructHyp H as ( x1 x2 x3 x4 ) pat).
-Tactic Notation "iUpd" open_constr(lem) "as" "(" simple_intropattern(x1)
+ iModCore H; last iDestructHyp H as ( x1 x2 x3 x4 ) pat).
+Tactic Notation "iMod" 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 =>
- iUpdCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 ) pat).
-Tactic Notation "iUpd" open_constr(lem) "as" "(" simple_intropattern(x1)
+ iModCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 ) pat).
+Tactic Notation "iMod" 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 =>
- iUpdCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 x6 ) pat).
-Tactic Notation "iUpd" open_constr(lem) "as" "(" simple_intropattern(x1)
+ iModCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 x6 ) pat).
+Tactic Notation "iMod" 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 =>
- iUpdCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
-Tactic Notation "iUpd" open_constr(lem) "as" "(" simple_intropattern(x1)
+ iModCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
+Tactic Notation "iMod" 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 =>
- iUpdCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
+ iModCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
-Tactic Notation "iUpd" open_constr(lem) "as" "%" simple_intropattern(pat) :=
- iDestructCore lem as false (fun H => iUpdCore H; iPure H as pat).
+Tactic Notation "iMod" open_constr(lem) "as" "%" simple_intropattern(pat) :=
+ iDestructCore lem as false (fun H => iModCore 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 +1211,7 @@ Hint Extern 1 (of_envs _ ⊢ _) =>
| |- _ ⊢ ▷ _ => iNext
| |- _ ⊢ □ _ => iClear "*"; iAlways
| |- _ ⊢ ∃ _, _ => iExists _
- | |- _ ⊢ |==> _ => iUpdIntro
+ | |- _ ⊢ |==> _ => iModIntro
end.
Hint Extern 1 (of_envs _ ⊢ _) =>
match goal with |- _ ⊢ (_ ∨ _)%I => iLeft end.
diff --git a/tests/atomic.v b/tests/atomic.v
index 151517dbb81a81f98dc0cf6dc2a1d8ca2cd35bd3..985169b6a43a3af037799331e88b793fa945ff93 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -75,22 +75,22 @@ Section incr.
iIntros "!# HP".
wp_rec.
wp_bind (! _)%E.
- iUpd ("Hvs" with "HP") as (x) "[Hl [Hvs' _]]".
+ iMod ("Hvs" with "HP") as (x) "[Hl [Hvs' _]]".
wp_load.
- iUpd ("Hvs'" with "Hl") as "HP".
- iUpdIntro. wp_let. wp_bind (CAS _ _ _). wp_op.
- iUpd ("Hvs" with "HP") as (x') "[Hl Hvs']".
+ iMod ("Hvs'" with "Hl") as "HP".
+ iModIntro. wp_let. wp_bind (CAS _ _ _). wp_op.
+ iMod ("Hvs" with "HP") as (x') "[Hl Hvs']".
destruct (decide (x = x')).
- subst.
iDestruct "Hvs'" as "[_ Hvs']".
iSpecialize ("Hvs'" $! #x').
wp_cas_suc.
- iUpd ("Hvs'" with "[Hl]") as "HQ"; first by iFrame.
- iUpdIntro. wp_if. iUpdIntro. by iExists x'.
+ iMod ("Hvs'" with "[Hl]") as "HQ"; first by iFrame.
+ iModIntro. wp_if. iModIntro. by iExists x'.
- iDestruct "Hvs'" as "[Hvs' _]".
wp_cas_fail.
- iUpd ("Hvs'" with "[Hl]") as "HP"; first by iFrame.
- iUpdIntro. wp_if. by iApply "IH".
+ iMod ("Hvs'" with "[Hl]") as "HP"; first by iFrame.
+ iModIntro. wp_if. by iApply "IH".
Qed.
End incr.
@@ -112,7 +112,7 @@ Section user.
rewrite /incr_2.
wp_let.
wp_alloc l as "Hl".
- iUpd (inv_alloc N _ (∃x':Z, l ↦ #x')%I with "[Hl]") as "#?"; first eauto.
+ iMod (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 *)
- iUpd (fupd_intro_mask' _ heapN) as "Hclose'".
+ iMod (fupd_intro_mask' _ heapN) as "Hclose'".
{ apply ndisj_subseteq_difference; auto. }
- iUpdIntro. iExists x'. iFrame "Hl'". iSplit.
+ iModIntro. iExists x'. iFrame "Hl'". iSplit.
+ (* provide a way to rollback *)
iIntros "Hl'".
- iUpd "Hclose'". iUpd ("Hclose" with "[Hl']"); eauto.
+ iMod "Hclose'". iMod ("Hclose" with "[Hl']"); eauto.
+ (* provide a way to commit *)
iIntros (v) "[Heq Hl']".
- iUpd "Hclose'". iUpd ("Hclose" with "[Hl']"); eauto.
+ iMod "Hclose'". iMod ("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 8fab9362ddcdb37005714f9d3986d70ed925e4d2..67a78210009786ad462a1b5f91f026c9492a119e 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"). }
- iUpd (recv_split with "Hr") as "[H1 H2]"; first done.
+ iMod (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 935e1e136c603d1178a8eb4f30a94c8f8a4b5c87..8661b9b398eacd56c8f02234435684e6cb4848e2 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".
- iUpd (own_alloc (Auth 0)) as (γ) "Hγ"; first done.
+ iMod (own_alloc (Auth 0)) as (γ) "Hγ"; first done.
rewrite (auth_frag_op 0 0) //; iDestruct "Hγ" as "[Hγ Hγf]".
- iUpd (inv_alloc N _ (I γ l) with "[Hl Hγ]") as "#?".
+ iMod (inv_alloc N _ (I γ l) with "[Hl Hγ]") as "#?".
{ iIntros "!>". iExists 0%nat. by iFrame. }
- iUpdIntro. rewrite /C; eauto 10.
+ iModIntro. 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. iUpd ("Hclose" with "[Hl Hγ]"); [iNext; iExists c; by iFrame|].
- iUpdIntro. wp_let. wp_op.
+ wp_load. iMod ("Hclose" with "[Hl Hγ]"); [iNext; iExists c; by iFrame|].
+ iModIntro. 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 //.
- iUpd (own_update with "Hγ") as "Hγ"; first apply M_update.
+ iMod (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. iUpd ("Hclose" with "[Hl Hγ]").
+ wp_cas_suc. iMod ("Hclose" with "[Hl Hγ]").
{ iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
- iUpdIntro. wp_if. iUpdIntro; rewrite {3}/C; eauto 10.
+ iModIntro. wp_if. iModIntro; rewrite {3}/C; eauto 10.
- wp_cas_fail; first (intros [=]; abstract omega).
- iUpd ("Hclose" with "[Hl Hγ]"); [iNext; iExists c'; by iFrame|].
- iUpdIntro. wp_if. iApply ("IH" with "[Hγf]"). rewrite {3}/C; eauto 10.
+ iMod ("Hclose" with "[Hl Hγ]"); [iNext; iExists c'; by iFrame|].
+ iModIntro. 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']".
- iUpd ("Hclose" with "[Hl Hγ]"); [iNext; iExists c; by iFrame|].
- iUpdIntro; rewrite /C; eauto 10 with omega.
+ iMod ("Hclose" with "[Hl Hγ]"); [iNext; iExists c; by iFrame|].
+ iModIntro; rewrite /C; eauto 10 with omega.
Qed.
End proof.
diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index dc693644d5da3e2d1677afad1f968b8dc4759d57..6081ff86439194d8576eb217c2b56fbc4064ec51 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.
- iUpd (own_alloc (Pending : one_shotR Σ F)) as (γ) "Hγ"; first done.
+ iMod (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.
- iUpd (own_update with "Hγ") as "Hx".
+ iMod (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.
- iUpd (recv_split with "Hr") as "[H1 H2]"; first done.
+ iMod (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 1f95e90600b70f9cbeff469f93fba0ef12266233..a7e8cc36440914c1c3484c4e153456705efae443 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.
- iUpd (own_alloc Pending) as (γ) "Hγ"; first done.
- iUpd (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN".
+ iMod (own_alloc Pending) as (γ) "Hγ"; first done.
+ iMod (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN".
{ iNext. iLeft. by iSplitL "Hl". }
- iUpdIntro. iApply "Hf"; iSplit.
+ iModIntro. iApply "Hf"; iSplit.
- iIntros (n) "!#". wp_let.
iInv N as ">[[Hl Hγ]|H]" "Hclose"; last iDestruct "H" as (m) "[Hl Hγ]".
- + wp_cas_suc. iUpd (own_update with "Hγ") as "Hγ".
+ + wp_cas_suc. iMod (own_update with "Hγ") as "Hγ".
{ by apply cmra_update_exclusive with (y:=Shot n). }
- iUpd ("Hclose" with "[-]"); last eauto.
+ iMod ("Hclose" with "[-]"); last eauto.
iNext; iRight; iExists n; by iFrame.
- + wp_cas_fail. iUpd ("Hclose" with "[-]"); last eauto.
+ + wp_cas_fail. iMod ("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. }
- iUpd ("Hclose" with "[Hinv]") as "_"; eauto; iUpdIntro.
- wp_let. iUpdIntro. iIntros "!#". wp_seq.
+ iMod ("Hclose" with "[Hinv]") as "_"; eauto; iModIntro.
+ wp_let. iModIntro. 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.
- iUpd ("Hclose" with "[Hl]") as "_".
+ iMod ("Hclose" with "[Hl]") as "_".
{ iNext; iRight; by eauto. }
- iUpdIntro. wp_match. iApply wp_assert. wp_op=>?; simplify_eq/=; eauto.
+ iModIntro. wp_match. iApply wp_assert. wp_op=>?; simplify_eq/=; eauto.
Qed.
Lemma ht_one_shot (Φ : val → iProp Σ) :
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 73f1f0a830b892dfdbe97822d260c58ef89c7d36..f3c087059015d0818d47b17f80c6c5b05d28e114 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -94,7 +94,7 @@ Section iris.
(True -★ P -★ inv N Q -★ True -★ R) ⊢ P -★ ▷ Q ={E}=★ R.
Proof.
iIntros (?) "H HP HQ".
- iApply ("H" with "[#] HP ==>[HQ] ==>").
+ iApply ("H" with "[#] HP >[HQ] >").
- done.
- by iApply inv_alloc.
- done.