# Documentation

Std.Tactic.NormCast.Ext

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
Instances For
Equations
Equations

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.

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

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

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

Equations
• = do let __do_lift ← let __do_lift_1 ← pure (__do_lift - __do_lift_1)

Classifies a declaration of type ty as a norm_cast rule.

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

The push_cast simp attribute.

The norm_cast attribute stores three simp sets.

Instances For
Equations

The norm_cast extension data.

def Std.Tactic.NormCast.addElim (decl : Lean.Name) (prio : optParam Nat 1000) :

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

Equations
def Std.Tactic.NormCast.addMove (decl : Lean.Name) (prio : optParam Nat 1000) :

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

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

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) (prio : optParam Nat 1000) :

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.

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

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

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
↑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
↑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
↔ 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
∀ 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
↑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
↑(m + n) : ℤ) = ↑m + ↑n

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

@[norm_cast] theorem cast_one : ((1 : ℚ) : α) = 1
↑m + ↑n

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

@[norm_cast] theorem cast_one : ((1 : ℚ) : α) = 1
↑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]
← 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.