Equations
Instances For
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)
Instances For
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.
Instances For
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)
Instances For
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)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Meta.Simp.simpConst e = do let __do_lift ← Lean.Meta.Simp.reduce✝ e pure { expr := __do_lift }
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
Information about a single have
in a have
telescope.
Created by getHaveTelescopeInfo
.
- typeBackDeps : Std.HashSet Nat
Previous
have
s that the type of thishave
depends on, as indices intoHaveTelescopeInfo.haveInfo
. Used incomputeFixedUsed
to compute usedhave
s. - valueBackDeps : Std.HashSet Nat
Previous
have
s that the value of thishave
depends on, as indices intoHaveTelescopeInfo.haveInfo
. Used incomputeFixedUsed
to compute usedhave
s. - decl : LocalDecl
- level : Level
The level of the type for this
have
, cached.
Instances For
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 have
s in computeFixedUsed
.
In have x₁ := v; have x₂ := x₁; ⋯; have xₙ := xₙ₋₁; b
, if xₙ
is unused in b
, then all the
have
s are unused. Without a global computation of used have
s, the proof term would be quadratic
in the number of have
s (with n
iterations of simp
). Knowing which have
s are transitively
unused lets the proof term be linear in size.
Information about each
have
in the telescope.- bodyDeps : Std.HashSet Nat
The set of
have
s that the body depends on, as indices intohaveInfo
. Used incomputeFixedUsed
to compute usedhave
s. - bodyTypeDeps : Std.HashSet Nat
- 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.
Instances For
Equations
- One or more equations did not get rendered due to their size.
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 #[]
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Computes which have
s in the telescope are fixed and which are unused.
The length of the unused array may be less than the number of have
s: use unused.getD i true
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 have
s can be eliminated, which we do if cfg.zetaUnused
is true.
We clear have
s from the end, to be able to transitively clear chains of unused have
s.
This is why we honor zetaUnused
here even though reduceStep
is also responsible for it;
reduceStep
can only eliminate unused have
s at the start of a telescope.
Eliminating all transitively unused have
s 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.
- 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
.) - 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.
Instances For
Instances For
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 let
s 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 dsimp
ed.
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
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.
Instances For
Try to rewrite e
children using the given congruence theorem
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
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" 995 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 }
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
- 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))
Instances For
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))
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
See simpTarget
. This method assumes mvarId
is not assigned, and we are already using mvarId
s local context.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Instances For
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 mvarId
s local context.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Meta.applySimpResultToProp mvarId proof prop r mayCloseGoal = Lean.Meta.applySimpResult mvarId proof prop r mayCloseGoal
Instances For
Equations
- Lean.Meta.applySimpResultToFVarId mvarId fvarId r mayCloseGoal = do let localDecl ← fvarId.getDecl Lean.Meta.applySimpResult mvarId (Lean.mkFVar fvarId) localDecl.type r mayCloseGoal
Instances For
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 mvarId
s local context.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 mvarId
s local context.
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.