From c6f4eac5f9c6c5d2da7d99a1b2747fa3d0e806f0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 24 Oct 2017 00:12:24 +0200
Subject: [PATCH] =?UTF-8?q?Avoid=20exponential=20proof=20search=20due=20to?=
 =?UTF-8?q?=20Plain=20=E2=86=92=20Persistent=20instance.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/base_logic/derived.v | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 850cfcbba..7506e6d47 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -960,7 +960,8 @@ Global Instance limit_preserving_Plain {A:ofeT} `{Cofe A} (Φ : A → uPred M) :
   NonExpansive Φ → LimitPreserving (λ x, Plain (Φ x)).
 Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
 
-Global Instance Plain_Persistent P : Plain P → Persistent P.
+(* Not an instance, see the bottom of this file *)
+Lemma plain_persistent P : Plain P → Persistent P.
 Proof. rewrite /Plain /Persistent=> HP. by rewrite {1}HP plainly_elim'. Qed.
 
 Lemma plainly_plainly P `{!Plain P} : ■ P ⊣⊢ P.
@@ -1061,6 +1062,8 @@ Proof.
   rewrite /Persistent -impl_wand pure_impl_forall persistently_forall.
   auto using forall_mono.
 Qed.
+Global Instance plainly_persistent P : Persistent (â–  P).
+Proof. by rewrite /Persistent persistently_plainly. Qed.
 Global Instance persistently_persistent P : Persistent (â–¡ P).
 Proof. by intros; apply persistently_intro'. Qed.
 Global Instance and_persistent P Q :
@@ -1165,3 +1168,12 @@ Global Instance uPred_ownM_sep_homomorphism :
 Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed.
 End derived.
 End uPred.
+
+(* When declared as an actual instance, [plain_persistent] will give cause
+failing proof searches to take exponential time, as Coq will try to apply it
+the instance at any node in the proof search tree.
+
+To avoid that, we declare it using a [Hint Immediate], so that it will only be
+used at the leaves of the proof search tree, i.e. when the premise of the hint
+can be derived from just the current context. *)
+Hint Immediate uPred.plain_persistent : typeclass_instances.
-- 
GitLab