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.

def Mathlib.Tactic.runDefEqTactic (m : Lean.Expr → Lean.MetaM Lean.Expr) (loc? : Option (Lean.TSyntax `Lean.Parser.Tactic.location)) (tacticName : String) (checkDefEq : optParam Bool true) : Lean.Elab.Tactic.TacticM Unit

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.

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.

def Mathlib.Tactic.runDefEqConvTactic (m : Lean.Expr → Lean.MetaM Lean.Expr) : Lean.Elab.Tactic.TacticM Unit

Like Mathlib.Tactic.runDefEqTactic but for conv mode.

whnf

def Mathlib.Tactic.tacticWhnf__ : Lean.ParserDescr

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.

beta_reduce

def Mathlib.Tactic.betaReduceStx : Lean.ParserDescr

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.

def Mathlib.Tactic.convBeta_reduce : Lean.ParserDescr

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.

reduce

def Mathlib.Tactic.tacticReduce__ : Lean.ParserDescr

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.

unfold_let

def Mathlib.Tactic.unfoldFVars (fvars : Array Lean.FVarId) (e : Lean.Expr) : Lean.MetaM Lean.Expr

Unfold all the fvars from fvars in e that have local definitions (are "let-bound").

def Mathlib.Tactic.unfoldLetStx : Lean.ParserDescr

unfold_let x y z at loc unfolds the local definitions x, y, and z at the given location, which is known as "zeta reduction." This also exists as a conv-mode tactic.

If no local definitions are given, then all local definitions are unfolded. This variant also exists as the conv-mode tactic zeta.

This is similar to the unfold tactic, which instead is for unfolding global definitions.

def Mathlib.Tactic.convUnfold_let___ : Lean.ParserDescr

unfold_let x y z at loc unfolds the local definitions x, y, and z at the given location, which is known as "zeta reduction." This also exists as a conv-mode tactic.

If no local definitions are given, then all local definitions are unfolded. This variant also exists as the conv-mode tactic zeta.

This is similar to the unfold tactic, which instead is for unfolding global definitions.

unfold_projs

def Mathlib.Tactic.unfoldProjs (e : Lean.Expr) : Lean.MetaM Lean.Expr

Recursively unfold all the projection applications for class instances.

def Mathlib.Tactic.unfoldProjsStx : Lean.ParserDescr

unfold_projs at loc unfolds projections of class instances at the given location. This also exists as a conv-mode tactic.

def Mathlib.Tactic.convUnfold_projs : Lean.ParserDescr

unfold_projs at loc unfolds projections of class instances at the given location. This also exists as a conv-mode tactic.

eta_reduce

def Mathlib.Tactic.etaReduceAll (e : Lean.Expr) : Lean.MetaM Lean.Expr

Eta reduce everything

def Mathlib.Tactic.etaReduceStx : Lean.ParserDescr

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.

def Mathlib.Tactic.convEta_reduce : Lean.ParserDescr

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.

eta_expand

partial def Mathlib.Tactic.etaExpandAll (e : Lean.Expr) : Lean.MetaM Lean.Expr

Eta expand every sub-expression in the given expression.

As a side-effect, beta reduces any pre-existing instances of eta expanded terms.

def Mathlib.Tactic.etaExpandStx : Lean.ParserDescr

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.

def Mathlib.Tactic.convEta_expand : Lean.ParserDescr

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.

eta_struct

def Mathlib.Tactic.getProjectedExpr (e : Lean.Expr) : Lean.MetaM (Option (Lean.Name × Nat × Lean.Expr))

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.

def Mathlib.Tactic.etaStruct? (e : Lean.Expr) (tryWhnfR : optParam Bool true) : Lean.MetaM (Option Lean.Expr)

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.

def Mathlib.Tactic.etaStruct?.findProj (fVal : Lean.ConstructorVal) (args : Array Lean.Expr) (m : Lean.Expr → Lean.MetaM Lean.Expr) : Lean.MetaM (Lean.LOption Lean.Expr)

Check to see if there's an argument at some index i such that it's the ith projection of a some expression. Returns the expression.

def Mathlib.Tactic.etaStructAll (e : Lean.Expr) : Lean.MetaM Lean.Expr

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.

def Mathlib.Tactic.etaStructStx : Lean.ParserDescr

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.

def Mathlib.Tactic.convEta_struct : Lean.ParserDescr

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.