Merge branch 'fupd-commutes' into 'master'

Add missing commutations for `fupd`

See merge request iris/iris!688

CHANGELOG.md

@@ -40,6 +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`, and add
+  `{bupd,fupd}_{and,or,forall,exist}`.
 
 **Changes in `proofmode`:**
 
@@ -102,6 +104,7 @@ s/\bbig_sepM2_lookup_2\b/big_sepM2_lookup_r/g
 # big_*_intro
 s/\bbig_sep(L|L2|M|M2|S)_intuitionistically_forall\b/big_sep\1_intro/g
 s/\bbig_orL_lookup\b/big_orL_intro/g
+s/\bbupd_forall\b/bupd_plain_forall/g
 EOF
 ```
 

iris/bi/updates.v

@@ -201,10 +201,26 @@ Section bupd_derived.
     - apply bupd_intro.
   Qed.
 
-  Global Instance bupd_homomorphism :
+  Global Instance bupd_sep_homomorphism :
     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.
@@ -230,11 +246,11 @@ Section bupd_derived.
     Lemma bupd_plain P `{!Plain P} : (|==> P) ⊢ P.
     Proof. by rewrite {1}(plain P) bupd_plainly. Qed.
 
-    Lemma bupd_forall {A} (Φ : A → PROP) `{∀ x, Plain (Φ x)} :
+    Lemma bupd_plain_forall {A} (Φ : A → PROP) `{∀ x, Plain (Φ x)} :
       (|==> ∀ 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,10 +394,29 @@ 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.
 
-  Global Instance fupd_homomorphism E :
+  Global Instance fupd_sep_homomorphism E :
     MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (fupd (PROP:=PROP) E E).
   Proof. split; [split|]; try apply _; [apply fupd_sep | apply fupd_intro]. 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

@@ -22,7 +22,7 @@ Global Instance from_pure_bupd `{!BiBUpd PROP} a P φ :
 Proof. rewrite /FromPure=> <-. apply bupd_intro. Qed.
 Global Instance from_pure_fupd `{!BiFUpd PROP} a E P φ :
   FromPure a P φ → FromPure a (|={E}=> P) φ.
-Proof. rewrite /FromPure. intros <-. apply fupd_intro. Qed.
+Proof. rewrite /FromPure=> <-. apply fupd_intro. Qed.
 
 Global Instance into_wand_bupd `{!BiBUpd PROP} p q R P Q :
   IntoWand false false R P Q → IntoWand p q (|==> R) (|==> P) (|==> Q).
@@ -73,27 +73,31 @@ 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 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 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 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 :

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.