Stronger allocation updates for gset.

The new updates allow allocation fresh elements satisfying an arbitrary
proposition (for example, being even) instead of just not being in a given
finite set.

TODO: maybe also do this for finite maps (gmaps).

algebra/gset.v

@@ -57,34 +57,43 @@ Section gset.
   Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
   Arguments op _ _ _ _ : simpl never.
 
-  Lemma gset_alloc_updateP_strong (Q : gset_disj K → Prop) (I : gset K) X :
-    (∀ i, i ∉ X → i ∉ I → Q (GSet ({[i]} ∪ X))) → GSet X ~~>: Q.
+  Lemma gset_alloc_updateP_strong P (Q : gset_disj K → Prop) X :
+    (∀ Y, X ⊆ Y → ∃ j, j ∉ Y ∧ P j) →
+    (∀ i, i ∉ X → P i → Q (GSet ({[i]} ∪ X))) → GSet X ~~>: Q.
   Proof.
-    intros HQ; apply cmra_discrete_updateP=> ? /gset_disj_valid_inv_l [Y [->?]].
-    destruct (exist_fresh (X ∪ Y ∪ I)) as [i ?].
+    intros Hfresh HQ.
+    apply cmra_discrete_updateP=> ? /gset_disj_valid_inv_l [Y [->?]].
+    destruct (Hfresh (X ∪ Y)) as (i&?&?); first set_solver.
     exists (GSet ({[ i ]} ∪ X)); split.
     - apply HQ; set_solver by eauto.
     - apply gset_disj_valid_op. set_solver by eauto.
   Qed.
   Lemma gset_alloc_updateP (Q : gset_disj K → Prop) X :
     (∀ i, i ∉ X → Q (GSet ({[i]} ∪ X))) → GSet X ~~>: Q.
-  Proof. intro. eapply gset_alloc_updateP_strong with (I:=∅); eauto. Qed.
-  Lemma gset_alloc_updateP_strong' (I : gset K) X :
-    GSet X ~~>: λ Y, ∃ i, Y = GSet ({[ i ]} ∪ X) ∧ i ∉ I ∧ i ∉ X.
+  Proof.
+    intro; eapply gset_alloc_updateP_strong with (λ _, True); eauto.
+    intros Y ?; exists (fresh Y); eauto using is_fresh.
+  Qed.
+  Lemma gset_alloc_updateP_strong' P X :
+    (∀ Y, X ⊆ Y → ∃ j, j ∉ Y ∧ P j) →
+    GSet X ~~>: λ Y, ∃ i, Y = GSet ({[ i ]} ∪ X) ∧ i ∉ X ∧ P i.
   Proof. eauto using gset_alloc_updateP_strong. Qed.
   Lemma gset_alloc_updateP' X : GSet X ~~>: λ Y, ∃ i, Y = GSet ({[ i ]} ∪ X) ∧ i ∉ X.
   Proof. eauto using gset_alloc_updateP. Qed.
 
-  Lemma gset_alloc_empty_updateP_strong (Q : gset_disj K → Prop) (I : gset K) :
-    (∀ i, i ∉ I → Q (GSet {[i]})) → GSet ∅ ~~>: Q.
+  Lemma gset_alloc_empty_updateP_strong P (Q : gset_disj K → Prop) :
+    (∀ Y : gset K, ∃ j, j ∉ Y ∧ P j) →
+    (∀ i, P i → Q (GSet {[i]})) → GSet ∅ ~~>: Q.
   Proof.
-    intros. apply (gset_alloc_updateP_strong _ I)=> i. rewrite right_id_L. auto.
+    intros. apply (gset_alloc_updateP_strong P); eauto.
+    intros i; rewrite right_id_L; auto.
   Qed.
   Lemma gset_alloc_empty_updateP (Q : gset_disj K → Prop) :
     (∀ i, Q (GSet {[i]})) → GSet ∅ ~~>: Q.
-  Proof. intro. eapply gset_alloc_empty_updateP_strong with (I:=∅); eauto. Qed.
-  Lemma gset_alloc_empty_updateP_strong' (I : gset K) :
-    GSet ∅ ~~>: λ Y, ∃ i, Y = GSet {[ i ]} ∧ i ∉ I.
+  Proof. intro. apply gset_alloc_updateP. intros i; rewrite right_id_L; auto. Qed.
+  Lemma gset_alloc_empty_updateP_strong' P :
+    (∀ Y : gset K, ∃ j, j ∉ Y ∧ P j) →
+    GSet ∅ ~~>: λ Y, ∃ i, Y = GSet {[ i ]} ∧ P i.
   Proof. eauto using gset_alloc_empty_updateP_strong. Qed.
   Lemma gset_alloc_empty_updateP' : GSet ∅ ~~>: λ Y, ∃ i, Y = GSet {[ i ]}.
   Proof. eauto using gset_alloc_empty_updateP. Qed.