- 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
Instances For
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)
Equations
- Std.Tactic.NormCast.instReprLabel = { reprPrec := Std.Tactic.NormCast.reprLabel✝ }
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.
Instances For
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
- 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)
Instances For
Classifies a declaration of type ty
as a norm_cast
rule.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Instances For
Equations
- Std.Tactic.NormCast.instInhabitedNormCastExtension = { default := { up := default, down := default, squash := default } }
The norm_cast
extension data.
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
Instances For
addMove decl
adds decl
as a move
lemma to the cache.
Equations
- One or more equations did not get rendered due to their size.
Instances For
addSquash decl
adds decl
as a squash
lemma to the cache.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Instances For
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.