Generalize `elim_modal_fupd_fupd` to handle different masks.

iris/proofmode/class_instances_updates.v

-From stdpp Require Import nat_cancel.
+From stdpp Require Import nat_cancel coPset.
 From iris.bi Require Import bi.
 From iris.proofmode Require Import modality_instances classes.
 From iris.proofmode Require Import ltac_tactics class_instances.
@@ -155,11 +155,39 @@ Proof.
   by rewrite /ElimModal intuitionistically_if_elim
     (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans.
 Qed.
-Global Instance elim_modal_fupd_fupd `{!BiFUpd PROP} p E1 E2 E3 P Q :
-  ElimModal True p false (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
-Proof.
-  by rewrite /ElimModal intuitionistically_if_elim
-    fupd_frame_r wand_elim_r fupd_trans.
+
+Class ElimFUpdChangeMask (φ : Prop) (E1' E2' E1 E2 : coPset) := {
+  elim_fupd_change_mask_subseteq : φ → E1' ⊆ E1;
+  elim_fupd_change_mask_eq : φ → E2 = E2' ∪ E1 ∖ E1';
+}.
+Hint Mode ElimFUpdChangeMask - ! ! ! - : typeclass_instances.
+
+Global Instance elim_fupd_change_mask_same_src E1 E2 :
+  ElimFUpdChangeMask True E1 E2 E1 E2 | 0.
+Proof. split; set_solver. Qed.
+Global Instance elim_fupd_change_mask_src_empty E' E :
+  ElimFUpdChangeMask True ∅ E' E (E ∪ E') | 1.
+Proof. split; set_solver. Qed.
+Global Instance elim_fupd_change_mask_no_change E' E :
+  ElimFUpdChangeMask (E' ⊆ E) E' E' E E | 2.
+Proof. split; [done|]. intros. by apply union_difference_L. Qed.
+Global Instance elim_fupd_change_mask_tgt_empty E' E :
+  ElimFUpdChangeMask (E' ⊆ E) E' ∅ E (E ∖ E') | 3.
+Proof. split; set_solver. Qed.
+Global Instance elim_fupd_change_mask_default E1' E2' E1 :
+  ElimFUpdChangeMask (E1' ⊆ E1) E1' E2' E1 (E2' ∪ E1 ∖ E1') | 100.
+Proof. split; set_solver. Qed.
+
+Global Instance elim_modal_fupd_fupd `{!BiFUpd PROP} φ p E1' E2' E1 E2 E3 P Q :
+  ElimFUpdChangeMask φ E1' E2' E1 E2 →
+  ElimModal φ p false
+    (|={E1',E2'}=> P) P
+    (|={E1,E3}=> Q) (|={E2,E3}=> Q).
+Proof.
+  intros [? HE] ?.
+  rewrite intuitionistically_if_elim /= fupd_frame_r wand_elim_r.
+  rewrite {1}(fupd_mask_frame_r _ _ (E1 ∖ E1')); last set_solver.
+  rewrite HE // fupd_trans -union_difference_L; auto.
 Qed.
 
 Global Instance add_modal_bupd `{!BiBUpd PROP} P Q : AddModal (|==> P) P (|==> Q).