From d0176db3d4b8ae673aa161a562be6f895db799c7 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 21 Jul 2021 09:55:15 +0200
Subject: [PATCH] solve_ndisj: solve more goals involving chains of differences

---
 tests/solve_ndisj.v   | 8 ++++++++
 theories/namespaces.v | 5 +++++
 theories/sets.v       | 4 ++++
 3 files changed, 17 insertions(+)

diff --git a/tests/solve_ndisj.v b/tests/solve_ndisj.v
index fee607f8..fe6aebdb 100644
--- a/tests/solve_ndisj.v
+++ b/tests/solve_ndisj.v
@@ -35,3 +35,11 @@ Proof. solve_ndisj. Qed.
 Lemma test7 N :
   ↑N ⊆@{coPset} ⊤ ∖ ∅.
 Proof. solve_ndisj. Qed.
+
+Lemma test8 N1 N2 :
+  ⊤ ∖ (↑N1 ∪ ↑N2) ⊆@{coPset} ⊤ ∖ ↑N1.@"counter".
+Proof. solve_ndisj. Qed.
+
+Lemma test9 N1 N2 :
+  ⊤ ∖ (↑N1 ∪ ↑N2) ⊆@{coPset} ⊤ ∖ ↑N1.@"counter" ∖ ↑N1.@"state" ∖ ↑N2.
+Proof. solve_ndisj. Qed.
diff --git a/theories/namespaces.v b/theories/namespaces.v
index b2e15d73..094afabc 100644
--- a/theories/namespaces.v
+++ b/theories/namespaces.v
@@ -84,6 +84,11 @@ Local Definition coPset_empty_subseteq := empty_subseteq (C:=coPset).
 Global Hint Resolve coPset_empty_subseteq : ndisj.
 Local Definition coPset_union_least := union_least (C:=coPset).
 Global Hint Resolve coPset_union_least : ndisj.
+(** For goals like [X ⊆ L ∪ R], backtrack for the two sides. *)
+Local Definition coPset_union_subseteq_l' := union_subseteq_l' (C:=coPset).
+Global Hint Resolve coPset_union_subseteq_l' | 50 : ndisj.
+Local Definition coPset_union_subseteq_r' := union_subseteq_r' (C:=coPset).
+Global Hint Resolve coPset_union_subseteq_r' | 50 : ndisj.
 (** Fallback, loses lots of information but lets other rules make progress. *)
 Local Definition coPset_subseteq_difference_l := subseteq_difference_l (C:=coPset).
 Global Hint Resolve coPset_subseteq_difference_l | 100 : ndisj.
diff --git a/theories/sets.v b/theories/sets.v
index 0d892c9f..3bfef576 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -385,8 +385,12 @@ Section semi_set.
 
   Lemma union_subseteq_l X Y : X ⊆ X ∪ Y.
   Proof. set_solver. Qed.
+  Lemma union_subseteq_l' X X' Y : X ⊆ X' → X ⊆ X' ∪ Y.
+  Proof. set_solver. Qed.
   Lemma union_subseteq_r X Y : Y ⊆ X ∪ Y.
   Proof. set_solver. Qed.
+  Lemma union_subseteq_r' X Y Y' : Y ⊆ Y' → Y ⊆ X ∪ Y'.
+  Proof. set_solver. Qed.
   Lemma union_least X Y Z : X ⊆ Z → Y ⊆ Z → X ∪ Y ⊆ Z.
   Proof. set_solver. Qed.
 
-- 
GitLab