From c72bfec9e38531b7dc70f05c2415ed1e3f806899 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Fri, 16 Dec 2016 15:17:49 +0100
Subject: [PATCH] on a newer Iris version, the solve_ndisj works somewhat
better
---
opam.pins | 2 +-
theories/typing/own.v | 7 +++----
theories/typing/shr_bor.v | 19 ++++++-------------
theories/typing/sum.v | 2 +-
theories/typing/uniq_bor.v | 14 ++++++++------
5 files changed, 19 insertions(+), 25 deletions(-)
diff --git a/opam.pins b/opam.pins
index 1664a075..722cf26d 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq b1fa82f0ef47d01f88b9032f265d3754adf5fa5b
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 2472f932c13e0e00b08eb1e00c2fcaaf78b260a8
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 150a35ad..6c8ec1a2 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -72,14 +72,13 @@ Section own.
iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ ty_shr ty κ tid l')%I
with "[Hpbown]") as "#Hinv"; first by eauto.
iIntros "!> !# * % Htok". iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
- (* FIXME We shouldn't have to add this manually to make the set_solver below work (instead, solve_ndisj below should do it). Also, this goal itself should be handled by solve_ndisj. *)
- assert (↑shrN ⊥ ↑lftN). { eapply ndot_preserve_disjoint_l. solve_ndisj. }
iDestruct "INV" as "[>Hbtok|#Hshr]".
- iMod (bor_later with "LFT [Hbtok]") as "Hb".
- { set_solver. }
+ { apply ndisj_subseteq_difference. solve_ndisj. set_solver. } (* FIXME: some tactic should solve this in one go. *)
{ rewrite bor_unfold_idx. eauto. }
iModIntro. iNext. iMod "Hb".
- iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ Htok]". set_solver.
+ iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ Htok]".
+ { apply ndisj_subseteq_difference. solve_ndisj. set_solver. } (* FIXME: some tactic should solve this in one go. *)
iFrame "Htok". iApply "Hclose". auto.
- iMod fupd_intro_mask' as "Hclose'"; last iModIntro. set_solver.
iNext. iMod "Hclose'" as "_". iMod ("Hclose" with "[]") as "_"; by eauto.
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index e951318d..ead69ede 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -80,9 +80,8 @@ Section typing.
iMod (lft_incl_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
rewrite (union_difference_L (↑lrustN) ⊤); last done.
setoid_rewrite ->na_own_union; try set_solver. iDestruct "Htl" as "[Htl ?]".
- (* FIXME We shouldn't have to add this manually to make the set_solver below work (instead, solve_ndisj below should do it). *)
- assert (↑shrN ⊆ (↑lrustN : coPset)). { solve_ndisj. }
- iMod (copy_shr_acc with "LFT Hshr [$Htok $Htl]") as (q'') "[H↦ Hclose']"; first set_solver.
+ iMod (copy_shr_acc with "LFT Hshr [$Htok $Htl]") as (q'') "[H↦ Hclose']".
+ { assert (↑shrN ⊆ (↑lrustN : coPset)) by solve_ndisj. set_solver. } (* FIXME: some tactic should solve this in one go. *)
{ rewrite ->shr_locsE_shrN. solve_ndisj. }
iDestruct "H↦" as (vl) "[>H↦ #Hown]".
iAssert (â–· ⌜length vl = ty_size tyâŒ)%I with "[#]" as ">%".
@@ -104,11 +103,8 @@ Section typing.
iDestruct "H↦" as (vl) "[H↦b #Hown]".
iMod (frac_bor_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
iMod (lft_incl_acc with "H⊑ Htok2") as (q2) "[Htok2 Hclose'']". solve_ndisj.
- iApply (wp_fupd_step _ (⊤∖↑lrustN∖↑lftN) with "[Hown Htok2]"); try done.
- - (* FIXME: mask reasoning at its worst. Really we'd want the mask in the line above to be
- ⊤∖↑shrN∖↑lftN, but then the wp_read fails. *)
- assert (↑shrN ⊆ (↑lrustN : coPset)). { solve_ndisj. }
- iApply step_fupd_mask_mono; last iApply ("Hown" with "* [%] Htok2"); [|reflexivity|]. set_solver. set_solver.
+ iApply (wp_fupd_step _ (_∖_) with "[Hown Htok2]"); try done.
+ - iApply ("Hown" with "* [%] Htok2"). set_solver+.
- wp_read. iIntros "!>[Hshr Htok2]{$H⊑}". iMod ("Hclose''" with "Htok2") as "$".
iSplitL "Hshr"; first by iExists _; auto. iApply ("Hclose" with ">").
iFrame. iApply "Hclose'". auto.
@@ -129,11 +125,8 @@ Section typing.
{ iApply (lft_incl_glb with "H⊑2 []"). iApply lft_incl_refl. }
iMod (lft_incl_acc with "[] Htok2") as (q2) "[Htok2 Hclose'']". solve_ndisj.
{ iApply (lft_incl_trans with "[]"); done. }
- iApply (wp_fupd_step _ (⊤∖↑lrustN∖↑lftN) with "[Hown Htok2]"); try done.
- - (* FIXME: mask reasoning at its worst. Really we'd want the mask in the line above to be
- ⊤∖↑shrN∖↑lftN, but then the wp_read fails. *)
- assert (↑shrN ⊆ (↑lrustN : coPset)). { solve_ndisj. }
- iApply step_fupd_mask_mono; last iApply ("Hown" with "* [%] Htok2"); [|reflexivity|]. set_solver. set_solver.
+ iApply (wp_fupd_step _ (_∖_) with "[Hown Htok2]"); try done.
+ - iApply ("Hown" with "* [%] Htok2"). set_solver+.
- wp_read. iIntros "!>[#Hshr Htok2]{$H⊑1}".
iMod ("Hclose''" with "Htok2") as "$". iSplitR.
* iExists _. iSplitR. done. by iApply (ty_shr_mono with "LFT H⊑3 Hshr").
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index b393efb7..6984b5c8 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -111,7 +111,7 @@ Section sum.
{ rewrite nth_overflow // nth_overflow; first by iApply type_incl_refl.
by erewrite <-Forall2_length. }
edestruct @Forall2_lookup_l as (ty2 & Hl2 & Hty2); [done..|].
- rewrite (nth_lookup tyl2 _ _ ty2) //.
+ rewrite (nth_lookup_Some tyl2 _ _ ty2) //.
by iApply (Hty2 with "* [] []"). }
clear -Hleq. iSplit; last (iSplit; iAlways).
- simpl. by rewrite Hleq.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 50518824..22c6617f 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -37,14 +37,16 @@ Section uniq_bor.
iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ ty_shr ty (κ∪κ') tid l')%I
with "[Hpbown]") as "#Hinv"; first by eauto.
iIntros "!> !# * % Htok". iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
- (* FIXME We shouldn't have to add this manually to make the set_solver below work (instead, solve_ndisj below should do it). Also, this goal itself should be handled by solve_ndisj. *)
- assert (↑shrN ⊥ ↑lftN). { eapply ndot_preserve_disjoint_l. solve_ndisj. }
iDestruct "INV" as "[>Hbtok|#Hshr]".
- iMod (bor_unnest _ _ _ P with "LFT [Hbtok]") as "Hb".
- { set_solver. } { iApply bor_unfold_idx. eauto. }
- iModIntro. iNext. iMod "Hb".
- iMod (bor_iff with "LFT [] Hb") as "Hb". set_solver. by eauto.
- iMod (ty.(ty_share) with "LFT Hb Htok") as "[#Hshr $]". set_solver.
+ { apply ndisj_subseteq_difference. solve_ndisj. set_solver. } (* FIXME: some tactic should solve this in one go. *)
+ { iApply bor_unfold_idx. eauto. }
+ iModIntro. iNext. iMod "Hb".
+ iMod (bor_iff with "LFT [] Hb") as "Hb".
+ { apply ndisj_subseteq_difference. solve_ndisj. set_solver. } (* FIXME: some tactic should solve this in one go. *)
+ { by eauto. }
+ iMod (ty.(ty_share) with "LFT Hb Htok") as "[#Hshr $]".
+ { apply ndisj_subseteq_difference. solve_ndisj. set_solver. } (* FIXME: some tactic should solve this in one go. *)
iMod ("Hclose" with "[]") as "_"; auto.
- iMod ("Hclose" with "[]") as "_". by eauto.
iApply step_fupd_intro. set_solver. auto.
--
GitLab