Merge branch 'ralf/solve_ndisj' into 'master'

solve_ndisj: solve more goals involving chains of differences

See merge request !300

CHANGELOG.md

@@ -119,6 +119,8 @@ API-breaking change is listed.
 - Rename `map_union_subseteq_l_alt` → `map_union_subseteq_l'` and
   `map_union_subseteq_r_alt` → `map_union_subseteq_r'` to be consistent with
   `or_intro_{l,r}'`.
+- Add `union_subseteq_l'`, `union_subseteq_r'` as transitive versions of
+  `union_subseteq_l`, `union_subseteq_r` that can be more easily `apply`ed.
 
 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

@@ -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.

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.

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.