From b2bb853ffd1ac0c92cf28636f9dee80a92c50cb3 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Fri, 21 May 2021 13:02:19 +0200
Subject: [PATCH] Add (non-persistent) IntoAnd & IntoForall for bupd/fupd

---
 iris/proofmode/class_instances_updates.v | 14 +++++++++++++
 tests/proofmode.v                        | 25 ++++++++++++++++++++++++
 2 files changed, 39 insertions(+)

diff --git a/iris/proofmode/class_instances_updates.v b/iris/proofmode/class_instances_updates.v
index 638d1ce28..135109503 100644
--- a/iris/proofmode/class_instances_updates.v
+++ b/iris/proofmode/class_instances_updates.v
@@ -78,6 +78,13 @@ Global Instance from_or_fupd `{!BiFUpd PROP} E1 E2 P Q1 Q2 :
   FromOr P Q1 Q2 → FromOr (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2).
 Proof. rewrite /FromOr=><-. apply fupd_or. Qed.
 
+Global Instance into_and_bupd `{!BiBUpd PROP} P Q1 Q2 :
+  IntoAnd false P Q1 Q2 → IntoAnd false (|==> P) (|==> Q1) (|==> Q2).
+Proof. rewrite /IntoAnd/==>->. apply bupd_and. Qed.
+Global Instance into_and_fupd `{!BiFUpd PROP} E1 E2 P Q1 Q2 :
+  IntoAnd false P Q1 Q2 → IntoAnd false (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2).
+Proof. rewrite /IntoAnd/==>->. apply fupd_and. Qed.
+
 Global Instance from_exist_bupd `{!BiBUpd PROP} {A} P (Φ : A → PROP) :
   FromExist P Φ → FromExist (|==> P) (λ a, |==> Φ a)%I.
 Proof. rewrite /FromExist=><-. apply bupd_exist. Qed.
@@ -85,6 +92,13 @@ Global Instance from_exist_fupd `{!BiFUpd PROP} {A} E1 E2 P (Φ : A → PROP) :
   FromExist P Φ → FromExist (|={E1,E2}=> P) (λ a, |={E1,E2}=> Φ a)%I.
 Proof. rewrite /FromExist=><-. apply fupd_exist. Qed.
 
+Global Instance into_forall_bupd `{!BiBUpd PROP} {A} P (Φ : A → PROP) :
+  IntoForall P Φ → IntoForall (|==> P) (λ a, |==> Φ a)%I.
+Proof. rewrite /IntoForall=>->. apply bupd_forall. Qed.
+Global Instance into_forall_fupd `{!BiFUpd PROP} {A} E1 E2 P (Φ : A → PROP) :
+  IntoForall P Φ → IntoForall (|={E1,E2}=> P) (λ a, |={E1,E2}=> Φ a)%I.
+Proof. rewrite /IntoForall=>->. apply fupd_forall. Qed.
+
 Global Instance from_forall_fupd
     `{!BiFUpd PROP, !BiPlainly PROP, !BiFUpdPlainly PROP} E1 E2 {A} P (Φ : A → PROP) name :
   (* Some cases in which [E2 ⊆ E1] holds *)
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 9cfc2beb4..71fabc8ba 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1054,6 +1054,31 @@ Lemma test_iDestruct_clear P Q R :
 Proof.
   iIntros "HP HQR". iDestruct "HQR" as "{HP} [HQ HR]". done.
 Qed.
+
+Lemma test_iSpecialize_bupd `{BiBUpd PROP} A (a : A) (P : A -> PROP) :
+  (|==> ∀ x, P x) ⊢ |==> P a.
+Proof.
+  iIntros "H". iSpecialize ("H" $! a). done.
+Qed.
+
+Lemma test_iSpecialize_fupd `{BiFUpd PROP} A (a : A) (P : A -> PROP) E1 E2 :
+  (|={E1, E2}=> ∀ x, P x) ⊢ |={E1, E2}=> P a.
+Proof.
+  iIntros "H". iSpecialize ("H" $! a). done.
+Qed.
+
+Lemma test_iDestruct_and_bupd `{BiBUpd PROP} (P Q : PROP) :
+  (|==> P ∧ Q) ⊢ |==> P.
+Proof.
+  iIntros "[P _]". done.
+Qed.
+
+Lemma test_iDestruct_and_fupd `{BiFUpd PROP} (P Q : PROP) E1 E2 :
+  (|={E1, E2}=> P ∧ Q) ⊢ |={E1, E2}=> P.
+Proof.
+  iIntros "[P _]". done.
+Qed.
+
 End tests.
 
 Section parsing_tests.
-- 
GitLab