From e8a59e0017dabcd4dd93875b99c68bfd020fff6e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 14 Jun 2018 14:54:02 +0200
Subject: [PATCH] bump Iris; fix for new monPred framing and WP

Also remove uses of monPred_at_sep
---
 opam                        |  2 +-
 theories/gps/cas.v          |  2 +-
 theories/gps/fractional.v   | 17 ++++++++---------
 theories/gps/plain.v        | 12 +++++-------
 theories/gps/singlewriter.v | 16 ++++++++--------
 theories/weakestpre.v       |  9 +++++----
 6 files changed, 28 insertions(+), 30 deletions(-)

diff --git a/opam b/opam
index 588720cf..9327471f 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-06-10.4.237fd8c7") | (= "dev") }
+  "coq-iris" { (= "branch.gen_proofmode.2018-06-14.8.bf9fd4f5") | (= "dev") }
 ]
diff --git a/theories/gps/cas.v b/theories/gps/cas.v
index db351cfa..496a4c9d 100644
--- a/theories/gps/cas.v
+++ b/theories/gps/cas.v
@@ -115,7 +115,7 @@ Section CAS.
           { apply union_subseteq_l. }
 
         iMod ("VS2" $! s' s'' V' with "[//] [$T oW']") as "(F & Fp & Q)".
-        { do 2 iSplit=>//. auto 10. }
+        { do 2 iSplit=>//. rewrite monPred_at_embed. auto 10. }
 
         iMod ("Q" $! V' with "[oA' oAX Hist' oBEI oAI F Fp ofX]"); last first.
         { iApply ("Post" $! s'' true v_n V' V').
diff --git a/theories/gps/fractional.v b/theories/gps/fractional.v
index 0c2e12b3..3e09141e 100644
--- a/theories/gps/fractional.v
+++ b/theories/gps/fractional.v
@@ -162,7 +162,7 @@ Section Fractional.
           iExists Vr, v. rewrite monPred_in_eq /=.
           iSplit; last iFrame "oR'"; iPureIntro; auto.
           do 4 (etrans; eauto). }
-      setoid_rewrite monPred_at_wand. do 2 setoid_rewrite monPred_at_sep.
+      setoid_rewrite monPred_at_wand.
       iMod ("VS" $! _ j0 with "[% ] [$]") as "$".
       { repeat (etrans; eauto). }
       iApply fupd_intro_mask'. solve_ndisj. }
@@ -171,7 +171,7 @@ Section Fractional.
     iFrame. setoid_rewrite monPred_at_wand.
     iApply ("Post" $! _ _ _ with "[%]").
     { etrans; eauto. }
-    setoid_rewrite monPred_at_sep. by iFrame "Hs'".
+    by iFrame "Hs'".
   Qed.
 
   Lemma GPS_FP_Read l q (P : vPred) (Q : pr_state Prtcl → Z → vPred)
@@ -238,7 +238,7 @@ Section Fractional.
     iIntros (s' v Vr V'') "(% & kS' & #Hs' & oQ & #oR' & % & %)".
     iFrame. setoid_rewrite monPred_at_wand.
     iApply ("Post" $! _ _ _ with "[%]"); [solve_jsl|].
-    setoid_rewrite monPred_at_sep. by iFrame "Hs'".
+    by iFrame "Hs'".
   Qed.
 
   Lemma GPS_FP_Read_abs l q (P : vPred) (Q : pr_state Prtcl → Z → vPred)
@@ -303,7 +303,7 @@ Section Fractional.
     }
     assert (V ⊑ V') by (do 2 (etrans; eauto)).
     iMod ("VS" $! _ with "[%] [oP oW]") as "($ & oF & oFp)"; first done.
-    { rewrite monPred_at_sep. rewrite vGPS_FP_eq /=; iFrame. }
+    { rewrite vGPS_FP_eq /=; iFrame. }
     iSpecialize ("oI" with "[$oF $oFp]").
     iMod ("HClose" with "[-]") as "$"; [|done].
     iNext. iExists γ, γ_x, ({[s', (v, V')]} ∪ ζ).
@@ -354,7 +354,7 @@ Section Fractional.
     setoid_rewrite monPred_at_wand.
     iFrame; iApply ("Post" $! _ _ _ with "[%]").
     { etrans; eauto. }
-    rewrite monPred_at_sep. iFrame "Hs' Q".
+    iFrame "Hs' Q".
     iApply "HClose". iSplitL "oI wTok".
     - iNext. iDestruct "wTok" as (ζ') "wTok".
       iExists γ, γ_x, _.
@@ -405,7 +405,7 @@ Section Fractional.
       [solve_ndisj|solve_ndisj|solve_ndisj| |].
     { iSplitL "VS"; last iSplitL "VSDup"; last iSplitL "VSF"; last (by iFrame; iExists _); iNext.
       - iIntros (s' j ?) "(Hs' & F & oP & HClose)".
-        setoid_rewrite monPred_at_wand. do 2 setoid_rewrite monPred_at_sep.
+        setoid_rewrite monPred_at_wand.
         iMod ("VS" $! _ _ with "[%] [$Hs' $F $oP]") as (s'') "(? & ? & ? & Q)".
         { etrans; eauto. }
         iExists s''; iFrame.
@@ -431,8 +431,7 @@ Section Fractional.
             iExists Vr, v. rewrite monPred_in_eq /=.
             iSplit; last iFrame "oR'"; iPureIntro; auto.
             do 4 (etrans; eauto). }
-        setoid_rewrite monPred_at_wand. do 4 setoid_rewrite monPred_at_sep.
-        setoid_rewrite monPred_at_later.
+        setoid_rewrite monPred_at_wand.
         iMod ("VSF" $! _ _ _ with "[%] [$Hs' $Hv $Fp $oW $oP]") as "$".
         { etrans; eauto. }
         iApply fupd_intro_mask'. solve_ndisj. }
@@ -443,7 +442,7 @@ Section Fractional.
     iFrame. setoid_rewrite monPred_at_wand.
     iSpecialize ("Post" $! s'' b v _ with "[%]").
     { etrans; eauto. }
-    iApply "Post". rewrite monPred_at_sep. iFrame "Hs'". by destruct b.
+    iApply "Post". iFrame "Hs'". by destruct b.
   Qed.
 
   Lemma GPS_FP_CAS l q s v_o v_n (E : coPset)
diff --git a/theories/gps/plain.v b/theories/gps/plain.v
index 742a7aa4..79290895 100644
--- a/theories/gps/plain.v
+++ b/theories/gps/plain.v
@@ -175,12 +175,11 @@ Section Plain.
           iExists Vr, v. iSplit; last iFrame "oR'"; iPureIntro; auto.
           do 4 (etrans; eauto). }
       setoid_rewrite monPred_at_wand.
-      iMod ("VS" $! _ j0 with "[%] [-]") as "$"; [solve_jsl|..].
-      { iFrame. done. }
+      iMod ("VS" $! _ j0 with "[%] [-]") as "$"; [solve_jsl|by iFrame|..].
       iApply fupd_intro_mask'. solve_ndisj. }
     iNext.
     iIntros (s' v Vr V') "(% & kS' & % & oQ & #oR' & % & %)".
-    iFrame. setoid_rewrite monPred_at_wand. setoid_rewrite monPred_at_sep.
+    iFrame. setoid_rewrite monPred_at_wand.
     iApply ("Post" $! s' _ _). { iPureIntro. by etrans. }
     by iFrame "%".
   Qed.
@@ -297,7 +296,7 @@ Section Plain.
       [solve_ndisj|solve_ndisj|solve_ndisj| |].
     { iSplitL "VS"; last iSplitL "VSDup"; last iSplitL "VSF"; last (by iFrame; iExists _); iNext.
       - iIntros (s' j ?) "(Hs' & F & oP & HClose)".
-        setoid_rewrite monPred_at_wand. setoid_rewrite monPred_at_sep.
+        setoid_rewrite monPred_at_wand.
         iMod ("VS" $! _ _ with "[%] [$Hs' $F $oP]") as (s'') "(? & ? & ? & Q)".
         { etrans; eauto. }
         iExists s''; iFrame.
@@ -323,8 +322,7 @@ Section Plain.
             iExists Vr, v.
             iSplit; last iFrame "oR'"; iPureIntro; auto.
             do 4 (etrans; eauto). }
-        setoid_rewrite monPred_at_wand. do 4 setoid_rewrite monPred_at_sep.
-        setoid_rewrite monPred_at_later.
+        setoid_rewrite monPred_at_wand.
         iMod ("VSF" $! _ _ _ with "[%] [$Hs' $Hv $Fp $oW $oP]") as "$".
         { etrans; eauto. }
         iApply fupd_intro_mask'. solve_ndisj. }
@@ -335,7 +333,7 @@ Section Plain.
     iFrame. setoid_rewrite monPred_at_wand.
     iSpecialize ("Post" $! s'' b v _ with "[%]").
     { etrans; eauto. }
-    iApply "Post". rewrite monPred_at_sep. iFrame. by destruct b.
+    iApply "Post". iFrame. by destruct b.
   Qed.
 
   Lemma GPS_PP_CAS l p s v_o v_n (E : coPset)
diff --git a/theories/gps/singlewriter.v b/theories/gps/singlewriter.v
index 67b18c61..629b8f80 100644
--- a/theories/gps/singlewriter.v
+++ b/theories/gps/singlewriter.v
@@ -414,13 +414,13 @@ Section Gname_StrongSW.
       { iSplit.
         + iNext. iExists γ_x. by iFrame "oI".
         + iExists γ_x. iSplit; first done. iExists Vr, v. by iFrame "oR'". }
-      setoid_rewrite monPred_at_wand. do 2 setoid_rewrite monPred_at_sep.
+      setoid_rewrite monPred_at_wand.
       iMod ("VS" $! _ _ with "[%] [$]") as "$"; first solve_jsl.
       iApply fupd_intro_mask'. solve_ndisj. }
     iIntros "!>" (s' v Vr V') "(% & kS' & Hs' & oQ & oR' & % & %)".
     setoid_rewrite monPred_at_wand.
     iFrame; iApply ("Post" $! _ _ _ with "[%]"); first done.
-    rewrite monPred_at_sep. by iFrame "Hs'".
+    by iFrame "Hs'".
   Qed.
 
   Lemma GPS_nFRP_Read l γ q (P : vPred) (Q : pr_state Prtcl → Z → vPred)
@@ -846,14 +846,14 @@ Section Gname_StrongSW_Param.
       { iSplit.
         + iNext. iExists γ_x. by iFrame "oI".
         + iExists γ_x. iSplit; first done. iExists Vr, v. by iFrame "oR'". }
-      setoid_rewrite monPred_at_wand. do 2 setoid_rewrite monPred_at_sep.
+      setoid_rewrite monPred_at_wand.
       iMod ("VS" $! _ _ with "[%] [$]") as "$"; [solve_jsl|].
       iApply fupd_intro_mask'. solve_ndisj. }
     iNext.
     iIntros (s' v Vr V') "(% & kS' & Hs' & >oQ & oR' & % & %)".
     setoid_rewrite monPred_at_wand.
     iFrame; iApply ("Post" $! _ _ _ with "[%]"); first solve_jsl.
-    rewrite monPred_at_sep. auto.
+    by iFrame.
   Qed.
 
   Lemma GPS_nSW_Read l γ p (P : vPred) (Q : pr_state Prtcl → Z → vPred)
@@ -1212,14 +1212,14 @@ Section SingleWriter.
       { iSplit.
         + iNext. iExists γ, γ_x. by iFrame "oI".
         + iExists γ, γ_x. iSplit; first done. iExists Vr, v. by iFrame "oR'". }
-      setoid_rewrite monPred_at_wand. do 2 setoid_rewrite monPred_at_sep.
+      setoid_rewrite monPred_at_wand.
       iMod ("VS" $! _ _ with "[%] [$]") as "$"; [solve_jsl|].
       iApply fupd_intro_mask'. solve_ndisj. }
     iIntros "!>" (s' v Vr V') "(% & kS' & Hs' & oQ & oR' & % & %)".
     setoid_rewrite monPred_at_wand.
     iFrame; iApply ("Post" $! _ _ _ with "[%]").
     { etrans; eauto. }
-    rewrite monPred_at_sep. by iFrame "Hs'".
+    by iFrame "Hs'".
   Qed.
 
   Lemma GPS_SW_Read l (P : vPred) (Q : pr_state Prtcl → Z → vPred)
@@ -1396,14 +1396,14 @@ Section SingleWriter.
       { iSplit.
         + iNext. iExists γ, γ_x. by iFrame "oI".
         + iExists γ, γ_x. iSplit; first done. iExists Vr, v. by iFrame "oR'". }
-      setoid_rewrite monPred_at_wand. do 2 setoid_rewrite monPred_at_sep.
+      setoid_rewrite monPred_at_wand.
       iMod ("VS" $! _ _ with "[%] [$]") as "$"; [solve_jsl|].
       iApply fupd_intro_mask'. solve_ndisj. }
     iIntros "!>" (s' v Vr V') "(% & kS' & Hs' & oQ & oR' & % & %)".
     setoid_rewrite monPred_at_wand.
     iFrame; iApply ("Post" $! _ _ _ with "[%]").
     { etrans; eauto. }
-    rewrite monPred_at_sep. by iFrame "Hs'".
+    by iFrame "Hs'".
   Qed.
 
   Lemma GPS_FRP_Read l q (P : vPred) (Q : pr_state Prtcl → Z → vPred)
diff --git a/theories/weakestpre.v b/theories/weakestpre.v
index b36a478e..7aac4c3f 100644
--- a/theories/weakestpre.v
+++ b/theories/weakestpre.v
@@ -147,8 +147,8 @@ Proof.
   }
   iIntros (σ1) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
   iMod ("H" with "[$]") as "[$ H]".
-  iModIntro. iNext. iIntros (e2 σ2 efs Hstep).
-  iMod ("H" with "[//]") as "($ & H & $)"; auto.
+  iModIntro. iIntros (e2 σ2 efs Hstep).
+  iMod ("H" with "[//]") as "H". iIntros "!> !>". iMod "H" as "($ & H & $)"; auto.
   iMod "Hclose" as "_". destruct e2 as [e2 V2]. iApply ("IH" with "[HΦ] H").
   iClear "IH".
   move/prim_step_view_mono : Hstep => HV.
@@ -202,8 +202,9 @@ Proof.
   iIntros (-> ?) "H". iIntros (V'' HV'' π) "S".
   iSpecialize ("H" with "[//]").
   iIntros (σ1) "Hσ". iMod "HR". iMod ("H" with "S [$]") as "[$ H]".
-  iModIntro; iNext; iIntros (e2 σ2 efs Hstep).
-  iMod ("H" $! e2 σ2 efs with "[% //]") as "($ & H & $)".
+  iModIntro; iIntros (e2 σ2 efs Hstep).
+  iMod ("H" $! e2 σ2 efs with "[% //]") as "H".
+  iIntros "!> !>". iMod "H" as "($ & H & $)".
   iMod "HR". iModIntro.
   destruct e2 as [e2 V2].
   iApply (wp_strong_mono_iris E2 with "[-$H]"); first done.
-- 
GitLab