diff --git a/algebra/gset.v b/algebra/gset.v index 12578fa50376eab67a59feb5e1b7d527ce9adc26..3ae61b0fd28e13e7f9400e3c1ae7443445112a99 100644 --- a/algebra/gset.v +++ b/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.