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

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

instance Lean.Meta.Grind.instReprGenPatternInfo : Repr GenPatternInfo

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

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.

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

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

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.