The norm_cast family of tactics.

A full description of the tactic, and the use of each theorem category, can be found at https://arxiv.org/abs/2001.10594.

def Lean.Elab.Tactic.NormCast.proveEqUsing (s : Meta.SimpTheorems) (a b : Expr) : MetaM (Option Meta.Simp.Result)

Proves a = b using the given simp set.

def Lean.Elab.Tactic.NormCast.proveEqUsingDown (a b : Expr) : MetaM (Option Meta.Simp.Result)

Proves a = b by simplifying using move and squash lemmas.

def Lean.Elab.Tactic.NormCast.mkCoe (e ty : Expr) : MetaM Expr

Constructs the expression (e : ty).

def Lean.Elab.Tactic.NormCast.isCoeOf? (e : Expr) : MetaM (Option Expr)

Checks whether an expression is the coercion of some other expression, and if so returns that expression.

def Lean.Elab.Tactic.NormCast.isNumeral? (e : Expr) : Option (Expr × Nat)

Checks whether an expression is a numeral in some type, and if so returns that type and the natural number.

def Lean.Elab.Tactic.NormCast.splittingProcedure (expr : Expr) : MetaM Meta.Simp.Result

This is the main heuristic used alongside the elim and move lemmas. The goal is to help casts move past operators by adding intermediate casts. An expression of the shape:

op (↑(x : α) : γ) (↑(y : β) : γ)

is rewritten to:

op (↑(↑(x : α) : β) : γ) (↑(y : β) : γ)

when

(↑(↑(x : α) : β) : γ) = (↑(x : α) : γ)

can be proven with a squash lemma

def Lean.Elab.Tactic.NormCast.prove (e : Expr) : Meta.SimpM (Option Expr)

Discharging function used during simplification in the "squash" step.

def Lean.Elab.Tactic.NormCast.upwardAndElim (up : Meta.SimpTheorems) (e : Expr) : Meta.SimpM Meta.Simp.Step

Core rewriting function used in the "squash" step, which moves casts upwards and eliminates them.

It tries to rewrite an expression using the elim and move lemmas. On failure, it calls the splitting procedure heuristic.

def Lean.Elab.Tactic.NormCast.numeralToCoe (e : Expr) : MetaM Meta.Simp.Result

If possible, rewrites (n : α) to (Nat.cast n : α) where n is a numeral and α ≠ ℕ. Returns a pair of the new expression and proof that they are equal.

def Lean.Elab.Tactic.NormCast.elabNormCastConfig : Syntax → TacticM Meta.Simp.NormCastConfig

def Lean.Elab.Tactic.NormCast.derive (e : Expr) (config : Meta.Simp.NormCastConfig := { }) : MetaM Meta.Simp.Result

The core simplification routine of normCast.

def Lean.Elab.Tactic.NormCast.elabModCast : Term.TermElab

def Lean.Elab.Tactic.NormCast.normCastTarget (cfg : Meta.Simp.NormCastConfig) : TacticM Unit

Implementation of the norm_cast tactic when operating on the main goal.

def Lean.Elab.Tactic.NormCast.normCastHyp (cfg : Meta.Simp.NormCastConfig) (fvarId : FVarId) : TacticM Unit

Implementation of the norm_cast tactic when operating on a hypothesis.

def Lean.Elab.Tactic.NormCast.evalNormCast0 : Tactic

def Lean.Elab.Tactic.NormCast.evalConvNormCast : Tactic

def Lean.Elab.Tactic.NormCast.evalPushCast : Tactic

def Lean.Elab.Tactic.NormCast.elabAddElim : Command.CommandElab