feat: filter MePo candidates to theorems and order output by iteration (#13750)

This PR refines MePo premise selection so that (1) candidates are
restricted to theorems, matching the convention already used by
`SineQuaNon` and `SymbolFrequency`, and (2) the result is ordered
lexicographically by `(iteration, score)` rather than by score alone.

Before the theorem filter, `mepoSelector` returned functions, recursors,
and casts (e.g. `Int.add`, `Eq.ndrec`, `cast`, `proof_irrel`) alongside
real premises. With it, those go away and the obvious lemmas — e.g.
`Int.add_comm` for `a + b = b + a` — rank well above the remaining
noise.

The `(iteration, score)` ordering preserves the iteration priority of
the original Meng–Paulson MePo: an iter-1 premise scoring 0.6 always
ranks above an iter-2 premise scoring 1.0, since later iterations score
against a strictly larger `relevant` set and a higher threshold, so
their raw scores are not comparable.

Thanks to Xavier Généreux for the report. Further tuning of the score
function (the remaining problem: small generic theorems still score 1.0)
is tracked in https://github.com/leanprover/lean4/issues/13749.

Depends on https://github.com/leanprover/lean4/pull/13747.

🤖 Prepared with Claude Code

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

src/Lean/LibrarySuggestions/MePo.lean

@@ -57,11 +57,16 @@ def mepo (initialRelevant : NameSet) (score : NameSet → NameSet → Float) (ac
       |>.partition fun (_, _, s) => p ≤ s
     if newAccepted.isEmpty then return accepted
     trace[mepo] m!"Accepted {newAccepted.map fun (n, _, s) => (n, s)}."
+    -- Scores from different iterations are not comparable: each iteration accepts
+    -- against a strictly larger `relevant` set and a higher threshold. We order the
+    -- output by `(iteration, score)`: earlier iterations always rank first, and
+    -- within an iteration we sort by descending score.
+    let newAccepted := newAccepted.qsort (fun (_, _, s₁) (_, _, s₂) => s₁ > s₂)
     accepted := newAccepted.foldl (fun acc (n, _, s) => acc.push { name := n, score := s }) accepted
     candidates := candidates'.map fun (n, c, _) => (n, c)
     relevant := newAccepted.foldl (fun acc (_, ns, _) => acc ++ ns) relevant
     p := p + (1 - p) / c
-  return accepted.qsort (fun a b => a.score > b.score)
+  return accepted
 
 end MePo
 
@@ -76,7 +81,8 @@ public def mepoSelector (useRarity : Bool) (p : Float := 0.6) (c : Float := 2.4)
     pure <| frequencyScore (fun n => frequency.getD n 0)
   else
     pure <| unweightedScore
-  let accept := fun ci => return !isDeniedPremise env ci.name
+  let accept := fun ci =>
+    return !isDeniedPremise env ci.name && wasOriginallyTheorem env ci.name
   let suggestions ← mepo constants score accept config.maxSuggestions p c
-  -- `mepo` already returns suggestions in score-descending order.
+  -- `mepo` already returns suggestions ordered by `(iteration, score)`.
   return suggestions.take config.maxSuggestions

tests/elab/library_suggestions_mepo_order.lean

@@ -1,12 +1,13 @@
 import Lean.LibrarySuggestions.MePo
 
 /-!
-Regression test: the MePo premise selector must return suggestions in
-score-descending order.
+Regression test: the MePo premise selector filters candidates to theorems
+(matching the convention already used by `SineQuaNon` and `SymbolFrequency`)
+and finds the obvious lemma for an arithmetic equality goal.
 
-A stale `.reverse` in `mepoSelector` (left over from before the selector was
-made score-sorting) flipped the order to score-ascending, so `.take` returned
-the lowest-scoring premises instead of the best ones.
+Output is ordered by `(iteration, score)` rather than by score alone, so the
+score sequence is not globally monotonic — a score jump signals an iteration
+boundary.
 -/
 
 open Lean Lean.Elab.Tactic Lean.LibrarySuggestions
@@ -15,11 +16,13 @@ example (a b : Int) : a + b = b + a := by
   run_tac do
     let sel : Selector := mepoSelector (useRarity := false)
     let s ← sel (← getMainGoal) {}
-    let mut prev? : Option Float := none
-    for x in s do
-      if let some prev := prev? then
-        unless prev ≥ x.score do
-          throwError "MePo suggestions are not score-descending: \
-            score {prev} precedes score {x.score}"
-      prev? := some x.score
+    let names := s.map (·.name)
+    if names.contains ``Eq.ndrec then
+      throwError "Eq.ndrec (a recursor) should be filtered out by the theorem-only \
+        accept filter"
+    if names.contains ``Int.add then
+      throwError "Int.add (a function) should be filtered out by the theorem-only \
+        accept filter"
+    unless names.contains ``Int.add_comm do
+      throwError "Int.add_comm should appear in the MePo suggestions for `a + b = b + a`"
   sorry

tests/elab/library_suggestions_mepo_order.lean.out.expected

@@ -1 +1 @@
-library_suggestions_mepo_order.lean:14:0-14:7: warning: declaration uses `sorry`
+library_suggestions_mepo_order.lean:15:0-15:7: warning: declaration uses `sorry`