From e99d05fbae862cbd76ec86ab54b3fa7c5201948f 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 | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 8bc2fbbc3..9d152c84b 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -961,7 +961,7 @@ Global Instance limit_preserving_PlainP {A:ofeT} `{Cofe A} (Φ : A → uPred M)
   NonExpansive Φ → LimitPreserving (λ x, PlainP (Φ x)).
 Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
 
-Global Instance Plain_Persistent P : PlainP P → PersistentP P.
+Lemma plain_persistent P : PlainP P → PersistentP P.
 Proof. rewrite /PlainP /PersistentP => HP. by rewrite {1}HP plainly_elim'. Qed.
 
 Lemma plainly_plainly P `{!PlainP P} : ☃ P ⊣⊢ P.
@@ -1062,6 +1062,8 @@ Proof.
   rewrite /PersistentP -always_impl_wand pure_impl_forall always_forall.
   auto using forall_mono.
 Qed.
+Global Instance plainly_persistent P : PersistentP (☃ P).
+Proof. by rewrite /PersistentP always_plainly. Qed.
 Global Instance always_persistent P : PersistentP (â–¡ P).
 Proof. by intros; apply always_intro'. Qed.
 Global Instance and_persistent P Q :
@@ -1166,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