Merge branch 'ralf/own-alloc-dep' into 'master'

add dependent allocation lemma to own

See merge request iris/iris!354

theories/algebra/gmap.v

@@ -353,9 +353,10 @@ Qed.
 Section freshness.
   Local Set Default Proof Using "Type*".
   Context `{!Infinite K}.
-  Lemma alloc_updateP_strong (Q : gmap K A → Prop) (I : K → Prop) m x :
+  Lemma alloc_updateP_strong_dep (Q : gmap K A → Prop) (I : K → Prop) m (f : K → A) :
     pred_infinite I →
-    ✓ x → (∀ i, m !! i = None → I i → Q (<[i:=x]>m)) → m ~~>: Q.
+    (∀ i, m !! i = None → I i → ✓ (f i)) →
+    (∀ i, m !! i = None → I i → Q (<[i:=f i]>m)) → m ~~>: Q.
   Proof.
     move=> /(pred_infinite_set I (C:=gset K)) HP ? HQ.
     apply cmra_total_updateP. intros n mf Hm.
@@ -363,12 +364,18 @@ Section freshness.
     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.
+    exists (<[i:=f i]>m); split.
     - 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|].
+    apply insert_validN; [apply cmra_valid_validN|]; auto.
+  Qed.
+  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.
+    move=> HP ? HQ. eapply alloc_updateP_strong_dep with (f := λ _, x); eauto.
   Qed.
   Lemma alloc_updateP (Q : gmap K A → Prop) m x :
     ✓ x → (∀ i, m !! i = None → Q (<[i:=x]>m)) → m ~~>: Q.
@@ -377,13 +384,6 @@ Section freshness.
     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.
@@ -392,6 +392,20 @@ Section freshness.
     intros E. exists (fresh (J ∪ E)).
     apply not_elem_of_union, is_fresh.
   Qed.
+
+  (* Variants without the universally quantified Q, for use in case that is an evar. *)
+  Lemma alloc_updateP_strong_dep' m (f : K → A) (I : K → Prop) :
+    pred_infinite I →
+    (∀ i, m !! i = None → I i → ✓ (f i)) →
+    m ~~>: λ m', ∃ i, I i ∧ m' = <[i:=f i]>m ∧ m !! i = None.
+  Proof. eauto using alloc_updateP_strong_dep. 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' 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.

theories/base_logic/lib/own.v

@@ -146,34 +146,47 @@ 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 (P : gname → Prop) :
+Lemma own_alloc_strong_dep (f : gname → A) (P : gname → Prop) :
   pred_infinite P →
-  ✓ a → (|==> ∃ γ, ⌜P γ⌝ ∧ own γ a)%I.
+  (∀ γ, P γ → ✓ (f γ)) →
+  (|==> ∃ γ, ⌜P γ⌝ ∧ own γ (f γ))%I.
 Proof.
   intros HP Ha.
-  rewrite -(bupd_mono (∃ m, ⌜∃ γ, P γ ∧ m = iRes_singleton γ a⌝ ∧ uPred_ownM m)%I).
+  rewrite -(bupd_mono (∃ m, ⌜∃ γ, P γ ∧ m = iRes_singleton γ (f γ)⌝ ∧ uPred_ownM m)%I).
   - rewrite /uPred_valid /bi_emp_valid (ownM_unit emp).
-    eapply bupd_ownM_updateP, (discrete_fun_singleton_updateP_empty (inG_id Hin));
-      first (eapply alloc_updateP_strong', cmra_transport_valid, Ha);
-      naive_solver.
+    eapply bupd_ownM_updateP, (discrete_fun_singleton_updateP_empty (inG_id Hin)).
+    + eapply alloc_updateP_strong_dep'; first done.
+      intros i _ ?. eapply cmra_transport_valid, Ha. done.
+    + naive_solver.
   - 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.
+Lemma own_alloc_cofinite_dep (f : gname → A) (G : gset gname) :
+  (∀ γ, γ ∉ G → ✓ (f γ)) → (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ own γ (f γ))%I.
 Proof.
   intros Ha.
-  apply (own_alloc_strong a (λ γ, γ ∉ G))=> //.
+  apply (own_alloc_strong_dep f (λ γ, γ ∉ 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.
+Lemma own_alloc_dep (f : gname → A) :
+  (∀ γ, ✓ (f γ)) → (|==> ∃ γ, own γ (f γ))%I.
 Proof.
-  intros Ha. rewrite /uPred_valid /bi_emp_valid (own_alloc_cofinite a ∅) //; [].
+  intros Ha. rewrite /uPred_valid /bi_emp_valid (own_alloc_cofinite_dep f ∅) //; [].
   apply bupd_mono, exist_mono=>?. eauto using and_elim_r.
 Qed.
 
+Lemma own_alloc_strong a (P : gname → Prop) :
+  pred_infinite P →
+  ✓ a → (|==> ∃ γ, ⌜P γ⌝ ∧ own γ a)%I.
+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)%I.
+Proof. intros Ha. eapply own_alloc_cofinite_dep with (f := λ _, a); eauto. Qed.
+Lemma own_alloc a : ✓ a → (|==> ∃ γ, own γ a)%I.
+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'.
 Proof.