Commit dcfb5aee authored by Robbert Krebbers's avatar Robbert Krebbers

Curry tl_own_disjoint.

parent 5ee92991
...@@ -39,8 +39,9 @@ Section proofs. ...@@ -39,8 +39,9 @@ Section proofs.
Lemma tl_alloc : (|==> tid, tl_own tid )%I. Lemma tl_alloc : (|==> tid, tl_own tid )%I.
Proof. by apply own_alloc. Qed. Proof. by apply own_alloc. Qed.
Lemma tl_own_disjoint tid E1 E2 : tl_own tid E1 tl_own tid E2 E1 E2. Lemma tl_own_disjoint tid E1 E2 : tl_own tid E1 - tl_own tid E2 - E1 E2.
Proof. Proof.
apply wand_intro_r.
rewrite /tl_own -own_op own_valid -coPset_disj_valid_op. by iIntros ([? _]). rewrite /tl_own -own_op own_valid -coPset_disj_valid_op. by iIntros ([? _]).
Qed. Qed.
...@@ -85,7 +86,6 @@ Section proofs. ...@@ -85,7 +86,6 @@ Section proofs.
+ iDestruct (own_valid_2 with "Hdis Hdis2") as %[_ Hval%gset_disj_valid_op]. + iDestruct (own_valid_2 with "Hdis Hdis2") as %[_ Hval%gset_disj_valid_op].
set_solver. set_solver.
+ iFrame. iApply "Hclose". iNext. iLeft. by iFrame. + iFrame. iApply "Hclose". iNext. iLeft. by iFrame.
- iDestruct (tl_own_disjoint tid {[i]} {[i]} with "[-]") as %?; first by iFrame. - iDestruct (tl_own_disjoint with "Htoki Htoki2") as %?. set_solver.
set_solver.
Qed. Qed.
End proofs. End proofs.
Markdown is supported
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