diff --git a/iris/bi/plainly.v b/iris/bi/plainly.v index aa9906ef64697b716219af18fdc4f035cf4aff5b..a5839999645167744e727c35186d7c92056aa3b4 100644 --- a/iris/bi/plainly.v +++ b/iris/bi/plainly.v @@ -362,8 +362,7 @@ Proof. intros; destruct p; simpl; apply _. Qed. Lemma plain_persistent P : Plain P → Persistent P. Proof. intros. by rewrite /Persistent -plainly_elim_persistently. Qed. -(* Not an instance, see the bottom of this file *) -Lemma impl_persistent P Q : +Global Instance impl_persistent P Q : Absorbing P → Plain P → Persistent Q → Persistent (P → Q). Proof. intros. by rewrite /Persistent {2}(plain P) -persistently_impl_plainly @@ -645,10 +644,3 @@ 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. *) Global Hint Immediate plain_persistent : typeclass_instances. - -(* Not defined using an ordinary [Instance] because the default -[class_apply @impl_persistent] shelves the [BiPlainly] premise, making proof -search for the other premises fail. See the proof of [coreP_persistent] for an -example where it would fail with a regular [Instance].*) -Global Hint Extern 4 (Persistent _) => - notypeclasses refine (impl_persistent _ _ _ _ _) : typeclass_instances. diff --git a/tests/bi.ref b/tests/bi.ref new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/tests/bi.v b/tests/bi.v new file mode 100644 index 0000000000000000000000000000000000000000..92f797609a9d6fb3d00f982206b91dd3ba0f6d9a --- /dev/null +++ b/tests/bi.v @@ -0,0 +1,9 @@ +From iris.bi Require Import bi plainly. + +(** See https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/610 *) +Lemma test_impl_persistent_1 `{!BiPlainly PROP} : + Persistent (PROP:=PROP) (True → True). +Proof. apply _. Qed. +Lemma test_impl_persistent_2 `{!BiPlainly PROP} : + Persistent (PROP:=PROP) (True → True → True). +Proof. apply _. Qed.