From 71cd889a9db63a9c764b90273067585cc640fae0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 25 Oct 2018 01:02:04 +0200
Subject: [PATCH] =?UTF-8?q?Allow=20introduction=20of=20`=E2=88=80`=20under?=
 =?UTF-8?q?=20`|=3D{E1,E2}=3D>`=20in=20case=20the=20predicate=20is=20plain?=
 =?UTF-8?q?.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/proofmode/class_instances_sbi.v | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/theories/proofmode/class_instances_sbi.v b/theories/proofmode/class_instances_sbi.v
index e622f11a8..5d8aae731 100644
--- a/theories/proofmode/class_instances_sbi.v
+++ b/theories/proofmode/class_instances_sbi.v
@@ -321,6 +321,24 @@ Global Instance from_forall_plainly `{BiPlainly PROP} {A} P (Φ : A → PROP) :
   FromForall P Φ → FromForall (■ P)%I (λ a, ■ (Φ a))%I.
 Proof. rewrite /FromForall=> <-. by rewrite plainly_forall. Qed.
 
+Global Instance from_forall_fupd `{BiFUpdPlainly PROP} E1 E2 {A} P (Φ : A → PROP) :
+  (* Some cases in which [E2 ⊆ E1] holds *)
+  TCOr (TCEq E1 E2) (TCOr (TCEq E1 ⊤) (TCEq E2 ∅)) →
+  FromForall P Φ → (∀ x, Plain (Φ x)) →
+  FromForall (|={E1,E2}=> P)%I (λ a, |={E1,E2}=> (Φ a))%I.
+Proof.
+  rewrite /FromForall=> -[->|[->|->]] <- ?; rewrite fupd_plain_forall; set_solver.
+Qed.
+
+Global Instance from_forall_step_fupd `{BiFUpdPlainly PROP} E1 E2 {A} P (Φ : A → PROP) :
+  (* Some cases in which [E2 ⊆ E1] holds *)
+  TCOr (TCEq E1 E2) (TCOr (TCEq E1 ⊤) (TCEq E2 ∅)) →
+  FromForall P Φ → (∀ x, Plain (Φ x)) →
+  FromForall (|={E1,E2}▷=> P)%I (λ a, |={E1,E2}▷=> (Φ a))%I.
+Proof.
+  rewrite /FromForall=> -[->|[->|->]] <- ?; rewrite step_fupd_plain_forall; set_solver.
+Qed.
+
 (** IsExcept0 *)
 Global Instance is_except_0_except_0 P : IsExcept0 (â—‡ P).
 Proof. by rewrite /IsExcept0 except_0_idemp. Qed.
-- 
GitLab