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.reprGenPatternInfo✝ }

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

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

theorem Lean.Meta.Grind.normConfig_zeta : Lean.Meta.Grind.normConfig✝.zeta = true

theorem Lean.Meta.Grind.normConfig_zetaDelta : Lean.Meta.Grind.normConfig✝.zetaDelta = true

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.

inductive Lean.Meta.Grind.Origin : Type

• decl (declName : Name) : Origin

  A global declaration in the environment.

• fvar (fvarId : FVarId) : Origin

  A local hypothesis.

• stx (id : Name) (ref : Syntax) : Origin

  A proof term provided directly to a call to grind where ref is the provided grind argument. The id is a unique identifier for the call.

• local (id : Name) : Origin

  It is local, but we don't have a local hypothesis for it.

instance Lean.Meta.Grind.instInhabitedOrigin : Inhabited Origin

Equations

• Lean.Meta.Grind.instInhabitedOrigin = { default := Lean.Meta.Grind.Origin.decl default }

instance Lean.Meta.Grind.instReprOrigin : Repr Origin

Equations

• Lean.Meta.Grind.instReprOrigin = { reprPrec := Lean.Meta.Grind.reprOrigin✝ }

def Lean.Meta.Grind.Origin.key : Origin → Name

A unique identifier corresponding to the origin.

Equations

• (Lean.Meta.Grind.Origin.decl a).key = a
• (Lean.Meta.Grind.Origin.fvar a).key = a.name
• (Lean.Meta.Grind.Origin.stx a a_1).key = a
• (Lean.Meta.Grind.Origin.local a).key = a

def Lean.Meta.Grind.Origin.pp {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] (o : Origin) : m MessageData

Equations

• (Lean.Meta.Grind.Origin.decl a).pp = do let __do_lift ← Lean.mkConstWithLevelParams a pure (Lean.MessageData.ofConst __do_lift)
• (Lean.Meta.Grind.Origin.fvar a).pp = pure (Lean.MessageData.ofExpr (Lean.mkFVar a))
• (Lean.Meta.Grind.Origin.stx a a_1).pp = pure (Lean.MessageData.ofSyntax a_1)
• (Lean.Meta.Grind.Origin.local a).pp = pure (Lean.MessageData.ofName a)

instance Lean.Meta.Grind.instBEqOrigin : BEq Origin

Equations

• Lean.Meta.Grind.instBEqOrigin = { beq := fun (a b : Lean.Meta.Grind.Origin) => a.key == b.key }

instance Lean.Meta.Grind.instHashableOrigin : Hashable Origin

Equations

• Lean.Meta.Grind.instHashableOrigin = { hash := fun (a : Lean.Meta.Grind.Origin) => hash a.key }

inductive Lean.Meta.Grind.EMatchTheoremKind : Type

• eqLhs (gen : Bool) : EMatchTheoremKind
• eqRhs (gen : Bool) : EMatchTheoremKind
• eqBoth (gen : Bool) : EMatchTheoremKind
• eqBwd : EMatchTheoremKind
• fwd : EMatchTheoremKind
• bwd (gen : Bool) : EMatchTheoremKind
• leftRight : EMatchTheoremKind
• rightLeft : EMatchTheoremKind
• default (gen : Bool) : EMatchTheoremKind
• user : EMatchTheoremKind

instance Lean.Meta.Grind.instInhabitedEMatchTheoremKind : Inhabited EMatchTheoremKind

Equations

• Lean.Meta.Grind.instInhabitedEMatchTheoremKind = { default := Lean.Meta.Grind.EMatchTheoremKind.eqLhs default }

instance Lean.Meta.Grind.instBEqEMatchTheoremKind : BEq EMatchTheoremKind

Equations

• Lean.Meta.Grind.instBEqEMatchTheoremKind = { beq := Lean.Meta.Grind.beqEMatchTheoremKind✝ }

instance Lean.Meta.Grind.instReprEMatchTheoremKind : Repr EMatchTheoremKind

Equations

• Lean.Meta.Grind.instReprEMatchTheoremKind = { reprPrec := Lean.Meta.Grind.reprEMatchTheoremKind✝ }

instance Lean.Meta.Grind.instHashableEMatchTheoremKind : Hashable EMatchTheoremKind

Equations

• Lean.Meta.Grind.instHashableEMatchTheoremKind = { hash := Lean.Meta.Grind.hashEMatchTheoremKind✝ }

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

structure Lean.Meta.Grind.EMatchTheorem : Type

A theorem for heuristic instantiation based on E-matching.

• levelParams : Array Name

  It stores universe parameter names for universe polymorphic proofs. Recall that it is non-empty only when we elaborate an expression provided by the user. When proof is just a constant, we can use the universe parameter names stored in the declaration.

• proof : Expr
• numParams : Nat
• patterns : List Expr
• symbols : List HeadIndex

  Contains all symbols used in patterns.

• origin : Origin
• kind : EMatchTheoremKind

  The kind is used for generating the patterns. We save it here to implement grind?.

instance Lean.Meta.Grind.instInhabitedEMatchTheorem : Inhabited EMatchTheorem

Equations

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

structure Lean.Meta.Grind.EMatchTheorems : Type

Set of E-matching theorems.

• smap : Lean.PHashMap Lean.Name (List Lean.Meta.Grind.EMatchTheorem)

  The key is a symbol from EMatchTheorem.symbols.

• origins : Lean.PHashSet Lean.Meta.Grind.Origin

  Set of theorem ids that have been inserted using insert.

• erased : Lean.PHashSet Lean.Meta.Grind.Origin

  Theorems that have been marked as erased

• omap : Lean.PHashMap Lean.Meta.Grind.Origin (List Lean.Meta.Grind.EMatchTheorem)

  Mapping from origin to E-matching theorems associated with this origin.

instance Lean.Meta.Grind.instInhabitedEMatchTheorems : Inhabited EMatchTheorems

Equations

• Lean.Meta.Grind.instInhabitedEMatchTheorems = { default := { smap := default, origins := default, erased := default, omap := default } }

def Lean.Meta.Grind.EMatchTheorems.insert (s : EMatchTheorems) (thm : EMatchTheorem) : EMatchTheorems

Inserts a thm with symbols [s_1, ..., s_n] to s. We add s_1 -> { thm with symbols := [s_2, ..., s_n] }. When grind internalizes a term containing symbol s, we process all theorems thm associated with key s. If their thm.symbols is empty, we say they are activated. Otherwise, we reinsert into map.

Equations

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

def Lean.Meta.Grind.EMatchTheorems.contains (s : EMatchTheorems) (origin : Origin) : Bool

Returns true if s contains a theorem with the given origin.

Equations

• s.contains origin = Lean.PersistentHashSet.contains (Lean.Meta.Grind.EMatchTheorems.origins✝ s) origin

def Lean.Meta.Grind.EMatchTheorems.erase (s : EMatchTheorems) (origin : Origin) : EMatchTheorems

Mark the theorem with the given origin as erased

Equations

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

def Lean.Meta.Grind.EMatchTheorems.isErased (s : EMatchTheorems) (origin : Origin) : Bool

Returns true if the theorem has been marked as erased.

Equations

• s.isErased origin = Lean.PersistentHashSet.contains (Lean.Meta.Grind.EMatchTheorems.erased✝ s) origin

@[inline]

def Lean.Meta.Grind.EMatchTheorems.retrieve? (s : EMatchTheorems) (sym : Name) : Option (List EMatchTheorem × EMatchTheorems)

Retrieves theorems from s associated with the given symbol. See EMatchTheorem.insert. The theorems are removed from s.

Equations

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

def Lean.Meta.Grind.EMatchTheorems.find (s : EMatchTheorems) (origin : Origin) : List EMatchTheorem

Returns theorems associated with the given origin.

Equations

• s.find origin = match Lean.PersistentHashMap.find? (Lean.Meta.Grind.EMatchTheorems.omap✝ s) origin with | some thms => thms | x => []

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

Equations

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

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

Returns true if declName has been tagged as an E-match theorem using [grind].

Equations

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

def Lean.Meta.Grind.resetEMatchTheoremsExt : CoreM Unit

Equations

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

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

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

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

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

@[reducible, inline]

abbrev Lean.Meta.Grind.NormalizePattern.M (α : Type) : Type

Equations

• Lean.Meta.Grind.NormalizePattern.M = StateRefT' IO.RealWorld Lean.Meta.Grind.NormalizePattern.State Lean.MetaM

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.

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

Equations

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

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) : MetaM (List Expr × List HeadIndex × Std.HashSet Nat)

Equations

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

def Lean.Meta.Grind.NormalizePattern.normalizePattern (e : Expr) : M Expr

Equations

• Lean.Meta.Grind.NormalizePattern.normalizePattern e = Lean.Meta.Grind.NormalizePattern.go✝ e false

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) (showInfo : 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) : 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.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.addEMatchTheorem (declName : Name) (numParams : Nat) (patterns : List Expr) (kind : EMatchTheoremKind) : 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.addEMatchEqTheorem (declName : Name) : MetaM Unit

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

Equations

• Lean.Meta.Grind.addEMatchEqTheorem declName = do let __do_lift ← Lean.Meta.Grind.mkEMatchEqTheorem declName Lean.ScopedEnvExtension.add Lean.Meta.Grind.ematchTheoremsExt✝ __do_lift

def Lean.Meta.Grind.getEMatchTheorems : CoreM EMatchTheorems

Returns the E-matching theorems registered in the environment.

Equations

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

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.mkEMatchTheoremWithKind? (origin : Origin) (levelParams : Array Name) (proof : Expr) (kind : EMatchTheoremKind) (groundPatterns : Bool := true) (showInfo : 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.mkEMatchTheoremWithKind?.go (origin : Origin) (levelParams : Array Name) (proof : Expr) (kind : EMatchTheoremKind) (groundPatterns : Bool := true) (showInfo : Bool := false) (xs searchPlaces : Array Expr) : MetaM (Option EMatchTheorem)

Equations

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

def Lean.Meta.Grind.mkEMatchTheoremForDecl (declName : Name) (thmKind : EMatchTheoremKind) (showInfo : 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.addEMatchAttr (declName : Name) (attrKind : AttributeKind) (thmKind : EMatchTheoremKind) (showInfo : Bool := false) : MetaM Unit

Equations

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

def Lean.Meta.Grind.eraseEMatchAttr (declName : Name) : MetaM Unit

Equations

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