simp should try more specific lemmas first

[nomeata]

Consider the following code

set_option autoImplicit false 

inductive DOW where
 | monday | tuesday | wednesday | thursday | friday | saturday | sunday

 def DOW.isWorkday (n : Nat) (d : DOW) : Bool :=
  match d with
   | monday | tuesday | wednesday | thursday | friday => true
   | _ => match n with | 0 => false | n+1 => d.isWorkday n

example : DOW.friday.isWorkday 0 := by
  set_option trace.Meta.Tactic.simp true in
  simp  [DOW.isWorkday]

/-- info: DOW.isWorkday.eq_5 (n : Nat) : DOW.isWorkday n DOW.friday = true -/
#guard_msgs in
#check DOW.isWorkday.eq_5
/--
info: DOW.isWorkday.eq_6 (d : DOW) (x_1 : d = DOW.monday → False) (x_2 : d = DOW.tuesday → False)
  (x_3 : d = DOW.wednesday → False) (x_4 : d = DOW.thursday → False) (x_5 : d = DOW.friday → False) :
  DOW.isWorkday 0 d = false
-/
#guard_msgs in
#check DOW.isWorkday.eq_6

The recursion in DOW.isWorkday is there so that we get equational theorems; with #3983 this would apply to a non-recursive function as well.

The lemma DOW.isWorkday.eq_5 should solve this rather quickly. But as the trace reveals, simp tries the rather more complicated DOW.isWorkday.eq_6 first!

(In fact, it does something even weirder that I don’t fully understand, unfolding the definition and then trying to appliy .match_2.eq_n lemmas, or so; the trace is far longer than I would have expected here, so there may be another issue lurking here.)

A possible fix, explored in #4158, might be to tweak the DiscrTree to return more specific lemmas first, but there might be other approaches (e.g. ordering all lemmas returned from the discrtree somehow, maybe trying unconstrainted lemmas before those with side-conditions), hence opening this as an issue.

[JovanGerb]

In type class synthesis, this code gets the result from the discrimination tree:

      let result ← globalInstances.getUnify type tcDtConfig
      -- Using insertion sort because it is stable and the array `result` should be mostly sorted.
      -- Most instances have default priority.
      let result := result.insertionSort fun e₁ e₂ => e₁.priority < e₂.priority

They purposefully use a stable sorting algorithm, and the results are used in the order back-to-front in the array. My interpretation is that this is good because the patterns with more * patterns are at the start of the array. The implementation of DiscrTree is that whenever it has to choose between a star and a non-star search branch, it does the star branch first.

This means that earlier results aren't necessarily always more general than later results, but it does means that earlier results are usually more general than later results

[JovanGerb]

In my RefinedDiscrTree, I output a natural number score that indicates how good the match is, and I sort the result based on the scores of the entries. This a better way of determining which lemmas are more/less specific. This is especially useful for a human-interactive library search, because you really want to show the more relevant results first. It would be possible to also add this to Lean's DiscrTree, or we could see if simp works with RefinedDiscrTree.

[nomeata]

Thanks for the cross-references, that's helpful! It also means that my experiment in #4158 may have affected type class inference negatively, which may skew perf results.