From bb8ce569ce941eb3318f13756bb130a2c59a019c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 10 Mar 2021 21:59:09 +0100
Subject: [PATCH] Tweak `multiset_simplify_singletons` to avoid needless
 case-splits.

---
 theories/gmultiset.v | 18 ++++++++++++++----
 1 file changed, 14 insertions(+), 4 deletions(-)

diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index 77a21724..ddbcf4b5 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -225,8 +225,8 @@ Section multiset_unfold.
   Proof. constructor. by rewrite <-(multiset_unfold x X n). Qed.
 End multiset_unfold.
 
+(** Step 3: instantiate hypotheses *)
 Ltac multiset_instantiate :=
-  (* Step 3.1: instantiate hypotheses *)
   repeat match goal with
   | H : (∀ x : ?A, @?P x) |- _ =>
      let e := fresh in evar (e:A);
@@ -245,20 +245,30 @@ Ltac multiset_instantiate :=
      (* 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)
-  end;
-  (* Step 3.2: simplify singletons. *)
+  end.
+
+(** Step 4: simplify singletons *)
+Local Lemma multiplicity_singleton_forget `{Countable A} x y :
+  ∃ n, multiplicity (A:=A) x {[ y ]} = n ∧ n ≤ 1.
+Proof. rewrite multiplicity_singleton'. case_decide; eauto with lia. Qed.
+
+Ltac multiset_simplify_singletons :=
   repeat match goal with
   | H : context [multiplicity ?x {[ ?y ]}] |- _ =>
      first
        [progress rewrite ?multiplicity_singleton, ?multiplicity_singleton_ne in H by done
+       |destruct (multiplicity_singleton_forget x y) as (?&->&?); clear y
        |rewrite multiplicity_singleton' in H; destruct (decide (x = y)); simplify_eq/=]
   | |- context [multiplicity ?x {[ ?y ]}] =>
      first
        [progress rewrite ?multiplicity_singleton, ?multiplicity_singleton_ne by done
+       |destruct (multiplicity_singleton_forget x y) as (?&->&?); clear y
        |rewrite multiplicity_singleton'; destruct (decide (x = y)); simplify_eq/=]
   end.
 
-Ltac multiset_solver := set_solver by (multiset_instantiate; lia).
+(** Putting it all together *)
+Ltac multiset_solver :=
+  set_solver by (multiset_instantiate; multiset_simplify_singletons; lia).
 
 Section more_lemmas.
   Context `{Countable A}.
-- 
GitLab