This module contains types to manages simp theorems and sets theirof.

Overview of types in this module:

• Origin: Identifies where a simp theorem comes from (global declaration or local expression). Includes the direction of the theorem for global declarations.
• SimpTheorem: Represents a single simp theorem, including its origin and proof.
• SimpEntry: The effect of a simp attribute; either a SimpTheorem or information about a definition to unfold. This is stored in oleans.
• SimpTheorems: Main data structure to store the simp set for a given simp invocation, including discrimination trees, sets of erased theorem, declarations to unfold.
• SimpExtension: Environment extension to store the default simp set, or user-defined simp sets. Each simp extension maintains its own SimpTheorems within a module.
• SimpTheoremsArray: Array of SimpTheorems, to avoid the need for merging SimpTheorems when more than one simp extension is enabled.

opaque Lean.Meta.backward.dsimp.useDefEqAttr : Lean.Option Bool

opaque Lean.Meta.debug.tactic.simp.checkDefEqAttr : Lean.Option Bool

inductive Lean.Meta.Origin : Type

An Origin is an identifier for simp theorems which indicates roughly what action the user took which lead to this theorem existing in the simp set.

• decl (declName : Name) (post : Bool := true) (inv : Bool := false) : Origin

  A global declaration in the environment.

• fvar (fvarId : FVarId) : Origin

  A local hypothesis. When contextual := true is enabled, this fvar may exist in an extension of the current local context; it will not be used for rewriting by simp once it is out of scope but it may end up in the usedSimps trace.

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

  A proof term provided directly to a call to simp [ref, ...] where ref is the provided simp argument (of kind Parser.Tactic.simpLemma). The id is a unique identifier for the call.

• other (name : Name) : Origin

  Some other origin. name should not collide with the other types for erasure to work correctly, and simp trace will ignore this lemma. The other origins should be preferred if possible.

instance Lean.Meta.instInhabitedOrigin : Inhabited Origin

Equations

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

instance Lean.Meta.instReprOrigin : Repr Origin

Equations

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

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

A unique identifier corresponding to the origin.

Equations

• (Lean.Meta.Origin.decl a a_1 a_2).key = a
• (Lean.Meta.Origin.fvar a).key = a.name
• (Lean.Meta.Origin.stx a a_1).key = a
• (Lean.Meta.Origin.other a).key = a

def Lean.Meta.Origin.converse : Origin → Option Origin

The origin corresponding to the converse direction (← thm vs. thm)

Equations

• (Lean.Meta.Origin.decl declName phase inv).converse = some (Lean.Meta.Origin.decl declName phase !inv)
• x✝.converse = none

instance Lean.Meta.instBEqOrigin : BEq Origin

Equations

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

instance Lean.Meta.instHashableOrigin : Hashable Origin

Equations

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

def Lean.Meta.Origin.lt : Origin → Origin → Bool

Equations

• (Lean.Meta.Origin.decl declName₁ post inv₁).lt (Lean.Meta.Origin.decl declName₂ post_1 inv₂) = (declName₁.lt declName₂ || declName₁ == declName₂ && !inv₁ && inv₂)
• (Lean.Meta.Origin.decl declName post inv).lt x✝ = false
• x.lt (Lean.Meta.Origin.decl declName post inv) = true
• x✝¹.lt x✝ = x✝¹.key.lt x✝.key

instance Lean.Meta.instLTOrigin : LT Origin

Equations

• Lean.Meta.instLTOrigin = { lt := fun (a b : Lean.Meta.Origin) => a.lt b = true }

instance Lean.Meta.instDecidableLtOrigin (a b : Origin) : Decidable (a < b)

Equations

• Lean.Meta.instDecidableLtOrigin a b = inferInstanceAs (Decidable (a.lt b = true))

@[reducible, inline]

abbrev Lean.Meta.SimpTheoremKey : Type

Equations

• Lean.Meta.SimpTheoremKey = Lean.Meta.DiscrTree.Key

structure Lean.Meta.SimpTheorem : Type

The fields levelParams and proof are used to encode the proof of the simp theorem. If the proof is a global declaration c, we store Expr.const c [] at proof without the universe levels, and levelParams is set to #[] When using the lemma, we create fresh universe metavariables. Motivation: most simp theorems are global declarations, and this approach is faster and saves memory.

The field levelParams is not empty only when we elaborate an expression provided by the user, and it contains universe metavariables. Then, we use abstractMVars to abstract the universe metavariables and create new fresh universe parameters that are stored at the field levelParams.

• keys : Array SimpTheoremKey
• 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
• priority : Nat
• post : Bool
• perm : Bool

  perm is true if lhs and rhs are identical modulo permutation of variables.

• origin : Origin

  origin is mainly relevant for producing trace messages. It is also viewed an id used to "erase" simp theorems from SimpTheorems.

• rfl : Bool

  rfl is true if proof is by Eq.refl, rfl or a @[defeq] theorem.

instance Lean.Meta.instInhabitedSimpTheorem : Inhabited SimpTheorem

Equations

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

def Lean.Meta.isRflTheorem (declName : Name) : CoreM Bool

Equations

• Lean.Meta.isRflTheorem declName = Lean.withoutExporting (Lean.Meta.isRflTheoremCore✝ declName)

def Lean.Meta.isRflProof (proof : Expr) : MetaM Bool

Equations

• Lean.Meta.isRflProof (Lean.Expr.const declName us) = Lean.withoutExporting (liftM (Lean.Meta.isRflTheoremCore✝ declName))
• Lean.Meta.isRflProof proof = Lean.withoutExporting do let __do_lift ← Lean.Meta.inferType proof liftM (Lean.Meta.isRflProofCore✝ __do_lift proof)

instance Lean.Meta.instToFormatSimpTheorem : ToFormat SimpTheorem

Equations

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

def Lean.Meta.ppOrigin {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] : Origin → m MessageData

Equations

• Lean.Meta.ppOrigin (Lean.Meta.Origin.decl a true true) = pure (Lean.toMessageData "← " ++ Lean.toMessageData (Lean.MessageData.ofConstName a) ++ Lean.toMessageData "")
• Lean.Meta.ppOrigin (Lean.Meta.Origin.decl a) = pure (Lean.MessageData.ofConstName a)
• Lean.Meta.ppOrigin (Lean.Meta.Origin.decl a false true) = pure (Lean.toMessageData "↓ ← " ++ Lean.toMessageData (Lean.MessageData.ofConstName a) ++ Lean.toMessageData "")
• Lean.Meta.ppOrigin (Lean.Meta.Origin.decl a false) = pure (Lean.toMessageData "↓ " ++ Lean.toMessageData (Lean.MessageData.ofConstName a) ++ Lean.toMessageData "")
• Lean.Meta.ppOrigin (Lean.Meta.Origin.fvar a) = pure (Lean.MessageData.ofExpr (Lean.mkFVar a))
• Lean.Meta.ppOrigin (Lean.Meta.Origin.stx a a_1) = pure (Lean.MessageData.ofSyntax a_1)
• Lean.Meta.ppOrigin (Lean.Meta.Origin.other a) = pure (Lean.MessageData.ofName a)

def Lean.Meta.ppSimpTheorem {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] (s : SimpTheorem) : m MessageData

Equations

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

instance Lean.Meta.instBEqSimpTheorem : BEq SimpTheorem

Equations

• Lean.Meta.instBEqSimpTheorem = { beq := fun (e₁ e₂ : Lean.Meta.SimpTheorem) => e₁.proof == e₂.proof }

def Lean.Meta.simpGlobalConfig : ConfigWithKey

Configuration for MetaM used to process global simp theorems

Equations

• Lean.Meta.simpGlobalConfig = { transparency := Lean.Meta.TransparencyMode.reducible, iota := false, proj := Lean.Meta.ProjReductionKind.no, zetaDelta := false }.toConfigWithKey

@[inline]

def Lean.Meta.withSimpGlobalConfig {α : Type} : MetaM α → MetaM α

Equations

• Lean.Meta.withSimpGlobalConfig = Lean.Meta.withConfigWithKey Lean.Meta.simpGlobalConfig

def Lean.Meta.mkSimpTheoremFromConst (declName : Name) (post : Bool := true) (inv : Bool := false) (prio : Nat := 1000) : MetaM (Array SimpTheorem)

Creates a SimpTheorem from a global theorem. Because some theorems lead to multiple SimpTheorems (in particular conjunctions), returns an array.

Equations

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

def Lean.Meta.SimpTheorem.getValue (simpThm : SimpTheorem) : MetaM Expr

Equations

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

def Lean.Meta.mkSimpTheoremFromExpr (id : Origin) (levelParams : Array Name) (proof : Expr) (inv : Bool := false) (post : Bool := true) (prio : Nat := 1000) (config : ConfigWithKey := simpGlobalConfig) : MetaM (Array SimpTheorem)

Equations

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

inductive Lean.Meta.SimpEntry : Type

A simp theorem or information about a declaration to unfold by simp. This is stored in the oleans to implement the simp attribute and user-defined simp sets.

• thm : SimpTheorem → SimpEntry
• toUnfold : Name → SimpEntry
• toUnfoldThms : Name → Array Name → SimpEntry

instance Lean.Meta.instInhabitedSimpEntry : Inhabited SimpEntry

Equations

• Lean.Meta.instInhabitedSimpEntry = { default := Lean.Meta.SimpEntry.thm default }

def Lean.Meta.Simp.ignoreEquations (declName : Name) : CoreM Bool

Reducible functions and projection functions should always be put in toUnfold, instead of trying to use equational theorems.

The simplifiers has special support for structure and class projections, and gets confused when they suddenly rewrite, so ignore equations for them

Equations

• Lean.Meta.Simp.ignoreEquations declName = do let __do_lift ← Lean.isProjectionFn declName let __do_lift_1 ← Lean.isReducible declName pure (__do_lift || __do_lift_1)

def Lean.Meta.Simp.unfoldEvenWithEqns (declName : Name) : CoreM Bool

Even if a function has equation theorems, we also store it in the toUnfold set in the following two cases: 1- It was defined by structural recursion and has a smart-unfolding associated declaration. 2- It is non-recursive.

Reason: unfoldPartialApp := true or conditional equations may not apply.

Remark: In the future, we are planning to disable this behavior unless unfoldPartialApp := true. Moreover, users will have to use f.eq_def if they want to force the definition to be unfolded.

Equations

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

def Lean.Meta.mkSimpEntryOfDeclToUnfold (declName : Name) : MetaM (Array SimpEntry)

Given the name of a declaration to unfold, return the SimpEntry (or entries) that implement this unfolding, using either the equational theorems, or SimpEntry.toUnfold, or both.

Equations

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

@[reducible, inline]

abbrev Lean.Meta.SimpTheoremTree : Type

Equations

• Lean.Meta.SimpTheoremTree = Lean.Meta.DiscrTree Lean.Meta.SimpTheorem

structure Lean.Meta.SimpTheorems : Type

The theorems in a simp set.

• pre : SimpTheoremTree
• post : SimpTheoremTree
• lemmaNames : PHashSet Origin
• toUnfold : PHashSet Name

  Constants (and let-declaration FVarId) to unfold. When zetaDelta := false, the simplifier will expand a let-declaration if it is in this set.

• erased : PHashSet Origin
• toUnfoldThms : PHashMap Name (Array Name)

instance Lean.Meta.instInhabitedSimpTheorems : Inhabited SimpTheorems

Equations

• Lean.Meta.instInhabitedSimpTheorems = { default := { pre := default, post := default, lemmaNames := default, toUnfold := default, erased := default, toUnfoldThms := default } }

partial def Lean.Meta.SimpTheorems.eraseCore (d : SimpTheorems) (thmId : Origin) : SimpTheorems

def Lean.Meta.SimpTheorems.unerase (d : SimpTheorems) (thmId : Origin) : SimpTheorems

Equations

• d.unerase thmId = { pre := d.pre, post := d.post, lemmaNames := d.lemmaNames, toUnfold := d.toUnfold, erased := Lean.PersistentHashSet.erase d.erased thmId, toUnfoldThms := d.toUnfoldThms }

def Lean.Meta.SimpTheorems.addSimpTheorem (d : SimpTheorems) (e : SimpTheorem) : SimpTheorems

Equations

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

def Lean.Meta.SimpTheorems.addSimpTheorem.updateLemmaNames (e : SimpTheorem) (s : PHashSet Origin) : PHashSet Origin

Equations

• Lean.Meta.SimpTheorems.addSimpTheorem.updateLemmaNames e s = Lean.PersistentHashSet.insert s e.origin

@[deprecated Lean.Meta.SimpTheorems.addSimpTheorem (since := "2025-06-17")]

def Lean.Meta.addSimpTheoremEntry (d : SimpTheorems) (e : SimpTheorem) : SimpTheorems

Equations

• Lean.Meta.addSimpTheoremEntry = Lean.Meta.SimpTheorems.addSimpTheorem

def Lean.Meta.SimpTheorems.addDeclToUnfoldCore (d : SimpTheorems) (declName : Name) : SimpTheorems

Equations

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

def Lean.Meta.SimpTheorems.addLetDeclToUnfold (d : SimpTheorems) (fvarId : FVarId) : SimpTheorems

Equations

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

def Lean.Meta.SimpTheorems.isDeclToUnfold (d : SimpTheorems) (declName : Name) : Bool

Return true if declName is tagged to be unfolded using unfoldDefinition? (i.e., without using equational theorems).

Equations

• d.isDeclToUnfold declName = Lean.PersistentHashSet.contains d.toUnfold declName

def Lean.Meta.SimpTheorems.isLetDeclToUnfold (d : SimpTheorems) (fvarId : FVarId) : Bool

Equations

• d.isLetDeclToUnfold fvarId = Lean.PersistentHashSet.contains d.toUnfold fvarId.name

def Lean.Meta.SimpTheorems.isLemma (d : SimpTheorems) (thmId : Origin) : Bool

Equations

• d.isLemma thmId = Lean.PersistentHashSet.contains d.lemmaNames thmId

def Lean.Meta.SimpTheorems.registerDeclToUnfoldThms (d : SimpTheorems) (declName : Name) (eqThms : Array Name) : SimpTheorems

Register the equational theorems for the given definition.

Equations

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

def Lean.Meta.SimpTheorems.erase {m : Type → Type} [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (d : SimpTheorems) (thmId : Origin) : m SimpTheorems

Equations

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

def Lean.Meta.SimpTheorems.addSimpEntry (d : SimpTheorems) (e : SimpEntry) : SimpTheorems

Equations

• d.addSimpEntry (Lean.Meta.SimpEntry.thm e_2) = d.addSimpTheorem e_2
• d.addSimpEntry (Lean.Meta.SimpEntry.toUnfold n) = d.addDeclToUnfoldCore n
• d.addSimpEntry (Lean.Meta.SimpEntry.toUnfoldThms n thms) = d.registerDeclToUnfoldThms n thms

def Lean.Meta.SimpTheorems.uneraseSimpEntry (d : SimpTheorems) (e : SimpEntry) : SimpTheorems

simp [foo] should undo a previous attribute @[-simp] foo. (Note that attribute @[simp] foo does not undo a attribute @[simp] foo, see #5852)

Equations

• d.uneraseSimpEntry (Lean.Meta.SimpEntry.thm e_2) = d.unerase e_2.origin
• d.uneraseSimpEntry e = d

def Lean.Meta.SimpTheorems.addConst (s : SimpTheorems) (declName : Name) (post : Bool := true) (inv : Bool := false) (prio : Nat := 1000) : MetaM SimpTheorems

Auxiliary method for adding a global declaration to a SimpTheorems datastructure.

Equations

• s.addConst declName post inv prio = do let simpThms ← Lean.Meta.mkSimpTheoremFromConst declName post inv prio pure (Array.foldl Lean.Meta.SimpTheorems.addSimpTheorem s simpThms)

@[reducible, inline]

abbrev Lean.Meta.SimpExtension : Type

The environment extension that contains a simp set, returned by Lean.Meta.registerSimpAttr.

Use the simp set's attribute or Lean.Meta.addSimpTheorem to add theorems to the simp set. Use Lean.Meta.SimpExtension.getTheorems to get the contents.

Equations

• Lean.Meta.SimpExtension = Lean.SimpleScopedEnvExtension Lean.Meta.SimpEntry Lean.Meta.SimpTheorems

def Lean.Meta.SimpExtension.getTheorems (ext : SimpExtension) : CoreM SimpTheorems

Equations

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

def Lean.Meta.addSimpTheorem (ext : SimpExtension) (declName : Name) (post inv : Bool) (attrKind : AttributeKind) (prio : Nat) : MetaM Unit

Adds a simp theorem to a simp extension

Equations

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

def Lean.Meta.mkSimpExt (name : Name := by exact decl_name%) : IO SimpExtension

Equations

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

@[reducible, inline]

abbrev Lean.Meta.SimpExtensionMap : Type

Equations

• Lean.Meta.SimpExtensionMap = Std.HashMap Lean.Name Lean.Meta.SimpExtension

opaque Lean.Meta.simpExtensionMapRef : IO.Ref SimpExtensionMap

def Lean.Meta.getSimpExtension? (attrName : Name) : IO (Option SimpExtension)

Equations

• Lean.Meta.getSimpExtension? attrName = do let __do_lift ← ST.Ref.get Lean.Meta.simpExtensionMapRef pure __do_lift[attrName]?

def Lean.Meta.SimpTheorems.addDeclToUnfold (d : SimpTheorems) (declName : Name) : MetaM SimpTheorems

Equations

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

def Lean.Meta.SimpTheorems.add (s : SimpTheorems) (id : Origin) (levelParams : Array Name) (proof : Expr) (inv : Bool := false) (post : Bool := true) (prio : Nat := 1000) (config : ConfigWithKey := simpGlobalConfig) : MetaM SimpTheorems

Auxiliary method for adding a local simp theorem to a SimpTheorems datastructure.

Equations

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

@[reducible, inline]

abbrev Lean.Meta.SimpTheoremsArray : Type

A SimpTheoremsArray is a collection of SimpTheorems. The first entry is the default simp set and possible extensions as simp args (simp [thm]), further entries are custom simp sets added a s simp arguments (simp [my_simp_set]). The array is scanned linear during rewriting. This avoids the need for efficiently merging the SimpTheorems data structure.

Equations

• Lean.Meta.SimpTheoremsArray = Array Lean.Meta.SimpTheorems

def Lean.Meta.SimpTheoremsArray.addTheorem (thmsArray : SimpTheoremsArray) (id : Origin) (h : Expr) (config : ConfigWithKey := simpGlobalConfig) : MetaM SimpTheoremsArray

Equations

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

def Lean.Meta.SimpTheoremsArray.eraseTheorem (thmsArray : SimpTheoremsArray) (thmId : Origin) : SimpTheoremsArray

Equations

• thmsArray.eraseTheorem thmId = Array.map (fun (thms : Lean.Meta.SimpTheorems) => thms.eraseCore thmId) thmsArray

def Lean.Meta.SimpTheoremsArray.isErased (thmsArray : SimpTheoremsArray) (thmId : Origin) : Bool

Equations

• thmsArray.isErased thmId = Array.any thmsArray fun (thms : Lean.Meta.SimpTheorems) => Lean.PersistentHashSet.contains thms.erased thmId

def Lean.Meta.SimpTheoremsArray.isDeclToUnfold (thmsArray : SimpTheoremsArray) (declName : Name) : Bool

Equations

• thmsArray.isDeclToUnfold declName = Array.any thmsArray fun (thms : Lean.Meta.SimpTheorems) => thms.isDeclToUnfold declName

def Lean.Meta.SimpTheoremsArray.isLetDeclToUnfold (thmsArray : SimpTheoremsArray) (fvarId : FVarId) : Bool

Equations

• thmsArray.isLetDeclToUnfold fvarId = Array.any thmsArray fun (thms : Lean.Meta.SimpTheorems) => thms.isLetDeclToUnfold fvarId