From b217790fbbd5c99f06f483c408d20cb9a4e8f8bc Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 8 Jul 2021 09:37:56 +0200
Subject: [PATCH] handle more goals in solve_ndisj

---
 CHANGELOG.md          |  2 ++
 tests/solve_ndisj.v   | 21 ++++++++++++++++-----
 theories/namespaces.v | 11 +++++++++++
 3 files changed, 29 insertions(+), 5 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2207c555..2cbbeaca 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -111,6 +111,8 @@ API-breaking change is listed.
 - Make `done` work on goals of the form `is_Some`.
 - 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 `∅ ## _`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
diff --git a/tests/solve_ndisj.v b/tests/solve_ndisj.v
index 37747539..09ec7934 100644
--- a/tests/solve_ndisj.v
+++ b/tests/solve_ndisj.v
@@ -1,21 +1,32 @@
 From stdpp Require Import namespaces strings.
 
-Lemma test1 (N1 N2 : namespace) :
+Section tests.
+Implicit Types (N : namespace) (E : coPset).
+
+Lemma test1 N1 N2 :
   N1 ## N2 → ↑N1 ⊆@{coPset} ⊤ ∖ ↑N2.
 Proof. solve_ndisj. Qed.
 
-Lemma test2 (N1 N2 : namespace) :
+Lemma test2 N1 N2 :
   N1 ## N2 → ↑N1.@"x" ⊆@{coPset} ⊤ ∖ ↑N1.@"y" ∖ ↑N2.
 Proof. solve_ndisj. Qed.
 
-Lemma test3 (N : namespace) :
+Lemma test3 N :
   ⊤ ∖ ↑N ⊆@{coPset} ⊤ ∖ ↑N.@"x".
 Proof. solve_ndisj. Qed.
 
-Lemma test4 (N : namespace) :
+Lemma test4 N :
   ⊤ ∖ ↑N ⊆@{coPset} ⊤ ∖ ↑N.@"x" ∖ ↑N.@"y".
 Proof. solve_ndisj. Qed.
 
-Lemma test5 (N1 N2 : namespace) :
+Lemma test5 N1 N2 :
   ⊤ ∖ ↑N1 ∖ ↑N2 ⊆@{coPset} ⊤ ∖ ↑N1.@"x" ∖ ↑N2 ∖ ↑N1.@"y".
 Proof. solve_ndisj. Qed.
+
+Lemma test6 E N :
+  ↑N ⊆ E → ↑N ⊆ ⊤ ∖ (E ∖ ↑N).
+Proof. solve_ndisj. Qed.
+
+Lemma test7 N :
+  ↑N ⊆@{coPset} ⊤ ∖ ∅.
+Proof. solve_ndisj. Qed.
diff --git a/theories/namespaces.v b/theories/namespaces.v
index 7065e423..b2e15d73 100644
--- a/theories/namespaces.v
+++ b/theories/namespaces.v
@@ -99,6 +99,17 @@ 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.
+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).
+Global Hint Resolve coPset_disjoint_empty_r : ndisj.
+(** We prefer ∖ on the left of ## (for the [disjoint_difference] lemmas to
+apply), so try moving it there. *)
+Global Hint Extern 10 (_ ## (_ ∖ _)) =>
+  lazymatch goal with
+  | |- (_ ∖ _) ## _ => fail (* ∖ on both sides, leave it be *)
+  | |- _ => symmetry
+  end : ndisj.
 
 Ltac solve_ndisj :=
   repeat match goal with
-- 
GitLab