Skip to content
Snippets Groups Projects
Commit 98be0049 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bump Iris version and make use of improved solve_ndisj.

parent 3e2ae1fc
No related branches found
No related tags found
No related merge requests found
coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 7b36d0e4c312b99b081f05b6575071b56bf12a55
coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 857f9909b773754d521d47f0fe6f43aec6c3214d
......@@ -77,12 +77,10 @@ Section own.
with "[Hpbown]") as "#Hinv"; first by eauto.
iIntros "!> !# * % Htok". iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
iDestruct "INV" as "[>Hbtok|#Hshr]".
- iMod (bor_later with "LFT [Hbtok]") as "Hb".
{ apply ndisj_subseteq_difference. solve_ndisj. set_solver. } (* FIXME: some tactic should solve this in one go. *)
- iMod (bor_later with "LFT [Hbtok]") as "Hb"; first solve_ndisj.
{ rewrite bor_unfold_idx. eauto. }
iModIntro. iNext. iMod "Hb".
iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ $]".
{ apply ndisj_subseteq_difference. solve_ndisj. set_solver. } (* FIXME: some tactic should solve this in one go. *)
iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ $]"; first solve_ndisj.
iApply "Hclose". auto.
- iMod fupd_intro_mask' as "Hclose'"; last iModIntro. set_solver.
iNext. iMod "Hclose'" as "_". iMod ("Hclose" with "[]") as "_"; by eauto.
......
......@@ -7,7 +7,6 @@ Set Default Proof Using "Type".
Section uniq_bor.
Context `{typeG Σ}.
Local Hint Extern 1000 (_ _) => set_solver : ndisj.
Program Definition uniq_bor (κ:lft) (ty:type) :=
{| ty_size := 1;
......
......@@ -8,7 +8,6 @@ Set Default Proof Using "Type".
Section cell.
Context `{typeG Σ}.
Local Hint Extern 1000 (_ _) => set_solver : ndisj.
Program Definition cell (ty : type) :=
{| ty_size := ty.(ty_size);
......@@ -50,7 +49,7 @@ Section cell.
intros ty Hcopy. split; first by intros; simpl; apply _.
iIntros (κ tid E F l q ??) "#LFT #Hshr Htl Htok". iExists 1%Qp. simpl in *.
(* Size 0 needs a special case as we can't keep the thread-local invariant open. *)
destruct (ty_size ty) as [|sz] eqn:Hsz.
destruct (ty_size ty) as [|sz] eqn:Hsz; simpl in *.
{ iMod (na_bor_acc with "LFT Hshr Htok Htl") as "(Hown & Htl & Hclose)"; [solve_ndisj..|].
iDestruct "Hown" as (vl) "[H↦ #Hown]".
simpl. assert (F = F) as -> by set_solver+.
......
......@@ -8,7 +8,6 @@ Set Default Proof Using "Type".
Section refmut.
Context `{typeG Σ, refcellG Σ}.
Local Hint Extern 1000 (_ _) => set_solver : ndisj.
Program Definition refmut (α : lft) (ty : type) :=
{| ty_size := 2;
......
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