Reorganize algebra/gset a bit.

algebra/gset.v

@@ -55,8 +55,6 @@ Section gset.
     discreteUR (gset_disj K) gset_disj_ra_mixin gset_disj_ucmra_mixin.
 
   Arguments op _ _ _ _ : simpl never.
-  Section fpu.
-  Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
 
   Lemma gset_alloc_updateP_strong P (Q : gset_disj K → Prop) X :
     (∀ Y, X ⊆ Y → ∃ j, j ∉ Y ∧ P j) →
@@ -69,18 +67,10 @@ Section gset.
     - 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 (λ _, 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 P (Q : gset_disj K → Prop) :
     (∀ Y : gset K, ∃ j, j ∉ Y ∧ P j) →
@@ -89,17 +79,29 @@ Section gset.
     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. 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.
 
-  End fpu.
+  Section fresh_updates.
+    Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
+
+    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 (λ _, True); eauto.
+      intros Y ?; exists (fresh Y); eauto using is_fresh.
+    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 (Q : gset_disj K → Prop) :
+      (∀ i, Q (GSet {[i]})) → GSet ∅ ~~>: Q.
+    Proof. intro. apply gset_alloc_updateP. intros i; rewrite right_id_L; auto. Qed.
+    Lemma gset_alloc_empty_updateP' : GSet ∅ ~~>: λ Y, ∃ i, Y = GSet {[ i ]}.
+    Proof. eauto using gset_alloc_empty_updateP. Qed.
+  End fresh_updates.
 
   Lemma gset_alloc_local_update X i Xf :
     i ∉ X → i ∉ Xf → GSet X ~l~> GSet ({[i]} ∪ X) @ Some (GSet Xf).