From 0ea97ab3853a8a16bce35f040aaa1e4cef6da8d9 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 25 Jan 2018 10:43:33 +0100
Subject: [PATCH] Make iStartProof convert Coq universals into bi universals.

---
 theories/proofmode/class_instances.v | 9 +++++++++
 theories/tests/proofmode_monpred.v   | 9 +++++++++
 2 files changed, 18 insertions(+)

diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index e2c19865a..b0794eba7 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -1024,6 +1024,7 @@ Global Instance elim_modal_bupd_plain `{BUpdFacts PROP} P Q :
   Plain P → ElimModal (|==> P) P Q Q.
 Proof. intros. by rewrite /ElimModal bupd_plain wand_elim_r. Qed.
 
+(* AsValid *)
 Global Instance as_valid_valid {PROP : bi} (P : PROP) : AsValid0 (bi_valid P) P | 0.
 Proof. by rewrite /AsValid. Qed.
 Global Instance as_valid_entails {PROP : bi} (P Q : PROP) : AsValid0 (P ⊢ Q) (P -∗ Q).
@@ -1031,6 +1032,14 @@ Proof. split. apply bi.entails_wand. apply bi.wand_entails. Qed.
 Global Instance as_valid_equiv {PROP : bi} (P Q : PROP) : AsValid0 (P ≡ Q) (P ∗-∗ Q).
 Proof. split. apply bi.equiv_wand_iff. apply bi.wand_iff_equiv. Qed.
 
+Global Instance as_valid_forall {A : Type} (φ : A → Prop) (P : A → PROP) :
+  (∀ x, AsValid (φ x) (P x)) → AsValid (∀ x, φ x) (∀ x, P x).
+Proof.
+  rewrite /AsValid=>H1. split=>H2.
+  - apply bi.forall_intro=>?. apply H1, H2.
+  - intros x. apply H1. revert H2. by rewrite (bi.forall_elim x).
+Qed.
+
 Global Instance as_valid_embed `{BiEmbedding PROP PROP'} (φ : Prop) (P : PROP) :
   AsValid0 φ P → AsValid φ ⎡P⎤.
 Proof. rewrite /AsValid0 /AsValid=> ->. rewrite bi_embed_valid //. Qed.
diff --git a/theories/tests/proofmode_monpred.v b/theories/tests/proofmode_monpred.v
index 7f97a1d07..8532b4817 100644
--- a/theories/tests/proofmode_monpred.v
+++ b/theories/tests/proofmode_monpred.v
@@ -55,4 +55,13 @@ Section tests.
   Proof.
     iIntros. by iApply monPred_in_elim.
   Qed.
+
+  Lemma test_iStartProof_forall_1 (Φ : nat → monPredI) : ∀ n, Φ n -∗ Φ n.
+  Proof.
+    iStartProof PROP. iIntros (n i) "$".
+  Qed.
+  Lemma test_iStartProof_forall_2 (Φ : nat → monPredI) : ∀ n, Φ n -∗ Φ n.
+  Proof.
+    iStartProof. iIntros (n) "$".
+  Qed.
 End tests.
-- 
GitLab