opaque Lean.Meta.Simp.backward.dsimp.proofs : Lean.Option Bool

opaque Lean.Meta.Simp.debug.simp.check.have : Lean.Option Bool

opaque Lean.Meta.Simp.congrHypothesisExceptionId : InternalExceptionId

def Lean.Meta.Simp.throwCongrHypothesisFailed {α : Type} : MetaM α

Equations

• Lean.Meta.Simp.throwCongrHypothesisFailed = throw (Lean.Exception.internal Lean.Meta.Simp.congrHypothesisExceptionId)

def Lean.Meta.Simp.isOfNatNatLit (e : Expr) : Bool

Return true if e is of the form ofNat n where n is a kernel Nat literal

Equations

• Lean.Meta.Simp.isOfNatNatLit e = (e.isAppOf `OfNat.ofNat && decide (e.getAppNumArgs ≥ 3) && (e.getArg! 1).isRawNatLit)

def Lean.Meta.Simp.foldRawNatLit (e : Expr) : SimpM Expr

If e is a raw Nat literal and OfNat.ofNat is not in the list of declarations to unfold, return an OfNat.ofNat-application.

Equations

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

def Lean.Meta.Simp.isOfScientificLit (e : Expr) : Bool

Return true if e is of the form ofScientific n b m where n and m are kernel Nat literals.

Equations

• Lean.Meta.Simp.isOfScientificLit e = (e.isAppOfArity `OfScientific.ofScientific 5 && (e.getArg! 4).isRawNatLit && (e.getArg! 2).isRawNatLit)

def Lean.Meta.Simp.isCharLit (e : Expr) : Bool

Return true if e is of the form Char.ofNat n where n is a kernel Nat literals.

Equations

• Lean.Meta.Simp.isCharLit e = (e.isAppOfArity `Char.ofNat 1 && e.appArg!.isRawNatLit)

instance Lean.Meta.Simp.instInhabitedSimpM {α : Type} : Inhabited (SimpM α)

Equations

• Lean.Meta.Simp.instInhabitedSimpM = { default := fun (x : Lean.Meta.Simp.MethodsRef) (x : Lean.Meta.Simp.Context) (x : ST.Ref IO.RealWorld Lean.Meta.Simp.State) => default }

def Lean.Meta.Simp.lambdaTelescopeDSimp {α : Type} (e : Expr) (k : Array Expr → Expr → SimpM α) : SimpM α

Equations

• Lean.Meta.Simp.lambdaTelescopeDSimp e k = Lean.Meta.Simp.lambdaTelescopeDSimp.go✝ k #[] e

def Lean.Meta.Simp.withNewLemmas {α : Type} (xs : Array Expr) (f : SimpM α) : SimpM α

We use withNewLemmas whenever updating the local context.

Equations

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

def Lean.Meta.Simp.simpProj (e : Expr) : SimpM Result

Equations

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

def Lean.Meta.Simp.simpConst (e : Expr) : SimpM Result

Equations

• Lean.Meta.Simp.simpConst e = do let __do_lift ← Lean.Meta.Simp.reduce✝ e pure { expr := __do_lift }

def Lean.Meta.Simp.simpLambda (e : Expr) : SimpM Result

Equations

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

def Lean.Meta.Simp.simpArrow (e : Expr) : SimpM Result

Equations

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

def Lean.Meta.Simp.simpForall (e : Expr) : SimpM Result

Equations

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

structure Lean.Meta.Simp.HaveInfo : Type

Information about a single have in a have telescope. Created by getHaveTelescopeInfo.

• typeBackDeps : Std.HashSet Nat

  Previous haves that the type of this have depends on, as indices into HaveTelescopeInfo.haveInfo. Used in computeFixedUsed to compute used haves.

• valueBackDeps : Std.HashSet Nat

  Previous haves that the value of this have depends on, as indices into HaveTelescopeInfo.haveInfo. Used in computeFixedUsed to compute used haves.

• decl : LocalDecl

  The local decl for the have, so that the local context can be re-entered have-by-have. N.B. This stores the fvarid for the have as well as cached versions of the value and type instantiated with the fvars from the telescope.

• level : Level

  The level of the type for this have, cached.

instance Lean.Meta.Simp.instInhabitedHaveInfo : Inhabited HaveInfo

Equations

• Lean.Meta.Simp.instInhabitedHaveInfo = { default := Lean.Meta.Simp.instInhabitedHaveInfo.default }

def Lean.Meta.Simp.instInhabitedHaveInfo.default : HaveInfo

Equations

• Lean.Meta.Simp.instInhabitedHaveInfo.default = { typeBackDeps := default, valueBackDeps := default, decl := default, level := default }

structure Lean.Meta.Simp.HaveTelescopeInfo : Type

Information about a have telescope. Created by getHaveTelescopeInfo and used in simpHaveTelescope.

The data is used to avoid applying Expr.abstract more than once on any given subexpression when constructing terms and proofs during simplification. Abstraction is linear in the size t of a term, and so in a depth-n telescope it is O(nt), quadratic in n, since n ≤ t. For example, given have x₁ := v₁; ...; have xₙ := vₙ; b and h : b = b', we need to construct

have_body_congr (fun x₁ => ... have_body_congr (fun xₙ => h)))

We apply Expr.abstract to h once and then build the term, rather than using mkLambdaFVars #[fvarᵢ] pfᵢ at each step.

As an additional optimization, we save the fvar-instantiated terms calculated by getHaveTelescopeInfo so that we don't have to compute them again. This is only saving a constant factor.

It is also used for computing used haves in computeFixedUsed. In have x₁ := v; have x₂ := x₁; ⋯; have xₙ := xₙ₋₁; b, if xₙ is unused in b, then all the haves are unused. Without a global computation of used haves, the proof term would be quadratic in the number of haves (with n iterations of simp). Knowing which haves are transitively unused lets the proof term be linear in size.

• haveInfo : Array HaveInfo

  Information about each have in the telescope.

• bodyDeps : Std.HashSet Nat

  The set of haves that the body depends on, as indices into haveInfo. Used in computeFixedUsed to compute used haves.

• bodyTypeDeps : Std.HashSet Nat

  The set of haves that the type of the body depends on, as indices into haveInfo. This is the set of fixed haves.

• body : Expr

  A cached version of the telescope body, instantiated with fvars from each HaveInfo.decl.

• bodyType : Expr

  A cached version of the telescope body's type, instantiated with fvars from each HaveInfo.decl.

• level : Level

  The universe level for the have expression, cached.

instance Lean.Meta.Simp.instInhabitedHaveTelescopeInfo : Inhabited HaveTelescopeInfo

Equations

• Lean.Meta.Simp.instInhabitedHaveTelescopeInfo = { default := Lean.Meta.Simp.instInhabitedHaveTelescopeInfo.default }

def Lean.Meta.Simp.instInhabitedHaveTelescopeInfo.default : HaveTelescopeInfo

Equations

• Lean.Meta.Simp.instInhabitedHaveTelescopeInfo.default = { haveInfo := default, bodyDeps := default, bodyTypeDeps := default, body := default, bodyType := default, level := default }

def Lean.Meta.Simp.getHaveTelescopeInfo (e : Expr) : MetaM HaveTelescopeInfo

Efficiently collect dependency information for a have telescope. This is part of a scheme to avoid quadratic overhead from the locally nameless discipline (see HaveTelescopeInfo and simpHaveTelescope).

The expression e must not have loose bvars.

Equations

• Lean.Meta.Simp.getHaveTelescopeInfo e = do let __do_lift ← Lean.getLCtx Lean.Meta.Simp.getHaveTelescopeInfo.collect✝ e 0 { } __do_lift #[]

def Lean.Meta.Simp.HaveTelescopeInfo.computeFixedUsed (info : HaveTelescopeInfo) (keepUnused : Bool) : MetaM (Std.HashSet Nat × Array Bool)

Computes which haves in the telescope are fixed and which are unused. The length of the unused array may be less than the number of haves: use unused.getD i true.

Equations

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

def Lean.Meta.Simp.simpHaveTelescope (e : Expr) : SimpM Result

Routine for simplifying have telescopes. Used by simpLet. This is optimized to be able to handle deep have telescopes while avoiding quadratic complexity arising from the locally nameless expression representations.

Overview

Consider a have telescope:

have x₁ : T₁ := v₁; ...; have xₙ : Tₙ := vₙ; b

We say xᵢ is fixed if it appears in the type of b. If xᵢ is fixed, then it can only be rewritten using definitional equalities. Otherwise, we can freely rewrite the value using a propositional equality vᵢ = vᵢ'. The body b can always be freely rewritten using a propositional equality b = b'. (All the mentioned equalities must be type correct with respect to the obvious local contexts.)

If xᵢ neither appears in b nor any Tⱼ nor any vⱼ, then its have is unused. Unused haves can be eliminated, which we do if cfg.zetaUnused is true. We clear haves from the end, to be able to transitively clear chains of unused haves. This is why we honor zetaUnused here even though reduceStep is also responsible for it; reduceStep can only eliminate unused haves at the start of a telescope. Eliminating all transitively unused haves at once like this also avoids quadratic complexity.

If debug.simp.check.have is enabled then we typecheck the resulting expression and proof.

Proof generation

There are two main complications with generating proofs.

1. We work almost exclusively with expressions with loose bound variables, to avoid overhead from instantiating and abstracting free variables, which can lead to complexity quadratic in the telescope length. (See HaveTelescopeInfo.)
2. We want to avoid triggering zeta reductions in the kernel.

Regarding this second point, the issue is that we cannot organize the proof using congruence theorems in the obvious way. For example, given

theorem have_congr {α : Sort u} {β : Sort v} {a a' : α} {f f' : α → β}
    (h₁ : a = a') (h₂ : ∀ x, f x = f' x) :
    (have x := a; f x) = (have x := a'; f' x)

the kernel sees that the type of have_congr (fun x => b) (fun x => b') h₁ h₂ is (have x := a; (fun x => b) x) = (have x := a'; (fun x => b') x), since when instantiating values it does not beta reduce at the same time. Hence, when is_def_eq is applied to the LHS and have x := a; b for example, it will do whnf_core to both sides.

Instead, we use the form (fun x => b) a = (fun x => b') a' in the proofs, which we can reliably match up without triggering beta reductions in the kernel. The zeta/beta reductions are then limited to the type hint for the entire telescope, when we convert this back into have form. In the base case, we include an optimization to avoid unnecessary zeta/beta reductions, by detecting a simpHaveTelescope proofs and removing the type hint.

Equations

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

def Lean.Meta.Simp.simpLet (e : Expr) : SimpM Result

Routine for simplifying let expressions.

If it is a have, we use simpHaveTelescope to simplify entire telescopes at once, to avoid quadratic behavior arising from locally nameless expression representations.

We assume that dependent lets are dependent, but if Config.letToHave is enabled then we attempt to transform it into a have. If that does not change it, then it is only dsimped.

Equations

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

def Lean.Meta.Simp.visitFn (e : Expr) : SimpM Result

Equations

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

def Lean.Meta.Simp.congrDefault (e : Expr) : SimpM Result

Equations

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

def Lean.Meta.Simp.processCongrHypothesis (h hType : Expr) : SimpM Bool

Process the given congruence theorem hypothesis. Return true if it made "progress".

Equations

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

def Lean.Meta.Simp.trySimpCongrTheorem? (c : SimpCongrTheorem) (e : Expr) : SimpM (Option Result)

Try to rewrite e children using the given congruence theorem

Equations

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

def Lean.Meta.Simp.congr (e : Expr) : SimpM Result

Equations

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

def Lean.Meta.Simp.simpApp (e : Expr) : SimpM Result

Equations

• Lean.Meta.Simp.simpApp e = if (Lean.Meta.Simp.isOfNatNatLit e || Lean.Meta.Simp.isOfScientificLit e || Lean.Meta.Simp.isCharLit e) = true then pure { expr := e } else Lean.Meta.Simp.congr e

def Lean.Meta.Simp.simpStep (e : Expr) : SimpM Result

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Simp.simpStep (Lean.Expr.mdata m e_2) = do let r ← Lean.Meta.Simp.simp e_2 pure { expr := Lean.mkMData m r.expr, proof? := r.proof?, cache := r.cache }
• Lean.Meta.Simp.simpStep (Lean.Expr.proj typeName idx struct) = Lean.Meta.Simp.simpProj (Lean.Expr.proj typeName idx struct)
• Lean.Meta.Simp.simpStep (fn.app arg) = Lean.Meta.Simp.simpApp (fn.app arg)
• Lean.Meta.Simp.simpStep (Lean.Expr.lam binderName binderType body binderInfo) = Lean.Meta.Simp.simpLambda (Lean.Expr.lam binderName binderType body binderInfo)
• Lean.Meta.Simp.simpStep (Lean.Expr.forallE binderName binderType body binderInfo) = Lean.Meta.Simp.simpForall (Lean.Expr.forallE binderName binderType body binderInfo)
• Lean.Meta.Simp.simpStep (Lean.Expr.letE declName type value body nondep) = Lean.Meta.Simp.simpLet (Lean.Expr.letE declName type value body nondep)
• Lean.Meta.Simp.simpStep (Lean.Expr.const declName us) = Lean.Meta.Simp.simpConst (Lean.Expr.const declName us)
• Lean.Meta.Simp.simpStep (Lean.Expr.bvar deBruijnIndex) = panicWithPosWithDecl "Lean.Meta.Tactic.Simp.Main" "Lean.Meta.Simp.simpStep" 1000 20 "unreachable code has been reached"
• Lean.Meta.Simp.simpStep (Lean.Expr.sort u) = pure { expr := Lean.Expr.sort u }
• Lean.Meta.Simp.simpStep (Lean.Expr.lit a) = pure { expr := Lean.Expr.lit a }
• Lean.Meta.Simp.simpStep (Lean.Expr.mvar mvarId) = do let __do_lift ← Lean.instantiateMVars (Lean.Expr.mvar mvarId) pure { expr := __do_lift }

def Lean.Meta.Simp.cacheResult (e : Expr) (cfg : Config) (r : Result) : SimpM Result

Equations

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

partial def Lean.Meta.Simp.simpLoop (e : Expr) : SimpM Result

@[export lean_simp]

def Lean.Meta.Simp.simpImpl (e : Expr) : SimpM Result

Equations

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

@[inline]

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

Equations

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

def Lean.Meta.Simp.mainCore (e : Expr) (ctx : Context) (s : State := { }) (methods : Methods := { }) : MetaM (Result × State)

Equations

• Lean.Meta.Simp.mainCore e ctx s methods = Lean.Meta.Simp.SimpM.run ctx s methods (Lean.Meta.Simp.withCatchingRuntimeEx (Lean.Meta.Simp.simp e))

def Lean.Meta.Simp.main (e : Expr) (ctx : Context) (stats : Stats := { }) (methods : Methods := { }) : MetaM (Result × Stats)

Equations

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

def Lean.Meta.Simp.dsimpMainCore (e : Expr) (ctx : Context) (s : State := { }) (methods : Methods := { }) : MetaM (Expr × State)

Equations

• Lean.Meta.Simp.dsimpMainCore e ctx s methods = Lean.Meta.Simp.SimpM.run ctx s methods (Lean.Meta.Simp.withCatchingRuntimeEx (Lean.Meta.Simp.dsimp e))

def Lean.Meta.Simp.dsimpMain (e : Expr) (ctx : Context) (stats : Stats := { }) (methods : Methods := { }) : MetaM (Expr × Stats)

Equations

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

def Lean.Meta.simpCore (e : Expr) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none) (s : Simp.State := { }) : MetaM (Simp.Result × Simp.State)

Equations

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

def Lean.Meta.simp (e : Expr) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none) (stats : Simp.Stats := { }) : MetaM (Simp.Result × Simp.Stats)

Equations

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

def Lean.Meta.dsimp (e : Expr) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (stats : Simp.Stats := { }) : MetaM (Expr × Simp.Stats)

Equations

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

def Lean.Meta.simpTargetCore (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none) (mayCloseGoal : Bool := true) (stats : Simp.Stats := { }) : MetaM (Option MVarId × Simp.Stats)

See simpTarget. This method assumes mvarId is not assigned, and we are already using mvarIds local context.

Equations

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

def Lean.Meta.simpTarget (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none) (mayCloseGoal : Bool := true) (stats : Simp.Stats := { }) : MetaM (Option MVarId × Simp.Stats)

Simplify the given goal target (aka type). Return none if the goal was closed. Return some mvarId' otherwise, where mvarId' is the simplified new goal.

Equations

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

def Lean.Meta.applySimpResult (mvarId : MVarId) (val type : Expr) (r : Simp.Result) (mayCloseGoal : Bool := true) : MetaM (Option (Expr × Expr))

Applies the result r for type (which is inhabited by val). Returns none if the goal was closed. Returns some (val', type') otherwise, where val' : type' and type' is the simplified type.

This method assumes mvarId is not assigned, and we are already using mvarIds local context.

Equations

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

@[deprecated Lean.Meta.applySimpResult (since := "2025-03-26")]

def Lean.Meta.applySimpResultToProp (mvarId : MVarId) (proof prop : Expr) (r : Simp.Result) (mayCloseGoal : Bool := true) : MetaM (Option (Expr × Expr))

Equations

• Lean.Meta.applySimpResultToProp mvarId proof prop r mayCloseGoal = Lean.Meta.applySimpResult mvarId proof prop r mayCloseGoal

def Lean.Meta.applySimpResultToFVarId (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Result) (mayCloseGoal : Bool) : MetaM (Option (Expr × Expr))

Equations

• Lean.Meta.applySimpResultToFVarId mvarId fvarId r mayCloseGoal = do let localDecl ← fvarId.getDecl Lean.Meta.applySimpResult mvarId (Lean.mkFVar fvarId) localDecl.type r mayCloseGoal

def Lean.Meta.simpStep (mvarId : MVarId) (proof prop : Expr) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none) (mayCloseGoal : Bool := true) (stats : Simp.Stats := { }) : MetaM (Option (Expr × Expr) × Simp.Stats)

Simplify prop (which is inhabited by proof). Return none if the goal was closed. Return some (proof', prop') otherwise, where proof' : prop' and prop' is the simplified prop.

This method assumes mvarId is not assigned, and we are already using mvarIds local context.

Equations

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

def Lean.Meta.applySimpResultToLocalDeclCore (mvarId : MVarId) (fvarId : FVarId) (r : Option (Expr × Expr)) : MetaM (Option (FVarId × MVarId))

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.applySimpResultToLocalDeclCore mvarId fvarId none = pure none

def Lean.Meta.applySimpResultToLocalDecl (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Result) (mayCloseGoal : Bool) : MetaM (Option (FVarId × MVarId))

Simplify simp result to the given local declaration. Return none if the goal was closed. This method assumes mvarId is not assigned, and we are already using mvarIds local context.

Equations

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

def Lean.Meta.simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none) (mayCloseGoal : Bool := true) (stats : Simp.Stats := { }) : MetaM (Option (FVarId × MVarId) × Simp.Stats)

Equations

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

def Lean.Meta.simpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[]) (stats : Simp.Stats := { }) : MetaM (Option (Array FVarId × MVarId) × Simp.Stats)

Equations

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

def Lean.Meta.simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none) (stats : Simp.Stats := { }) : MetaM (TacticResultCNM × Simp.Stats)

Equations

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

def Lean.Meta.dsimpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[]) (stats : Simp.Stats := { }) : MetaM (Option MVarId × Simp.Stats)

Equations

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