Return true if e is of the form ofNat n where n is a kernel Nat literal
Equations
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
Instances For
Return true if e is of the form ofScientific n b m where n and m are kernel Nat literals.
Equations
Instances For
Return true if e is of the form Char.ofNat n where n is a kernel Nat literals.
Equations
Instances For
Information about a single have in a have telescope.
Created by getHaveTelescopeInfo.
- typeBackDeps : Std.HashSet Nat
Previous
haves that the type of thishavedepends on, as indices intoHaveTelescopeInfo.haveInfo. Used incomputeFixedUsedto compute usedhaves. - valueBackDeps : Std.HashSet Nat
Previous
haves that the value of thishavedepends on, as indices intoHaveTelescopeInfo.haveInfo. Used incomputeFixedUsedto compute usedhaves. - 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 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.
Information about each
havein the telescope.- bodyDeps : Std.HashSet Nat
The set of
haves that the body depends on, as indices intohaveInfo. Used incomputeFixedUsedto compute usedhaves. - 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
haveexpression, cached.
Instances For
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
Instances For
Equations
Instances For
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
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 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.
- 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
Instances For
Equations
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 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
Instances For
Process the given congruence theorem hypothesis. Return true if it made "progress".
Equations
Instances For
Try to rewrite e children using the given congruence theorem
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
See simpTarget. This method assumes mvarId is not assigned, and we are already using mvarIds local context.
Equations
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
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 mvarIds local context.
Equations
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 mvarIds local context.
Equations
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 mvarIds local context.