Skip to content
Snippets Groups Projects
Commit ad13438b authored by Ralf Jung's avatar Ralf Jung
Browse files

change gen_inv_heap notation to get out of the way of persistent points-to

parent 989f0ffd
No related branches found
No related tags found
No related merge requests found
...@@ -67,12 +67,12 @@ Section definitions. ...@@ -67,12 +67,12 @@ Section definitions.
End definitions. End definitions.
Local Notation "l '↦□' I" := (inv_mapsto l I%stdpp%type)
(at level 20, format "l '↦□' I") : bi_scope.
Local Notation "l '↦_' I v" := (inv_mapsto_own l v I%stdpp%type) Local Notation "l '↦_' I v" := (inv_mapsto_own l v I%stdpp%type)
(at level 20, I at level 9, format "l '↦_' I v") : bi_scope. (at level 20, I at level 9, format "l '↦_' I v") : bi_scope.
Local Notation "l '↦_' I □" := (inv_mapsto l I%stdpp%type)
(at level 20, I at level 9, format "l '↦_' I '□'") : bi_scope.
(* [inv_heap_inv] has no parameters to infer the types from, so we need to (* [inv_heap_inv] has no parameters to infer the types from, so we need to
make them explicit. *) make them explicit. *)
Arguments inv_heap_inv _ _ {_ _ _ _ _ _}. Arguments inv_heap_inv _ _ {_ _ _ _ _ _}.
...@@ -133,7 +133,7 @@ Section inv_heap. ...@@ -133,7 +133,7 @@ Section inv_heap.
(** * Helpers *) (** * Helpers *)
Lemma inv_mapsto_lookup_Some l h I : Lemma inv_mapsto_lookup_Some l h I :
l I -∗ own (inv_heap_name gG) ( to_inv_heap h) -∗ l _I -∗ own (inv_heap_name gG) ( to_inv_heap h) -∗
⌜∃ v I', h !! l = Some (v, I') w, I w I' w ⌝. ⌜∃ v I', h !! l = Some (v, I') w, I w I' w ⌝.
Proof. Proof.
iIntros "Hl_inv H◯". iIntros "Hl_inv H◯".
...@@ -179,10 +179,10 @@ Section inv_heap. ...@@ -179,10 +179,10 @@ Section inv_heap.
Global Instance inv_heap_inv_persistent : Persistent (inv_heap_inv L V). Global Instance inv_heap_inv_persistent : Persistent (inv_heap_inv L V).
Proof. apply _. Qed. Proof. apply _. Qed.
Global Instance inv_mapsto_persistent l I : Persistent (l I). Global Instance inv_mapsto_persistent l I : Persistent (l _I ).
Proof. apply _. Qed. Proof. apply _. Qed.
Global Instance inv_mapsto_timeless l I : Timeless (l I). Global Instance inv_mapsto_timeless l I : Timeless (l _I ).
Proof. apply _. Qed. Proof. apply _. Qed.
Global Instance inv_mapsto_own_timeless l v I : Timeless (l ↦_I v). Global Instance inv_mapsto_own_timeless l v I : Timeless (l ↦_I v).
...@@ -215,7 +215,7 @@ Section inv_heap. ...@@ -215,7 +215,7 @@ Section inv_heap.
+ iModIntro. by rewrite /inv_mapsto_own to_inv_heap_singleton. + iModIntro. by rewrite /inv_mapsto_own to_inv_heap_singleton.
Qed. Qed.
Lemma inv_mapsto_own_inv l v I : l ↦_I v -∗ l I. Lemma inv_mapsto_own_inv l v I : l ↦_I v -∗ l _I .
Proof. Proof.
apply own_mono, auth_frag_mono. rewrite singleton_included pair_included. apply own_mono, auth_frag_mono. rewrite singleton_included pair_included.
right. split; [apply: ucmra_unit_least|done]. right. split; [apply: ucmra_unit_least|done].
...@@ -266,7 +266,7 @@ Section inv_heap. ...@@ -266,7 +266,7 @@ Section inv_heap.
Lemma inv_mapsto_acc l I E : Lemma inv_mapsto_acc l I E :
inv_heapN E inv_heapN E
inv_heap_inv L V -∗ l I ={E, E inv_heapN}=∗ inv_heap_inv L V -∗ l _I ={E, E inv_heapN}=∗
v, I v l v (l v ={E inv_heapN, E}=∗ True). v, I v l v (l v ={E inv_heapN, E}=∗ True).
Proof. Proof.
iIntros (HN) "#Hinv Hl_inv". iIntros (HN) "#Hinv Hl_inv".
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment