From 1b619ec7ce89abba241000fa8048c122f9b02914 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 14 Feb 2018 11:31:20 +0100
Subject: [PATCH] Bump Iris.
---
opam | 2 +-
theories/examples/circ_buffer.v | 19 +++++-----
theories/examples/hashtable.v | 6 ++--
theories/examples/message_passing.v | 5 ++-
theories/examples/msqueue.v | 5 ++-
theories/examples/ticket_lock.v | 8 ++---
theories/gps/fractional.v | 18 +++++-----
theories/gps/plain.v | 14 ++++----
theories/gps/singlewriter.v | 28 +++++++--------
theories/weakestpre.v | 54 ++---------------------------
theories/wp_tactics.v | 6 ++--
theories/wp_tactics_vProp.v | 6 ++--
12 files changed, 59 insertions(+), 112 deletions(-)
diff --git a/opam b/opam
index 83b7b9d2..a960912f 100644
--- a/opam
+++ b/opam
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/igps" ]
depends: [
- "coq-iris" { (= "branch.gen_proofmode.2018-02-06.3") | (= "dev") }
+ "coq-iris" { (= "branch.gen_proofmode.2018-02-14.0") | (= "dev") }
]
diff --git a/theories/examples/circ_buffer.v b/theories/examples/circ_buffer.v
index 8bcf493d..024842a6 100644
--- a/theories/examples/circ_buffer.v
+++ b/theories/examples/circ_buffer.v
@@ -164,8 +164,7 @@ Section CircBuffer.
([∗ list] i ∈ seq (Z.to_nat b) ni, (ZplusPos (Z.of_nat i) q) ↦ ?)%I
={↑escrowN}=∗ ([∗ list] i ∈ seq 0 ni, PE γ q i)%I.
Proof.
- move => Le. iIntros "OL".
- iApply (fupd_big_sepL (PROP:=vProp _)).
+ move => Le. iIntros "OL". iApply fupd_big_sepL.
rewrite (Nat2Z.id 2) -2!fmap_seq -list_fmap_compose bi.big_sepL_fmap.
iApply (bi.big_sepL_mono with "OL").
iIntros (? i H) "ol".
@@ -233,7 +232,7 @@ Section CircBuffer.
iAssert (|={⊤}=> ([∗ list] i ∈ seq 0 (Z.to_nat n), PE γ q i)%I)%I
with "[oLs]" as ">#PEs".
- { iApply (fupd_mask_mono (PROP:=vProp) (↑escrowN)); first auto.
+ { iApply (fupd_mask_mono (↑escrowN)); first auto.
iApply (cb_escrows_list_alloc with "oLs"). lia'. }
wp_let. wp_op. wp_bind ([_]_na <- _)%E.
@@ -334,7 +333,7 @@ Section CircBuffer.
iSpecialize ("EA" with "[$PEi $iTok]"); first auto.
- iMod (fupd_mask_mono (PROP:=vProp) with "EA") as ">oL"; first auto.
+ iMod (fupd_mask_mono with "EA") as ">oL"; first auto.
(* arithmetic *)
rewrite (_: ZplusPos w (ZplusPos b q) = loc_at q i); last first.
@@ -347,7 +346,7 @@ Section CircBuffer.
iDestruct (escrow_alloc ⎡cTok γ i⎤%I (∃ v : Z, P v ∗ loc_at q i ↦ v)%I with "[oL P]")
as "CEi".
{ iNext. iExists v. iFrame "P oL". }
- iMod (fupd_mask_mono (PROP:=vProp) with "CEi") as "#CEi"; first auto.
+ iMod (fupd_mask_mono with "CEi") as "#CEi"; first auto.
wp_seq. wp_bind ([_]_at <- _)%E. wp_op.
rewrite H0 Z.add_mod_idemp_l ; last omega.
@@ -363,8 +362,7 @@ Section CircBuffer.
iSplitL ""; iIntros "!#"; [by rewrite Nat2Z.inj_add|].
cbn. iIntros (k). iIntros (Hk).
iApply ("Px"). iPureIntro. lia'.
- - iIntros "!#". iIntros (k). iIntros "%".
- apply Zlt_succ_le, Zle_lt_or_eq in a as [Lt|Eq].
+ - iIntros (k ?). apply Zlt_succ_le, Zle_lt_or_eq in a as [Lt|Eq].
+ by iApply ("CEs" with "[%]").
+ apply Nat2Z.inj in Eq. by rewrite Eq. }
@@ -432,7 +430,7 @@ Section CircBuffer.
with "[] [$CEj $jTok]") as "EA".
{ iIntros "cTok". iApply (cTok_exclusive with "cTok"). }
- iMod (fupd_mask_mono (PROP:=vProp) with "EA") as (v) "(P & >oL)"; [done|].
+ iMod (fupd_mask_mono with "EA") as (v) "(P & >oL)"; [done|].
(* arithmetic *)
rewrite (_: ZplusPos r (ZplusPos b q) = loc_at q j); last first.
@@ -452,7 +450,7 @@ Section CircBuffer.
- rewrite /loc_at. do 2 f_equal.
rewrite Nat2Z.inj_add Z2Nat.id; last omega.
by rewrite -{1}(Z.mul_1_l n) Z_mod_plus_full. }
- iMod (fupd_mask_mono (PROP:=vProp) with "PEj") as "#PEj"; first auto.
+ iMod (fupd_mask_mono with "PEj") as "#PEj"; first auto.
wp_let. wp_bind ([_]_at <- _)%E. wp_op.
wp_op. wp_op.
@@ -472,8 +470,7 @@ Section CircBuffer.
iSplitL ""; iIntros "!#"; [by rewrite Nat2Z.inj_add|auto].
cbn. iIntros (k). iIntros (Hk).
iApply ("Px"). iPureIntro. lia'.
- - iIntros "!#". iIntros (k). iIntros "%".
- rewrite Z.add_succ_l in a.
+ - iIntros (k ?). rewrite Z.add_succ_l in a.
apply Zlt_succ_le, Zle_lt_or_eq in a as [Lt|Eq].
+ by iApply ("PEs" with "[%]").
+ rewrite -(Nat2Z.id j) -Z2Nat.inj_add -?Eq ?Nat2Z.id;
diff --git a/theories/examples/hashtable.v b/theories/examples/hashtable.v
index c1b999de..62023fe5 100644
--- a/theories/examples/hashtable.v
+++ b/theories/examples/hashtable.v
@@ -1967,7 +1967,7 @@ Section proof.
destruct ls as [|b3]; [discriminate|].
destruct ls; [|discriminate].
iExists b1, b2, b3, h; simpl in *; iFrame; auto. }
- iApply (fupd_mask_mono (PROP := vProp _) (↑escrowN)).
+ iApply (fupd_mask_mono (↑escrowN)).
{ apply namespaces.ndisj_subseteq_difference; last done.
do 2 apply namespaces.ndot_preserve_disjoint_r.
apply namespaces.ndot_ne_disjoint; done. }
@@ -2054,7 +2054,7 @@ Section proof.
iPoseProof (big_sepL_mono with "Hentries") as "Hentries".
{ intros; iIntros "[Hctx H]".
iApply (na_frac_from_non with "[$Hctx $H]"); auto. }
- iMod (fupd_big_sepL (PROP:=vProp _) with "Hentries") as "Hentries".
+ iMod (fupd_big_sepL with "Hentries") as "Hentries".
iApply (wp_for_simple with "[] [Hentries Ht Hhist Hresults]").
{ instantiate (1 := (fun i : Z => ⌜0 <= i <= 3⌠∗
([∗ list] j↦x ∈ entries, ZplusPos j m_entries ↦{1/Z.to_pos (2^i)} Z.pos x) ∗
@@ -2172,7 +2172,7 @@ Section proof.
iPoseProof (escrow_apply with "[] [$H $Htok]") as "H".
{ iIntros "[H1 H2]".
iPoseProof (own_valid_2 with "H1 H2") as "%"; done. }
- iPoseProof (fupd_mask_mono (PROP:=vProp _)(↑escrowN) with "H") as ">H".
+ iPoseProof (fupd_mask_mono (↑escrowN) with "H") as ">H".
{ apply namespaces.ndisj_subseteq_difference; last done.
do 2 apply namespaces.ndot_preserve_disjoint_r.
apply namespaces.ndot_ne_disjoint; done. }
diff --git a/theories/examples/message_passing.v b/theories/examples/message_passing.v
index 73a986d6..9dcc9ddd 100644
--- a/theories/examples/message_passing.v
+++ b/theories/examples/message_passing.v
@@ -107,8 +107,7 @@ Section proof.
erewrite bool_decide_false; last auto.
iSpecialize ("EA" with "[$XE $Tok]").
iNext. iNext.
- iApply fupd_wp.
- iMod (fupd_mask_mono (PROP:=vProp _) with "EA") as "Nax"; [done|].
+ iApply fupd_wp. iMod (fupd_mask_mono with "EA") as "Nax"; [done|].
iModIntro.
wp_seq.
iApply (na_read with "[$kI $Nax]"); [done|].
@@ -129,7 +128,7 @@ Section proof.
(* allocate escrow *)
iDestruct (escrow_alloc (Tok γ) (x ↦ 37)%I with "[$Nax]") as "XE".
- iMod (fupd_mask_mono (PROP:=vProp _) _ ⊤ with "XE") as "XE"; first auto.
+ iMod (fupd_mask_mono _ ⊤ with "XE") as "XE"; first auto.
(* write release to final state *)
iApply (GPS_PP_Write (p:=()) (mpInt x γ) true (XE x γ) (λ _, True%I)
diff --git a/theories/examples/msqueue.v b/theories/examples/msqueue.v
index ce3b2471..d349367e 100644
--- a/theories/examples/msqueue.v
+++ b/theories/examples/msqueue.v
@@ -336,8 +336,7 @@ Section MSQueue.
(∃ v, ZplusPos data n ↦ v ∗ P v ∗ Tok γ'))%I as [EA].
iDestruct (escrow_alloc (Tok γ) (∃ v, ZplusPos data n ↦ v ∗ P v ∗ Tok γ')%I with "[P']") as "DEQ".
{ iNext. iExists x. by iFrame "P'". }
- iMod (fupd_mask_mono (PROP:=vProp _) with "DEQ") as "#DEQ";
- first namespaces.solve_ndisj. (* TODO: make it work without (PROP:=..) *)
+ iMod (fupd_mask_mono with "DEQ") as "#DEQ"; first namespaces.solve_ndisj.
iModIntro. iNext.
rewrite !(unf_int (Link P)).
iSplitL ""; (iSplitL ""; first done);
@@ -436,7 +435,7 @@ Section MSQueue.
with "[]") as "EA".
{ iIntros "[? ?]". iApply unit_tok_exclusive. iFrame. }
iSpecialize ("EA" with "[$DEQ $Tok]").
- iDestruct (fupd_mask_mono (PROP:=vProp _) with "EA") as "EA";
+ iDestruct (fupd_mask_mono with "EA") as "EA";
[|iMod "EA" as (x) "(od & P & >Tok)"]; [namespaces.solve_ndisj|].
iModIntro. iExists (). iSplitL ""; first auto.
iSplitL "od P".
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index 87e2178b..a9349652 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -544,7 +544,7 @@ Section TicketLock.
[done|done| |].
{ iIntros "oW".
iDestruct (GPS_SW_Writer_Reader (IP := NSP P γ) with "oW") as "[oW $]".
- iApply (fupd_mask_mono (PROP:=vProp _));
+ iApply fupd_mask_mono;
last iMod (escrow_alloc (Perm γ 0)
(P ∗ [XP ZplusPos 0 x in O |NSP P γ ]_W)%I
with "[$P $oW]") as "#?";
@@ -694,7 +694,7 @@ Section TicketLock.
{ by rewrite Perm_exclusive. }
iSpecialize ("EA" with "[$ES $Perm]").
- iMod (fupd_mask_mono (PROP:=vProp _) with "EA") as "(P & NSW)"; [done|].
+ iMod (fupd_mask_mono with "EA") as "(P & NSW)"; [done|].
iDestruct (GPS_SW_Writer_max (IP := NSP P γ) x n t ⊤ with "[$NSR $NSW]") as ">(NSW & %)"; [done|].
cbn in H3. exfalso. omega. }
@@ -703,7 +703,7 @@ Section TicketLock.
iDestruct (escrow_apply (Perm γ n) (P ∗ [XP x in n | NSP P γ]_W)%I
with "[] [$ES $Perm]") as "EA".
{ by rewrite Perm_exclusive. }
- iMod (fupd_mask_mono (PROP:=vProp _) with "EA") as "(P & NSW)"; first auto.
+ iMod (fupd_mask_mono with "EA") as "(P & NSW)"; first auto.
iDestruct (GPS_SW_Writer_max (IP := NSP P γ) x n n ⊤ with "[$NSR $NSW]") as ">(NSW & _)"; [done|].
iApply ("Post" with "[$P Tkt' NSW]").
iExists γ, i, n. destruct s. iFrame "Tkt' NSW TCP".
@@ -749,7 +749,7 @@ Section TicketLock.
(P ∗ [XP x in (S t) | NSP P γ]_W)%I
with "[$P $NSW]"
) as "CEi".
- iMod (fupd_mask_mono (PROP:=vProp _) with "CEi") as "#CEi"; [namespaces.solve_ndisj|].
+ iMod (fupd_mask_mono with "CEi") as "#CEi"; [namespaces.solve_ndisj|].
iModIntro. iNext.
rewrite (unf_int (NSP P γ)).
iSplitL "".
diff --git a/theories/gps/fractional.v b/theories/gps/fractional.v
index 4c43e020..ff160d85 100644
--- a/theories/gps/fractional.v
+++ b/theories/gps/fractional.v
@@ -162,9 +162,9 @@ Section Fractional.
iExists Vr, v. rewrite monPred_in_eq /=.
iSplit; last iFrame "oR'"; iPureIntro; auto.
do 4 (etrans; eauto). }
- iMod ("VS" $! _ j0 with "[% ] [-]") as "VS"; [|by iFrame|].
+ iMod ("VS" $! _ j0 with "[% ] [$]") as "$".
{ repeat (etrans; eauto). }
- iApply fupd_intro_mask; [solve_ndisj | done]. }
+ iApply fupd_intro_mask'. solve_ndisj. }
iNext.
iIntros (s' v Vr V') "(% & kS' & #Hs' & oQ & #oR' & % & %)".
iFrame.
@@ -230,8 +230,8 @@ Section Fractional.
+ iNext. iExists γ, γ_x, ζ. iFrame; auto.
+ iExists γ, γ_x, e_x. iFrame "Hex". iSplitL ""; first auto.
iExists V_r, v_r. rewrite monPred_in_eq /=; auto. }
- iMod ("VS" $! _ j0 with "[//] [$]") as "VS".
- iApply fupd_intro_mask; [solve_ndisj | done]. }
+ iMod ("VS" $! _ j0 with "[//] [$]") as "$".
+ iApply fupd_intro_mask'. solve_ndisj. }
iNext.
iIntros (s' v Vr V'') "(% & kS' & #Hs' & oQ & #oR' & % & %)".
iFrame.
@@ -413,8 +413,8 @@ Section Fractional.
iExists Vr, v_n. rewrite monPred_in_eq /=.
iSplit; last iFrame "oR'"; iPureIntro; auto.
do 4 (etrans; eauto). }
- iMod ("Q" $! j0 with "[//] [$oW]").
- iApply fupd_intro_mask; [solve_ndisj | done].
+ iMod ("Q" $! j0 with "[//] [$oW]") as "$".
+ iApply fupd_intro_mask'. solve_ndisj.
- by iSpecialize ("VSDup" $! _).
- iIntros (s' v Vr j ?) "(Hs' & Hv & Fp & (oP & HClose) & % & % & oI & ex & Writer & oR')".
iDestruct "Writer" as (ζ') "Writer".
@@ -425,9 +425,9 @@ Section Fractional.
iExists Vr, v. rewrite monPred_in_eq /=.
iSplit; last iFrame "oR'"; iPureIntro; auto.
do 4 (etrans; eauto). }
- iMod ("VSF" $! _ _ _ with "[%] [$Hs' $Hv $Fp $oW $oP]").
+ iMod ("VSF" $! _ _ _ with "[%] [$Hs' $Hv $Fp $oW $oP]") as "$".
{ etrans; eauto. }
- iApply fupd_intro_mask; [solve_ndisj | done]. }
+ iApply fupd_intro_mask'. solve_ndisj. }
iNext.
iIntros (s'' b v Vr V')
@@ -463,7 +463,7 @@ Section Fractional.
iExists s''; iFrame.
iModIntro; auto.
- iIntros (??) "(? & ? & ? & ? & ?)"; iFrame.
- iApply (fupd_mask_mono (PROP:=vProp _)); last by iApply "VSF"; iFrame.
+ iApply fupd_mask_mono; last by iApply "VSF"; iFrame.
solve_ndisj. }
iIntros (s'' b v) "(? & ?)".
destruct b; iApply ("Post" $! s'' _ v); iFrame.
diff --git a/theories/gps/plain.v b/theories/gps/plain.v
index d221c454..5fabc465 100644
--- a/theories/gps/plain.v
+++ b/theories/gps/plain.v
@@ -174,8 +174,8 @@ Section Plain.
iExists Vr, v.
iSplit; last iFrame "oR'"; iPureIntro; auto.
do 4 (etrans; eauto). }
- iMod ("VS" $! _ j0 with "[%] [-]") as "VS"; [solve_jsl|by iFrame|].
- iApply fupd_intro_mask; [solve_ndisj | done]. }
+ iMod ("VS" $! _ j0 with "[%] [$]") as "$"; [solve_jsl|].
+ iApply fupd_intro_mask'. solve_ndisj. }
iNext.
iIntros (s' v Vr V') "(% & kS' & % & oQ & #oR' & % & %)".
iFrame. iApply ("Post" $! s' _ _ with "[//]"). by iFrame "%".
@@ -305,8 +305,8 @@ Section Plain.
iExists Vr, v_n.
iSplit; last iFrame "oR'"; iPureIntro; auto.
do 4 (etrans; eauto). }
- iMod ("Q" $! _ with "[//] [oW //]").
- iApply fupd_intro_mask; [solve_ndisj | done].
+ iMod ("Q" $! _ with "[//] [oW //]") as "$".
+ iApply fupd_intro_mask'. solve_ndisj.
- by iSpecialize ("VSDup" $! _).
- iIntros (s' v Vr j ?) "(Hs' & Hv & Fp & (oP & HClose) & % & % & oI & ex & Writer & oR')".
iDestruct "Writer" as (ζ') "Writer".
@@ -317,9 +317,9 @@ Section Plain.
iExists Vr, v.
iSplit; last iFrame "oR'"; iPureIntro; auto.
do 4 (etrans; eauto). }
- iMod ("VSF" $! _ _ _ with "[%] [$Hs' $Hv $Fp $oW $oP]").
+ iMod ("VSF" $! _ _ _ with "[%] [$Hs' $Hv $Fp $oW $oP]") as "$".
{ etrans; eauto. }
- iApply fupd_intro_mask; [solve_ndisj | done]. }
+ iApply fupd_intro_mask'. solve_ndisj. }
iNext.
iIntros (s'' b v Vr V')
@@ -354,7 +354,7 @@ Section Plain.
iExists s''; iFrame.
iModIntro; auto.
- iIntros (??) "(? & ? & ? & ? & ?)"; iFrame.
- iApply (fupd_mask_mono (PROP:=vProp _)); last by iApply "VSF"; iFrame.
+ iApply fupd_mask_mono; last by iApply "VSF"; iFrame.
solve_ndisj. }
iIntros (s'' b v) "(? & ?)".
destruct b; iApply ("Post" $! s'' _ v); iFrame.
diff --git a/theories/gps/singlewriter.v b/theories/gps/singlewriter.v
index 89ab52e8..3ba264c4 100644
--- a/theories/gps/singlewriter.v
+++ b/theories/gps/singlewriter.v
@@ -411,8 +411,8 @@ Section Gname_StrongSW.
{ iSplit.
+ iNext. iExists γ_x. by iFrame "oI".
+ iExists γ_x. iSplit; first done. iExists Vr, v. by iFrame "oR'". }
- iMod ("VS" $! _ _ with "[%] [-]") as "VS"; first done; first iFrame.
- iApply fupd_intro_mask; [solve_ndisj | done]. }
+ iMod ("VS" $! _ _ with "[%] [$]") as "$"; first done.
+ iApply fupd_intro_mask'. solve_ndisj. }
iNext.
iIntros (s' v Vr V') "(% & kS' & Hs' & oQ & oR' & % & %)".
iFrame; iApply ("Post" $! _ _ _ with "[%]"); first done.
@@ -480,9 +480,9 @@ Section Gname_StrongSW.
{ iSplitL "oI".
+ iNext. iExists γ_x. iFrame; auto.
+ iExists γ_x. iSplit; first done. iExists V1, v1. by iFrame "oR1". }
- iMod ("VS" $! _ _ with "[%] [-]") as "VS"; first done.
+ iMod ("VS" $! _ _ with "[%] [-]") as "$"; first done.
{ iFrame. }
- iApply fupd_intro_mask; [solve_ndisj | done].
+ iApply fupd_intro_mask'. solve_ndisj.
- iIntros (s' v ??) "[% Fp]".
iApply ("VSDup" $! _ s' v _ with "[%] [$Fp]"); first reflexivity.
iPureIntro. split; [by etrans|auto]. }
@@ -501,9 +501,9 @@ Section Gname_StrongSW.
{ iSplitL "oI".
+ iNext. iExists γ_x. iFrame; auto.
+ iExists γ_x. iSplit; first done. iExists V1, v1. by iFrame "oR1". }
- iMod ("VS" $! _ _ with "[%] [-]") as "VS"; first done.
+ iMod ("VS" $! _ _ with "[%] [-]") as "$"; first done.
{ iFrame. }
- iApply fupd_intro_mask; [solve_ndisj | done].
+ iApply fupd_intro_mask'. solve_ndisj.
- iIntros (s' v ??) "[% Fp]".
iApply ("VSDup" $! _ s' v _ with "[%] [$Fp]"); first reflexivity.
iPureIntro. split; solve_jsl. }
@@ -572,9 +572,9 @@ Section Gname_StrongSW.
{ iSplitL "oI".
+ iNext. iExists γ_x. iFrame; auto.
+ iExists γ_x. iSplit; first done. iExists V1, v1. by iFrame "oR". }
- iMod ("VS" $! _ _ with "[%] [-]") as "VS"; first done.
+ iMod ("VS" $! _ _ with "[%] [-]") as "$"; first done.
{ iFrame. }
- iApply fupd_intro_mask; [solve_ndisj | done]. }
+ iApply fupd_intro_mask'. solve_ndisj. }
iNext. iIntros (s' v Vr V'') "(% & kS & % & Q & oR' & % & %)".
iFrame; iApply ("Post" $! _ _ V'' with "[%]"). { solve_jsl. }
iMod "Q"; iFrame; auto.
@@ -829,8 +829,8 @@ Section Gname_StrongSW_Param.
{ iSplit.
+ iNext. iExists γ_x. by iFrame "oI".
+ iExists γ_x. iSplit; first done. iExists Vr, v. by iFrame "oR'". }
- iMod ("VS" $! _ _ with "[%] [-]") as "VS"; first done; first iFrame.
- iApply fupd_intro_mask; [solve_ndisj | done]. }
+ iMod ("VS" $! _ _ with "[% //] [$]") as "$".
+ iApply fupd_intro_mask'. solve_ndisj. }
iNext.
iIntros (s' v Vr V') "(% & kS' & Hs' & >oQ & oR' & % & %)".
iFrame; iApply ("Post" $! _ _ _ with "[%]"); [solve_jsl|auto].
@@ -1191,8 +1191,8 @@ Section SingleWriter.
{ iSplit.
+ iNext. iExists γ, γ_x. by iFrame "oI".
+ iExists γ, γ_x. iSplit; first done. iExists Vr, v. by iFrame "oR'". }
- iMod ("VS" $! _ _ with "[%] [-]") as "VS"; first done; first iFrame.
- iApply fupd_intro_mask; [solve_ndisj | done]. }
+ iMod ("VS" $! _ _ with "[% //] [$]") as "$".
+ iApply fupd_intro_mask'. solve_ndisj. }
iNext.
iIntros (s' v Vr V') "(% & kS' & Hs' & oQ & oR' & % & %)".
iFrame; iApply ("Post" $! _ _ _ with "[%]").
@@ -1373,8 +1373,8 @@ Section SingleWriter.
{ iSplit.
+ iNext. iExists γ, γ_x. by iFrame "oI".
+ iExists γ, γ_x. iSplit; first done. iExists Vr, v. by iFrame "oR'". }
- iMod ("VS" $! _ _ with "[%] [-]") as "VS"; first done; first iFrame.
- iApply fupd_intro_mask; [solve_ndisj | done]. }
+ iMod ("VS" $! _ _ with "[% //] [$]") as "$".
+ iApply fupd_intro_mask'. solve_ndisj. }
iNext.
iIntros (s' v Vr V') "(% & kS' & Hs' & oQ & oR' & % & %)".
iFrame; iApply ("Post" $! _ _ _ with "[%]").
diff --git a/theories/weakestpre.v b/theories/weakestpre.v
index d100fd26..6d3e29cb 100644
--- a/theories/weakestpre.v
+++ b/theories/weakestpre.v
@@ -22,7 +22,6 @@ Import WP_Def.
Arguments wp {_ _} _ _%E _.
Instance: Params (@wp) 4.
-
Notation "'WP' e @ E {{ Φ } }" := (wp E e%E Φ)
(at level 20, e, Φ at level 200,
format "'WP' e @ E {{ Φ } }") : bi_scope.
@@ -367,65 +366,18 @@ Section proofmode_classes.
Proof. by rewrite /IsExcept0 -{2}fupd_wp -except_0_fupd -fupd_intro. Qed.
Global Instance elim_modal_bupd_wp E e P Φ :
- ElimModal (|==> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
+ ElimModal True (|==> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
Proof. by rewrite /ElimModal (bupd_fupd E) fupd_frame_r bi.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 {{ Φ }}).
+ ElimModal True (|={E}=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
Proof. by rewrite /ElimModal fupd_frame_r bi.wand_elim_r fupd_wp. Qed.
(* lower precedence, if possible, it should always pick elim_upd_fupd_wp *)
Global Instance elim_modal_fupd_wp_atomic E1 E2 e P Φ :
(∀ V, Atomic WeaklyAtomic ((e,V) : ra_lang.expr)) →
- ElimModal (|={E1,E2}=> P) P
+ ElimModal True (|={E1,E2}=> P) P
(WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
Proof. intros. by rewrite /ElimModal fupd_frame_r bi.wand_elim_r wp_atomic. Qed.
End proofmode_classes.
-
-Section proofmode_classes_embedding.
- Context `{foundationG Σ}.
- Implicit Types P Q : vProp Σ.
- Implicit Types Φ : base.val → vProp Σ.
-
- Global Instance elim_modal_bupd_wp_emb E e A Φ :
- ElimModal (⎡|==> A⎤) ⎡A⎤ (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
- Proof.
- rewrite /ElimModal.
- iStartProof (upred.uPredSI _); iIntros (?) "[U WP]".
- iIntros (V -> π) "kS".
- iMod "U".
- iSpecialize ("WP" with "[U //]").
- iApply ("WP" with "kS").
- Qed.
-
- Global Instance elim_modal_fupd_wp_emb E e A Φ :
- ElimModal (⎡|={E}=> A⎤) ⎡A⎤ (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
- Proof.
- rewrite /ElimModal.
- iStartProof (upred.uPredSI _); iIntros (?) "[U WP]".
- iIntros (V -> π) "kS".
- iMod "U".
- iSpecialize ("WP" with "[U //]").
- iApply ("WP" with "kS").
- Qed.
-
- (* lower precedence, if possible, it should always pick elim_upd_fupd_wp *)
- Global Instance elim_modal_fupd_wp_atomic_emb E1 E2 e A Φ :
- (∀ V, Atomic WeaklyAtomic ((e,V) : ra_lang.expr)) →
- ElimModal (⎡|={E1,E2}=> A⎤) ⎡A⎤
- (WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
- Proof.
- rewrite /ElimModal.
- iStartProof (upred.uPredSI _). iIntros (??) "[U WP]".
- iIntros (V -> π) "kS".
- iMod "U".
- iSpecialize ("WP" with "[U //]").
- iApply iris.program_logic.weakestpre.wp_mono; cycle 1.
- iApply ("WP" with "kS").
- by iIntros ([v V']) "[$ >$]".
- Qed.
-
-End proofmode_classes_embedding.
-
-Delimit Scope val_scope with Val. (* TODO: what is this? *)
diff --git a/theories/wp_tactics.v b/theories/wp_tactics.v
index 8c7462f3..6f00bcf0 100644
--- a/theories/wp_tactics.v
+++ b/theories/wp_tactics.v
@@ -12,7 +12,7 @@ Lemma tac_wp_pure `{ghosts.foundationG Σ} K Δ Δ' E e1 e2 φ Φ :
envs_entails Δ' (WP fill K e2 @ E {{ Φ }}) →
envs_entails Δ (WP fill K e1 @ E {{ Φ }}).
Proof.
- rewrite /envs_entails=> ??? HΔ'. rewrite into_laterN_env_sound /=.
+ rewrite envs_entails_eq=> ??? HΔ'. rewrite into_laterN_env_sound /=.
rewrite -weakestpre.wp_bind HΔ' -lifting.wp_pure_step_later //.
by rewrite -weakestpre.wp_bind_inv.
Qed.
@@ -20,7 +20,7 @@ Qed.
Lemma tac_wp_value `{ghosts.foundationG Σ} Δ E Φ e v :
IntoVal e v →
envs_entails Δ (Φ v) → envs_entails Δ (WP e @ E {{ Φ }}).
-Proof. rewrite /envs_entails=> ? ->. by apply wp_value. Qed.
+Proof. rewrite envs_entails_eq=> ? ->. by apply wp_value. Qed.
Ltac wp_value_head := eapply tac_wp_value; [apply _|lazy beta].
@@ -53,7 +53,7 @@ Tactic Notation "wp_seq" := wp_lam.
Lemma tac_wp_bind `{ghosts.foundationG Σ} K Δ E Φ e :
envs_entails Δ (WP e @ E {{ v, WP fill K (ectxi_language.of_val v) @ E {{ Φ }} }})%I →
envs_entails Δ (WP fill K e @ E {{ Φ }}).
-Proof. rewrite /envs_entails=> ->. exact: wp_bind. Qed.
+Proof. rewrite envs_entails_eq=> ->. exact: wp_bind. Qed.
Ltac wp_bind_core K :=
lazymatch eval hnf in K with
diff --git a/theories/wp_tactics_vProp.v b/theories/wp_tactics_vProp.v
index 1f64da17..9d2c5417 100644
--- a/theories/wp_tactics_vProp.v
+++ b/theories/wp_tactics_vProp.v
@@ -23,14 +23,14 @@ Lemma tac_wp_pure `{foundationG Σ} Δ Δ' E e1 e2 φ Φ :
envs_entails Δ' (WP e2 @ E {{ Φ }}) →
envs_entails Δ (WP e1 @ E {{ Φ }}).
Proof.
- rewrite /envs_entails=> ??? HΔ'. rewrite into_laterN_env_sound /=.
+ rewrite envs_entails_eq=> ??? HΔ'. rewrite into_laterN_env_sound /=.
rewrite HΔ' -wp_pure_step_later //.
Qed.
Lemma tac_wp_value `{foundationG Σ} Δ E Φ e v :
(IntoVal (e) (v)) →
envs_entails Δ (Φ v) → envs_entails Δ (WP e @ E {{ Φ }}).
-Proof. rewrite /envs_entails=> IV ->. now apply: wp_value. Qed.
+Proof. rewrite envs_entails_eq=> IV ->. now apply: wp_value. Qed.
Ltac wp_value_head := eapply tac_wp_value; [apply _|lazy beta].
@@ -67,7 +67,7 @@ Tactic Notation "wp_seq" := wp_lam.
Lemma tac_wp_bind `{foundationG Σ} K Δ E Φ e :
envs_entails Δ (WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }})%I →
envs_entails Δ (WP fill K e @ E {{ Φ }}).
-Proof. rewrite /envs_entails=> ->. by apply wp_bind. Qed.
+Proof. rewrite envs_entails_eq=> ->. by apply wp_bind. Qed.
Ltac wp_bind_core K :=
lazymatch eval hnf in K with
--
GitLab