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

add gmap_view_auth_dfrac_validN 

It seems to just have been missed
parent 255341dd
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
iris/algebra/lib/gmap_view.v
+ 4
− 0
View file @ 4664687c
...@@ -198,6 +198,10 @@ Section lemmas. ...@@ -198,6 +198,10 @@ Section lemmas.
✓ (gmap_view_auth dp m1 ⋅ gmap_view_auth dq m2) → m1 = m2. ✓ (gmap_view_auth dp m1 ⋅ gmap_view_auth dq m2) → m1 = m2.
Proof. apply view_auth_dfrac_op_inv_L, _. Qed. Proof. apply view_auth_dfrac_op_inv_L, _. Qed.
Lemma gmap_view_auth_dfrac_validN m n dq : ✓{n} gmap_view_auth dq m ↔ ✓ dq.
Proof.
rewrite view_auth_dfrac_validN. intuition eauto using gmap_view_rel_unit.
Qed.
Lemma gmap_view_auth_dfrac_valid m dq : ✓ gmap_view_auth dq m ↔ ✓ dq. Lemma gmap_view_auth_dfrac_valid m dq : ✓ gmap_view_auth dq m ↔ ✓ dq.
Proof. Proof.
rewrite view_auth_dfrac_valid. intuition eauto using gmap_view_rel_unit. rewrite view_auth_dfrac_valid. intuition eauto using gmap_view_rel_unit.
......
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