solve_ndisj: handle goals containing _ ∖ _ ∖ _

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

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.

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