Merge branch 'ralf/solve_ndisj' into 'master'

handle more goals in solve_ndisj

See merge request !294

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`).

tests/solve_ndisj.v

 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 test_ndisjoint_difference_l N : ⊤ ∖ ↑N ##@{coPset} ↑N.
+Proof. solve_ndisj. Qed.
+Lemma test_ndisjoint_difference_r N : ↑N ##@{coPset} ⊤ ∖ ↑N.
+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.

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