From 7c3203e79d3219a946f17b596757cd3a35f6c8ee Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 20 Jun 2019 17:32:48 +0200
Subject: [PATCH] make solve_ndisj more powerful

---
 tests/solve_ndisj.ref | 3 ---
 tests/solve_ndisj.v   | 9 +--------
 theories/namespaces.v | 6 ++++--
 theories/sets.v       | 4 ++++
 4 files changed, 9 insertions(+), 13 deletions(-)

diff --git a/tests/solve_ndisj.ref b/tests/solve_ndisj.ref
index 64a2dc8e..e69de29b 100644
--- a/tests/solve_ndisj.ref
+++ b/tests/solve_ndisj.ref
@@ -1,3 +0,0 @@
-The command has indeed failed with message:
-Ltac call to "solve_ndisj" failed.
-No applicable tactic.
diff --git a/tests/solve_ndisj.v b/tests/solve_ndisj.v
index 7a58ba3a..37747539 100644
--- a/tests/solve_ndisj.v
+++ b/tests/solve_ndisj.v
@@ -1,7 +1,5 @@
 From stdpp Require Import namespaces strings.
 
-Set Ltac Backtrace.
-
 Lemma test1 (N1 N2 : namespace) :
   N1 ## N2 → ↑N1 ⊆@{coPset} ⊤ ∖ ↑N2.
 Proof. solve_ndisj. Qed.
@@ -20,9 +18,4 @@ Proof. solve_ndisj. Qed.
 
 Lemma test5 (N1 N2 : namespace) :
   ⊤ ∖ ↑N1 ∖ ↑N2 ⊆@{coPset} ⊤ ∖ ↑N1.@"x" ∖ ↑N2 ∖ ↑N1.@"y".
-Proof.
-  Fail solve_ndisj. (* FIXME: it should be able to solve this. *)
-  apply namespace_subseteq_difference.
-  { apply ndot_preserve_disjoint_r. set_solver. }
-  solve_ndisj.
-Qed.
+Proof. solve_ndisj. Qed.
diff --git a/theories/namespaces.v b/theories/namespaces.v
index 38862b12..35e01cc5 100644
--- a/theories/namespaces.v
+++ b/theories/namespaces.v
@@ -88,13 +88,15 @@ 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.
-Hint Resolve namespace_subseteq_difference_l | 100 : 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 (disjoint_difference_l (A:=positive) (C:=coPset)) | 100 : ndisj.
 
 Ltac solve_ndisj :=
   repeat match goal with
   | H : _ ∪ _ ⊆ _ |- _ => apply union_subseteq in H as [??]
   end;
-  solve [eauto 10 with ndisj].
+  solve [eauto 12 with ndisj].
 Hint Extern 1000 => solve_ndisj : solve_ndisj.
diff --git a/theories/sets.v b/theories/sets.v
index 90aeda1f..71ab0b72 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -656,6 +656,10 @@ Section set.
   (** Disjointness *)
   Lemma disjoint_intersection X Y : X ## Y ↔ X ∩ Y ≡ ∅.
   Proof. set_solver. Qed.
+  Lemma disjoint_difference_l X Y1 Y2 : Y1 ## X → Y1 ∖ Y2 ## X.
+  Proof. set_solver. Qed.
+  Lemma disjoint_difference_r X Y1 Y2 : X ## Y1 → X ## Y1 ∖ Y2.
+  Proof. set_solver. Qed.
 
   Section leibniz.
     Context `{!LeibnizEquiv C}.
-- 
GitLab