The norm_cast family of tactics.

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

Prove a = b using the given simp set.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Construct the expression (e : ty).

Equations

• Std.Tactic.NormCast.mkCoe e ty = do let __discr ← Lean.Meta.coerce? e ty match __discr with | Lean.LOption.some e' => pure e' | x => failure

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

Check if an expression is the coercion of some other expression, and if so return that expression.

Equations

• One or more equations did not get rendered due to their size.

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

Check if an expression is a numeral in some type, and if so return that type and the natural number.

Equations

• One or more equations did not get rendered due to their size.

def Std.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.

def Std.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.

def Std.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.

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

If possible, rewrite (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.

def Std.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.

def Std.Tactic.NormCast.termMod_cast_ : Lean.ParserDescr

Term elaborator which uses the expected type to insert coercions.

Equations

• One or more equations did not get rendered due to their size.

def Std.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.

def Std.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.

def Std.Tactic.NormCast.tacticNorm_cast0_ : Lean.ParserDescr

Implementation of norm_cast (the full norm_cast calls trivial afterwards).

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.NormCast.tacticAssumption_mod_cast : Lean.ParserDescr

assumption_mod_cast runs norm_cast on the goal. For each local hypothesis h, it also normalizes h and tries to use that to close the goal.

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.NormCast.tacticNorm_cast_ : Lean.ParserDescr

The norm_cast family of tactics is used to normalize casts inside expressions. It is basically a simp tactic with a specific set of lemmas to move casts upwards in the expression. Therefore it can be used more safely as a non-terminating tactic. It also has special handling of numerals.

For instance, given an assumption

a b : ℤ
h : ↑a + ↑b < (10 : ℚ)

writing norm_cast at h will turn h into

h : a + b < 10

You can also use exact_mod_cast, apply_mod_cast, rw_mod_cast or assumption_mod_cast. Writing exact_mod_cast h and apply_mod_cast h will normalize the goal and h before using exact h or apply h. Writing assumption_mod_cast will normalize the goal and for every expression h in the context it will try to normalize h and use exact h. rw_mod_cast acts like the rw tactic but it applies norm_cast between steps.

See also push_cast, for move casts inwards.

The implementation and behavior of the norm_cast family is described in detail at .

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.NormCast.tacticRw_mod_cast___ : Lean.ParserDescr

Rewrite with the given rules and normalize casts between steps.

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.NormCast.tacticExact_mod_cast_ : Lean.ParserDescr

Normalize the goal and the given expression, then close the goal with exact.

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.NormCast.tacticApply_mod_cast_ : Lean.ParserDescr

Normalize the goal and the given expression, then apply the expression to the goal.

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.NormCast.convNormCast : Lean.ParserDescr

norm_cast tactic in conv mode.

Equations

• Std.Tactic.NormCast.convNormCast = Lean.ParserDescr.node `Std.Tactic.NormCast.convNormCast 1024 (Lean.ParserDescr.nonReservedSymbol "norm_cast" false)

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

norm_cast tactic in conv mode.

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.NormCast.pushCast : Lean.ParserDescr

push_cast rewrites the expression to move casts toward the leaf nodes. This uses norm_cast lemmas in the forward direction. For example, ↑(a + b) will be written to ↑a + ↑b. It is equivalent to simp only with push_cast. It can also be used at hypotheses with push_cast at h and with extra simp lemmas with push_cast [int.add_zero].

example (a b : ℕ) (h1 : ((a + b : ℕ) : ℤ) = 10) (h2 : ((a + b + 0 : ℕ) : ℤ) = 10) :
  ((a + b : ℕ) : ℤ) = 10 :=
begin
  push_cast,
  push_cast at h1,
  push_cast [int.add_zero] at h2,
end

The implementation and behavior of the norm_cast family is described in detail at .

Equations

• One or more equations did not get rendered due to their size.

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

push_cast rewrites the expression to move casts toward the leaf nodes. This uses norm_cast lemmas in the forward direction. For example, ↑(a + b) will be written to ↑a + ↑b. It is equivalent to simp only with push_cast. It can also be used at hypotheses with push_cast at h and with extra simp lemmas with push_cast [int.add_zero].

example (a b : ℕ) (h1 : ((a + b : ℕ) : ℤ) = 10) (h2 : ((a + b + 0 : ℕ) : ℤ) = 10) :
  ((a + b : ℕ) : ℤ) = 10 :=
begin
  push_cast,
  push_cast at h1,
  push_cast [int.add_zero] at h2,
end

The implementation and behavior of the norm_cast family is described in detail at .

Equations

• One or more equations did not get rendered due to their size.