structure Lean.Meta.Simp.Result : Type

• expr : Lean.Expr
• proof? : Option Lean.Expr
• dischargeDepth : UInt32

  Save the field dischargeDepth at Simp.Context because it impacts the simplifier result.

• cache : Bool

  If cache := true the result is cached.

instance Lean.Meta.Simp.instInhabitedResult : Inhabited Lean.Meta.Simp.Result

Equations

• Lean.Meta.Simp.instInhabitedResult = { default := { expr := default, proof? := default, dischargeDepth := default, cache := default } }

def Lean.Meta.Simp.mkEqTransOptProofResult (h? : Option Lean.Expr) (cache : Bool) (r : Lean.Meta.Simp.Result) : Lean.MetaM Lean.Meta.Simp.Result

Equations

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

def Lean.Meta.Simp.Result.mkEqTrans (r₁ : Lean.Meta.Simp.Result) (r₂ : Lean.Meta.Simp.Result) : Lean.MetaM Lean.Meta.Simp.Result

Equations

• Lean.Meta.Simp.Result.mkEqTrans r₁ r₂ = Lean.Meta.Simp.mkEqTransOptProofResult r₁.proof? r₁.cache r₂

@[inline, reducible]

abbrev Lean.Meta.Simp.Cache : Type

Equations

• Lean.Meta.Simp.Cache = Lean.ExprMap Lean.Meta.Simp.Result

@[inline, reducible]

abbrev Lean.Meta.Simp.CongrCache : Type

Equations

• Lean.Meta.Simp.CongrCache = Lean.ExprMap (Option Lean.Meta.CongrTheorem)

structure Lean.Meta.Simp.Context : Type

• config : Lean.Meta.Simp.Config
• maxDischargeDepth : UInt32

  maxDischargeDepth from config as an UInt32.

• simpTheorems : Lean.Meta.SimpTheoremsArray
• congrTheorems : Lean.Meta.SimpCongrTheorems
• parent? : Option Lean.Expr

  Stores the "parent" term for the term being simplified. If a simplification procedure result depends on this value, then it is its reponsability to set Result.cache := false.

  Motivation for this field: Suppose we have a simplication procedure for normalizing arithmetic terms. Then, given a term such as t_1 + ... + t_n, we don't want to apply the procedure to every subterm t_1 + ... + t_i for i < n for performance issues. The procedure can accomplish this by checking whether the parent term is also an arithmetical expression and do nothing if it is. However, it should set Result.cache := false to ensure we don't miss simplification opportunities. For example, consider the following:

  example (x y : Nat) (h : y = 0) : id ((x + x) + y) = id (x + x) := by
    simp_arith only
    ...
  

  If we don't set Result.cache := false for the first x + x, then we get the resulting state:

  ... |- id (2*x + y) = id (x + x)
  

  instead of

  ... |- id (2*x + y) = id (2*x)
  

  as expected.

  Remark: given an application f a b c the "parent" term for f, a, b, and c is f a b c.

• dischargeDepth : UInt32

instance Lean.Meta.Simp.instInhabitedContext : Inhabited Lean.Meta.Simp.Context

Equations

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

def Lean.Meta.Simp.Context.isDeclToUnfold (ctx : Lean.Meta.Simp.Context) (declName : Lake.Name) : Bool

Equations

• Lean.Meta.Simp.Context.isDeclToUnfold ctx declName = Lean.Meta.SimpTheoremsArray.isDeclToUnfold ctx.simpTheorems declName

def Lean.Meta.Simp.Context.mkDefault : Lean.MetaM Lean.Meta.Simp.Context

Equations

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

@[inline, reducible]

abbrev Lean.Meta.Simp.UsedSimps : Type

Equations

• Lean.Meta.Simp.UsedSimps = Lean.HashMap Lean.Meta.Origin Nat

structure Lean.Meta.Simp.State : Type

• cache : Lean.Meta.Simp.Cache
• congrCache : Lean.Meta.Simp.CongrCache
• usedTheorems : Lean.Meta.Simp.UsedSimps
• numSteps : Nat

instance Lean.Meta.Simp.instNonemptyMethodsRef : Nonempty Lean.Meta.Simp.MethodsRef

Equations

• Lean.Meta.Simp.instNonemptyMethodsRef = (_ : Nonempty Lean.Meta.Simp.MethodsRefPointed.val)

@[inline, reducible]

abbrev Lean.Meta.Simp.SimpM (α : Type) : Type

Equations

• Lean.Meta.SimpM = ReaderT Lean.Meta.Simp.MethodsRef (ReaderT Lean.Meta.Simp.Context (StateRefT' IO.RealWorld Lean.Meta.Simp.State Lean.MetaM))

@[extern lean_simp]

opaque Lean.Meta.Simp.simp (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Result

@[extern lean_dsimp]

opaque Lean.Meta.Simp.dsimp (e : Lean.Expr) : Lean.Meta.SimpM Lean.Expr

inductive Lean.Meta.Simp.Step : Type

Result type for a simplification procedure. We have pre and post simplication procedures.

• done: Lean.Meta.Simp.Result → Lean.Meta.Simp.Step

  For pre procedures, it returns the result without visiting any subexpressions.

  For post procedures, it returns the result.

• visit: Lean.Meta.Simp.Result → Lean.Meta.Simp.Step

  For pre procedures, the resulting expression is passed to pre again.

  For post procedures, the resulting expression is passed to pre again IF Simp.Config.singlePass := false and resulting expression is not equal to initial expression.

• continue: optParam (Option Lean.Meta.Simp.Result) none → Lean.Meta.Simp.Step

  For pre procedures, continue transformation by visiting subexpressions, and then executing post procedures.

  For post procedures, this is equivalent to returning visit.

instance Lean.Meta.Simp.instInhabitedStep : Inhabited Lean.Meta.Simp.Step

Equations

• Lean.Meta.Simp.instInhabitedStep = { default := Lean.Meta.Simp.Step.done default }

@[inline, reducible]

abbrev Lean.Meta.Simp.Simproc : Type

A simplification procedure. Recall that we have pre and post procedures. See Step.

Equations

• Lean.Meta.Simp.Simproc = (Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Step)

def Lean.Meta.Simp.mkEqTransResultStep (r : Lean.Meta.Simp.Result) (s : Lean.Meta.Simp.Step) : Lean.MetaM Lean.Meta.Simp.Step

Equations

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

@[always_inline]

def Lean.Meta.Simp.andThen (f : Lean.Meta.Simp.Simproc) (g : Lean.Meta.Simp.Simproc) : Lean.Meta.Simp.Simproc

"Compose" the two given simplification procedures. We use the following semantics.

• If f produces done or visit, then return f's result.
• If f produces continue, then apply g to new expression returned by f.

See Simp.Step type.

Equations

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

instance Lean.Meta.Simp.instAndThenSimproc : AndThen Lean.Meta.Simp.Simproc

Equations

• Lean.Meta.Simp.instAndThenSimproc = { andThen := fun (s₁ : Lean.Meta.Simp.Simproc) (s₂ : Unit → Lean.Meta.Simp.Simproc) => Lean.Meta.Simp.andThen s₁ (s₂ ()) }

structure Lean.Meta.Simp.SimprocOLeanEntry : Type

Simproc .olean entry.

• declName : Lake.Name

  Name of a declaration stored in the environment which has type Simproc.

• post : Bool
• keys : Array Lean.Meta.SimpTheoremKey

instance Lean.Meta.Simp.instInhabitedSimprocOLeanEntry : Inhabited Lean.Meta.Simp.SimprocOLeanEntry

Equations

• Lean.Meta.Simp.instInhabitedSimprocOLeanEntry = { default := { declName := default, post := default, keys := default } }

structure Lean.Meta.Simp.SimprocEntryextends Lean.Meta.Simp.SimprocOLeanEntry : Type

Simproc entry. It is the .olean entry plus the actual function.

• declName : Lake.Name
• post : Bool
• keys : Array Lean.Meta.SimpTheoremKey
• proc : Lean.Meta.Simp.Simproc

  Recall that we cannot store Simproc into .olean files because it is a closure. Given SimprocOLeanEntry.declName, we convert it into a Simproc by using the unsafe function evalConstCheck.

@[inline, reducible]

abbrev Lean.Meta.Simp.SimprocTree : Type

Equations

• Lean.Meta.Simp.SimprocTree = Lean.Meta.DiscrTree Lean.Meta.Simp.SimprocEntry

structure Lean.Meta.Simp.Simprocs : Type

• pre : Lean.Meta.Simp.SimprocTree
• post : Lean.Meta.Simp.SimprocTree
• simprocNames : Lean.PHashSet Lake.Name
• erased : Lean.PHashSet Lake.Name

instance Lean.Meta.Simp.instInhabitedSimprocs : Inhabited Lean.Meta.Simprocs

Equations

• Lean.Meta.Simp.instInhabitedSimprocs = { default := { pre := default, post := default, simprocNames := default, erased := default } }

structure Lean.Meta.Simp.Methods : Type

• pre : Lean.Meta.Simp.Simproc
• post : Lean.Meta.Simp.Simproc
• discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)

instance Lean.Meta.Simp.instInhabitedMethods : Inhabited Lean.Meta.Simp.Methods

Equations

• Lean.Meta.Simp.instInhabitedMethods = { default := { pre := default, post := default, discharge? := default } }

unsafe def Lean.Meta.Simp.Methods.toMethodsRefImpl (m : Lean.Meta.Simp.Methods) : Lean.Meta.Simp.MethodsRef

Equations

• Lean.Meta.Simp.Methods.toMethodsRefImpl m = unsafeCast m

@[implemented_by Lean.Meta.Simp.Methods.toMethodsRefImpl]

opaque Lean.Meta.Simp.Methods.toMethodsRef (m : Lean.Meta.Simp.Methods) : Lean.Meta.Simp.MethodsRef

unsafe def Lean.Meta.Simp.MethodsRef.toMethodsImpl (m : Lean.Meta.Simp.MethodsRef) : Lean.Meta.Simp.Methods

Equations

• Lean.Meta.Simp.MethodsRef.toMethodsImpl m = unsafeCast m

@[implemented_by Lean.Meta.Simp.MethodsRef.toMethodsImpl]

opaque Lean.Meta.Simp.MethodsRef.toMethods (m : Lean.Meta.Simp.MethodsRef) : Lean.Meta.Simp.Methods

def Lean.Meta.Simp.getMethods : Lean.Meta.SimpM Lean.Meta.Simp.Methods

Equations

• Lean.Meta.Simp.getMethods = do let __do_lift ← read pure (Lean.Meta.Simp.MethodsRef.toMethods __do_lift)

def Lean.Meta.Simp.pre (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Step

Equations

• Lean.Meta.Simp.pre e = do let __do_lift ← Lean.Meta.Simp.getMethods __do_lift.pre e

def Lean.Meta.Simp.post (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Step

Equations

• Lean.Meta.Simp.post e = do let __do_lift ← Lean.Meta.Simp.getMethods __do_lift.post e

def Lean.Meta.Simp.discharge? (e : Lean.Expr) : Lean.Meta.SimpM (Option Lean.Expr)

Equations

• Lean.Meta.Simp.discharge? e = do let __do_lift ← Lean.Meta.Simp.getMethods __do_lift.discharge? e

@[inline]

def Lean.Meta.Simp.getContext : Lean.Meta.SimpM Lean.Meta.Simp.Context

Equations

• Lean.Meta.Simp.getContext = readThe Lean.Meta.Simp.Context

def Lean.Meta.Simp.getConfig : Lean.Meta.SimpM Lean.Meta.Simp.Config

Equations

• Lean.Meta.Simp.getConfig = do let __do_lift ← Lean.Meta.Simp.getContext pure __do_lift.config

@[inline]

def Lean.Meta.Simp.withParent {α : Type} (parent : Lean.Expr) (f : Lean.Meta.SimpM α) : Lean.Meta.SimpM α

Equations

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

def Lean.Meta.Simp.getSimpTheorems : Lean.Meta.SimpM Lean.Meta.SimpTheoremsArray

Equations

• Lean.Meta.Simp.getSimpTheorems = do let __do_lift ← readThe Lean.Meta.Simp.Context pure __do_lift.simpTheorems

def Lean.Meta.Simp.getSimpCongrTheorems : Lean.Meta.SimpM Lean.Meta.SimpCongrTheorems

Equations

• Lean.Meta.Simp.getSimpCongrTheorems = do let __do_lift ← readThe Lean.Meta.Simp.Context pure __do_lift.congrTheorems

@[inline]

def Lean.Meta.Simp.savingCache {α : Type} (x : Lean.Meta.SimpM α) : Lean.Meta.SimpM α

Equations

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

@[inline]

def Lean.Meta.Simp.withSimpTheorems {α : Type} (s : Lean.Meta.SimpTheoremsArray) (x : Lean.Meta.SimpM α) : Lean.Meta.SimpM α

Equations

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

@[inline]

def Lean.Meta.Simp.withDischarger {α : Type} (discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)) (x : Lean.Meta.SimpM α) : Lean.Meta.SimpM α

Equations

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

def Lean.Meta.Simp.recordSimpTheorem (thmId : Lean.Meta.Origin) : Lean.Meta.SimpM Unit

Equations

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

def Lean.Meta.Simp.Result.getProof (r : Lean.Meta.Simp.Result) : Lean.MetaM Lean.Expr

Equations

• Lean.Meta.Simp.Result.getProof r = match r.proof? with | some p => pure p | none => Lean.Meta.mkEqRefl r.expr

def Lean.Meta.Simp.Result.getProof' (source : Lean.Expr) (r : Lean.Meta.Simp.Result) : Lean.MetaM Lean.Expr

Similar to Result.getProof, but adds a mkExpectedTypeHint if proof? is none (i.e., result is definitionally equal to input), but we cannot establish that source and r.expr are definitionally when using TransparencyMode.reducible.

Equations

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

def Lean.Meta.Simp.mkCongrFun (r : Lean.Meta.Simp.Result) (a : Lean.Expr) : Lean.MetaM Lean.Meta.Simp.Result

Equations

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

def Lean.Meta.Simp.mkCongr (r₁ : Lean.Meta.Simp.Result) (r₂ : Lean.Meta.Simp.Result) : Lean.MetaM Lean.Meta.Simp.Result

Equations

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

def Lean.Meta.Simp.mkImpCongr (src : Lean.Expr) (r₁ : Lean.Meta.Simp.Result) (r₂ : Lean.Meta.Simp.Result) : Lean.MetaM Lean.Meta.Simp.Result

Equations

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

def Lean.Meta.Simp.removeUnnecessaryCasts (e : Lean.Expr) : Lean.MetaM Lean.Expr

Given the application e, remove unnecessary casts of the form Eq.rec a rfl and Eq.ndrec a rfl.

Equations

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

def Lean.Meta.Simp.removeUnnecessaryCasts.isDummyEqRec (e : Lean.Expr) : Bool

Equations

• Lean.Meta.Simp.removeUnnecessaryCasts.isDummyEqRec e = ((Lean.Expr.isAppOfArity e `Eq.rec 6 || Lean.Expr.isAppOfArity e `Eq.ndrec 6) && Lean.Expr.isAppOf (Lean.Expr.appArg! e) `Eq.refl)

partial def Lean.Meta.Simp.removeUnnecessaryCasts.elimDummyEqRec (e : Lean.Expr) : Lean.Expr

def Lean.Meta.Simp.congrArgs (r : Lean.Meta.Simp.Result) (args : Array Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Result

Given a simplified function result r and arguments args, simplify arguments using simp and dsimp. The resulting proof is built using congr and congrFun theorems.

Equations

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

def Lean.Meta.Simp.mkCongrSimp? (f : Lean.Expr) : Lean.Meta.SimpM (Option Lean.Meta.CongrTheorem)

Retrieve auto-generated congruence lemma for f.

Remark: If all argument kinds are fixed or eq, it returns none because using simple congruence theorems congr, congrArg, and congrFun produces a more compact proof.

Equations

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

def Lean.Meta.Simp.tryAutoCongrTheorem? (e : Lean.Expr) : Lean.Meta.SimpM (Option Lean.Meta.Simp.Result)

Try to use automatically generated congruence theorems. See mkCongrSimp?.

Equations

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

def Lean.Meta.Simp.getDtConfig (cfg : Lean.Meta.Simp.Config) : Lean.Meta.WhnfCoreConfig

Return a WHNF configuration for retrieving [simp] from the discrimination tree. If user has disabled zeta and/or beta reduction in the simplifier, we must also disable them when retrieving lemmas from discrimination tree. See issues: #2669 and #2281

Equations

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

def Lean.Meta.Simp.Result.addExtraArgs (r : Lean.Meta.Simp.Result) (extraArgs : Array Lean.Expr) : Lean.MetaM Lean.Meta.Simp.Result

Equations

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

def Lean.Meta.Simp.Step.addExtraArgs (s : Lean.Meta.Simp.Step) (extraArgs : Array Lean.Expr) : Lean.MetaM Lean.Meta.Simp.Step

Equations

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

def Lean.Meta.applySimpResultToTarget (mvarId : Lean.MVarId) (target : Lean.Expr) (r : Lean.Meta.Simp.Result) : Lean.MetaM Lean.MVarId

Auxiliary method. Given the current target of mvarId, apply r which is a new target and proof that it is equal to the current one.

Equations

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