Merge branch 'ralf/alloc-sep-conj' into 'master'

use sep. conjunction instead of conjunction for allocation lemmas

See merge request iris/iris!508

CHANGELOG.md

@@ -40,6 +40,14 @@ With this release, we dropped support for Coq 8.9.
 
 * Add a `ghost_var` library that provides (fractional) ownership of a ghost
   variable of arbitrary `Type`.
+* Change type of some ghost state lemmas (mostly about allocation) to use `∗`
+  instead of `∧` (consistent with our usual style).  This affects the following
+  lemmas: `own_alloc_strong_dep`, `own_alloc_cofinite_dep`, `own_alloc_strong`,
+  `own_alloc_cofinite`, `own_updateP`, `saved_anything_alloc_strong`,
+  `saved_anything_alloc_cofinite`, `saved_prop_alloc_strong`,
+  `saved_prop_alloc_cofinite`, `saved_pred_alloc_strong`,
+  `saved_pred_alloc_cofinite`, `auth_alloc_strong`, `auth_alloc_cofinite`,
+  `auth_alloc`.
 
 The following `sed` script helps adjust your code to the renaming (on macOS,
 replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).

theories/base_logic/lib/auth.v

@@ -147,7 +147,7 @@ Section auth.
 
   Lemma auth_alloc_strong N E t (I : gname → Prop) :
     pred_infinite I →
-    ✓ (f t) → ▷ φ t ={E}=∗ ∃ γ, ⌜I γ⌝ ∧ auth_ctx γ N f φ ∧ auth_own γ (f t).
+    ✓ (f t) → ▷ φ t ={E}=∗ ∃ γ, ⌜I γ⌝ ∗ auth_ctx γ N f φ ∗ auth_own γ (f t).
   Proof.
     iIntros (??) "Hφ". rewrite /auth_own /auth_ctx.
     iMod (own_alloc_strong (● f t ⋅ ◯ f t) I) as (γ) "[% [Hγ Hγ']]";
@@ -158,7 +158,7 @@ Section auth.
   Qed.
 
   Lemma auth_alloc_cofinite N E t (G : gset gname) :
-    ✓ (f t) → ▷ φ t ={E}=∗ ∃ γ, ⌜γ ∉ G⌝ ∧ auth_ctx γ N f φ ∧ auth_own γ (f t).
+    ✓ (f t) → ▷ φ t ={E}=∗ ∃ γ, ⌜γ ∉ G⌝ ∗ auth_ctx γ N f φ ∗ auth_own γ (f t).
   Proof.
     intros ?. apply auth_alloc_strong=>//.
     apply (pred_infinite_set (C:=gset gname)) => E'.
@@ -166,7 +166,7 @@ Section auth.
   Qed.
 
   Lemma auth_alloc N E t :
-    ✓ (f t) → ▷ φ t ={E}=∗ ∃ γ, auth_ctx γ N f φ ∧ auth_own γ (f t).
+    ✓ (f t) → ▷ φ t ={E}=∗ ∃ γ, auth_ctx γ N f φ ∗ auth_own γ (f t).
   Proof.
     iIntros (?) "Hφ".
     iMod (auth_alloc_cofinite N E t ∅ with "Hφ") as (γ) "[_ ?]"; eauto.

theories/base_logic/lib/ghost_var.v

@@ -38,14 +38,10 @@ Section lemmas.
   Lemma ghost_var_alloc_strong a (P : gname → Prop) :
     pred_infinite P →
     ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ ghost_var γ 1 a.
-  Proof.
-    iIntros (?). rewrite /ghost_var.
-    iMod (own_alloc_strong (to_frac_agree (A:=leibnizO A) 1 a) P)
-      as (γ ?) "Hown"; by eauto.
-  Qed.
+  Proof. intros. iApply own_alloc_strong; done. Qed.
   Lemma ghost_var_alloc a :
     ⊢ |==> ∃ γ, ghost_var γ 1 a.
-  Proof. rewrite /ghost_var. iApply own_alloc. done. Qed.
+  Proof. iApply own_alloc. done. Qed.
 
   Lemma ghost_var_op_valid γ a1 q1 a2 q2 :
     ghost_var γ q1 a1 -∗ ghost_var γ q2 a2 -∗ ⌜✓ (q1 + q2)%Qp ∧ a1 = a2⌝.

theories/base_logic/lib/own.v

@@ -150,7 +150,7 @@ Qed.
 Lemma own_alloc_strong_dep (f : gname → A) (P : gname → Prop) :
   pred_infinite P →
   (∀ γ, P γ → ✓ (f γ)) →
-  ⊢ |==> ∃ γ, ⌜P γ⌝ ∧ own γ (f γ).
+  ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ own γ (f γ).
 Proof.
   intros HP Ha.
   rewrite -(bupd_mono (∃ m, ⌜∃ γ, P γ ∧ m = iRes_singleton γ (f γ)⌝ ∧ uPred_ownM m)%I).
@@ -163,7 +163,7 @@ Proof.
     by rewrite !own_eq /own_def -(exist_intro γ) pure_True // left_id.
 Qed.
 Lemma own_alloc_cofinite_dep (f : gname → A) (G : gset gname) :
-  (∀ γ, γ ∉ G → ✓ (f γ)) → ⊢ |==> ∃ γ, ⌜γ ∉ G⌝ ∧ own γ (f γ).
+  (∀ γ, γ ∉ G → ✓ (f γ)) → ⊢ |==> ∃ γ, ⌜γ ∉ G⌝ ∗ own γ (f γ).
 Proof.
   intros Ha.
   apply (own_alloc_strong_dep f (λ γ, γ ∉ G))=> //.
@@ -175,21 +175,21 @@ Lemma own_alloc_dep (f : gname → A) :
   (∀ γ, ✓ (f γ)) → ⊢ |==> ∃ γ, own γ (f γ).
 Proof.
   intros Ha. rewrite /bi_emp_valid (own_alloc_cofinite_dep f ∅) //; [].
-  apply bupd_mono, exist_mono=>?. eauto using and_elim_r.
+  apply bupd_mono, exist_mono=>?. apply: sep_elim_r.
 Qed.
 
 Lemma own_alloc_strong a (P : gname → Prop) :
   pred_infinite P →
-  ✓ a → ⊢ |==> ∃ γ, ⌜P γ⌝ ∧ own γ a.
+  ✓ a → ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ own γ a.
 Proof. intros HP Ha. eapply own_alloc_strong_dep with (f := λ _, a); eauto. Qed.
 Lemma own_alloc_cofinite a (G : gset gname) :
-  ✓ a → ⊢ |==> ∃ γ, ⌜γ ∉ G⌝ ∧ own γ a.
+  ✓ a → ⊢ |==> ∃ γ, ⌜γ ∉ G⌝ ∗ own γ a.
 Proof. intros Ha. eapply own_alloc_cofinite_dep with (f := λ _, a); eauto. Qed.
 Lemma own_alloc a : ✓ a → ⊢ |==> ∃ γ, own γ a.
 Proof. intros Ha. eapply own_alloc_dep with (f := λ _, a); eauto. Qed.
 
 (** ** Frame preserving updates *)
-Lemma own_updateP P γ a : a ~~>: P → own γ a ==∗ ∃ a', ⌜P a'⌝ ∧ own γ a'.
+Lemma own_updateP P γ a : a ~~>: P → own γ a ==∗ ∃ a', ⌜P a'⌝ ∗ own γ a'.
 Proof.
   intros Ha. rewrite !own_eq.
   rewrite -(bupd_mono (∃ m, ⌜∃ a', m = iRes_singleton γ a' ∧ P a'⌝ ∧ uPred_ownM m)%I).
@@ -197,13 +197,14 @@ Proof.
       first by (eapply singleton_updateP', cmra_transport_updateP', Ha).
     naive_solver.
   - apply exist_elim=>m; apply pure_elim_l=>-[a' [-> HP]].
-    rewrite -(exist_intro a'). by apply and_intro; [apply pure_intro|].
+    rewrite -(exist_intro a'). rewrite -persistent_and_sep.
+      by apply and_intro; [apply pure_intro|].
 Qed.
 
 Lemma own_update γ a a' : a ~~> a' → own γ a ==∗ own γ a'.
 Proof.
   intros; rewrite (own_updateP (a' =.)); last by apply cmra_update_updateP.
-  by apply bupd_mono, exist_elim=> a''; apply pure_elim_l=> ->.
+  apply bupd_mono, exist_elim=> a''. rewrite sep_and. apply pure_elim_l=> -> //.
 Qed.
 Lemma own_update_2 γ a1 a2 a' :
   a1 ⋅ a2 ~~> a' → own γ a1 -∗ own γ a2 ==∗ own γ a'.

theories/base_logic/lib/saved_prop.v

@@ -41,11 +41,11 @@ Section saved_anything.
 
   Lemma saved_anything_alloc_strong x (I : gname → Prop) :
     pred_infinite I →
-    ⊢ |==> ∃ γ, ⌜I γ⌝ ∧ saved_anything_own γ x.
+    ⊢ |==> ∃ γ, ⌜I γ⌝ ∗ saved_anything_own γ x.
   Proof. intros ?. by apply own_alloc_strong. Qed.
 
   Lemma saved_anything_alloc_cofinite x (G : gset gname) :
-    ⊢ |==> ∃ γ, ⌜γ ∉ G⌝ ∧ saved_anything_own γ x.
+    ⊢ |==> ∃ γ, ⌜γ ∉ G⌝ ∗ saved_anything_own γ x.
   Proof. by apply own_alloc_cofinite. Qed.
 
   Lemma saved_anything_alloc x : ⊢ |==> ∃ γ, saved_anything_own γ x.
@@ -81,11 +81,11 @@ Proof. solve_contractive. Qed.
 
 Lemma saved_prop_alloc_strong `{!savedPropG Σ} (I : gname → Prop) (P: iProp Σ) :
   pred_infinite I →
-  ⊢ |==> ∃ γ, ⌜I γ⌝ ∧ saved_prop_own γ P.
+  ⊢ |==> ∃ γ, ⌜I γ⌝ ∗ saved_prop_own γ P.
 Proof. iIntros (?). by iApply saved_anything_alloc_strong. Qed.
 
 Lemma saved_prop_alloc_cofinite `{!savedPropG Σ} (G : gset gname) (P: iProp Σ) :
-  ⊢ |==> ∃ γ, ⌜γ ∉ G⌝ ∧ saved_prop_own γ P.
+  ⊢ |==> ∃ γ, ⌜γ ∉ G⌝ ∗ saved_prop_own γ P.
 Proof. iApply saved_anything_alloc_cofinite. Qed.
 
 Lemma saved_prop_alloc `{!savedPropG Σ} (P: iProp Σ) :
@@ -114,11 +114,11 @@ Qed.
 
 Lemma saved_pred_alloc_strong `{!savedPredG Σ A} (I : gname → Prop) (Φ : A → iProp Σ) :
   pred_infinite I →
-  ⊢ |==> ∃ γ, ⌜I γ⌝ ∧ saved_pred_own γ Φ.
+  ⊢ |==> ∃ γ, ⌜I γ⌝ ∗ saved_pred_own γ Φ.
 Proof. iIntros (?). by iApply saved_anything_alloc_strong. Qed.
 
 Lemma saved_pred_alloc_cofinite `{!savedPredG Σ A} (G : gset gname) (Φ : A → iProp Σ) :
-  ⊢ |==> ∃ γ, ⌜γ ∉ G⌝ ∧ saved_pred_own γ Φ.
+  ⊢ |==> ∃ γ, ⌜γ ∉ G⌝ ∗ saved_pred_own γ Φ.
 Proof. iApply saved_anything_alloc_cofinite. Qed.
 
 Lemma saved_pred_alloc `{!savedPredG Σ A} (Φ : A → iProp Σ) :