Design Note: Symbol Priorities and Extension State

We considered including SymbolPriorities in ExtensionState to allow each grind attribute/extension to define its own symbol priorities. However, this design was rejected because E-match patterns are selected with respect to symbol priorities. When using multiple grind attributes simultaneously (e.g., grind only [attr_1, attr_2]), patterns would need to be re-selected using the union of all symbol priorities and then re-normalized using the union of all normalizers, an expensive operation we want to avoid.

Instead, we use a single global SymbolPriorities set shared across all grind attributes. See also: the related note in Extension.lean regarding normalization.

structure Lean.Meta.Grind.SymbolPriorityEntry : Type

• declName : Name
• prio : Nat

def Lean.Meta.Grind.instInhabitedSymbolPriorityEntry.default : SymbolPriorityEntry

@[implicit_reducible]

instance Lean.Meta.Grind.instInhabitedSymbolPriorityEntry : Inhabited SymbolPriorityEntry

def Lean.Meta.Grind.SymbolPriorities.erase (s : SymbolPriorities) (declName : Name) : SymbolPriorities

Removes the given declaration from s.

def Lean.Meta.Grind.SymbolPriorities.getPrio (s : SymbolPriorities) (declName : Name) : Nat

Returns declName priority for E-matching pattern inference in s.

def Lean.Meta.Grind.SymbolPriorities.contains (s : SymbolPriorities) (declName : Name) : Bool

Returns true, if there is an entry declName ↦ prio in s. Recall that symbols not in s are assumed to have default priority.

def Lean.Meta.Grind.resetSymbolPrioExt : CoreM Unit

def Lean.Meta.Grind.getGlobalSymbolPriorities : CoreM SymbolPriorities

def Lean.Meta.Grind.addSymbolPriorityAttr (declName : Name) (attrKind : AttributeKind) (prio : Nat) : MetaM Unit

Sets declName priority to be used during E-matching pattern inference

def Lean.Meta.Grind.mkOffsetPattern (pat : Expr) (k : Nat) : Expr

def Lean.Meta.Grind.isOffsetPattern? (pat : Expr) : Option (Expr × Nat)

def Lean.Meta.Grind.mkEqBwdPattern (u : List Level) (α lhs rhs : Expr) : Expr

def Lean.Meta.Grind.isEqBwdPattern (e : Expr) : Bool

def Lean.Meta.Grind.isEqBwdPattern? (e : Expr) : Option (Expr × Expr)

def Lean.Meta.Grind.mkGenPattern (u : List Level) (α h x val : Expr) : Expr

def Lean.Meta.Grind.mkGenHEqPattern (u : List Level) (α β h x val : Expr) : Expr

structure Lean.Meta.Grind.GenPatternInfo : Type

Generalized pattern information. See Grind.genPattern gadget.

• heq : Bool
• hIdx : Nat
• xIdx : Nat

def Lean.Meta.Grind.instReprGenPatternInfo.repr : GenPatternInfo → Nat → Format

@[implicit_reducible]

instance Lean.Meta.Grind.instReprGenPatternInfo : Repr GenPatternInfo

def Lean.Meta.Grind.isGenPattern? (pat : Expr) : Option (GenPatternInfo × Expr)

def Lean.Meta.Grind.isMatchCongrEqDeclName (declName : Name) : CoreM Bool

Returns true if declName is the name of a match-expression congruence equation.

def Lean.Meta.Grind.preprocessPattern (pat : Expr) (normalizePattern : Bool := true) : MetaM Expr

def Lean.Meta.Grind.EMatchTheoremKind.isEqLhs : EMatchTheoremKind → Bool

def Lean.Meta.Grind.EMatchTheoremKind.isDefault : EMatchTheoremKind → Bool

def Lean.Meta.Grind.EMatchTheoremKind.toAttributeCore (kind : EMatchTheoremKind) : String

def Lean.Meta.Grind.EMatchTheoremKind.toAttribute (k : EMatchTheoremKind) (minIndexable : Bool) : String

@[reducible, inline]

abbrev Lean.Meta.Grind.EMatchTheorems : Type

Set of E-matching theorems.

@[reducible, inline]

abbrev Lean.Meta.Grind.EMatchTheoremsArray : Type

A collection of sets of E-matching theorems.

def Lean.Meta.Grind.EMatchTheorems.containsWithSamePatterns (s : EMatchTheorems) (origin : Origin) (patterns : List Expr) (cnstrs : List EMatchTheoremConstraint) : Bool

Returns true if there is a theorem with exactly the same pattern and constraints is already in s

def Lean.Meta.Grind.ExtensionStateArray.containsWithSamePatterns (s : ExtensionStateArray) (origin : Origin) (patterns : List Expr) (cnstrs : List EMatchTheoremConstraint) : Bool

def Lean.Meta.Grind.EMatchTheorems.getKindsFor (s : EMatchTheorems) (origin : Origin) : List EMatchTheoremKind

def Lean.Meta.Grind.EMatchTheorem.getProofWithFreshMVarLevels (thm : EMatchTheorem) : MetaM Expr

partial def Lean.Meta.Grind.splitWhileForbidden (pat : Expr) : List Expr

Auxiliary function to expand a pattern containing forbidden application symbols into a multi-pattern.

This function enhances the usability of the [grind =] attribute by automatically handling forbidden pattern symbols. For example, consider the following theorem tagged with this attribute:

getLast?_eq_some_iff {xs : List α} {a : α} : xs.getLast? = some a ↔ ∃ ys, xs = ys ++ [a]

Here, the selected pattern is xs.getLast? = some a, but Eq is a forbidden pattern symbol. Instead of producing an error, this function converts the pattern into a multi-pattern, allowing the attribute to be used conveniently.

The function recursively expands patterns with forbidden symbols by splitting them into their sub-components. If the pattern does not contain forbidden symbols, it is returned as-is.

def Lean.Meta.Grind.mkGroundPattern (e : Expr) : Expr

def Lean.Meta.Grind.groundPattern? (e : Expr) : Option Expr

def Lean.Meta.Grind.isPatternDontCare (e : Expr) : Bool

partial def Lean.Meta.Grind.ppPattern (pattern : Expr) : MessageData

structure Lean.Meta.Grind.NormalizePattern.State : Type

• symbols : Array HeadIndex
• symbolSet : Std.HashSet HeadIndex
• bvarsFound : Std.HashSet Nat

inductive Lean.Meta.Grind.NormalizePattern.PatternArgKind : Type

• relevant : PatternArgKind

  Argument is relevant for E-matching.

• instImplicit : PatternArgKind

  Instance implicit arguments are considered support and handled using isDefEq.

• proof : PatternArgKind

  Proofs are ignored during E-matching. Lean is proof irrelevant.

• typeFormer : PatternArgKind

  Types and type formers are mostly ignored during E-matching, and processed using isDefEq. However, if the argument is of the form C .. where C is inductive type we process it as part of the pattern. Suppose we have as bs : List α, and a pattern candidate expression as ++ bs, i.e., @HAppend.hAppend (List α) (List α) (List α) inst as bs. If we completely ignore the types, the pattern will just be

  @HAppend.hAppend _ _ _ _ #1 #0
  

  This is not ideal because the E-matcher will try it in any goal that contains ++, even if it does not even mention lists.

• outParam : PatternArgKind

  outParam arguments are uniquely determined by type class resolution and should not be part of the e-matching pattern. Including them is redundant (the instance, which is already wildcarded, determines the outParam value) and harmful when the normalizer changes their syntactic form.

  Motivation. Consider the ToInt class used by the grind linear arithmetic module:

  class ToInt (α : Type) (range : outParam IntInterval) where ...
  instance : ToInt (Fin n) (.co 0 n) where ...
  @[grind =] theorem toInt_fin (x : Fin n) : ToInt.toInt x = x.val
  

  The elaborated pattern for toInt_fin is:

  @ToInt.toInt (Fin #1) (IntInterval.co 0 (NatCast.natCast #1)) _ #0
  

  The range argument IntInterval.co 0 (NatCast.natCast #1) is included in the pattern because the pattern generator treats it as relevant. However, the grind normalizer pushes NatCast.natCast inside arithmetic operations, rewriting ↑(n + 1) to ↑n + 1. So when grind processes Fin (n + 1), the e-graph contains:

  @ToInt.toInt (Fin (n + 1)) (IntInterval.co 0 (↑n + 1)) inst x
  

  The pattern expects NatCast.natCast #1 at the second position of IntInterval.co, but the e-graph has HAdd.hAdd (NatCast.natCast n) 1 — a different head symbol. The pattern cannot match, and toInt_fin never fires.

  Since outParam arguments are determined by type class resolution (just like instance arguments, which are already wildcarded), they can be safely ignored in patterns. This is justified by the same reasoning: after e-matching finds candidate substitutions, the instantiation step checks all arguments via isDefEq, preserving soundness.

@[implicit_reducible]

instance Lean.Meta.Grind.NormalizePattern.instReprPatternArgKind : Repr PatternArgKind

def Lean.Meta.Grind.NormalizePattern.instReprPatternArgKind.repr : PatternArgKind → Nat → Format

def Lean.Meta.Grind.NormalizePattern.PatternArgKind.isSupport : PatternArgKind → Bool

def Lean.Meta.Grind.NormalizePattern.getPatternArgKinds (f : Expr) (numArgs : Nat) : MetaM (Array PatternArgKind)

Returns an array kinds s.ts kinds[i] is the kind of the corresponding argument.

• a type (that is not a proposition) or type former (which has forward dependencies) or
• a proof, or
• an instance implicit argument

When kinds[i].isSupport is true, we say the corresponding argument is a "support" argument.

def Lean.Meta.Grind.NormalizePattern.main (patterns : List Expr) (symPrios : SymbolPriorities) (minPrio : Nat) : MetaM (List Expr × List HeadIndex × Std.HashSet Nat)

inductive Lean.Meta.Grind.CheckCoverageResult : Type

Auxiliary type for the checkCoverage function.

• ok : CheckCoverageResult

  checkCoverage succeeded

• missing (pos : List Nat) : CheckCoverageResult

  checkCoverage failed because some of the theorem parameters are missing, pos contains their positions

def Lean.Meta.Grind.mkEMatchTheoremCore (origin : Origin) (levelParams : Array Name) (numParams : Nat) (proof : Expr) (patterns : List Expr) (kind : EMatchTheoremKind) (cnstrs : List EMatchTheoremConstraint := []) (showInfo minIndexable : Bool := false) : MetaM EMatchTheorem

Creates an E-matching theorem for a theorem with proof proof, numParams parameters, and the given set of patterns. Pattern variables are represented using de Bruijn indices.

def Lean.Meta.Grind.mkEMatchTheorem (declName : Name) (numParams : Nat) (patterns : List Expr) (kind : EMatchTheoremKind) (minIndexable : Bool) (cnstrs : List EMatchTheoremConstraint) : MetaM EMatchTheorem

Creates an E-matching theorem for declName with numParams parameters, and the given set of patterns. Pattern variables are represented using de Bruijn indices.

def Lean.Meta.Grind.mkEMatchEqTheoremCore (origin : Origin) (levelParams : Array Name) (proof : Expr) (normalizePattern useLhs gen : Bool) (showInfo : Bool := false) : MetaM EMatchTheorem

Given a theorem with proof proof and type of the form ∀ (a_1 ... a_n), lhs = rhs, creates an E-matching pattern for it using addEMatchTheorem n [lhs] If normalizePattern is true, it applies the grind simplification theorems and simprocs to the pattern.

def Lean.Meta.Grind.mkEMatchEqBwdTheoremCore (origin : Origin) (levelParams : Array Name) (proof : Expr) (showInfo : Bool := false) : MetaM EMatchTheorem

def Lean.Meta.Grind.Extension.isEMatchTheorem (ext : Extension) (declName : Name) : CoreM Bool

def Lean.Meta.Grind.Extension.getEMatchTheorems (ext : Extension) : CoreM EMatchTheorems

def Lean.Meta.Grind.Extension.getEMatchTheoremsForNamespace (ext : Extension) (namespaceName : Name) : CoreM (Array EMatchTheorem)

Returns the scoped E-matching theorems declared in the given namespace.

def Lean.Meta.Grind.mkEMatchEqTheorem (declName : Name) (normalizePattern useLhs : Bool := true) (gen showInfo : Bool := false) : MetaM EMatchTheorem

Given theorem with name declName and type of the form ∀ (a_1 ... a_n), lhs = rhs, creates an E-matching pattern for it using addEMatchTheorem n [lhs]

If normalizePattern is true, it applies the grind simplification theorems and simprocs to the pattern.

def Lean.Meta.Grind.Extension.addEMatchTheorem (ext : Extension) (declName : Name) (numParams : Nat) (patterns : List Expr) (kind : EMatchTheoremKind) (minIndexable : Bool) (attrKind : AttributeKind := AttributeKind.global) (cnstrs : List EMatchTheoremConstraint) : MetaM Unit

Adds an E-matching theorem to the environment. See mkEMatchTheorem.

def Lean.Meta.Grind.Extension.addEMatchEqTheorem (ext : Extension) (declName : Name) : MetaM Unit

Adds an E-matching equality theorem to the environment. See mkEMatchEqTheorem.

opaque Lean.Meta.Grind.backward.grind.inferPattern : Lean.Option Bool

opaque Lean.Meta.Grind.backward.grind.checkInferPatternDiscrepancy : Lean.Option Bool

def Lean.Meta.Grind.EMatchTheoremKind.gen : EMatchTheoremKind → Bool

def Lean.Meta.Grind.mkEMatchTheoremUsingSingletonPatterns (origin : Origin) (levelParams : Array Name) (proof : Expr) (minPrio : Nat) (symPrios : SymbolPriorities) (showInfo : Bool := false) : MetaM (Array EMatchTheorem)

Collects all singleton patterns in the type of the given proof. We use this function to implement local forall expressions in a grind goal.

def Lean.Meta.Grind.mkEMatchTheoremWithKind? (origin : Origin) (levelParams : Array Name) (proof : Expr) (kind : EMatchTheoremKind) (symPrios : SymbolPriorities) (groundPatterns : Bool := true) (showInfo minIndexable : Bool := false) : MetaM (Option EMatchTheorem)

Creates an E-match theorem using the given proof and kind. If groundPatterns is true, it accepts patterns without pattern variables. This is useful for theorems such as theorem evenZ : Even 0. For local theorems, we use groundPatterns := false since the theorem is already in the grind state and there is nothing to be instantiated.

def Lean.Meta.Grind.mkEMatchTheoremForDecl (declName : Name) (thmKind : EMatchTheoremKind) (prios : SymbolPriorities) (showInfo minIndexable : Bool := false) : MetaM EMatchTheorem

def Lean.Meta.Grind.mkEMatchEqTheoremsForDef? (declName : Name) (showInfo : Bool := false) : MetaM (Option (Array EMatchTheorem))

def Lean.Meta.Grind.EMatchTheorems.eraseDecl (s : EMatchTheorems) (declName : Name) : MetaM EMatchTheorems

def Lean.Meta.Grind.Extension.addEMatchAttr (ext : Extension) (declName : Name) (attrKind : AttributeKind) (thmKind : EMatchTheoremKind) (prios : SymbolPriorities) (showInfo minIndexable : Bool := false) : MetaM Unit

def Lean.Meta.Grind.EMatchTheoremKind.toSyntax (kind : EMatchTheoremKind) : CoreM (TSyntax `Lean.Parser.Attr.grindMod)

opaque Lean.Meta.Grind.grind.param.codeAction : Lean.Option Bool

inductive Lean.Meta.Grind.MinIndexableMode : Type

Helper type for generating suggestions for grind parameters

• yes : MinIndexableMode

  minIndexable := true

• no : MinIndexableMode

  minIndexable := false

• both : MinIndexableMode

  Tries with and without the minimal indexable subexpression condition, if both produce the same pattern, use the one minIndexable := false since it is more compact.

def Lean.Meta.Grind.mkEMatchTheoremAndSuggest (ref : Syntax) (declName : Name) (prios : SymbolPriorities) (minIndexable : Bool) (isParam : Bool := false) : MetaM EMatchTheorem

Tries different modifiers, logs info messages with modifiers that worked, but returns just the first one that worked.

def Lean.Meta.Grind.Extension.addEMatchAttrAndSuggest (ext : Extension) (ref : Syntax) (declName : Name) (attrKind : AttributeKind) (prios : SymbolPriorities) (minIndexable showInfo : Bool) (isParam : Bool := false) : MetaM Unit

Tries different modifiers, logs info messages with modifiers that worked, but stores just the first one that worked.

Remark: if backward.grind.inferPattern is true, then .default false is used. The parameter showInfo is only taken into account when backward.grind.inferPattern is true.