Commit 7dc83979 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix instance for ndisjoint.

parent 93faeb10
Pipeline #1951 passed with stage
......@@ -34,7 +34,7 @@ Section ndisjoint.
Context `{Countable A}.
Implicit Types x y : A.
Global Instance ndisjoint_comm : Comm iff ndisjoint.
Global Instance ndisjoint_symmetric : Symmetric ndisjoint.
Proof. intros N1 N2. rewrite /disjoint /ndisjoint; naive_solver. Qed.
Lemma ndot_ne_disjoint N x y : x y N .@ x N .@ y.
......@@ -47,7 +47,7 @@ Section ndisjoint.
Qed.
Lemma ndot_preserve_disjoint_r N1 N2 x : N1 N2 N1 N2 .@ x .
Proof. rewrite ![N1 _]comm. apply ndot_preserve_disjoint_l. Qed.
Proof. intros. by apply symmetry, ndot_preserve_disjoint_l. Qed.
Lemma ndisj_disjoint N1 N2 : N1 N2 nclose N1 nclose N2.
Proof.
......
......@@ -77,8 +77,9 @@ Proof.
wp_apply (newbarrier_spec heapN N (barrier_res γ Φ)); auto.
iFrame "Hh". iIntros {l} "[Hr Hs]".
set (workers_post (v : val) := (barrier_res γ Ψ1 barrier_res γ Ψ2)%I).
wp_let. wp_apply (wp_par _ _ (λ _, True)%I workers_post); first done.
iFrame "Hh". iSplitL "HP Hs Hγ"; [|iSplitL "Hr"].
wp_let. wp_apply (wp_par _ _ (λ _, True)%I workers_post);
try iFrame "Hh"; first done.
iSplitL "HP Hs Hγ"; [|iSplitL "Hr"].
- wp_focus eM. iApply wp_wand_l; iSplitR "HP"; [|by iApply "He"].
iIntros {v} "HP"; iDestruct "HP" as {x} "HP". wp_let.
iPvs (own_update _ _ (Cinr (to_agree _)) with "Hγ") as "Hx".
......@@ -88,8 +89,8 @@ Proof.
- iDestruct (recv_weaken with "[] Hr") as "Hr"; first by iApply P_res_split.
iPvs (recv_split with "Hr") as "[H1 H2]"; first done.
wp_apply (wp_par _ _ (λ _, barrier_res γ Ψ1)%I
(λ _, barrier_res γ Ψ2)%I); first done.
iSplit; [done|]; iSplitL "H1"; [|iSplitL "H2"].
(λ _, barrier_res γ Ψ2)%I); try iFrame "Hh"; first done.
iSplitL "H1"; [|iSplitL "H2"].
+ iApply worker_spec; auto.
+ iApply worker_spec; auto.
+ auto.
......
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