Merge branch 'robbert/inv_combine' into 'master'

Add lemma `inv_combine`.

See merge request iris/iris!431

CHANGELOG.md

@@ -193,6 +193,9 @@ Coq development, but not every API-breaking change is listed.  Changes marked
     instead of `■ ⎡P⎤ ⊢ ⎡■ P⎤`) as it has been generalized to BIs without a
     internal equality. In the past, the left-to-right direction was obtained for
     "free" using the rules of internal equality.
+* Rename `inv_sep_1` → `inv_split_1`, `inv_sep_2` → `inv_split_2`, and
+  `inv_sep` → `inv_split` to be consistent with the naming convention in boxes.
+* Add lemmas `inv_combine` and `inv_combine_dup_l` for combining invariants.
 
 The following `sed` script should perform most of the renaming (FIXME: incomplete)
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
@@ -212,6 +215,8 @@ s/\blist_alter_singletonM\b/list_alter_singleton/g
 s/\blist_singletonM_included\b/list_singleton_included/g
 # auth_both_frac_op rename
 s/\bauth_both_frac_op\b/auth_both_op/g
+# inv_sep
+s/\binv_sep\b/inv_split/g
 ' $(find theories -name "*.v")
 ```
 

theories/base_logic/lib/invariants.v

@@ -132,6 +132,31 @@ Section inv.
     rewrite inv_eq /inv_def; iIntros (?) "#HI". by iApply "HI".
   Qed.
 
+  Lemma inv_combine N1 N2 N P Q :
+    N1 ## N2 →
+    ↑N1 ∪ ↑N2 ⊆@{coPset} ↑N →
+    inv N1 P -∗ inv N2 Q -∗ inv N (P ∗ Q).
+  Proof.
+    rewrite inv_eq. iIntros (??) "#HinvP #HinvQ !#"; iIntros (E ?).
+    iMod ("HinvP" with "[%]") as "[$ HcloseP]"; first set_solver.
+    iMod ("HinvQ" with "[%]") as "[$ HcloseQ]"; first set_solver.
+    iMod (fupd_intro_mask' _ (E ∖ ↑N)) as "Hclose"; first set_solver.
+    iIntros "!> [HP HQ]".
+    iMod "Hclose" as %_. iMod ("HcloseQ" with "HQ") as %_. by iApply "HcloseP".
+  Qed.
+
+  Lemma inv_combine_dup_l N P Q :
+    □ (P -∗ P ∗ P) -∗
+    inv N P -∗ inv N Q -∗ inv N (P ∗ Q).
+  Proof.
+    rewrite inv_eq. iIntros "#HPdup #HinvP #HinvQ !#" (E ?).
+    iMod ("HinvP" with "[//]") as "[HP HcloseP]".
+    iDestruct ("HPdup" with "HP") as "[$ HP]".
+    iMod ("HcloseP" with "HP") as %_.
+    iMod ("HinvQ" with "[//]") as "[$ HcloseQ]".
+    iIntros "!> [HP HQ]". by iApply "HcloseQ".
+  Qed.
+
   (** ** Proof mode integration *)
   Global Instance into_inv_inv N P : IntoInv (inv N P) N := {}.
 
@@ -165,22 +190,20 @@ Section inv.
     iIntros "!> {$HP} HP". iApply "Hclose"; auto.
   Qed.
 
-  Lemma inv_sep_l N P Q : inv N (P ∗ Q) -∗ inv N P.
+  Lemma inv_split_l N P Q : inv N (P ∗ Q) -∗ inv N P.
   Proof.
     iIntros "#HI". iApply inv_alter; eauto.
     iIntros "!> !> [$ $] $".
   Qed.
-
-  Lemma inv_sep_r N P Q : inv N (P ∗ Q) -∗ inv N Q.
+  Lemma inv_split_r N P Q : inv N (P ∗ Q) -∗ inv N Q.
   Proof.
-    rewrite (comm _ P Q). eapply inv_sep_l.
+    rewrite (comm _ P Q). eapply inv_split_l.
   Qed.
-
-  Lemma inv_sep N P Q : inv N (P ∗ Q) -∗ inv N P ∗ inv N Q.
+  Lemma inv_split N P Q : inv N (P ∗ Q) -∗ inv N P ∗ inv N Q.
   Proof.
     iIntros "#H".
-    iPoseProof (inv_sep_l with "H") as "$".
-    iPoseProof (inv_sep_r with "H") as "$".
+    iPoseProof (inv_split_l with "H") as "$".
+    iPoseProof (inv_split_r with "H") as "$".
   Qed.
 
 End inv.