chore: exact? runs nonspecific lemmas too (#8459)

Previously, `exact?` has only indexed lemmas with a "specific" `DiscrTree` key (this meant: anything except `#[star]` or `#[Eq, star, star, star]`).

This means that it wouldn't apply some very general lemmas, e.g. `le_antisymm`.

The performance improvement here is pretty minor: the `DiscrTree` returns the more specific matches first, so we only attempt to apply the nonspecific keys last (i.e. if we would otherwise have already failed).



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

Mathlib/Tactic/LibrarySearch.lean

@@ -64,18 +64,6 @@ def processLemma (name : Name) (constInfo : ConstantInfo) :
         |>.push (← DiscrTree.mkPath lhs discrTreeConfig, (name, .mpr))
     | _ => return r
 
-/-- Insert a lemma into the discrimination tree. -/
--- Recall that `apply?` caches the discrimination tree on disk.
--- If you are modifying this file, you will probably want to delete
--- `.lake/build/lib/MathlibExtras/LibrarySearch.extra`
--- so that the cache is rebuilt.
-def addLemma (name : Name) (constInfo : ConstantInfo)
-    (lemmas : DiscrTree (Name × DeclMod)) : MetaM (DiscrTree (Name × DeclMod)) := do
-  let mut lemmas := lemmas
-  for (key, value) in ← processLemma name constInfo do
-    lemmas := lemmas.insertIfSpecific key value discrTreeConfig
-  return lemmas
-
 /-- Construct the discrimination tree of all lemmas. -/
 def buildDiscrTree : IO (DiscrTreeCache (Name × DeclMod)) :=
   DiscrTreeCache.mk "apply?: init cache" processLemma

test/LibrarySearch/basic.lean

@@ -3,6 +3,7 @@ import Mathlib.Util.AssertNoSorry
 import Mathlib.Algebra.Order.Ring.Canonical
 import Mathlib.Data.Quot
 import Mathlib.Data.Nat.Prime
+import Mathlib.Data.Real.Basic
 
 set_option autoImplicit true
 
@@ -222,7 +223,10 @@ lemma prime_of_prime (n : ℕ) : Prime n ↔ Nat.Prime n := by
 lemma ex' (x : ℕ) (_h₁ : x = 0) (h : 2 * 2 ∣ x) : 2 ∣ x := by
   exact? says exact dvd_of_mul_left_dvd h
 
+-- Example from https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Exact.3F.20fails.20on.20le_antisymm/near/388993167
+example {x y : ℝ} (hxy : x ≤ y) (hyx : y ≤ x) : x = y := by
+  exact? says exact le_antisymm hxy hyx
+
 -- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/apply.3F.20failure/near/402534407
-#guard_msgs in
 example (P Q : Prop) (h : P → Q) (h' : ¬Q) : ¬P := by
   exact? says exact mt h h'