Documentation

Lean.Elab.Tactic.NormCast

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.

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

Proves a = b using the given simp set.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.NormCast.proveEqUsingDown (a : Lean.Expr) (b : Lean.Expr) :
Lean.MetaM (Option Lean.Meta.Simp.Result)

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

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.NormCast.mkCoe (e : Lean.Expr) (ty : Lean.Expr) :
Lean.MetaM Lean.Expr

Constructs the expression (e : ty).

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

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

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.NormCast.isNumeral? (e : Lean.Expr) :
Option (Lean.Expr × Nat)

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

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.NormCast.splittingProcedure (expr : Lean.Expr) :
Lean.MetaM Lean.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

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.NormCast.prove (e : Lean.Expr) :
Lean.Meta.SimpM (Option Lean.Expr)

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

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.NormCast.upwardAndElim (up : Lean.Meta.SimpTheorems) (e : Lean.Expr) :
Lean.Meta.SimpM Lean.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.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.NormCast.numeralToCoe (e : Lean.Expr) :
Lean.MetaM Lean.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.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.NormCast.derive (e : Lean.Expr) :
Lean.MetaM Lean.Meta.Simp.Result

The core simplification routine of normCast.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.NormCast.elabModCast :
Lean.Elab.Term.TermElab
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.NormCast.normCastTarget :
Lean.Elab.Tactic.TacticM Unit

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

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.NormCast.normCastHyp (fvarId : Lean.FVarId) :
Lean.Elab.Tactic.TacticM Unit

Implementation of the norm_cast tactic when operating on a hypothesis.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.NormCast.evalNormCast0 :
Lean.Elab.Tactic.Tactic
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.NormCast.evalConvNormCast :
Lean.Elab.Tactic.Tactic
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.NormCast.evalPushCast :
Lean.Elab.Tactic.Tactic
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.NormCast.elabAddElim :
Lean.Elab.Command.CommandElab
Equations
  • One or more equations did not get rendered due to their size.