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

token: support iCombine ... gives

parent 9e782b4f
No related branches found
No related tags found
No related merge requests found
......@@ -49,6 +49,12 @@ Section lemmas.
unseal. iIntros "Htok1 Htok2".
iCombine "Htok1 Htok2" gives %[].
Qed.
Global Instance token_combine_gives γ :
CombineSepGives (token γ) (token γ) False⌝.
Proof.
rewrite /CombineSepGives. iIntros "[H1 H2]".
iDestruct (token_exclusive with "H1 H2") as %[].
Qed.
End lemmas.
......@@ -34,7 +34,7 @@ Section proof.
Local Definition locked (γ : gname) : iProp Σ := token γ.
Local Lemma locked_exclusive (γ : gname) : locked γ -∗ locked γ -∗ False.
Proof. iIntros "H1 H2". by iDestruct (token_exclusive with "H1 H2") as %?. Qed.
Proof. iIntros "H1 H2". by iCombine "H1 H2" gives %?. Qed.
(** The main proofs. *)
Local Lemma is_lock_iff γ lk R1 R2 :
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment