From e181f73749d2fcabd38bb9d60a12fd7cf616a28d Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 18 Jan 2018 20:58:13 +0100
Subject: [PATCH] The types of propositions for monPred lemma need to be
 [monPred I PROP] and not [bi_car (monPredI I PROP)], otherwise iIntoValid
 fails in a very weird way. Seems to be related to a Coq bug.

---
 theories/bi/monpred.v              | 12 +++++++-----
 theories/tests/proofmode_monpred.v |  5 +++++
 2 files changed, 12 insertions(+), 5 deletions(-)

diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index aa90cfe25..5b70ef429 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -395,11 +395,12 @@ End canonical_sbi.
 
 Section bi_facts.
 Context {I : biIndex} {PROP : bi}.
+Local Notation monPred := (monPred I PROP).
 Local Notation monPredI := (monPredI I PROP).
 Local Notation monPred_at := (@monPred_at I PROP).
 Local Notation BiIndexBottom := (@BiIndexBottom I).
 Implicit Types i : I.
-Implicit Types P Q : monPredI.
+Implicit Types P Q : monPred.
 
 (** Instances *)
 
@@ -565,9 +566,9 @@ Lemma monPred_at_or i P Q : (P ∨ Q) i ⊣⊢ P i ∨ Q i.
 Proof. by unseal. Qed.
 Lemma monPred_at_impl i P Q : (P → Q) i ⊣⊢ ∀ j, ⌜i ⊑ j⌝ → P j → Q j.
 Proof. by unseal. Qed.
-Lemma monPred_at_forall {A} i (Φ : A → monPredI) : (∀ x, Φ x) i ⊣⊢ ∀ x, Φ x i.
+Lemma monPred_at_forall {A} i (Φ : A → monPred) : (∀ x, Φ x) i ⊣⊢ ∀ x, Φ x i.
 Proof. by unseal. Qed.
-Lemma monPred_at_exist {A} i (Φ : A → monPredI) : (∃ x, Φ x) i ⊣⊢ ∃ x, Φ x i.
+Lemma monPred_at_exist {A} i (Φ : A → monPred) : (∃ x, Φ x) i ⊣⊢ ∃ x, Φ x i.
 Proof. by unseal. Qed.
 Lemma monPred_at_sep i P Q : (P ∗ Q) i ⊣⊢ P i ∗ Q i.
 Proof. by unseal. Qed.
@@ -743,9 +744,10 @@ End bi_facts.
 
 Section sbi_facts.
 Context {I : biIndex} {PROP : sbi}.
+Local Notation monPred := (monPred I PROP).
 Local Notation monPredSI := (monPredSI I PROP).
 Implicit Types i : I.
-Implicit Types P Q : monPredSI.
+Implicit Types P Q : monPred.
 
 Global Instance monPred_at_timeless P i : Timeless P → Timeless (P i).
 Proof. move => [] /(_ i). unfold Timeless. by unseal. Qed.
@@ -810,7 +812,7 @@ Lemma monPred_at_except_0 i P : (◇ P) i ⊣⊢ ◇ P i.
 Proof. by unseal. Qed.
 
 Lemma monPred_fupd_embed `{FUpdFacts PROP} E1 E2 (P : PROP) :
-  ⎡|={E1,E2}=> P⎤ ⊣⊢ fupd E1 E2 (PROP:=monPred I PROP) ⎡P⎤.
+  ⎡|={E1,E2}=> P⎤ ⊣⊢ fupd E1 E2 (PROP:=monPred) ⎡P⎤.
 Proof.
   unseal. split=>i /=. setoid_rewrite bi.pure_impl_forall. apply bi.equiv_spec; split.
   - by do 2 apply bi.forall_intro=>?.
diff --git a/theories/tests/proofmode_monpred.v b/theories/tests/proofmode_monpred.v
index 7ed60b324..7f97a1d07 100644
--- a/theories/tests/proofmode_monpred.v
+++ b/theories/tests/proofmode_monpred.v
@@ -50,4 +50,9 @@ Section tests.
     iStartProof PROP. iIntros (i) "HW". iIntros (j ->) "HP".
     iSpecialize ("HW" with "HP"). done.
   Qed.
+
+  Lemma test_apply_in_elim (P : monPredI) (i : I) : monPred_in i ∧ ⎡ P i ⎤ -∗ P.
+  Proof.
+    iIntros. by iApply monPred_in_elim.
+  Qed.
 End tests.
-- 
GitLab