From 4e8a8de6d86b6a5668a6c056d3fda5c36c98d0d1 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Sun, 14 Feb 2016 21:57:43 +0100 Subject: [PATCH] Misc fin_map CMRA properties. --- algebra/fin_maps.v | 39 ++++++++++++++++++++------------------- 1 file changed, 20 insertions(+), 19 deletions(-) diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v index 4e5eea65..c9971cc9 100644 --- a/algebra/fin_maps.v +++ b/algebra/fin_maps.v @@ -106,6 +106,8 @@ Proof. by apply lookup_merge. Qed. Lemma lookup_unit m i : unit m !! i = unit (m !! i). Proof. by apply lookup_fmap. Qed. +Lemma map_valid_spec m : ✓ m ↔ ∀ i, ✓ (m !! i). +Proof. split; intros Hm ??; apply Hm. Qed. Lemma map_included_spec (m1 m2 : gmap K A) : m1 ≼ m2 ↔ ∀ i, m1 !! i ≼ m2 !! i. Proof. split. @@ -188,36 +190,32 @@ Implicit Types a : A. Lemma map_lookup_validN n m i x : ✓{n} m → m !! i ≡{n}≡ Some x → ✓{n} x. Proof. by move=> /(_ i) Hm Hi; move:Hm; rewrite Hi. Qed. +Lemma map_lookup_valid m i x : ✓ m → m !! i ≡ Some x → ✓ x. +Proof. move=>Hm Hi n. move:(Hm n i). by rewrite Hi. Qed. Lemma map_insert_validN n m i x : ✓{n} x → ✓{n} m → ✓{n} <[i:=x]>m. Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_equality. Qed. +Lemma map_insert_valid m i x : ✓ x → ✓ m → ✓ <[i:=x]>m. +Proof. intros ?? n j; apply map_insert_validN; auto. Qed. Lemma map_singleton_validN n i x : ✓{n} ({[ i ↦ x ]} : gmap K A) ↔ ✓{n} x. Proof. split; [|by intros; apply map_insert_validN, cmra_empty_valid]. by move=>/(_ i); simplify_map_equality. Qed. - -Lemma map_lookup_valid m i x : ✓ m → m !! i ≡ Some x → ✓ x. -Proof. move=>Hm Hi n. move:(Hm n i). by rewrite Hi. Qed. -Lemma map_insert_valid m i x : ✓ x → ✓ m → ✓ <[i:=x]>m. -Proof. intros ?? n j; apply map_insert_validN; auto. Qed. Lemma map_singleton_valid i x : ✓ ({[ i ↦ x ]} : gmap K A) ↔ ✓ x. Proof. split; intros ? n; eapply map_singleton_validN; eauto. Qed. -Lemma map_insert_op_None m1 m2 i x : - m2 !! i = None → <[i:=x]>(m1 ⋅ m2) = <[i:=x]>m1 ⋅ m2. -Proof. by intros Hi; apply (insert_merge_l _ m1 m2); rewrite Hi. Qed. -Lemma map_insert_op_unit m1 m2 i x : - m2 !! i ≡ Some (unit x) → <[i:=x]>(m1 ⋅ m2) ≡ <[i:=x]>m1 ⋅ m2. +Lemma map_insert_singleton_opN n m i x : + m !! i = None ∨ m !! i ≡{n}≡ Some (unit x) → <[i:=x]> m ≡{n}≡ {[ i ↦ x ]} ⋅ m. Proof. - intros Hu j; destruct (decide (i = j)) as [->|]. - * by rewrite lookup_insert lookup_op lookup_insert Hu cmra_unit_r. - * by rewrite lookup_insert_ne // !lookup_op lookup_insert_ne. + intros Hi j; destruct (decide (i = j)) as [->|]; + [|by rewrite lookup_op lookup_insert_ne // lookup_singleton_ne // left_id]. + rewrite lookup_op lookup_insert lookup_singleton. + by destruct Hi as [->| ->]; constructor; rewrite ?cmra_unit_r. Qed. -Lemma map_insert_op m1 m2 i x : - m2 !! i = None ∨ m2 !! i ≡ Some (unit x) → - <[i:=x]>(m1 ⋅ m2) ≡ <[i:=x]>m1 ⋅ m2. +Lemma map_insert_singleton_op m i x : + m !! i = None ∨ m !! i ≡ Some (unit x) → <[i:=x]> m ≡ {[ i ↦ x ]} ⋅ m. Proof. - by intros [?|?]; [rewrite map_insert_op_None|rewrite map_insert_op_unit]. + rewrite !equiv_dist; naive_solver eauto using map_insert_singleton_opN. Qed. Lemma map_unit_singleton (i : K) (x : A) : @@ -301,8 +299,11 @@ Proof. intros ? HQ mf n Hm. set (i := fresh (I ∪ dom (gset K) (m ⋅ mf))). assert (i ∉ I ∧ i ∉ dom (gset K) m ∧ i ∉ dom (gset K) mf) as [?[??]]. { rewrite -not_elem_of_union -map_dom_op -not_elem_of_union; apply is_fresh. } - exists (<[i:=x]>m). split; first by (apply HQ; last done; apply not_elem_of_dom). - rewrite -map_insert_op_None; last by apply not_elem_of_dom. + exists (<[i:=x]>m); split. + { by apply HQ; last done; apply not_elem_of_dom. } + rewrite map_insert_singleton_opN; last by left; apply not_elem_of_dom. + rewrite -assoc -map_insert_singleton_opN; + last by left; apply not_elem_of_dom; rewrite map_dom_op not_elem_of_union. by apply map_insert_validN; [apply cmra_valid_validN|]. Qed. Lemma map_updateP_alloc (Q : gmap K A → Prop) m x : -- GitLab