Add missing commutations for `fupd`

Suggestion from Gregory Malecha, forall lemmas suggested by Robbert & Ralf,
proof scripts from me.

CHANGELOG.md

@@ -40,7 +40,8 @@ Coq 8.11 is no longer supported in this version of Iris.
 * Add lemmas for swapping nested big-ops: `big_sep{L,M,S,MS}_sep{L,M,S,MS}`.
 * Rename `big_sep{L,L2,M,M2,S}_intuitionistically_forall` →
   `big_sep{L,L2,M,M2,S}_intro`, and `big_orL_lookup` → `big_orL_intro`.
-* Rename `bupd_forall` to `bupd_plain_forall`.
+* Rename `bupd_forall` to `bupd_plain_forall`, and add
+  `{bupd,fupd}_{and,or,forall,exist}`.
 
 **Changes in `proofmode`:**
 

iris/bi/updates.v

@@ -205,6 +205,22 @@ Section bupd_derived.
     MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (bupd (PROP:=PROP)).
   Proof. split; [split|]; try apply _; [apply bupd_sep | apply bupd_intro]. Qed.
 
+  Lemma bupd_or P Q : (|==> P) ∨ (|==> Q) ⊢ |==> (P ∨ Q).
+  Proof. apply or_elim; apply bupd_mono; [ apply or_intro_l | apply or_intro_r ]. Qed.
+
+  Global Instance bupd_or_homomorphism :
+    MonoidHomomorphism bi_or bi_or (flip (⊢)) (bupd (PROP:=PROP)).
+  Proof. split; [split|]; try apply _; [apply bupd_or | apply bupd_intro]. Qed.
+
+  Lemma bupd_and P Q : (|==> (P ∧ Q)) ⊢ (|==> P) ∧ (|==> Q).
+  Proof. apply and_intro; apply bupd_mono; [apply and_elim_l | apply and_elim_r]. Qed.
+
+  Lemma bupd_exist A (Φ : A → PROP) : (∃ x : A, |==> Φ x) ⊢ |==> ∃ x : A, Φ x.
+  Proof. apply exist_elim=> a. by rewrite -(exist_intro a). Qed.
+
+  Lemma bupd_forall A (Φ : A → PROP) : (|==> ∀ x : A, Φ x) ⊢ ∀ x : A, |==> Φ x.
+  Proof. apply forall_intro=> a. by rewrite -(forall_elim a). Qed.
+
   Lemma big_sepL_bupd {A} (Φ : nat → A → PROP) l :
     ([∗ list] k↦x ∈ l, |==> Φ k x) ⊢ |==> [∗ list] k↦x ∈ l, Φ k x.
   Proof. by rewrite (big_opL_commute _). Qed.
@@ -234,7 +250,7 @@ Section bupd_derived.
       (|==> ∀ x, Φ x) ⊣⊢ (∀ x, |==> Φ x).
     Proof.
       apply (anti_symm _).
-      - apply forall_intro=> x. by rewrite (forall_elim x).
+      - apply bupd_forall.
       - rewrite -bupd_intro. apply forall_intro=> x.
         by rewrite (forall_elim x) bupd_plain.
     Qed.
@@ -378,6 +394,25 @@ Section fupd_derived.
     apply fupd_mask_intro_subseteq; set_solver.
   Qed.
 
+  Lemma fupd_or E1 E2 P Q :
+    (|={E1,E2}=> P) ∨ (|={E1,E2}=> Q) ⊢@{PROP}
+    (|={E1,E2}=> (P ∨ Q)).
+  Proof. apply or_elim; apply fupd_mono; [ apply or_intro_l | apply or_intro_r ]. Qed.
+
+  Global Instance fupd_or_homomorphism E :
+    MonoidHomomorphism bi_or bi_or (flip (⊢)) (fupd (PROP:=PROP) E E).
+  Proof. split; [split|]; try apply _; [apply fupd_or | apply fupd_intro]. Qed.
+
+  Lemma fupd_and E1 E2 P Q :
+    (|={E1,E2}=> (P ∧ Q)) ⊢@{PROP} (|={E1,E2}=> P) ∧ (|={E1,E2}=> Q).
+  Proof. apply and_intro; apply fupd_mono; [apply and_elim_l | apply and_elim_r]. Qed.
+
+  Lemma fupd_exist E1 E2 A (Φ : A → PROP) : (∃ x : A, |={E1, E2}=> Φ x) ⊢ |={E1, E2}=> ∃ x : A, Φ x.
+  Proof. apply exist_elim=> a. by rewrite -(exist_intro a). Qed.
+
+  Lemma fupd_forall E1 E2 A (Φ : A → PROP) : (|={E1, E2}=> ∀ x : A, Φ x) ⊢ ∀ x : A, |={E1, E2}=> Φ x.
+  Proof. apply forall_intro=> a. by rewrite -(forall_elim a). Qed.
+
   Lemma fupd_sep E P Q : (|={E}=> P) ∗ (|={E}=> Q) ={E}=∗ P ∗ Q.
   Proof. by rewrite fupd_frame_r fupd_frame_l fupd_trans. Qed.
 
@@ -536,8 +571,7 @@ Section fupd_derived.
       E2 ⊆ E1 →
       (|={E1,E2}=> ∀ x, Φ x) ⊣⊢ (∀ x, |={E1,E2}=> Φ x).
     Proof.
-      intros. apply (anti_symm _).
-      { apply forall_intro=> x. by rewrite (forall_elim x). }
+      intros. apply (anti_symm _); first apply fupd_forall.
       trans (∀ x, |={E1}=> Φ x)%I.
       { apply forall_mono=> x. by rewrite fupd_plain_mask. }
       rewrite fupd_plain_forall_2. apply fupd_elim.

iris/proofmode/class_instances_updates.v

@@ -73,27 +73,17 @@ Proof. rewrite /FromSep =><-. apply fupd_sep. Qed.
 
 Global Instance from_or_bupd `{!BiBUpd PROP} P Q1 Q2 :
   FromOr P Q1 Q2 → FromOr (|==> P) (|==> Q1) (|==> Q2).
-Proof.
-  rewrite /FromOr=><-.
-  apply or_elim; apply bupd_mono; auto using or_intro_l, or_intro_r.
-Qed.
+Proof. rewrite /FromOr=><-. apply bupd_or. Qed.
 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 or_elim; apply fupd_mono;
-                         [apply bi.or_intro_l|apply bi.or_intro_r].
-Qed.
+Proof. rewrite /FromOr=><-. apply fupd_or. Qed.
 
 Global Instance from_exist_bupd `{!BiBUpd PROP} {A} P (Φ : A → PROP) :
   FromExist P Φ → FromExist (|==> P) (λ a, |==> Φ a)%I.
-Proof.
-  rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
-Qed.
+Proof. rewrite /FromExist=><-. apply bupd_exist. Qed.
 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 exist_elim=> a. by rewrite -(exist_intro a).
-Qed.
+Proof. rewrite /FromExist=><-. apply fupd_exist. Qed.
 
 Global Instance from_forall_fupd
     `{!BiFUpd PROP, !BiPlainly PROP, !BiFUpdPlainly PROP} E1 E2 {A} P (Φ : A → PROP) name :