Merge branch 'robbert/multiset_solver_by' into 'master'

Add `by` parameter to `multiset_solver`

See merge request !457

CHANGELOG.md

@@ -22,6 +22,7 @@ Coq 8.12 and 8.13 are no longer supported by this release.
 - Improve `bijective_finite`: do not require an inverse, do not unnecessarily
   remove duplicates.
 - Add operation `*:` for "scalar" multiplication of multisets.
+- Add `by` parameter to `multiset_solver`, which defaults to `eauto`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).

stdpp/gmultiset.v

@@ -332,8 +332,16 @@ Ltac multiset_simplify_singletons :=
   end.
 
 (** Putting it all together *)
-Ltac multiset_solver :=
-  set_solver by (multiset_instantiate; multiset_simplify_singletons; lia).
+(** Similar to [set_solver] and [naive_solver], [multiset_solver] has a [by]
+parameter whose default is [eauto]. *)
+Tactic Notation "multiset_solver" "by" tactic3(tac) :=
+  set_solver by (multiset_instantiate;
+                 multiset_simplify_singletons;
+                 (* [fast_done] to solve trivial equalities or contradictions,
+                 [lia] for the common case that involves arithmetic,
+                 [tac] if all else fails *)
+                 solve [fast_done|lia|tac]).
+Tactic Notation "multiset_solver" := multiset_solver by eauto.
 
 Section more_lemmas.
   Context `{Countable A}.
@@ -659,13 +667,7 @@ Section more_lemmas.
   Proof. multiset_solver. Qed.
   Lemma gmultiset_singleton_subseteq x y :
     {[+ x +]} ⊆@{gmultiset A} {[+ y +]} ↔ x = y.
-  Proof.
-    split; [|multiset_solver].
-    (* FIXME: [multiset_solver] should solve this *)
-    intros Hxy. specialize (Hxy x).
-    rewrite multiplicity_singleton, multiplicity_singleton' in Hxy.
-    case_decide; [done|lia].
-  Qed.
+  Proof. multiset_solver. Qed.
 
   Lemma gmultiset_elem_of_subseteq X1 X2 x : x ∈ X1 → X1 ⊆ X2 → x ∈ X2.
   Proof. multiset_solver. Qed.

tests/multiset_solver.v

@@ -58,6 +58,19 @@ Section test.
   Lemma test_elem_of_6 x y X : {[+ x; y +]} ⊆ X → x ∈ X ∧ y ∈ X.
   Proof. multiset_solver. Qed.
 
+  (** Tests where the goals do not involve the multiset connectives *)
+  Lemma test_goal_1 x y X : {[+ x +]} ∪ X ⊆ {[+ y +]} → x = y.
+  Proof. multiset_solver. Qed.
+  Lemma test_goal_2 x y X : {[+ x +]} ∪ X ⊆ {[+ y +]} → [x] = [y].
+  Proof. multiset_solver. Qed.
+  Lemma test_goal_3 x y X l :
+    {[+ x +]} ∪ X ⊆ {[+ y +]} → [x] `suffix_of` l ++ [y].
+  Proof.
+    (* [multiset_solver] will first substitute [x]/[y], and then [eauto] is used
+    on the leaf. *)
+    multiset_solver by eauto using suffix_app_r.
+  Qed.
+
   Lemma test_big_1 x1 x2 x3 x4 :
     {[+ x1; x2; x3; x4; x4 +]} ⊆@{gmultiset A} {[+ x1; x1; x2; x3; x4; x4 +]}.
   Proof. multiset_solver. Qed.