From a9c8861dd7f95bb4e58999de15ca91cfddd66b68 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 22 Jul 2021 11:55:34 +0200
Subject: [PATCH] =?UTF-8?q?solve=5Fndisj:=20handle=20goals=20containing=20?=
 =?UTF-8?q?=5F=20=E2=88=96=20=5F=20=E2=88=96=20=5F?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 CHANGELOG.md          |  3 ++-
 tests/solve_ndisj.v   |  4 ++++
 theories/namespaces.v | 19 ++++++++++++-------
 3 files changed, 18 insertions(+), 8 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index ccdb0394..0282b1e8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -112,7 +112,8 @@ API-breaking change is listed.
 - Add `mk_evar` tactic to generate evars (intended as a more useful replacement
   for Coq's `evar` tactic).
 - Make `solve_ndisj` able to solve more goals of the form `_ ⊆ ⊤ ∖ _`,
-  `_ ∖ _ ## _`, `_ ## _ ∖ _`, as well as `_ ## ∅` and `∅ ## _`.
+  `_ ∖ _ ## _`, `_ ## _ ∖ _`, as well as `_ ## ∅` and `∅ ## _`,
+  and goals containing `_ ∖ _ ∖ _`.
 - Improvements to curry:
   + Swap names of `curry`/`uncurry`, `curry3`/`uncurry3`, `curry4`/`uncurry4`,
     `gmap_curry`/`gmap_uncurry`, and `hcurry`/`huncurry` to be consistent with
diff --git a/tests/solve_ndisj.v b/tests/solve_ndisj.v
index fe6aebdb..662824d0 100644
--- a/tests/solve_ndisj.v
+++ b/tests/solve_ndisj.v
@@ -43,3 +43,7 @@ Proof. solve_ndisj. Qed.
 Lemma test9 N1 N2 :
   ⊤ ∖ (↑N1 ∪ ↑N2) ⊆@{coPset} ⊤ ∖ ↑N1.@"counter" ∖ ↑N1.@"state" ∖ ↑N2.
 Proof. solve_ndisj. Qed.
+
+Lemma test10 N1 N2 E :
+  ↑N1 ∪ E ## ⊤ ∖ ↑N1 ∖ ↑N2 ∖ E.
+Proof. solve_ndisj. Qed.
diff --git a/theories/namespaces.v b/theories/namespaces.v
index 094afabc..3c0f1b19 100644
--- a/theories/namespaces.v
+++ b/theories/namespaces.v
@@ -97,13 +97,7 @@ Global Hint Resolve nclose_subseteq' | 100 : ndisj.
 (** Rules for goals of the form [_ ## _] *)
 (** The base rule that we want to ultimately get down to. *)
 Global Hint Extern 0 (_ ## _) => apply ndot_ne_disjoint; congruence : ndisj.
-(** Fallback, loses lots of information but lets other rules make progress.
-Tests show trying [disjoint_difference_l1] first gives better performance. *)
-Local Definition coPset_disjoint_difference_l1 := disjoint_difference_l1 (C:=coPset).
-Global Hint Resolve coPset_disjoint_difference_l1 | 50 : ndisj.
-Local Definition coPset_disjoint_difference_l2 := disjoint_difference_l2 (C:=coPset).
-Global Hint Resolve coPset_disjoint_difference_l2 | 100 : ndisj.
-Global Hint Resolve ndot_preserve_disjoint_l ndot_preserve_disjoint_r | 100 : ndisj.
+(** Trivial cases. *)
 Local Definition coPset_disjoint_empty_l := disjoint_empty_l (C:=coPset).
 Global Hint Resolve coPset_disjoint_empty_l : ndisj.
 Local Definition coPset_disjoint_empty_r := disjoint_empty_r (C:=coPset).
@@ -115,6 +109,17 @@ Global Hint Extern 10 (_ ## (_ ∖ _)) =>
   | |- (_ ∖ _) ## _ => fail (* ∖ on both sides, leave it be *)
   | |- _ => symmetry
   end : ndisj.
+(** Before we apply disjoint_difference, let's make sure we normalize the goal
+to [_ ∖ (_ ∪ _)]. *)
+Global Hint Extern 20 ((?X ∖ ?Y ∖ ?Z) ## _) =>
+  rewrite (difference_difference_L (C:=coPset) X Y Z) : ndisj.
+(** Fallback, loses lots of information but lets other rules make progress.
+Tests show trying [disjoint_difference_l1] first gives better performance. *)
+Local Definition coPset_disjoint_difference_l1 := disjoint_difference_l1 (C:=coPset).
+Global Hint Resolve coPset_disjoint_difference_l1 | 50 : ndisj.
+Local Definition coPset_disjoint_difference_l2 := disjoint_difference_l2 (C:=coPset).
+Global Hint Resolve coPset_disjoint_difference_l2 | 100 : ndisj.
+Global Hint Resolve ndot_preserve_disjoint_l ndot_preserve_disjoint_r | 100 : ndisj.
 
 Ltac solve_ndisj :=
   repeat match goal with
-- 
GitLab