diff --git a/algebra/gset.v b/algebra/gset.v index fd82c6d471223c399feb0f76da261b9d75e15551..f0c1c709950bfb3ca13ae23bb615e2cbb7fea158 100644 --- a/algebra/gset.v +++ b/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).