Fix iInv for monpred and test that

tests/proofmode_iris.ref

@@ -5,7 +5,7 @@
   H0 : cinvG Σ
   H1 : na_invG Σ
   N : namespace
-  P : uPredI (iResUR Σ)
+  P : iProp Σ
   ============================
   "H" : inv N (<pers> P)%I
   "H2" : ▷ <pers> P
@@ -19,7 +19,7 @@
   H0 : cinvG Σ
   H1 : na_invG Σ
   N : namespace
-  P : uPredI (iResUR Σ)
+  P : iProp Σ
   ============================
   "H" : inv N (<pers> P)%I
   "H2" : ▷ <pers> P
@@ -37,7 +37,7 @@
   γ : gname
   p : Qp
   N : namespace
-  P : uPredI (iResUR Σ)
+  P : iProp Σ
   ============================
   _ : cinv N γ (<pers> P)%I
   "HP" : ▷ <pers> P
@@ -55,7 +55,7 @@
   γ : gname
   p : Qp
   N : namespace
-  P : uPredI (iResUR Σ)
+  P : iProp Σ
   ============================
   _ : cinv N γ (<pers> P)%I
   "HP" : ▷ <pers> P
@@ -74,7 +74,7 @@
   t : na_inv_pool_name
   N : namespace
   E1, E2 : coPset
-  P : uPredI (iResUR Σ)
+  P : iProp Σ
   H2 : ↑N ⊆ E2
   ============================
   _ : na_inv t N (<pers> P)%I
@@ -95,7 +95,7 @@
   t : na_inv_pool_name
   N : namespace
   E1, E2 : coPset
-  P : uPredI (iResUR Σ)
+  P : iProp Σ
   H2 : ↑N ⊆ E2
   ============================
   _ : na_inv t N (<pers> P)%I
@@ -108,3 +108,32 @@
   --------------------------------------∗
   |={⊤}=> na_own t E1 ∗ na_own t E2 ∗ ▷ P
   
+1 subgoal
+  
+  Σ : gFunctors
+  H : invG Σ
+  I : biIndex
+  N : namespace
+  E : coPset
+  𝓟 : iProp Σ
+  H0 : ↑N ⊆ E
+  ============================
+  "HP" : ⎡ ▷ 𝓟 ⎤
+  --------------------------------------∗
+  |={E ∖ ↑N}=> ⎡ ▷ 𝓟 ⎤ ∗ (|={E}=> emp)
+  
+1 subgoal
+  
+  Σ : gFunctors
+  H : invG Σ
+  I : biIndex
+  N : namespace
+  E : coPset
+  𝓟 : iProp Σ
+  H0 : ↑N ⊆ E
+  ============================
+  "HP" : ⎡ ▷ 𝓟 ⎤
+  "Hclose" : ⎡ ▷ 𝓟 ={E ∖ ↑N,E}=∗ emp ⎤
+  --------------------------------------∗
+  |={E ∖ ↑N,E}=> emp
+  

tests/proofmode_iris.v

-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import tactics monpred.
 From iris.base_logic Require Import base_logic.
 From iris.base_logic.lib Require Import invariants cancelable_invariants na_invariants.
 
@@ -50,6 +50,7 @@ End base_logic_tests.
 
 Section iris_tests.
   Context `{invG Σ, cinvG Σ, na_invG Σ}.
+  Implicit Types P Q R : iProp Σ.
 
   Lemma test_masks  N E P Q R :
     ↑N ⊆ E →
@@ -218,3 +219,32 @@ Section iris_tests.
     eauto.
   Qed.
 End iris_tests.
+
+Section monpred_tests.
+  Context `{invG Σ}.
+  Context {I : biIndex}.
+  Local Notation monPred := (monPred I (iPropI Σ)).
+  Local Notation monPredI := (monPredI I (iPropI Σ)).
+  Local Notation monPredSI := (monPredSI I (iPropSI Σ)).
+  Implicit Types P Q R : monPred.
+  Implicit Types 𝓟 𝓠 𝓡 : iProp Σ.
+
+  Lemma test_iInv N E 𝓟 :
+    ↑N ⊆ E →
+    ⎡inv N 𝓟⎤ ⊢@{monPredI} |={E}=> emp.
+  Proof.
+    iIntros (?) "Hinv".
+    iInv N as "HP". Show.
+    iFrame "HP". auto.
+  Qed.
+
+  Lemma test_iInv_with_close N E 𝓟 :
+    ↑N ⊆ E →
+    ⎡inv N 𝓟⎤ ⊢@{monPredI} |={E}=> emp.
+  Proof.
+    iIntros (?) "Hinv".
+    iInv N as "HP" "Hclose". Show.
+    iMod ("Hclose" with "HP"). auto.
+  Qed.
+
+End monpred_tests.

tests/proofmode_monpred.ref

+1 subgoal
+  
+  I : biIndex
+  PROP : sbi
+  P, Q : monpred.monPred I PROP
+  i : I
+  ============================
+  "HW" : (P -∗ Q) i
+  --------------------------------------∗
+  (P -∗ Q) i
+  
+1 subgoal
+  
+  I : biIndex
+  PROP : sbi
+  P, Q : monpred.monPred I PROP
+  i, j : I
+  ============================
+  "HW" : (P -∗ Q) j
+  "HP" : P j
+  --------------------------------------∗
+  Q j
+  
+1 subgoal
+  
+  I : biIndex
+  PROP : sbi
+  P, Q : monpred.monPred I PROP
+  Objective0 : Objective Q
+  𝓟, 𝓠 : PROP
+  ============================
+  "H2" : ∀ i : I, Q i
+  "H3" : 𝓟
+  "H4" : 𝓠
+  --------------------------------------∗
+  ∀ i : I, 𝓟 ∗ 𝓠 ∗ Q i
+  

tests/proofmode_monpred.v

@@ -29,7 +29,8 @@ Section tests.
 
   Lemma test_intowand_1 P Q : (P -∗ Q) -∗ P -∗ Q.
   Proof.
-    iStartProof PROP. iIntros (i) "HW". iIntros (j ->) "HP". by iApply "HW".
+    iStartProof PROP. iIntros (i) "HW". Show.
+    iIntros (j ->) "HP". Show. by iApply "HW".
   Qed.
   Lemma test_intowand_2 P Q : (P -∗ Q) -∗ P -∗ Q.
   Proof.
@@ -85,7 +86,7 @@ Section tests.
 
   Lemma test_iModIntro_embed_objective P `{!Objective Q} 𝓟 𝓠 :
     □ P -∗ Q -∗ ⎡𝓟⎤ -∗ ⎡𝓠⎤ -∗ ⎡ ∀ i, 𝓟 ∗ 𝓠 ∗ Q i ⎤.
-  Proof. iIntros "#H1 H2 H3 H4". iAlways. iFrame. Qed.
+  Proof. iIntros "#H1 H2 H3 H4". iAlways. Show. iFrame. Qed.
 
   Lemma test_iModIntro_embed_nested P 𝓟 𝓠 :
     □ P -∗ ⎡◇ 𝓟⎤ -∗ ⎡◇ 𝓠⎤ -∗ ⎡ ◇ (𝓟 ∗ 𝓠) ⎤.
@@ -93,7 +94,7 @@ Section tests.
 
   Lemma test_into_wand_embed 𝓟 𝓠 :
     (𝓟 -∗ ◇ 𝓠) →
-    ⎡𝓟⎤ ⊢@{monPredSI} ◇ ⎡𝓠⎤.
+    ⎡𝓟⎤ ⊢@{monPredI} ◇ ⎡𝓠⎤.
   Proof.
     iIntros (HPQ) "HP".
     iMod (HPQ with "[-]") as "$"; last by auto.

theories/base_logic/lib/iprop.v

@@ -118,6 +118,8 @@ Module Type iProp_solution_sig.
   Definition iResUR (Σ : gFunctors) : ucmraT :=
     ofe_funUR (λ i, gmapUR gname (Σ i (iPreProp Σ))).
   Notation iProp Σ := (uPredC (iResUR Σ)).
+  Notation iPropI Σ := (uPredI (iResUR Σ)).
+  Notation iPropSI Σ := (uPredSI (iResUR Σ)).
 
   Parameter iProp_unfold: ∀ {Σ}, iProp Σ -n> iPreProp Σ.
   Parameter iProp_fold: ∀ {Σ}, iPreProp Σ -n> iProp Σ.
@@ -149,7 +151,7 @@ End iProp_solution.
 
 (** * Properties of the solution to the recursive domain equation *)
 Lemma iProp_unfold_equivI {Σ} (P Q : iProp Σ) :
-  iProp_unfold P ≡ iProp_unfold Q ⊢ (P ≡ Q : iProp Σ).
+  iProp_unfold P ≡ iProp_unfold Q ⊢@{iPropI Σ} P ≡ Q.
 Proof.
   rewrite -{2}(iProp_fold_unfold P) -{2}(iProp_fold_unfold Q). apply: bi.f_equiv.
 Qed.

theories/proofmode/class_instances_sbi.v

@@ -552,11 +552,11 @@ Global Instance add_modal_embed_fupd_goal `{BiEmbedFUpd PROP PROP'}
 Proof. by rewrite /AddModal !embed_fupd. Qed.
 
 (* ElimAcc *)
-Global Instance elim_acc_vs `{BiFUpd PROP} {X} E1 E2 E α β mγ Q :
+Global Instance elim_acc_fupd `{BiFUpd PROP} {X} E1 E2 E α β mγ Q :
   (* FIXME: Why %I? ElimAcc sets the right scopes! *)
   ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1) α β mγ
           (|={E1,E}=> Q)
-          (λ x, |={E2}=> (β x ∗ (coq_tactics.maybe_wand (mγ x) (|={E1,E}=> Q))))%I.
+          (λ x, |={E2}=> β x ∗ (coq_tactics.maybe_wand (mγ x) (|={E1,E}=> Q)))%I.
 Proof.
   rewrite /ElimAcc. setoid_rewrite coq_tactics.maybe_wand_sound.
   iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".

theories/proofmode/monpred.v

@@ -482,18 +482,51 @@ Global Instance elim_modal_at_fupd_hyp `{BiFUpd PROP} φ p p' E1 E2 P 𝓟 𝓟'
   ElimModal φ p p' ((|={E1,E2}=> P) i) 𝓟' 𝓠 𝓠'.
 Proof. by rewrite /MakeMonPredAt /ElimModal monPred_at_fupd=><-. Qed.
 
+(* This instances are awfully specific, but that's what is needed. *)
+Global Instance elim_acc_at_fupd `{BiFUpd PROP} {X : Type} E1 E2 E
+       M1 M2 α β mγ Q (Q' : X → monPred) i :
+  ElimAcc (X:=X) M1 M2 α β mγ (|={E1,E}=> Q i)
+          (λ x, |={E2}=> β x ∗ (coq_tactics.maybe_wand (mγ x) (|={E1,E}=> Q' x i)))%I →
+  ElimAcc (X:=X) M1 M2 α β mγ ((|={E1,E}=> Q) i)
+          (λ x, (|={E2}=> ⎡β x⎤ ∗
+                         (coq_tactics.maybe_wand
+                            (match mγ x with Some 𝓟 => Some ⎡𝓟⎤ | None => None end)
+                            (|={E1,E}=> Q' x))) i)%I
+  | 1.
+Proof.
+  rewrite /ElimAcc monPred_at_fupd=><-. apply bi.forall_mono=>x.
+  destruct (mγ x); simpl.
+  - rewrite monPred_at_fupd monPred_at_sep monPred_wand_force monPred_at_fupd !monPred_at_embed //.
+  - rewrite monPred_at_fupd monPred_at_sep monPred_at_fupd !monPred_at_embed //.
+Qed.
+(* A separate, higher-priority instance for unit because otherwise unification
+fails. *)
+Global Instance elim_acc_at_fupd_unit `{BiFUpd PROP} E1 E2 E
+       M1 M2 α β mγ Q Q' i :
+  ElimAcc (X:=unit) M1 M2 α β mγ (|={E1,E}=> Q i)
+          (λ x, |={E2}=> β x ∗ (coq_tactics.maybe_wand (mγ x) (|={E1,E}=> Q' i)))%I →
+  ElimAcc (X:=unit) M1 M2 α β mγ ((|={E1,E}=> Q) i)
+          (λ x, (|={E2}=> ⎡β x⎤ ∗
+                         (coq_tactics.maybe_wand
+                            (match mγ x with Some 𝓟 => Some ⎡𝓟⎤ | None => None end)
+                            (|={E1,E}=> Q'))) i)%I
+  | 0.
+Proof. exact: elim_acc_at_fupd. Qed.
+
 Global Instance add_modal_at_fupd_goal `{BiFUpd PROP} E1 E2 𝓟 𝓟' Q i :
   AddModal 𝓟 𝓟' (|={E1,E2}=> Q i) → AddModal 𝓟 𝓟' ((|={E1,E2}=> Q) i).
 Proof. by rewrite /AddModal !monPred_at_fupd. Qed.
 
+(* This hard-codes the fact that ElimInv with_close returns a
+   [(λ _, ...)] as Q'. *)
 Global Instance elim_inv_embed_with_close {X : Type} φ
        𝓟inv 𝓟in (𝓟out 𝓟close : X → PROP)
        Pin (Pout Pclose : X → monPred)
-       Q (Q' : X → monPred) :
-  (∀ i, ElimInv φ 𝓟inv 𝓟in 𝓟out (Some 𝓟close) (Q i) (λ x, Q' x i)) →
+       Q Q' :
+  (∀ i, ElimInv φ 𝓟inv 𝓟in 𝓟out (Some 𝓟close) (Q i) (λ _, Q' i)) →
   MakeEmbed 𝓟in Pin → (∀ x, MakeEmbed (𝓟out x) (Pout x)) →
   (∀ x, MakeEmbed (𝓟close x) (Pclose x)) →
-  ElimInv (X:=X) φ ⎡𝓟inv⎤ Pin Pout (Some Pclose) Q Q'.
+  ElimInv (X:=X) φ ⎡𝓟inv⎤ Pin Pout (Some Pclose) Q (λ _, Q').
 Proof.
   rewrite /MakeEmbed /ElimInv=>H <- Hout Hclose ?. iStartProof PROP.
   setoid_rewrite <-Hout. setoid_rewrite <-Hclose.