Commit 0bb3cf85 authored by Ralf Jung's avatar Ralf Jung
Browse files

fix name of some auth lemmas

parent d69ec6c4
......@@ -91,7 +91,7 @@ Section heap.
rewrite to_heap_insert big_sepM_insert //.
rewrite (map_insert_singleton_op (to_heap σ));
last rewrite lookup_fmap Hl; auto.
by rewrite auto_own_op IH.
by rewrite auth_own_op IH.
Context `{heapG Σ}.
......@@ -103,7 +103,7 @@ Section heap.
(** General properties of mapsto *)
Lemma heap_mapsto_disjoint l v1 v2 : (l v1 l v2)%I False.
rewrite heap_mapsto_eq -auto_own_op auto_own_valid map_op_singleton.
rewrite heap_mapsto_eq -auth_own_op auth_own_valid map_op_singleton.
rewrite map_validI (forall_elim l) lookup_singleton.
by rewrite option_validI excl_validI.
......@@ -40,10 +40,10 @@ Section auth.
Proof. by rewrite /auth_own=> a b ->. Qed.
Global Instance auth_own_proper γ : Proper (() ==> ()) (auth_own γ).
Proof. by rewrite /auth_own=> a b ->. Qed.
Lemma auto_own_op γ a b :
Lemma auth_own_op γ a b :
auth_own γ (a b) (auth_own γ a auth_own γ b)%I.
Proof. by rewrite /auth_own -own_op auth_frag_op. Qed.
Lemma auto_own_valid γ a : auth_own γ a a.
Lemma auth_own_valid γ a : auth_own γ a a.
Proof. by rewrite /auth_own own_valid auth_validI. Qed.
Lemma auth_alloc E N a :
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment