From a0961de3b2ffac4a5af4bc80515dad1b57d06f9b Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Fri, 16 Dec 2016 15:24:39 +0100
Subject: [PATCH] locally teach solve_ndisj how to handle these inclusions
---
theories/typing/uniq_bor.v | 11 +++++------
1 file changed, 5 insertions(+), 6 deletions(-)
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 22c6617f..4d5551b2 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -8,6 +8,8 @@ From lrust.typing Require Import perm lft_contexts type_context typing own.
Section uniq_bor.
Context `{typeG Σ}.
+ Local Hint Extern 1000 (_ ⊆ _) => set_solver : ndisj.
+
Program Definition uniq_bor (κ:lft) (ty:type) :=
{| ty_size := 1;
(* We quantify over [P]s so that the Proper lemma
@@ -38,15 +40,12 @@ Section uniq_bor.
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_unnest _ _ _ P with "LFT [Hbtok]") as "Hb".
- { apply ndisj_subseteq_difference. solve_ndisj. set_solver. } (* FIXME: some tactic should solve this in one go. *)
+ - iMod (bor_unnest _ _ _ P with "LFT [Hbtok]") as "Hb". solve_ndisj.
{ 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. *)
+ iMod (bor_iff with "LFT [] Hb") as "Hb". solve_ndisj.
{ 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 (ty.(ty_share) with "LFT Hb Htok") as "[#Hshr $]". solve_ndisj.
iMod ("Hclose" with "[]") as "_"; auto.
- iMod ("Hclose" with "[]") as "_". by eauto.
iApply step_fupd_intro. set_solver. auto.
--
GitLab