From 3b800620104b34193b7b255c458ac58bfe871aeb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 24 Nov 2016 14:48:18 +0100
Subject: [PATCH] =?UTF-8?q?Enable=20solve=5Fndisj=20to=20handle=20E1=20?=
 =?UTF-8?q?=E2=88=96=20=E2=86=91N1=20=E2=8A=86=20E2=20=E2=88=96=20?=
 =?UTF-8?q?=E2=86=91N2=20=E2=88=96=20..=20=E2=88=96=20=E2=86=91Nn.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 base_logic/lib/namespaces.v | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/base_logic/lib/namespaces.v b/base_logic/lib/namespaces.v
index 35e0c148e..549ecf193 100644
--- a/base_logic/lib/namespaces.v
+++ b/base_logic/lib/namespaces.v
@@ -73,14 +73,25 @@ Section namespace.
 
   Lemma ndisj_subseteq_difference N E F : E ⊥ ↑N → E ⊆ F → E ⊆ F ∖ ↑N.
   Proof. set_solver. Qed.
+
+  Lemma namespace_subseteq_difference_l E1 E2 E3 : E1 ⊆ E3 → E1 ∖ E2 ⊆ E3.
+  Proof. set_solver. Qed.
+
+  Lemma ndisj_difference_l E N1 N2 : ↑N2 ⊆ (↑N1 : coPset) → E ∖ ↑N1 ⊥ ↑N2.
+  Proof. set_solver. Qed.
 End namespace.
 
 (* The hope is that registering these will suffice to solve most goals
-of the form [N1 ⊥ N2] and those of the form [↑N1 ⊆ E ∖ ↑N2 ∖ .. ∖ ↑Nn]. *)
+of the forms:
+- [N1 ⊥ N2] 
+- [↑N1 ⊆ E ∖ ↑N2 ∖ .. ∖ ↑Nn]
+- [E1 ∖ ↑N1 ⊆ E2 ∖ ↑N2 ∖ .. ∖ ↑Nn] *)
 Hint Resolve ndisj_subseteq_difference : ndisj.
 Hint Extern 0 (_ ⊥ _) => apply ndot_ne_disjoint; congruence : ndisj.
 Hint Resolve ndot_preserve_disjoint_l : ndisj.
 Hint Resolve ndot_preserve_disjoint_r : ndisj.
 Hint Extern 1 (_ ⊆ _) => apply nclose_subseteq' : ndisj.
+Hint Resolve 100 namespace_subseteq_difference_l : ndisj.
+Hint Resolve ndisj_difference_l : ndisj.
 
 Ltac solve_ndisj := solve [eauto with ndisj].
-- 
GitLab