From 11148461c0ac749f8de4f8104a09293fea3f4ec6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 7 Jan 2020 18:00:03 +0100
Subject: [PATCH] strengthen alloc_updateP_strong_dep and own_alloc_strong_dep

---
 theories/algebra/gmap.v       | 6 +++---
 theories/base_logic/lib/own.v | 6 +++---
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index ecf7cc5dc..25bc95c5b 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -355,7 +355,7 @@ Section freshness.
   Context `{!Infinite K}.
   Lemma alloc_updateP_strong_dep (Q : gmap K A → Prop) (I : K → Prop) m (f : K → A) :
     pred_infinite I →
-    (∀ i, ✓ (f i)) →
+    (∀ 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.
@@ -369,7 +369,7 @@ Section freshness.
     - 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 →
@@ -396,7 +396,7 @@ Section freshness.
   (* 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, ✓ (f 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) :
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 7042a0b11..4c03d6ba6 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -148,7 +148,7 @@ Qed.
    assertion. However, the map_updateP_alloc does not suffice to show this. *)
 Lemma own_alloc_strong_dep (f : gname → A) (P : gname → Prop) :
   pred_infinite P →
-  (∀ γ, ✓ (f γ)) →
+  (∀ γ, P γ → ✓ (f γ)) →
   (|==> ∃ γ, ⌜P γ⌝ ∧ own γ (f γ))%I.
 Proof.
   intros HP Ha.
@@ -156,7 +156,7 @@ Proof.
   - rewrite /uPred_valid /bi_emp_valid (ownM_unit emp).
     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.
+      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.
@@ -168,7 +168,7 @@ Proof.
   intros HP Ha. eapply own_alloc_strong_dep with (f := λ _, a); eauto.
 Qed.
 Lemma own_alloc_cofinite_dep (f : gname → A) (G : gset gname) :
-  (∀ γ, ✓ (f γ)) → (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ own γ (f γ))%I.
+  (∀ γ, γ ∉ G → ✓ (f γ)) → (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ own γ (f γ))%I.
 Proof.
   intros Ha.
   apply (own_alloc_strong_dep f (λ γ, γ ∉ G))=> //.
-- 
GitLab