Tactics that transform types into definitionally equal types #
This module defines a standard wrapper that can be used to create tactics that change hypotheses and the goal to things that are definitionally equal.
It then provides a number of tactics that transform local hypotheses and/or the target.
This is Lean.MVarId.changeLocalDecl
but makes sure to preserve local variable order.
Equations
- One or more equations did not get rendered due to their size.
Instances For
For the main goal, use m
to transform the types of locations specified by loc?
.
If loc?
is none, then transforms the type of target. m
is provided with an expression
with instantiated metavariables as well as, if the location is a local hypothesis, the fvar.
m
must transform expressions to defeq expressions.
If checkDefEq = true
(the default) then runDefEqTactic
will throw an error
if the resulting expression is not definitionally equal to the original expression.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Like Mathlib.Tactic.runDefEqTactic
but for conv
mode.
Equations
- One or more equations did not get rendered due to their size.
Instances For
whnf
#
whnf at loc
puts the given location into weak-head normal form.
This also exists as a conv
-mode tactic.
Weak-head normal form is when the outer-most expression has been fully reduced, the expression may contain subexpressions which have not been reduced.
Equations
- One or more equations did not get rendered due to their size.
Instances For
beta_reduce
#
beta_reduce at loc
completely beta reduces the given location.
This also exists as a conv
-mode tactic.
This means that whenever there is an applied lambda expression such as
(fun x => f x) y
then the argument is substituted into the lambda expression
yielding an expression such as f y
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
beta_reduce at loc
completely beta reduces the given location.
This also exists as a conv
-mode tactic.
This means that whenever there is an applied lambda expression such as
(fun x => f x) y
then the argument is substituted into the lambda expression
yielding an expression such as f y
.
Equations
- Mathlib.Tactic.convBeta_reduce = Lean.ParserDescr.node `Mathlib.Tactic.convBeta_reduce 1024 (Lean.ParserDescr.nonReservedSymbol "beta_reduce" false)
Instances For
reduce
#
reduce at loc
completely reduces the given location.
This also exists as a conv
-mode tactic.
This does the same transformation as the #reduce
command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
refold_let
#
For each fvar, looks for its body in e
and replaces it with the fvar.
Equations
- One or more equations did not get rendered due to their size.
Instances For
refold_let x y z at loc
looks for the bodies of local definitions x
, y
, and z
at the given
location and replaces them with x
, y
, or z
. This is the inverse of "zeta reduction."
This also exists as a conv
-mode tactic.
Equations
- One or more equations did not get rendered due to their size.
Instances For
refold_let x y z at loc
looks for the bodies of local definitions x
, y
, and z
at the given
location and replaces them with x
, y
, or z
. This is the inverse of "zeta reduction."
This also exists as a conv
-mode tactic.
Equations
- One or more equations did not get rendered due to their size.
Instances For
unfold_projs
#
Recursively unfold all the projection applications for class instances.
Equations
- One or more equations did not get rendered due to their size.
Instances For
unfold_projs at loc
unfolds projections of class instances at the given location.
This also exists as a conv
-mode tactic.
Equations
- One or more equations did not get rendered due to their size.
Instances For
unfold_projs at loc
unfolds projections of class instances at the given location.
This also exists as a conv
-mode tactic.
Equations
- Mathlib.Tactic.convUnfold_projs = Lean.ParserDescr.node `Mathlib.Tactic.convUnfold_projs 1024 (Lean.ParserDescr.nonReservedSymbol "unfold_projs" false)
Instances For
eta_reduce
#
Eta reduce everything
Equations
- One or more equations did not get rendered due to their size.
Instances For
eta_reduce at loc
eta reduces all sub-expressions at the given location.
This also exists as a conv
-mode tactic.
For example, fun x y => f x y
becomes f
after eta reduction.
Equations
- One or more equations did not get rendered due to their size.
Instances For
eta_reduce at loc
eta reduces all sub-expressions at the given location.
This also exists as a conv
-mode tactic.
For example, fun x y => f x y
becomes f
after eta reduction.
Equations
- Mathlib.Tactic.convEta_reduce = Lean.ParserDescr.node `Mathlib.Tactic.convEta_reduce 1024 (Lean.ParserDescr.nonReservedSymbol "eta_reduce" false)
Instances For
eta_expand
#
Eta expand every sub-expression in the given expression.
As a side-effect, beta reduces any pre-existing instances of eta expanded terms.
eta_expand at loc
eta expands all sub-expressions at the given location.
It also beta reduces any applications of eta expanded terms, so it puts it
into an eta-expanded "normal form."
This also exists as a conv
-mode tactic.
For example, if f
takes two arguments, then f
becomes fun x y => f x y
and f x
becomes fun y => f x y
.
This can be useful to turn, for example, a raw HAdd.hAdd
into fun x y => x + y
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
eta_expand at loc
eta expands all sub-expressions at the given location.
It also beta reduces any applications of eta expanded terms, so it puts it
into an eta-expanded "normal form."
This also exists as a conv
-mode tactic.
For example, if f
takes two arguments, then f
becomes fun x y => f x y
and f x
becomes fun y => f x y
.
This can be useful to turn, for example, a raw HAdd.hAdd
into fun x y => x + y
.
Equations
- Mathlib.Tactic.convEta_expand = Lean.ParserDescr.node `Mathlib.Tactic.convEta_expand 1024 (Lean.ParserDescr.nonReservedSymbol "eta_expand" false)
Instances For
eta_struct
#
Given an expression that's either a native projection or a registered projection function, gives (1) the name of the structure type, (2) the index of the projection, and (3) the object being projected.
Equations
- One or more equations did not get rendered due to their size.
- Mathlib.Tactic.getProjectedExpr (Lean.Expr.proj S i x) = pure (some (S, i, x))
Instances For
Checks if the expression is of the form S.mk x.1 ... x.n
with n
nonzero
and S.mk
a structure constructor and returns x
.
Each projection x.i
can be either a native projection or from a projection function.
tryWhnfR
controls whether to try applying whnfR
to arguments when none of them
are obviously projections.
Once an obviously correct projection is found, relies on the structure eta rule in isDefEq
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Check to see if there's an argument at some index i
such that it's the i
th projection of a some expression.
Returns the expression.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Finds all occurrences of expressions of the form S.mk x.1 ... x.n
where S.mk
is a structure constructor and replaces them by x
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
eta_struct at loc
transforms structure constructor applications such as S.mk x.1 ... x.n
(pretty printed as, for example, {a := x.a, b := x.b, ...}
) into x
.
This also exists as a conv
-mode tactic.
The transformation is known as eta reduction for structures, and it yields definitionally equal expressions.
For example, given x : α × β
, then (x.1, x.2)
becomes x
after this transformation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
eta_struct at loc
transforms structure constructor applications such as S.mk x.1 ... x.n
(pretty printed as, for example, {a := x.a, b := x.b, ...}
) into x
.
This also exists as a conv
-mode tactic.
The transformation is known as eta reduction for structures, and it yields definitionally equal expressions.
For example, given x : α × β
, then (x.1, x.2)
becomes x
after this transformation.
Equations
- Mathlib.Tactic.convEta_struct = Lean.ParserDescr.node `Mathlib.Tactic.convEta_struct 1024 (Lean.ParserDescr.nonReservedSymbol "eta_struct" false)