Add (non-persistent) IntoAnd & IntoForall for bupd/fupd

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 *)

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.