# Documentation

## Lean.Meta.Tactic.Simp.Types

The result of simplifying some expression e.

• expr : Lean.Expr

The simplified version of e

• proof? :

A proof that $e =$expr, where the simplified expression is on the RHS. If none, the proof is assumed to be refl.

• cache : Bool

If cache := true the result is cached. Warning: we will remove this field in the future. It is currently used by arith := true, but we can now refactor the code to avoid the hack.

Instances For
Equations
Equations
• One or more equations did not get rendered due to their size.
• = pure { expr := r.expr, proof? := r.proof?, cache := false }
Instances For
Equations
Instances For

Flip the proof in a Simp.Result.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Equations
Instances For
• maxDischargeDepth : UInt32

maxDischargeDepth from config as an UInt32.

• parent? :

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)


... |- 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
• lctxInitIndices : Nat

Number of indices in the local context when starting simp. We use this information to decide which assumptions we can use without invalidating the cache.

• inDSimp : Bool

If inDSimp := true, then simp is in dsimp mode, and only applying transformations that presereve definitional equality.

Instances For
Equations
• One or more equations did not get rendered due to their size.
Equations
• ctx.isDeclToUnfold declName = ctx.simpTheorems.isDeclToUnfold declName
Instances For
Instances For
Equations
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• s.toArray = Array.map (fun (x : ) => x.fst) (.qsort fun (x1 x2 : ) => decide (x1.snd < x2.snd))
Instances For
• usedThmCounter :

Number of times each simp theorem has been used/applied.

• triedThmCounter :

Number of times each simp theorem has been tried.

• congrThmCounter :

Number of times each congr theorem has been tried.

When using Simp.Config.index := false, and set_option diagnostics true, for every theorem used by simp, we check whether the theorem would be also applied if index := true, and we store it here if it would not have been tried.

Instances For
Equations
Instances For
Instances For
Equations
@[reducible, inline]
Equations
Instances For
@[extern lean_simp]
@[extern lean_dsimp]
@[inline]
Equations
• One or more equations did not get rendered due to their size.
Instances For

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

• done:

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

For post procedures, it returns the result.

• visit:

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:

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

For post procedures, this is equivalent to returning visit.

Instances For
@[reducible, inline]

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

Equations
Instances For
@[reducible, inline]
Equations
Instances For
@[reducible, inline]

Similar to Simproc, but resulting expression should be definitionally equal to the input one.

Equations
Instances For
Equations
Instances For
Equations
Instances For
@[always_inline]

"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.
Instances For
Equations
@[always_inline]
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations

Simproc .olean entry.

• declName : Lake.Name

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

• post : Bool
Instances For
Equations

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

• declName : Lake.Name
• post : Bool
• 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.

Instances For
@[reducible, inline]
Equations
Instances For
• simprocNames :
• erased :
Instances For
Equations
• discharge? :
• wellBehavedDischarge : Bool

wellBehavedDischarge must not be set to true IF discharge? access local declarations with index >= Context.lctxInitIndices when contextual := false. Reason: it would prevent us from aggressively caching simp results.

Instances For
Equations
Instances For
@[implemented_by Lean.Meta.Simp.Methods.toMethodsRefImpl]
Instances For
@[implemented_by Lean.Meta.Simp.MethodsRef.toMethodsImpl]
Equations
Instances For
Equations
Instances For
Equations
Instances For
@[inline]
Equations
Instances For
Equations
Instances For
@[inline]
def Lean.Meta.Simp.withParent {α : Type} (parent : Lean.Expr) (f : ) :
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
Instances For

Returns true if simp is in dsimp mode. That is, only transformations that preserve definitional equality should be applied.

Equations
Instances For
@[inline]
Equations
• One or more equations did not get rendered due to their size.
Instances For
@[inline]

Save current cache, reset it, execute x, and then restore original cache.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[inline]
def Lean.Meta.Simp.withDischarger {α : Type} (discharge? : ) (wellBehavedDischarge : Bool) (x : ) :
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For

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.
Instances For

Construct the Expr cast h e, from a Simp.Result with proof h.

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

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.
Instances For
Equations
• = ((e.isAppOfArity Eq.rec 6 || e.isAppOfArity Eq.ndrec 6) && e.appArg!.isAppOf Eq.refl)
Instances For

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.
Instances For

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.
Instances For

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

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

Return a WHNF configuration for retrieving [simp] from the discrimination tree. If user has disabled zeta and/or beta reduction in the simplifier, or enabled zetaDelta, we must also disable/enable 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.
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For

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.
Instances For