RFC: a consistent priority model for call-site lemma sets

Proposal

Motivation

Tactics that consult a lemma set accept extra lemmas at the call site: simp [h], vcgen [h]. Users expect a call-site lemma to beat whatever the ambient environment supplies. Today this holds only sometimes, and the semantics differ per tactic.

Both tactics select lemmas the same way. Retrieve candidates for a subterm from a discrimination tree. Sort by priority, descending. Try in order; the first lemma that applies wins. Priority is load-bearing: a mis-ordering silently shadows a lemma that would otherwise fire.

• simp at src/Lean/Meta/Tactic/Simp/Rewrite.lean:220:

  let candidates := candidates.insertionSort fun e₁ e₂ => e₁.1.priority > e₂.1.priority
  for (thm, numExtraArgs) in candidates do
    ...
    if let some result ← tryTheoremWithExtraArgs? e thm numExtraArgs then
      return some result   -- first applicable at this subterm commits
  return none
  

• vcgen in SpecAttr.SpecTheorems.findSpecs: same shape (sort descending, pattern.match? e | continue, first hit wins).

Priorities are plain Nat. The standardized priorities (src/Init/Notation.lean):

name	value
low	100
mid	500
default	1000
high	10000

Plus integer literals, parentheses, and + / - arithmetic (addPrio / subPrio). There is no max or highest for prio; max = 1024 belongs to prec. So high is the top named tier, but not a ceiling. The headroom above it is arithmetic (high + n) or a literal.

What priority each kind of entry receives today:

entry	simp	vcgen
@[attr] global	default (1000)	default .. high
@[attr high]	high (10000)	high
named arg tac [h]	default (1000)	high + 3000
splat tac [*]	default (1000)	high + 2000
bracketed def tac [f]	100 - i per equation	high + 1000
ambient auto-collected	n/a	low (100)

The named-arg and splat rows show the inconsistency: only vcgen lifts call-site lemmas above ordinarily-annotated globals. In simp, simp [h] nominally ties a plain @[simp] lemma. The global wins the tie: tree nodes keep insertion order, the call-site entry arrives last, and the sort is stable. The appendix gives an MWE: given @[simp] gA and a call-site gB matching the same subterm, simp fires gA. The unusedSimpArgs linter then suggests deleting gB. So any applicable global overrides a call-site lemma, whether marked high or not. The linter is right that gB had no effect; the defect is that it should have had one.

The bracketed-def row hides a second inversion, this one within simp. @[simp] def f registers f's equations at the attribute priority, default unless annotated. simp [f] registers them at 100 or less. The ambient annotation outranks the call-site bracket for the same definition. The attribute path also drops the specific-before-catch-all ordering: all equations tie at the attribute priority, and only the stable sort preserves their order.

The change

Add three standardized priorities to the prio category:

name	value	meaning
unfold	11000	equations of a definition bracketed at the call site
star	12000	splat / local capture at the call site
arg	13000	explicitly named call-site argument

The names follow prec, which ships short domain-specific names (max, arg, lead, min). The elaborator assigns them across the selection-commit family:

entry	assigned priority
explicit named arg (tac [h])	arg
splat / local capture (tac [*], simp_all locals, vcgen *)	star
equation i of a bracketed definition (tac [f])	unfold - i
@[attr] global	its annotated priority (default .. high)
ambient auto-collected	low

A call-site entry then outranks any ordinarily-annotated global, including @[attr high]. The - i on equations keeps specific ones ahead of the catch-all within the tier. The gaps of 1000 leave headroom for fine-tuning between and above the new priorities.

This applies uniformly: simp [f]'s equations move from 100 - i to unfold - i, and vcgen [f]'s from a flat high + 1000 to unfold - i. vcgen's named and splat tiers keep their values under the new names, arg and star.

Scope

grind is out of scope. E-matching saturates; no lemma wins over another, so grind [h] is additive. grind's prio steers pattern inference, a different axis. Its normalization simp-set accepts neither call-site lemmas nor priorities. There is no selection for a priority to steer.

simp's lemma-set array is also out of scope. simp commits to the first set that rewrites; priorities compete only within a set. Call-site lemmas land in set 0, next to the default simp set, so this proposal reaches them. An extension passed at the call site (simp [myExt]) becomes its own set at the end of the array. Lemmas in the default set therefore override any extension lemma, whatever the priorities. The fix is known: gather candidates across sets, sort once by priority, keep set order as the tie-break. It is also breaking, so it is left to a future RFC that builds on the design settled here.

Design notes

The three tiers order by deliberateness. A named argument is a deliberate pick. A splat captures whatever is in scope. An unfolding is coarser still: it rewrites by definition rather than by a stated property. The order matters at a recursive call: a spec supplied for f should stop the recursion, not lose to f's own unfolding.

Lifting simp [f]'s equations above the globals makes simp [f] unfold the way simp only [f] already does, with the simp set cleaning up afterwards. Eager unfolding terminates in practice: a catch-all rewrite produces a match that blocks on a stuck scrutinee. The attribute path supplies the field evidence, since @[simp] def f has always registered equations at global tier. At a recursive call, a spec or lemma supplied for f still stops the expansion: arg and star outrank unfold.

The lift also repairs the tie-break. Today, ties resolve by discrimination-tree insertion order, an accident of set construction. With star and arg, call-site precedence lives in the priority the sort actually consults.

Typeclass resolution sets the precedent. A local instance is tried before every global instance, whatever the global's priority. star and arg give simp the same discipline. The rule becomes uniform across core: the entry the user placed at the use site wins.

No named ceiling accompanies the new priorities. They mark provenance; none is a generic top tier, and there is still no highest. A library that must pre-empt call-site lemmas climbs with arithmetic (arg + n) or a literal. A named ceiling would invite exactly the shadowing this RFC removes: whoever grabs the top name wins unconditionally. The open scale keeps call-site priorities and library overrides comparable.

Compatibility

• simp, named args and splats: the lift changes which lemma wins wherever a global currently out-ranks a simp [h] at a shared subterm. The redundant idiom simp [foo] with foo already @[simp] is unaffected; the same lemma fires either way. A visible change needs a call-site lemma that rewrites a shared subterm differently from an applicable global. That should be rare.
• simp, bracketed definitions: the equations move from below every global to above them, so simp [f] now unfolds f at subterms a global also rewrites. This is the larger shift; proofs relying on a global pre-empting the unfolding need simp [f, -thatGlobal] or a reordering of their normal form.
• Both changes ship with a backward.simp.* option restoring the old priorities, Mathlib validation before landing, and a re-blessed test suite.
• vcgen: arg and star are value-identical renames. Equations move from a flat high + 1000 to unfold - i; the order against other tiers is unchanged, and the equation order within a definition becomes explicit instead of a tie resolved by insertion order.

In the template's terms: the user experience gain is that simp [h] behaves as it reads, the lemma the user typed wins, and the MWE below stops failing along with its misleading lint. Beneficiaries are every simp user, vcgen users, whose tactic keeps its semantics under shared vocabulary, and library authors, who get a documented scale to calibrate priorities against. Maintainability improves because one assignment rule in the elaborator replaces per-tactic offsets; vcgen's explicitSpecPrio / starSpecPrio / unfoldSpecPrio become uses of the shared names.

Appendix: tie-break experiment

Run against stage1; the trace shows gA:1000 firing and the linter flagging gB as unused.

opaque p : Nat → Nat
axiom gA : ∀ n, p n = n + 1
axiom gB : ∀ n, p n = n + 2

attribute [simp] gA

set_option trace.Meta.Tactic.simp.rewrite true

example : p 3 = 3 + 2 := by simp [gB]  -- gA fires; goal fails

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start with src/Init/Notation.lean, src/Lean/Meta/Tactic/Simp/Rewrite.lean around line 220, and the vcgen entry point SpecAttr.SpecTheorems.findSpecs; use the appendix MWE to reproduce the current ordering. Done means the shared priority names and assignments are implemented consistently, the relevant tests and re-blessed suite pass, and the compatibility option is covered.