diff --git a/algebra/gset.v b/algebra/gset.v index c60bd02cd2eb8cd673f0a4ef89341ecfc098ddd9..12578fa50376eab67a59feb5e1b7d527ce9adc26 100644 --- a/algebra/gset.v +++ b/algebra/gset.v @@ -68,13 +68,27 @@ Section gset. Qed. Lemma gset_alloc_updateP (Q : gset_disj K → Prop) X : (∀ i, i ∉ X → Q (GSet ({[i]} ∪ X))) → GSet X ~~>: Q. - Proof. move=>??. eapply gset_alloc_updateP_strong with (I:=∅); by eauto. Qed. + 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. 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. + Proof. + intros. apply (gset_alloc_updateP_strong _ I)=> 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. 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. + Lemma gset_alloc_local_update X i Xf : i ∉ X → i ∉ Xf → GSet X ~l~> GSet ({[i]} ∪ X) @ Some (GSet Xf). Proof. @@ -83,6 +97,12 @@ Section gset. - intros mZ ?%gset_disj_valid_op HXf. rewrite -gset_disj_union -?assoc ?HXf ?cmra_opM_assoc; set_solver. Qed. + Lemma gset_alloc_empty_local_update i Xf : + i ∉ Xf → GSet ∅ ~l~> GSet {[i]} @ Some (GSet Xf). + Proof. + intros. rewrite -(right_id_L _ _ {[i]}). + apply gset_alloc_local_update; set_solver. + Qed. End gset. Arguments gset_disjR _ {_ _}.