inductive Std.Tactic.NormCast.Label : Type

• elim: Std.Tactic.NormCast.Label

  elim lemma: LHS has 0 head coes and ≥ 1 internal coe

• move: Std.Tactic.NormCast.Label

  move lemma: LHS has 1 head coe and 0 internal coes, RHS has 0 head coes and ≥ 1 internal coes

• squash: Std.Tactic.NormCast.Label

  squash lemma: LHS has ≥ 1 head coes and 0 internal coes, RHS has fewer head coes

Label is a type used to classify norm_cast lemmas.

• elim lemma: LHS has 0 head coes and ≥ 1 internal coe
• move lemma: LHS has 1 head coe and 0 internal coes, RHS has 0 head coes and ≥ 1 internal coes
• squash lemma: LHS has ≥ 1 head coes and 0 internal coes, RHS has fewer head coes

instance Std.Tactic.NormCast.instDecidableEqLabel : DecidableEq Std.Tactic.NormCast.Label

Equations

• Std.Tactic.NormCast.instDecidableEqLabel x y = if h : Std.Tactic.NormCast.Label.toCtorIdx x = Std.Tactic.NormCast.Label.toCtorIdx y then isTrue (_ : x = y) else isFalse (_ : x = y → False)

instance Std.Tactic.NormCast.instReprLabel : Repr Std.Tactic.NormCast.Label

Equations

• Std.Tactic.NormCast.instReprLabel = { reprPrec := Std.Tactic.NormCast.reprLabel✝ }

instance Std.Tactic.NormCast.instInhabitedLabel : Inhabited Std.Tactic.NormCast.Label

Equations

• Std.Tactic.NormCast.instInhabitedLabel = { default := Std.Tactic.NormCast.Label.elim }

def Std.Tactic.NormCast.getSimpArgs (e : Lean.Expr) : Lean.MetaM (Array Lean.Expr)

Assuming e is an application, returns the list of subterms that simp will rewrite in.

Equations

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

partial def Std.Tactic.NormCast.countHeadCoes (e : Lean.Expr) : Lean.MetaM Nat

Count how many coercions are at the top of the expression.

partial def Std.Tactic.NormCast.countCoes (e : Lean.Expr) : Lean.MetaM Nat

Count how many coercions are inside the expression, including the top ones.

def Std.Tactic.NormCast.countInternalCoes (e : Lean.Expr) : Lean.MetaM Nat

Count how many coercions are inside the expression, excluding the top ones.

Equations

• Std.Tactic.NormCast.countInternalCoes e = do let __do_lift ← Std.Tactic.NormCast.countCoes e let __do_lift_1 ← Std.Tactic.NormCast.countHeadCoes e pure (__do_lift - __do_lift_1)

def Std.Tactic.NormCast.classifyType (ty : Lean.Expr) : Lean.MetaM Std.Tactic.NormCast.Label

Classifies a declaration of type ty as a norm_cast rule.

Equations

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

opaque Std.Tactic.NormCast.pushCastExt : Lean.Meta.SimpExtension

The push_cast simp attribute.

structure Std.Tactic.NormCast.NormCastExtension : Type

• up : Lean.Meta.SimpExtension

  A simp set which lifts coercion arrows to the top level.

• down : Lean.Meta.SimpExtension

  A simp set which pushes coercion arrows to the leaves.

• squash : Lean.Meta.SimpExtension

  A simp set which simplifies transitive coercions.

The norm_cast attribute stores three simp sets.

instance Std.Tactic.NormCast.instInhabitedNormCastExtension : Inhabited Std.Tactic.NormCast.NormCastExtension

Equations

• Std.Tactic.NormCast.instInhabitedNormCastExtension = { default := { up := default, down := default, squash := default } }

opaque Std.Tactic.NormCast.normCastExt : Std.Tactic.NormCast.NormCastExtension

The norm_cast extension data.

def Std.Tactic.NormCast.addElim (decl : Lean.Name) (kind : optParam Lean.AttributeKind Lean.AttributeKind.global) (prio : optParam Nat 1000) : Lean.MetaM Unit

addElim decl adds decl as an elim lemma to the cache.

Equations

• Std.Tactic.NormCast.addElim decl kind prio = Lean.Meta.addSimpTheorem Std.Tactic.NormCast.normCastExt.up decl true false kind prio

def Std.Tactic.NormCast.addMove (decl : Lean.Name) (kind : optParam Lean.AttributeKind Lean.AttributeKind.global) (prio : optParam Nat 1000) : Lean.MetaM Unit

addMove decl adds decl as a move lemma to the cache.

Equations

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

def Std.Tactic.NormCast.addSquash (decl : Lean.Name) (kind : optParam Lean.AttributeKind Lean.AttributeKind.global) (prio : optParam Nat 1000) : Lean.MetaM Unit

addSquash decl adds decl as a squash lemma to the cache.

Equations

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

def Std.Tactic.NormCast.addInfer (decl : Lean.Name) (kind : optParam Lean.AttributeKind Lean.AttributeKind.global) (prio : optParam Nat 1000) : Lean.MetaM Unit

addInfer decl infers the label of decl and adds it to the cache.

• elim lemma: LHS has 0 head coes and ≥ 1 internal coe
• move lemma: LHS has 1 head coe and 0 internal coes, RHS has 0 head coes and ≥ 1 internal coes
• squash lemma: LHS has ≥ 1 head coes and 0 internal coes, RHS has fewer head coes

Equations

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

def Std.Tactic.NormCast.Attr.normCastLabel : Lean.ParserDescr

The possible norm_cast kinds: elim, move, or squash.

Equations

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

def Std.Tactic.NormCast.Attr.norm_cast : Lean.ParserDescr

The norm_cast attribute should be given to lemmas that describe the behaviour of a coercion in regard to an operator, a relation, or a particular function.

It only concerns equality or iff lemmas involving ↑, ⇑ and ↥, describing the behavior of the coercion functions. It does not apply to the explicit functions that define the coercions.

Examples:

@[norm_cast] theorem coe_nat_inj' {m n : ℕ} : (↑m : ℤ) = ↑n ↔ m = n

@[norm_cast] theorem coe_int_denom (n : ℤ) : (n : ℚ).denom = 1

@[norm_cast] theorem cast_id : ∀ n : ℚ, ↑n = n

@[norm_cast] theorem coe_nat_add (m n : ℕ) : (↑(m + n) : ℤ) = ↑m + ↑n

@[norm_cast] theorem cast_coe_nat (n : ℕ) : ((n : ℤ) : α) = n

@[norm_cast] theorem cast_one : ((1 : ℚ) : α) = 1

Lemmas tagged with @[norm_cast] are classified into three categories: move, elim, and squash. They are classified roughly as follows:

• elim lemma: LHS has 0 head coes and ≥ 1 internal coe
• move lemma: LHS has 1 head coe and 0 internal coes, RHS has 0 head coes and ≥ 1 internal coes
• squash lemma: LHS has ≥ 1 head coes and 0 internal coes, RHS has fewer head coes

norm_cast uses move and elim lemmas to factor coercions toward the root of an expression and to cancel them from both sides of an equation or relation. It uses squash lemmas to clean up the result.

Occasionally you may want to override the automatic classification. You can do this by giving an optional elim, move, or squash parameter to the attribute.

@[simp, norm_cast elim] lemma nat_cast_re (n : ℕ) : (n : ℂ).re = n := by
  rw [← of_real_nat_cast, of_real_re]

Don't do this unless you understand what you are doing.

A full description of the tactic, and the use of each lemma category, can be found at https://lean-forward.github.io/norm_cast/norm_cast.pdf.

Equations

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