show na_own_acc

adfa0752 · Ralf Jung · e2b84307 · adfa0752
Commit adfa0752 authored Dec 20, 2016 by Ralf Jung
Hide whitespace changes
Inline Side-by-side

Showing with 7 additions and 0 deletions

theories/base_logic/lib/na_invariants.v theories/base_logic/lib/na_invariants.v +7 -0

No files found.
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -53,6 +53,13 @@ Section proofs.
    intros ?. by rewrite /na_own -own_op pair_op left_id coPset_disj_union.
  Qed.

+  Lemma na_own_acc E2 E1 tid :
+    E2 ⊆ E1 → na_own tid E1 -∗ na_own tid E2 ∗ (na_own tid E2 -∗ na_own tid E1).
+  Proof.
+    intros HF. assert (E1 = E2 ∪ (E1 ∖ E2)) as -> by exact: union_difference_L.
+    rewrite na_own_union; last by set_solver+. iIntros "[$ $]". auto.
+  Qed.
+
  Lemma na_inv_alloc p E N P : ▷ P ={E}=∗ na_inv p N P.
  Proof.
    iIntros "HP".