From d1b91fbe3bd50cb1e53167f0f5ab22063d29a7b6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 20 Jun 2019 18:20:06 +0200
Subject: [PATCH] move some general set lemmas to sets.v; organize ndisj hints
 a bit

---
 theories/namespaces.v | 21 ++++++++-------------
 theories/sets.v       |  6 ++++++
 2 files changed, 14 insertions(+), 13 deletions(-)

diff --git a/theories/namespaces.v b/theories/namespaces.v
index 35e01cc5..2bc4ad07 100644
--- a/theories/namespaces.v
+++ b/theories/namespaces.v
@@ -67,13 +67,6 @@ Section namespace.
   Lemma ndot_preserve_disjoint_r N E x : E ## ↑N → E ## ↑N.@x.
   Proof. intros. by apply symmetry, ndot_preserve_disjoint_l. Qed.
 
-  Lemma namespace_subseteq_difference E1 E2 E3 :
-    E1 ## E3 → E1 ⊆ E2 → E1 ⊆ E2 ∖ E3.
-  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.
@@ -84,14 +77,16 @@ of the forms:
 - [↑N1 ⊆ E ∖ ↑N2 ∖ .. ∖ ↑Nn]
 - [E1 ∖ ↑N1 ⊆ E2 ∖ ↑N2 ∖ .. ∖ ↑Nn] *)
 Create HintDb ndisj.
-Hint Resolve namespace_subseteq_difference : ndisj.
-Hint Extern 0 (_ ## _) => apply ndot_ne_disjoint; congruence : ndisj.
-Hint Resolve ndot_preserve_disjoint_l ndot_preserve_disjoint_r : ndisj.
-Hint Resolve nclose_subseteq' ndisj_difference_l : ndisj.
+(* Rules for goals of the form [_ ⊆ _] *)
+Hint Resolve (subseteq_difference_r (A:=positive) (C:=coPset)) : ndisj.
+Hint Resolve nclose_subseteq' : ndisj.
 Hint Resolve (empty_subseteq (A:=positive) (C:=coPset)) : ndisj.
 Hint Resolve (union_least (A:=positive) (C:=coPset)) : ndisj.
-(* Fall-back rules that lose information (but let other rules above apply). *)
-Hint Resolve namespace_subseteq_difference_l | 100 : ndisj.
+Hint Resolve (subseteq_difference_l (A:=positive) (C:=coPset)) | 100 : ndisj.
+(* Rules for goals of the form [_ ## _] *)
+Hint Extern 0 (_ ## _) => apply ndot_ne_disjoint; congruence : ndisj.
+Hint Resolve ndot_preserve_disjoint_l ndot_preserve_disjoint_r : ndisj.
+Hint Resolve ndisj_difference_l : ndisj.
 Hint Resolve (disjoint_difference_l (A:=positive) (C:=coPset)) | 100 : ndisj.
 
 Ltac solve_ndisj :=
diff --git a/theories/sets.v b/theories/sets.v
index 71ab0b72..fcd862b8 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -653,6 +653,12 @@ Section set.
   Lemma difference_mono_r X1 X2 Y : X1 ⊆ X2 → X1 ∖ Y ⊆ X2 ∖ Y.
   Proof. set_solver. Qed.
 
+  Lemma subseteq_difference_r X Y1 Y2 :
+    X ## Y2 → X ⊆ Y1 → X ⊆ Y1 ∖ Y2.
+  Proof. set_solver. Qed.
+  Lemma subseteq_difference_l X1 X2 Y : X1 ⊆ Y → X1 ∖ X2 ⊆ Y.
+  Proof. set_solver. Qed.
+
   (** Disjointness *)
   Lemma disjoint_intersection X Y : X ## Y ↔ X ∩ Y ≡ ∅.
   Proof. set_solver. Qed.
-- 
GitLab