Merge branch 'own_alloc_infinite' into 'master'

Implement `own_alloc_infinite`

Closes #207

See merge request iris/iris!217

CHANGELOG.md

@@ -100,6 +100,9 @@ Changes in Coq:
   steps that would require unlocking subterms. Every impure wp_ tactic executes
   this tactic before doing anything else.
 * Add `big_sepM_insert_acc`.
+* The `_strong` lemmas (e.g. `own_alloc_strong`) work for all infinite
+  sets, instead of just for cofinite sets. The versions with cofinite
+  sets have been renamed to use the `_cofinite` suffix.
 
 ## Iris 3.1.0 (released 2017-12-19)
 

theories/algebra/gmap.v

 From iris.algebra Require Export cmra.
-From stdpp Require Export gmap.
+From stdpp Require Export list gmap.
 From iris.algebra Require Import updates local_updates.
 From iris.base_logic Require Import base_logic.
 From iris.algebra Require Import proofmode_classes.
@@ -354,29 +354,48 @@ Qed.
 Section freshness.
   Local Set Default Proof Using "Type*".
   Context `{!Infinite K}.
-  Lemma alloc_updateP_strong (Q : gmap K A → Prop) (I : gset K) m x :
-    ✓ x → (∀ i, m !! i = None → i ∉ I → Q (<[i:=x]>m)) → m ~~>: Q.
+  Lemma alloc_updateP_strong (Q : gmap K A → Prop) (I : K → Prop) m x :
+    pred_infinite I →
+    ✓ x → (∀ i, m !! i = None → I i → Q (<[i:=x]>m)) → m ~~>: Q.
   Proof.
-    intros ? HQ. apply cmra_total_updateP.
-    intros n mf Hm. set (i := fresh (I ∪ dom (gset K) (m ⋅ mf))).
-    assert (i ∉ I ∧ i ∉ dom (gset K) m ∧ i ∉ dom (gset K) mf) as [?[??]].
-    { rewrite -not_elem_of_union -dom_op -not_elem_of_union; apply is_fresh. }
+    move=> /(pred_infinite_set I (C:=gset K)) HP ? HQ.
+    apply cmra_total_updateP. intros n mf Hm.
+    destruct (HP (dom (gset K) (m ⋅ mf))) as [i [Hi1 Hi2]].
+    assert (m !! i = None).
+    { eapply (not_elem_of_dom (D:=gset K)). revert Hi2.
+      rewrite dom_op not_elem_of_union. naive_solver. }
     exists (<[i:=x]>m); split.
-    { apply HQ; last done. by eapply not_elem_of_dom. }
-    rewrite insert_singleton_op; last by eapply not_elem_of_dom.
-    rewrite -assoc -insert_singleton_op;
-      last by eapply (not_elem_of_dom (D:=gset K)); rewrite dom_op not_elem_of_union.
+    - by apply HQ.
+    - rewrite insert_singleton_op //.
+      rewrite -assoc -insert_singleton_op;
+        last by eapply (not_elem_of_dom (D:=gset K)).
     by apply insert_validN; [apply cmra_valid_validN|].
   Qed.
   Lemma alloc_updateP (Q : gmap K A → Prop) m x :
     ✓ x → (∀ i, m !! i = None → Q (<[i:=x]>m)) → m ~~>: Q.
-  Proof. move=>??. eapply alloc_updateP_strong with (I:=∅); by eauto. Qed.
-  Lemma alloc_updateP_strong' m x (I : gset K) :
-    ✓ x → m ~~>: λ m', ∃ i, i ∉ I ∧ m' = <[i:=x]>m ∧ m !! i = None.
+  Proof.
+    move=>??.
+    eapply alloc_updateP_strong with (I:=λ _, True);
+    eauto using pred_infinite_True.
+  Qed.
+  Lemma alloc_updateP_strong' m x (I : K → Prop) :
+    pred_infinite I →
+    ✓ x → m ~~>: λ m', ∃ i, I i ∧ m' = <[i:=x]>m ∧ m !! i = None.
   Proof. eauto using alloc_updateP_strong. Qed.
   Lemma alloc_updateP' m x :
     ✓ x → m ~~>: λ m', ∃ i, m' = <[i:=x]>m ∧ m !! i = None.
   Proof. eauto using alloc_updateP. Qed.
+  Lemma alloc_updateP_cofinite (Q : gmap K A → Prop) (J : gset K) m x :
+    ✓ x → (∀ i, m !! i = None → i ∉ J → Q (<[i:=x]>m)) → m ~~>: Q.
+  Proof.
+    eapply alloc_updateP_strong.
+    apply (pred_infinite_set (C:=gset K)).
+    intros E. exists (fresh (J ∪ E)).
+    apply not_elem_of_union, is_fresh.
+  Qed.
+  Lemma alloc_updateP_cofinite' m x (J : gset K) :
+    ✓ x → m ~~>: λ m', ∃ i, i ∉ J ∧ m' = <[i:=x]>m ∧ m !! i = None.
+  Proof. eauto using alloc_updateP_cofinite. Qed.
 End freshness.
 
 Lemma alloc_unit_singleton_updateP (P : A → Prop) (Q : gmap K A → Prop) u i :

theories/base_logic/lib/auth.v

@@ -102,22 +102,31 @@ Section auth.
   Global Instance own_mono' γ : Proper (flip (≼) ==> (⊢)) (auth_own γ).
   Proof. intros a1 a2. apply auth_own_mono. Qed.
 
-  Lemma auth_alloc_strong N E t (G : gset gname) :
-    ✓ (f t) → ▷ φ t ={E}=∗ ∃ γ, ⌜γ ∉ G⌝ ∧ auth_ctx γ N f φ ∧ auth_own γ (f t).
+  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).
   Proof.
-    iIntros (?) "Hφ". rewrite /auth_own /auth_ctx.
-    iMod (own_alloc_strong (Auth (Excl' (f t)) (f t)) G) as (γ) "[% Hγ]"; first done.
+    iIntros (??) "Hφ". rewrite /auth_own /auth_ctx.
+    iMod (own_alloc_strong (Auth (Excl' (f t)) (f t)) I) as (γ) "[% Hγ]"; [done|done|].
     iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']".
     iMod (inv_alloc N _ (auth_inv γ f φ) with "[-Hγ']") as "#?".
     { iNext. rewrite /auth_inv. iExists t. by iFrame. }
     eauto.
   Qed.
 
+  Lemma auth_alloc_cofinite N E t (G : gset gname) :
+    ✓ (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'.
+    exists (fresh (G ∪ E')). apply not_elem_of_union, is_fresh.
+  Qed.
+
   Lemma auth_alloc N E t :
     ✓ (f t) → ▷ φ t ={E}=∗ ∃ γ, auth_ctx γ N f φ ∧ auth_own γ (f t).
   Proof.
     iIntros (?) "Hφ".
-    iMod (auth_alloc_strong N E t ∅ with "Hφ") as (γ) "[_ ?]"; eauto.
+    iMod (auth_alloc_cofinite N E t ∅ with "Hφ") as (γ) "[_ ?]"; eauto.
   Qed.
 
   Lemma auth_empty γ : (|==> auth_own γ ε)%I.

theories/base_logic/lib/boxes.v

@@ -108,7 +108,7 @@ Lemma slice_insert_empty E q f Q P :
     slice N γ Q ∗ ▷?q box N (<[γ:=false]> f) (Q ∗ P).
 Proof.
   iDestruct 1 as (Φ) "[#HeqP Hf]".
-  iMod (own_alloc_strong (● Excl' false ⋅ ◯ Excl' false,
+  iMod (own_alloc_cofinite (● Excl' false ⋅ ◯ Excl' false,
     Some (to_agree (Next (iProp_unfold Q)))) (dom _ f))
     as (γ) "[Hdom Hγ]"; first done.
   rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]".

theories/base_logic/lib/cancelable_invariants.v

@@ -62,15 +62,23 @@ Section proofs.
     - iIntros "?". iApply "HP'". iApply "HP''". done.
   Qed.
 
-  Lemma cinv_alloc_strong (G : gset gname) E N :
-    (|={E}=> ∃ γ, ⌜ γ ∉ G ⌝ ∧ cinv_own γ 1 ∗ ∀ P, ▷ P ={E}=∗ cinv N γ P)%I.
+  Lemma cinv_alloc_strong (I : gname → Prop) E N :
+    pred_infinite I →
+    (|={E}=> ∃ γ, ⌜ I γ ⌝ ∧ cinv_own γ 1 ∗ ∀ P, ▷ P ={E}=∗ cinv N γ P)%I.
   Proof.
-    iMod (own_alloc_strong 1%Qp G) as (γ) "[Hfresh Hγ]"; first done.
+    iIntros (?). iMod (own_alloc_strong 1%Qp I) as (γ) "[Hfresh Hγ]"; [done|done|].
     iExists γ; iIntros "!> {$Hγ $Hfresh}" (P) "HP".
     iMod (inv_alloc N _ (P ∨ own γ 1%Qp)%I with "[HP]"); first by eauto.
     iIntros "!>". iExists P. iSplit; last done. iIntros "!# !>"; iSplit; auto.
   Qed.
 
+  Lemma cinv_alloc_cofinite (G : gset gname) E N :
+    (|={E}=> ∃ γ, ⌜ γ ∉ G ⌝ ∧ cinv_own γ 1 ∗ ∀ P, ▷ P ={E}=∗ cinv N γ P)%I.
+  Proof.
+    apply cinv_alloc_strong. apply (pred_infinite_set (C:=gset gname))=> E'.
+    exists (fresh (G ∪ E')). apply not_elem_of_union, is_fresh.
+  Qed.
+
   Lemma cinv_open_strong E N γ p P :
     ↑N ⊆ E →
     cinv N γ P -∗ cinv_own γ p ={E,E∖↑N}=∗
@@ -88,7 +96,7 @@ Section proofs.
 
   Lemma cinv_alloc E N P : ▷ P ={E}=∗ ∃ γ, cinv N γ P ∗ cinv_own γ 1.
   Proof.
-    iIntros "HP". iMod (cinv_alloc_strong ∅ E N) as (γ _) "[Hγ Halloc]".
+    iIntros "HP". iMod (cinv_alloc_cofinite ∅ E N) as (γ _) "[Hγ Halloc]".
     iExists γ. iFrame "Hγ". by iApply "Halloc".
   Qed.
 

theories/base_logic/lib/own.v

@@ -143,11 +143,12 @@ Qed.
 (** ** Allocation *)
 (* TODO: This also holds if we just have ✓ a at the current step-idx, as Iris
    assertion. However, the map_updateP_alloc does not suffice to show this. *)
-Lemma own_alloc_strong a (G : gset gname) :
-  ✓ a → (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ own γ a)%I.
+Lemma own_alloc_strong a (P : gname → Prop) :
+  pred_infinite P →
+  ✓ a → (|==> ∃ γ, ⌜P γ⌝ ∧ own γ a)%I.
 Proof.
-  intros Ha.
-  rewrite -(bupd_mono (∃ m, ⌜∃ γ, γ ∉ G ∧ m = iRes_singleton γ a⌝ ∧ uPred_ownM m)%I).
+  intros HP Ha.
+  rewrite -(bupd_mono (∃ m, ⌜∃ γ, P γ ∧ m = iRes_singleton γ a⌝ ∧ uPred_ownM m)%I).
   - rewrite /uPred_valid /bi_emp_valid (ownM_unit emp).
     eapply bupd_ownM_updateP, (ofe_fun_singleton_updateP_empty (inG_id _));
       first (eapply alloc_updateP_strong', cmra_transport_valid, Ha);
@@ -155,9 +156,18 @@ Proof.
   - apply exist_elim=>m; apply pure_elim_l=>-[γ [Hfresh ->]].
     by rewrite !own_eq /own_def -(exist_intro γ) pure_True // left_id.
 Qed.
+Lemma own_alloc_cofinite a (G : gset gname) :
+  ✓ a → (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ own γ a)%I.
+Proof.
+  intros Ha.
+  apply (own_alloc_strong a (λ γ, γ ∉ G))=> //.
+  apply (pred_infinite_set (C:=gset gname)).
+  intros E. set (i := fresh (G ∪ E)).
+  exists i. apply not_elem_of_union, is_fresh.
+Qed.
 Lemma own_alloc a : ✓ a → (|==> ∃ γ, own γ a)%I.
 Proof.
-  intros Ha. rewrite /uPred_valid /bi_emp_valid (own_alloc_strong a ∅) //; [].
+  intros Ha. rewrite /uPred_valid /bi_emp_valid (own_alloc_cofinite a ∅) //; [].
   apply bupd_mono, exist_mono=>?. eauto using and_elim_r.
 Qed.
 

theories/base_logic/lib/saved_prop.v

@@ -37,9 +37,14 @@ Section saved_anything.
   Global Instance saved_anything_proper γ : Proper ((≡) ==> (≡)) (saved_anything_own γ).
   Proof. solve_proper. Qed.
 
-  Lemma saved_anything_alloc_strong x (G : gset gname) :
+  Lemma saved_anything_alloc_strong x (I : gname → Prop) :
+    pred_infinite I →
+    (|==> ∃ γ, ⌜I γ⌝ ∧ saved_anything_own γ x)%I.
+  Proof. intros ?. by apply own_alloc_strong. Qed.
+
+  Lemma saved_anything_alloc_cofinite x (G : gset gname) :
     (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ saved_anything_own γ x)%I.
-  Proof. by apply own_alloc_strong. Qed.
+  Proof. by apply own_alloc_cofinite. Qed.
 
   Lemma saved_anything_alloc x : (|==> ∃ γ, saved_anything_own γ x)%I.
   Proof. by apply own_alloc. Qed.
@@ -72,9 +77,14 @@ Instance saved_prop_own_contractive `{!savedPropG Σ} γ :
   Contractive (saved_prop_own γ).
 Proof. solve_contractive. Qed.
 
-Lemma saved_prop_alloc_strong `{!savedPropG Σ} (G : gset gname) (P: iProp Σ) :
+Lemma saved_prop_alloc_strong `{!savedPropG Σ} (I : gname → Prop) (P: iProp Σ) :
+  pred_infinite I →
+  (|==> ∃ γ, ⌜I γ⌝ ∧ saved_prop_own γ P)%I.
+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)%I.
-Proof. iApply saved_anything_alloc_strong. Qed.
+Proof. iApply saved_anything_alloc_cofinite. Qed.
 
 Lemma saved_prop_alloc `{!savedPropG Σ} (P: iProp Σ) :
   (|==> ∃ γ, saved_prop_own γ P)%I.
@@ -99,9 +109,14 @@ Proof.
   solve_proper_core ltac:(fun _ => first [ intros ?; progress simpl | by auto | f_contractive | f_equiv ]).
 Qed.
 
-Lemma saved_pred_alloc_strong `{!savedPredG Σ A} (G : gset gname) (Φ : A → iProp Σ) :
+Lemma saved_pred_alloc_strong `{!savedPredG Σ A} (I : gname → Prop) (Φ : A → iProp Σ) :
+  pred_infinite I →
+  (|==> ∃ γ, ⌜I γ⌝ ∧ saved_pred_own γ Φ)%I.
+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 γ Φ)%I.
-Proof. iApply saved_anything_alloc_strong. Qed.
+Proof. iApply saved_anything_alloc_cofinite. Qed.
 
 Lemma saved_pred_alloc `{!savedPredG Σ A} (Φ : A → iProp Σ) :
   (|==> ∃ γ, saved_pred_own γ Φ)%I.