on a newer Iris version, the solve_ndisj works somewhat better

opam.pins

-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq b1fa82f0ef47d01f88b9032f265d3754adf5fa5b
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 2472f932c13e0e00b08eb1e00c2fcaaf78b260a8

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.

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").

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. 

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.

[Ralf Jung]

@robbertkrebbers @jjourdan We have 6 examples in this commit of things that should be handled automatically by either solve_ndisj or set_solver. 5 of them would I thunk be handled by solve_ndisj if it had a fallback to set_solver. The one in shr_bor is more tricky, I don't see an obvious way to handle it.

[Ralf Jung]

Also see https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/a0961de3b2ffac4a5af4bc80515dad1b57d06f9b.