diff --git a/algebra/gmap.v b/algebra/gmap.v index c9858eba7755b01a9258b98ff8ea8f9bcb4eff6e..948d7f97ed0ee5f07d0cb23b5f0a418e7fa4d1d5 100644 --- a/algebra/gmap.v +++ b/algebra/gmap.v @@ -318,7 +318,7 @@ Section freshness. ✓ x → m ~~>: λ m', ∃ i, m' = <[i:=x]>m ∧ m !! i = None. Proof. eauto using alloc_updateP. Qed. - Lemma singleton_updateP_unit (P : A → Prop) (Q : gmap K A → Prop) u i : + Lemma alloc_unit_singleton_updateP (P : A → Prop) (Q : gmap K A → Prop) u i : ✓ u → LeftId (≡) u (⋅) → u ~~>: P → (∀ y, P y → Q {[ i := y ]}) → ∅ ~~>: Q. Proof. @@ -333,14 +333,15 @@ Section freshness. move:Hy; case: (gf !! i)=>[x|]; rewrite /= ?right_id //. - move:(Hg i'). by rewrite !lookup_op lookup_singleton_ne // !left_id. Qed. - Lemma singleton_updateP_unit' (P: A → Prop) u i : + Lemma alloc_unit_singleton_updateP' (P: A → Prop) u i : ✓ u → LeftId (≡) u (⋅) → u ~~>: P → ∅ ~~>: λ m, ∃ y, m = {[ i := y ]} ∧ P y. - Proof. eauto using singleton_updateP_unit. Qed. - Lemma singleton_update_unit u i (y : A) : + Proof. eauto using alloc_unit_singleton_updateP. Qed. + Lemma alloc_unit_singleton_update u i (y : A) : ✓ u → LeftId (≡) u (⋅) → u ~~> y → ∅ ~~> {[ i := y ]}. Proof. - rewrite !cmra_update_updateP; eauto using singleton_updateP_unit with subst. + rewrite !cmra_update_updateP; + eauto using alloc_unit_singleton_updateP with subst. Qed. End freshness. @@ -361,19 +362,21 @@ Lemma singleton_local_update i x y mf : x ~l~> y @ mf ≫= (!! i) → {[ i := x ]} ~l~> {[ i := y ]} @ mf. Proof. apply insert_local_update. Qed. -Lemma alloc_singleton_local_update i x mf : +Lemma alloc_singleton_local_update m i x mf : + (m ⋅? mf) !! i = None → ✓ x → m ~l~> <[i:=x]> m @ mf. +Proof. + rewrite lookup_opM op_None=> -[Hi Hif] ?. + rewrite insert_singleton_op // comm. apply alloc_local_update. + intros n Hm j. move: (Hm j). destruct (decide (i = j)); subst. + - intros _; rewrite !lookup_opM lookup_op !lookup_singleton Hif Hi. + by apply cmra_valid_validN. + - by rewrite !lookup_opM lookup_op !lookup_singleton_ne // right_id. +Qed. + +Lemma alloc_unit_singleton_local_update i x mf : mf ≫= (!! i) = None → ✓ x → ∅ ~l~> {[ i := x ]} @ mf. Proof. - intros Hi. split. - - intros n Hm j. move: (Hm j). destruct (decide (i = j)); subst. - + intros _; rewrite !lookup_opM !lookup_insert !Some_op_opM Hi /=. - by apply cmra_valid_validN. - + by rewrite !lookup_opM !lookup_insert_ne. - - intros n mf' Hm Hm' j. move: (Hm j) (Hm' j). - destruct (decide (i = j)); subst. - + intros _. rewrite !lookup_opM !lookup_insert !Hi !lookup_empty !left_id_L. - by intros <-. - + by rewrite !lookup_opM !lookup_insert_ne. + intros Hi; apply alloc_singleton_local_update. by rewrite lookup_opM Hi. Qed. Lemma delete_local_update m i x `{!Exclusive x} mf : diff --git a/algebra/updates.v b/algebra/updates.v index ab978f4e028cb33af7e21c7372007b30e7c16165..46dcfe7ab38a4786700c2e2e2aacdd697b672783 100644 --- a/algebra/updates.v +++ b/algebra/updates.v @@ -68,11 +68,11 @@ Proof. - intros n mz'. rewrite !cmra_opM_assoc. move=> Hv /(H1 _ (Some _) Hv) /=; auto. Qed. -Lemma alloc_local_update x y mz : ✓ (x ⋅ y ⋅? mz) → x ~l~> x ⋅ y @ mz. +Lemma alloc_local_update x y mz : + (∀ n, ✓{n} (x ⋅? mz) → ✓{n} (x ⋅ y ⋅? mz)) → x ~l~> x ⋅ y @ mz. Proof. - split. - - intros n _. by apply cmra_valid_validN. - - intros n mz' _. by rewrite !(comm _ x) !cmra_opM_assoc=> ->. + split; first done. + intros n mz' _. by rewrite !(comm _ x) !cmra_opM_assoc=> ->. Qed. (** ** Frame preserving updates *) diff --git a/heap_lang/heap.v b/heap_lang/heap.v index 2d57cc20278bb45046036d9f727d9b830fef4d3b..9ee470dfd8a98481ef5ab86388e3c3309ae7c217 100644 --- a/heap_lang/heap.v +++ b/heap_lang/heap.v @@ -154,7 +154,7 @@ Section heap. iIntros {l} "[% Hheap]". iExists {[ l := (1%Qp, DecAgree v) ]}. rewrite -of_heap_insert -(insert_singleton_op h); last by apply of_heap_None. iFrame "Hheap". iSplit; first iPureIntro. - { by apply alloc_singleton_local_update; first apply of_heap_None. } + { by apply alloc_unit_singleton_local_update; first apply of_heap_None. } iIntros "Hheap". iApply "HΦ". by rewrite /heap_mapsto. Qed. diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v index 5a64e3af7575ae642feaf306dc38f7cbb94c7b06..4b99d543590f448cd3ec8dbb7e10340cd2cb4b69 100644 --- a/program_logic/ghost_ownership.v +++ b/program_logic/ghost_ownership.v @@ -86,7 +86,7 @@ Implicit Types a : A. Lemma own_empty γ E : True ={E}=> own γ ∅. Proof. rewrite ownG_empty /own. apply pvs_ownG_update, iprod_singleton_update_empty. - apply (singleton_update_unit (cmra_transport inG_prf ∅)); last done. + apply (alloc_unit_singleton_update (cmra_transport inG_prf ∅)); last done. - apply cmra_transport_valid, ucmra_unit_valid. - intros x; destruct inG_prf. by rewrite left_id. Qed.