From 45b64e21a49c061fd5e7f1cd0a946d3d3bda2f1b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 25 Jun 2020 23:28:33 +0200
Subject: [PATCH] Make `multiset_solver` stronger by also considering
 `multiplicity` in hyps.

---
 tests/multiset_solver.v | 2 ++
 theories/gmultiset.v    | 9 +++++++--
 2 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/tests/multiset_solver.v b/tests/multiset_solver.v
index a52397cf..24f3106c 100644
--- a/tests/multiset_solver.v
+++ b/tests/multiset_solver.v
@@ -15,4 +15,6 @@ Section test.
     {[z]} ⊎ X = {[y]} ⊎ Y →
     {[x]} ⊎ ({[z]} ⊎ X) = {[y]} ⊎ ({[x]} ⊎ Y).
   Proof. multiset_solver. Qed.
+  Lemma test5 X x : X ⊎ ∅ = {[x]} → X ⊎ ∅ ≠@{gmultiset A} ∅.
+  Proof. multiset_solver. Qed.
 End test.
diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index 177069a1..736980c1 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -163,8 +163,9 @@ singleton [{[ y ]}] since the singleton receives special treatment in step (3).
 Step (3) is achieved using the tactic [multiset_instantiate], which instantiates
 universally quantified hypotheses [H : ∀ x : A, P x] in two ways:
 
-- If [P] contains a multiset singleton [{[ y ]}] it creates the hypothesis [H y].
-- If the goal contains [multiplicity y X] it creates the hypothesis [H y].
+- If [P] contains a multiset singleton [{[ y ]}] it adds the hypothesis [H y].
+- If the goal or some hypothesis contains [multiplicity y X] it adds the
+  hypothesis [H y].
 *)
 Class MultisetUnfold `{Countable A} (x : A) (X : gmultiset A) (n : nat) :=
   { multiset_unfold : multiplicity x X = n }.
@@ -233,6 +234,10 @@ Ltac multiset_instantiate :=
         already exists. *)
         unify y e'; unless (P y) by assumption; pose proof (H y)
      end
+  | H : (∀ x : ?A, @?P x), _ : context [multiplicity ?y _] |- _ =>
+     (* Use [unless] to avoid creating a new hypothesis [H y : P y] if [P y]
+     already exists. *)
+     unless (P y) by assumption; pose proof (H y)
   | H : (∀ x : ?A, @?P x) |- context [multiplicity ?y _] =>
      (* Use [unless] to avoid creating a new hypothesis [H y : P y] if [P y]
      already exists. *)
-- 
GitLab