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

Equations

• Lean.Meta.Grind.instInhabitedSymbolPriorityEntry.default = { declName := default, prio := default }

instance Lean.Meta.Grind.instInhabitedSymbolPriorityEntry : Inhabited SymbolPriorityEntry

Equations

• Lean.Meta.Grind.instInhabitedSymbolPriorityEntry = { default := Lean.Meta.Grind.instInhabitedSymbolPriorityEntry.default }

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

Removes the given declaration from s.

Equations

• s.erase declName = { map := Lean.PersistentHashMap.erase s.map declName }

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

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

Equations

• s.getPrio declName = match Lean.PersistentHashMap.find? s.map declName with | some prio => prio | x => 1000

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.

Equations

• s.contains declName = Lean.PersistentHashMap.contains s.map declName

def Lean.Meta.Grind.resetSymbolPrioExt : CoreM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.getGlobalSymbolPriorities : CoreM SymbolPriorities

Equations

• Lean.Meta.Grind.getGlobalSymbolPriorities = do let __do_lift ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState Lean.Meta.Grind.symbolPrioExt✝ __do_lift)

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

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

Equations

• Lean.Meta.Grind.addSymbolPriorityAttr declName attrKind prio = Lean.ScopedEnvExtension.add Lean.Meta.Grind.symbolPrioExt✝ { declName := declName, prio := prio } attrKind

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

Equations

• Lean.Meta.Grind.mkOffsetPattern pat k = Lean.mkApp2 (Lean.mkConst `Lean.Grind.offset) pat (Lean.mkRawNatLit k)

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Meta.Grind.mkEqBwdPattern u α lhs rhs = Lean.mkApp3 (Lean.mkConst `Lean.Grind.eqBwdPattern u) α lhs rhs

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

Equations

• Lean.Meta.Grind.isEqBwdPattern e = e.isAppOfArity `Lean.Grind.eqBwdPattern 3

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Meta.Grind.mkGenPattern u α h x val = Lean.mkApp4 (Lean.mkConst `Lean.Grind.genPattern u) α h x val

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

Equations

• Lean.Meta.Grind.mkGenHEqPattern u α β h x val = Lean.mkApp5 (Lean.mkConst `Lean.Grind.genHEqPattern u) α β h x val

structure Lean.Meta.Grind.GenPatternInfo : Type

Generalized pattern information. See Grind.genPattern gadget.

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

instance Lean.Meta.Grind.instReprGenPatternInfo : Repr GenPatternInfo

Equations

• Lean.Meta.Grind.instReprGenPatternInfo = { reprPrec := Lean.Meta.Grind.instReprGenPatternInfo.repr }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• Lean.Meta.Grind.isMatchCongrEqDeclName (p.str s) = (pure (Lean.Meta.Match.isCongrEqnReservedNameSuffix s) <&&> (Lean.Meta.isMatcher p <||> Lean.Meta.isMatcher (Lean.privateToUserName p)))
• Lean.Meta.Grind.isMatchCongrEqDeclName declName = pure false

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• (Lean.Meta.Grind.EMatchTheoremKind.eqLhs gen).isEqLhs = true
• x✝.isEqLhs = false

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

Equations

• (Lean.Meta.Grind.EMatchTheoremKind.default gen).isDefault = true
• x✝.isDefault = false

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

Equations

• (Lean.Meta.Grind.EMatchTheoremKind.eqLhs true).toAttributeCore = "= gen"
• (Lean.Meta.Grind.EMatchTheoremKind.eqLhs false).toAttributeCore = "="
• (Lean.Meta.Grind.EMatchTheoremKind.eqRhs true).toAttributeCore = "=_ gen"
• (Lean.Meta.Grind.EMatchTheoremKind.eqRhs false).toAttributeCore = "=_"
• (Lean.Meta.Grind.EMatchTheoremKind.eqBoth false).toAttributeCore = "_=_"
• (Lean.Meta.Grind.EMatchTheoremKind.eqBoth true).toAttributeCore = "_=_ gen"
• Lean.Meta.Grind.EMatchTheoremKind.eqBwd.toAttributeCore = "←="
• Lean.Meta.Grind.EMatchTheoremKind.fwd.toAttributeCore = "→"
• (Lean.Meta.Grind.EMatchTheoremKind.bwd false).toAttributeCore = "←"
• (Lean.Meta.Grind.EMatchTheoremKind.bwd true).toAttributeCore = "← gen"
• Lean.Meta.Grind.EMatchTheoremKind.leftRight.toAttributeCore = "=>"
• Lean.Meta.Grind.EMatchTheoremKind.rightLeft.toAttributeCore = "<="
• (Lean.Meta.Grind.EMatchTheoremKind.default false).toAttributeCore = "."
• (Lean.Meta.Grind.EMatchTheoremKind.default true).toAttributeCore = ". gen"
• Lean.Meta.Grind.EMatchTheoremKind.user.toAttributeCore = ""

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

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Lean.Meta.Grind.EMatchTheorems : Type

Set of E-matching theorems.

Equations

• Lean.Meta.Grind.EMatchTheorems = Lean.Meta.Grind.Theorems Lean.Meta.Grind.EMatchTheorem

@[reducible, inline]

abbrev Lean.Meta.Grind.EMatchTheoremsArray : Type

A collection of sets of E-matching theorems.

Equations

• Lean.Meta.Grind.EMatchTheoremsArray = Lean.Meta.Grind.TheoremsArray Lean.Meta.Grind.EMatchTheorem

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

Equations

• s.containsWithSamePatterns origin patterns cnstrs = (Lean.Meta.Grind.Theorems.find s origin).any fun (thm : Lean.Meta.Grind.EMatchTheorem) => thm.patterns == patterns && thm.cnstrs == cnstrs

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• s.getKindsFor origin = List.map (fun (x : Lean.Meta.Grind.EMatchTheorem) => x.kind) (Lean.Meta.Grind.Theorems.find s origin)

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

Equations

• thm.getProofWithFreshMVarLevels = Lean.Meta.Grind.getProofWithFreshMVarLevels thm

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

Equations

• Lean.Meta.Grind.mkGroundPattern e = Lean.mkAnnotation `grind.ground_pat e

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

Equations

• Lean.Meta.Grind.groundPattern? e = Lean.annotation? `grind.ground_pat e

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

Equations

• Lean.Meta.Grind.isPatternDontCare e = (e == Lean.Meta.Grind.dontCare✝)

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.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Meta.Grind.NormalizePattern.instReprPatternArgKind = { reprPrec := Lean.Meta.Grind.NormalizePattern.instReprPatternArgKind.repr }

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

Equations

• Lean.Meta.Grind.NormalizePattern.PatternArgKind.relevant.isSupport = false
• x✝.isSupport = true

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• ext.isEMatchTheorem declName = do let __do_lift ← Lean.getEnv pure ((Lean.ScopedEnvExtension.getState ext __do_lift).ematch.contains (Lean.Meta.Grind.Origin.decl declName))

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

Equations

• ext.getEMatchTheorems = do let __do_lift ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState ext __do_lift).ematch

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

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• ext.addEMatchEqTheorem declName = do let __do_lift ← Lean.Meta.Grind.mkEMatchEqTheorem declName Lean.ScopedEnvExtension.add ext (Lean.Meta.Grind.Entry.ematch __do_lift)

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

Equations

• (Lean.Meta.Grind.EMatchTheoremKind.eqLhs gen).gen = gen
• (Lean.Meta.Grind.EMatchTheoremKind.eqRhs gen).gen = gen
• (Lean.Meta.Grind.EMatchTheoremKind.eqBoth gen).gen = gen
• (Lean.Meta.Grind.EMatchTheoremKind.default gen).gen = gen
• (Lean.Meta.Grind.EMatchTheoremKind.bwd gen).gen = gen
• Lean.Meta.Grind.EMatchTheoremKind.eqBwd.gen = false
• Lean.Meta.Grind.EMatchTheoremKind.fwd.gen = false
• Lean.Meta.Grind.EMatchTheoremKind.rightLeft.gen = false
• Lean.Meta.Grind.EMatchTheoremKind.leftRight.gen = false
• Lean.Meta.Grind.EMatchTheoremKind.user.gen = false

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Grind.EMatchTheoremKind.user.toSyntax = Lean.throwError (Lean.toMessageData "`grind` theorem kind is not a modifier")

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.