From d51217e4fbc7fcc905a67f78324116ebbe9f3cfd Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 14 Feb 2018 13:57:05 +0100
Subject: [PATCH] Attempt at fixing #146 definitively by having better types
 for update properties.

Assertions should have type sbi_car PROP and not bi_car (sbi_bi PROP).
---
 theories/bi/updates.v              | 19 ++++++++++---------
 theories/tests/proofmode_monpred.v |  5 +----
 2 files changed, 11 insertions(+), 13 deletions(-)

diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index ab8117037..3592d4f96 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -103,18 +103,19 @@ Qed.
 Class FUpdFacts (PROP : sbi) `{BUpd PROP, FUpd PROP} : Prop :=
   { fupd_bupd_facts :> BUpdFacts PROP;
     fupd_ne E1 E2 :> NonExpansive (fupd E1 E2);
-    fupd_intro_mask E1 E2 P : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P;
-    bupd_fupd E P : (|==> P) ={E}=∗ P;
-    except_0_fupd E1 E2 P : ◇ (|={E1,E2}=> P) ={E1,E2}=∗ P;
-    fupd_mono E1 E2 P Q : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q;
-    fupd_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) ⊢ |={E1,E3}=> P;
-    fupd_mask_frame_r' E1 E2 Ef P :
+    fupd_intro_mask E1 E2 (P : PROP) : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P;
+    bupd_fupd E (P : PROP) : (|==> P) ={E}=∗ P;
+    except_0_fupd E1 E2 (P : PROP) : ◇ (|={E1,E2}=> P) ={E1,E2}=∗ P;
+    fupd_mono E1 E2 (P Q : PROP) : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q;
+    fupd_trans E1 E2 E3 (P : PROP) : (|={E1,E2}=> |={E2,E3}=> P) ⊢ |={E1,E3}=> P;
+    fupd_mask_frame_r' E1 E2 Ef (P : PROP) :
       E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌝ → P) ={E1 ∪ Ef,E2 ∪ Ef}=∗ P;
-    fupd_frame_r E1 E2 P Q : (|={E1,E2}=> P) ∗ Q ={E1,E2}=∗ P ∗ Q;
-    fupd_plain' E1 E2 E2' P Q `{!Plain P} :
+    fupd_frame_r E1 E2 (P Q : PROP) : (|={E1,E2}=> P) ∗ Q ={E1,E2}=∗ P ∗ Q;
+    fupd_plain' E1 E2 E2' (P Q : PROP) `{!Plain P} :
       E1 ⊆ E2 →
       (Q ={E1, E2'}=∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P;
-    later_fupd_plain E P `{!Plain P} : (▷ |={E}=> P) ={E}=∗ ▷ ◇ P }.
+    later_fupd_plain E (P : PROP) `{!Plain P} : (▷ |={E}=> P) ={E}=∗ ▷ ◇ P }.
+
 Hint Mode FUpdFacts ! - - : typeclass_instances.
 
 Section fupd_derived.
diff --git a/theories/tests/proofmode_monpred.v b/theories/tests/proofmode_monpred.v
index fb7b6b35f..b0c24e0af 100644
--- a/theories/tests/proofmode_monpred.v
+++ b/theories/tests/proofmode_monpred.v
@@ -89,10 +89,7 @@ Section tests.
   Lemma test_apply_fupd_intro_mask E1 E2 P :
     E2 ⊆ E1 → P -∗ |={E1,E2}=> |={E2,E1}=> P.
   Proof.
-    iIntros.
-    (* FIXME : a (PROP:=...) is needed. See #146. *)
-    Fail iApply fupd_intro_mask.
-    by iApply (fupd_intro_mask (PROP:=monPredSI)).
+    iIntros. iApply fupd_intro_mask.
   Qed.
   Lemma test_apply_fupd_intro_mask_2 E1 E2 P :
     E2 ⊆ E1 → P -∗ |={E1,E2}=> |={E2,E1}=> P.
-- 
GitLab