Merge branch 'ralf/solve_ndisj' into 'master'

make solve_ndisj work on goals of the form 'X1 ∪ X2 ## Y'

See merge request !427

stdpp/namespaces.v

@@ -102,6 +102,13 @@ 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.
+(** If-and-only-if rules for ∪ on the left/right. *)
+Local Definition coPset_disjoint_union_l X1 X2 Y :=
+  proj2 (disjoint_union_l (C:=coPset) X1 X2 Y).
+Global Hint Resolve coPset_disjoint_union_l : ndisj.
+Local Definition coPset_disjoint_union_r X Y1 Y2 :=
+  proj2 (disjoint_union_r (C:=coPset) X Y1 Y2).
+Global Hint Resolve coPset_disjoint_union_r : ndisj.
 (** We prefer ∖ on the left of ## (for the [disjoint_difference] lemmas to
 apply), so try moving it there. *)
 Global Hint Extern 10 (_ ## (_ ∖ _)) =>

tests/solve_ndisj.v

@@ -47,3 +47,17 @@ Proof. solve_ndisj. Qed.
 Lemma test10 N1 N2 E :
   ↑N1 ∪ E ## ⊤ ∖ ↑N1 ∖ ↑N2 ∖ E.
 Proof. solve_ndisj. Qed.
+
+Lemma test11 N :
+  ↑N.@"other" ⊆@{coPset} ⊤ ∖ (↑N.@"this" ∪ ↑N.@"that").
+Proof. solve_ndisj. Qed.
+
+Lemma test12 N :
+  ↑N.@"other" ##@{coPset} ↑N.@"this" ∪ ↑N.@"that" ∧
+  ↑N.@"other" ∪ ↑N.@"this" ##@{coPset} ↑N.@"that".
+Proof. split; solve_ndisj. Qed.
+
+Lemma test13 E N :
+  ↑N ⊆ E →
+  ⊤ ∖ E ⊆ ⊤ ∖ (E ∖ ↑N) ∖ ↑N.
+Proof. solve_ndisj. Qed.