Commit fb1de8a8 by Ralf Jung

### na_inv: avoid tying the masks together, that makes it hard(er) to apply the lemma

parent 683b7066
 ... @@ -71,14 +71,14 @@ Section proofs. ... @@ -71,14 +71,14 @@ Section proofs. iNext. iLeft. by iFrame. iNext. iLeft. by iFrame. Qed. Qed. Lemma na_inv_open tid E N P : Lemma na_inv_open tid E F N P : ↑N ⊆ E → ↑N ⊆ E → ↑N ⊆ F → na_inv tid N P -∗ na_own tid E ={E}=∗ ▷ P ∗ na_own tid (E∖↑N) ∗ na_inv tid N P -∗ na_own tid F ={E}=∗ ▷ P ∗ na_own tid (F∖↑N) ∗ (▷ P ∗ na_own tid (E∖↑N) ={E}=∗ na_own tid E). (▷ P ∗ na_own tid (F∖↑N) ={E}=∗ na_own tid F). Proof. Proof. rewrite /na_inv. iIntros (?) "#Htlinv Htoks". rewrite /na_inv. iIntros (??) "#Htlinv Htoks". iDestruct "Htlinv" as (i) "[% Hinv]". iDestruct "Htlinv" as (i) "[% Hinv]". rewrite [E as X in na_own tid X](union_difference_L (↑N) E) //. rewrite [F as X in na_own tid X](union_difference_L (↑N) F) //. rewrite [X in (X ∪ _)](union_difference_L {[i]} (↑N)) ?na_own_union; [|set_solver..]. rewrite [X in (X ∪ _)](union_difference_L {[i]} (↑N)) ?na_own_union; [|set_solver..]. iDestruct "Htoks" as "[[Htoki \$] \$]". iDestruct "Htoks" as "[[Htoki \$] \$]". iInv N as "[[\$ >Hdis]|>Htoki2]" "Hclose". iInv N as "[[\$ >Hdis]|>Htoki2]" "Hclose". ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!