Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+โCtrl+โto navigate, Ctrl+๐ฑ๏ธto focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Paul-Nicolas Madelaine, Robert Y. Lewis, Mario Carneiro, Gabriel Ebner
-/
import Lean.Meta.CongrTheorems
import Lean.Meta.Tactic.Simp.SimpTheorems
import Std.Tactic.CoeExt

open Lean Meta

namespace Std.Tactic.NormCast
open Tactic.Coe

/--
`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
-/
inductive Label: Sort ?u.1Label
/-- elim lemma: LHS has 0 head coes and โฅ 1 internal coe -/
| elim: Labelelim
/-- move lemma: LHS has 1 head coe and 0 internal coes,
RHS has 0 head coes and โฅ 1 internal coes -/
| move: Labelmove
/-- squash lemma: LHS has โฅ 1 head coes and 0 internal coes, RHS has fewer head coes -/
| squash: Labelsquash
deriving DecidableEq: Sort u โ Sort (max1u)DecidableEq, Repr: Type u โ Type uRepr, Inhabited: Sort u โ Sort (max1u)Inhabited

/-- Assuming `e` is an application, returns the list of subterms that `simp` will rewrite in. -/
def getSimpArgs: Expr โ MetaM (Array Expr)getSimpArgs (e: Expre : Expr: TypeExpr) : MetaM: Type โ TypeMetaM (Array: Type ?u.1007 โ Type ?u.1007Array Expr: TypeExpr) := do
match โ mkCongrSimp?: Expr โ optParam Bool true โ MetaM (Option CongrTheorem)mkCongrSimp? e: Expre.getAppFn: Expr โ ExprgetAppFn with
| none: {ฮฑ : Type ?u.1031} โ Option ฮฑnone => return e: Expre.getAppArgs: Expr โ Array ExprgetAppArgs
| some: {ฮฑ : Type ?u.1184} โ ฮฑ โ Option ฮฑsome {argKinds: Array CongrArgKindargKinds, ..} =>
let mut args: ?m.1352args := #[]: Array ?m.1210#[]
for a: ?m.1340a in e: Expre.getAppArgs: Expr โ Array ExprgetAppArgs, k: CongrArgKindk in argKinds: Array CongrArgKindargKinds do
if k: CongrArgKindk matches .eq: CongrArgKind.eq then
args: ?m.1352args := args: ?m.1352args.push: {ฮฑ : Type ?u.1667} โ Array ฮฑ โ ฮฑ โ Array ฮฑpush a: ?m.1340a
return args: Array Exprargs

/-- Count how many coercions are at the top of the expression. -/
partial def countHeadCoes: Expr โ MetaM NatcountHeadCoes (e: Expre : Expr: TypeExpr) : MetaM: Type โ TypeMetaM Nat: TypeNat := do
if let Expr.const: Name โ List Level โ ExprExpr.const fn: Namefn .. := e: Expre.getAppFn: Expr โ ExprgetAppFn then
if let some: {ฮฑ : Type ?u.5052} โ ฮฑ โ Option ฮฑsome info: CoeFnInfoinfo โ getCoeFnInfo?: Name โ CoreM (Option CoeFnInfo)getCoeFnInfo? fn: Namefn then
if e: Expre.getAppNumArgs: Expr โ NatgetAppNumArgs >= info: CoeFnInfoinfo.numArgs: CoeFnInfo โ NatnumArgs then
return (โ countHeadCoes: Expr โ MetaM NatcountHeadCoes (e: Expre.getArg!: (e : Expr) โ Nat โ optParam Nat (Expr.getAppNumArgs e) โ ExprgetArg! info: CoeFnInfoinfo.coercee: CoeFnInfo โ Natcoercee)) + 1: ?m.51691
return 0: ?m.59460

/-- Count how many coercions are inside the expression, including the top ones. -/
partial def countCoes: Expr โ MetaM NatcountCoes (e: Expre : Expr: TypeExpr) : MetaM: Type โ TypeMetaM Nat: TypeNat :=
lambdaTelescope: {n : Type โ Type ?u.7417} โ
[inst : MonadControlT MetaM n] โ [inst : Monad n] โ {ฮฑ : Type} โ Expr โ (Array Expr โ Expr โ n ฮฑ) โ n ฮฑlambdaTelescope e: Expre fun _: ?m.7458_ e: ?m.7461e => do
if let Expr.const: Name โ List Level โ ExprExpr.const fn: Namefn .. := e: ?m.7461e.getAppFn: Expr โ ExprgetAppFn then
if let some: {ฮฑ : Type ?u.7484} โ ฮฑ โ Option ฮฑsome info: CoeFnInfoinfo โ getCoeFnInfo?: Name โ CoreM (Option CoeFnInfo)getCoeFnInfo? fn: Namefn then
if e: ?m.7461e.getAppNumArgs: Expr โ NatgetAppNumArgs >= info: CoeFnInfoinfo.numArgs: CoeFnInfo โ NatnumArgs then
let mut coes: ?m.7898coes := (โ countHeadCoes: Expr โ MetaM NatcountHeadCoes (e: ?m.7461e.getArg!: (e : Expr) โ Nat โ optParam Nat (Expr.getAppNumArgs e) โ ExprgetArg! info: CoeFnInfoinfo.coercee: CoeFnInfo โ Natcoercee)) + 1: ?m.77601
for i: ?m.7892i in [info: CoeFnInfoinfo.numArgs: CoeFnInfo โ NatnumArgs:e: ?m.7461e.getAppNumArgs: Expr โ NatgetAppNumArgs] do
coes: ?m.7953coes := coes: ?m.7898coes + (โ countCoes: Expr โ MetaM NatcountCoes (e: ?m.7461e.getArg!: (e : Expr) โ Nat โ optParam Nat (Expr.getAppNumArgs e) โ ExprgetArg! i: ?m.7892i))
return coes: ?m.8157coes
return (โ (โ getSimpArgs e).mapM countCoes): ?m.8940(โ (โ getSimpArgs e): ?m.8850(โ getSimpArgs: Expr โ MetaM (Array Expr)getSimpArgs(โ getSimpArgs e): ?m.8850 e: ?m.7461e(โ getSimpArgs e): ?m.8850)(โ (โ getSimpArgs e).mapM countCoes): ?m.8940.mapM: {ฮฑ : Type ?u.8890} โ
{ฮฒ : Type ?u.8889} โ {m : Type ?u.8889 โ Type ?u.8888} โ [inst : Monad m] โ (ฮฑ โ m ฮฒ) โ Array ฮฑ โ m (Array ฮฒ)mapM(โ (โ getSimpArgs e).mapM countCoes): ?m.8940 countCoes: Expr โ MetaM NatcountCoes(โ (โ getSimpArgs e).mapM countCoes): ?m.8940).foldl: {ฮฑ : Type ?u.8968} โ
{ฮฒ : Type ?u.8967} โ (ฮฒ โ ฮฑ โ ฮฒ) โ ฮฒ โ (as : Array ฮฑ) โ optParam Nat 0 โ optParam Nat (Array.size as) โ ฮฒfoldl (ยท+ยท): Nat โ Nat โ Nat(ยท+ยท) 0: ?m.90100

/-- Count how many coercions are inside the expression, excluding the top ones. -/
def countInternalCoes: Expr โ MetaM NatcountInternalCoes (e: Expre : Expr: TypeExpr) : MetaM: Type โ TypeMetaM Nat: TypeNat :=
return (โ countCoes e) - (โ countHeadCoes e): ?m.11955(โ countCoes: Expr โ MetaM NatcountCoes(โ countCoes e) - (โ countHeadCoes e): ?m.11955 e: Expre(โ countCoes e) - (โ countHeadCoes e): ?m.11955) - (โ countHeadCoes: Expr โ MetaM NatcountHeadCoes(โ countCoes e) - (โ countHeadCoes e): ?m.11955 e: Expre(โ countCoes e) - (โ countHeadCoes e): ?m.11955)

/-- Classifies a declaration of type `ty` as a `norm_cast` rule. -/
def classifyType: Expr โ MetaM LabelclassifyType (ty: Exprty : Expr: TypeExpr) : MetaM: Type โ TypeMetaM Label: TypeLabel :=
forallTelescopeReducing: {n : Type โ Type ?u.12346} โ
[inst : MonadControlT MetaM n] โ [inst : Monad n] โ {ฮฑ : Type} โ Expr โ (Array Expr โ Expr โ n ฮฑ) โ n ฮฑforallTelescopeReducing ty: Exprty fun _: ?m.12387_ ty: ?m.12390ty => do
let ty: ?m.12465ty โ whnf: Expr โ MetaM Exprwhnf ty: ?m.12390ty
let (lhs: Exprlhs, rhs: Exprrhs) โ
if ty: ?m.12465ty.isAppOfArity: Expr โ Name โ Nat โ BoolisAppOfArity ``Eq: {ฮฑ : Sort u_1} โ ฮฑ โ ฮฑ โ PropEq 3: ?m.124803 then pure: {f : Type ?u.12615 โ Type ?u.12614} โ [self : Pure f] โ {ฮฑ : Type ?u.12615} โ ฮฑ โ f ฮฑpurepure (ty.getArg! 1, ty.getArg! 2): MetaM (?m.12472 yโ) (ty: ?m.12465typure (ty.getArg! 1, ty.getArg! 2): MetaM (?m.12472 yโ).getArg!: (e : Expr) โ Nat โ optParam Nat (Expr.getAppNumArgs e) โ ExprgetArg!pure (ty.getArg! 1, ty.getArg! 2): MetaM (?m.12472 yโ) 1: ?m.126471pure (ty.getArg! 1, ty.getArg! 2): MetaM (?m.12472 yโ), ty: ?m.12465typure (ty.getArg! 1, ty.getArg! 2): MetaM (?m.12472 yโ).getArg!: (e : Expr) โ Nat โ optParam Nat (Expr.getAppNumArgs e) โ ExprgetArg!pure (ty.getArg! 1, ty.getArg! 2): MetaM (?m.12472 yโ) 2: ?m.126552pure (ty.getArg! 1, ty.getArg! 2): MetaM (?m.12472 yโ))
else if ty: ?m.12465ty.isAppOfArity: Expr โ Name โ Nat โ BoolisAppOfArity ``Iff: Prop โ Prop โ PropIff 2: ?m.127282 then pure: {f : Type ?u.12830 โ Type ?u.12829} โ [self : Pure f] โ {ฮฑ : Type ?u.12830} โ ฮฑ โ f ฮฑpurepure (ty.getArg! 0, ty.getArg! 1): MetaM (?m.12472 yโ) (ty: ?m.12465typure (ty.getArg! 0, ty.getArg! 1): MetaM (?m.12472 yโ).getArg!: (e : Expr) โ Nat โ optParam Nat (Expr.getAppNumArgs e) โ ExprgetArg!pure (ty.getArg! 0, ty.getArg! 1): MetaM (?m.12472 yโ) 0: ?m.128620pure (ty.getArg! 0, ty.getArg! 1): MetaM (?m.12472 yโ), ty: ?m.12465typure (ty.getArg! 0, ty.getArg! 1): MetaM (?m.12472 yโ).getArg!: (e : Expr) โ Nat โ optParam Nat (Expr.getAppNumArgs e) โ ExprgetArg!pure (ty.getArg! 0, ty.getArg! 1): MetaM (?m.12472 yโ) 1: ?m.128701pure (ty.getArg! 0, ty.getArg! 1): MetaM (?m.12472 yโ))
else throwError "norm_cast: lemma must be = or โ, but is{indentExpr ty}": MetaM (?m.12472 yโ)throwErrorthrowError "norm_cast: lemma must be = or โ, but is{indentExpr ty}": MetaM (?m.12472 yโ) "norm_cast: lemma must be = or โ, but is{indentExpr: Expr โ MessageDataindentExprthrowError "norm_cast: lemma must be = or โ, but is{indentExpr ty}": MetaM (?m.12472 yโ) ty: ?m.12465tythrowError "norm_cast: lemma must be = or โ, but is{indentExpr ty}": MetaM (?m.12472 yโ)}"
let lhsCoes: ?m.13319lhsCoes โ countCoes: Expr โ MetaM NatcountCoes lhs: Exprlhs
if lhsCoes: ?m.13319lhsCoes = 0: ?m.133320 then throwError "norm_cast: badly shaped lemma, lhs must contain at least one coe{indentExpr lhs}": MetaM (?m.13326 yโ)throwErrorthrowError "norm_cast: badly shaped lemma, lhs must contain at least one coe{indentExpr lhs}": MetaM (?m.13326 yโ) "norm_cast: badly shaped lemma, lhs must contain at least one coe{indentExpr: Expr โ MessageDataindentExprthrowError "norm_cast: badly shaped lemma, lhs must contain at least one coe{indentExpr lhs}": MetaM (?m.13326 yโ) lhs: ExprlhsthrowError "norm_cast: badly shaped lemma, lhs must contain at least one coe{indentExpr lhs}": MetaM (?m.13326 yโ)}"
let rhsInternalCoes: ?m.13748rhsInternalCoes โ countInternalCoes: Expr โ MetaM NatcountInternalCoes rhs: Exprrhs
return Label.elim: LabelLabel.elim
if rhsInternalCoes: ?m.13748rhsInternalCoes = 0: ?m.141040 then
return Label.squash: LabelLabel.squash
else
return Label.move: LabelLabel.move
return Label.squash: LabelLabel.squash
else do
throwError "norm_cast: badly shaped shaped squash lemma, rhs must have fewer head coes than lhs{indentExpr: Expr โ MessageDataindentExpr ty: ?m.12465ty}"

/-- The `push_cast` simp attribute. -/
initialize pushCastExt: SimpExtensionpushCastExt : SimpExtension: TypeSimpExtension โ
registerSimpAttr: Name โ String โ autoParam Name _autoโ โ IO SimpExtensionregisterSimpAttr `push_cast: Name`push_cast <|
"The `push_cast` simp attribute uses `norm_cast` lemmas ": String"The `push_cast` simp attribute uses `norm_cast` lemmas " ++
"to move casts toward the leaf nodes of the expression.": String"to move casts toward the leaf nodes of the expression."

/--  The `norm_cast` attribute stores three simp sets. -/
structure NormCastExtension: SimpExtension โ SimpExtension โ SimpExtension โ NormCastExtensionNormCastExtension where
/-- A simp set which lifts coercion arrows to the top level. -/
up: NormCastExtension โ SimpExtensionup : SimpExtension: TypeSimpExtension
/-- A simp set which pushes coercion arrows to the leaves. -/
down: NormCastExtension โ SimpExtensiondown : SimpExtension: TypeSimpExtension
/-- A simp set which simplifies transitive coercions. -/
squash: NormCastExtension โ SimpExtensionsquash : SimpExtension: TypeSimpExtension
deriving Inhabited: Sort u โ Sort (max1u)Inhabited

/-- The `norm_cast` extension data. -/
initialize normCastExt: NormCastExtensionnormCastExt : NormCastExtension: TypeNormCastExtension โ pure: {f : Type ?u.19236 โ Type ?u.19235} โ [self : Pure f] โ {ฮฑ : Type ?u.19236} โ ฮฑ โ f ฮฑpure {
up := โ mkSimpExt (decl_name% ++ `up)
down := โ mkSimpExt (decl_name% ++ `down)
squash := โ mkSimpExt (decl_name% ++ `squash)
}: NormCastExtension{
up{
up := โ mkSimpExt (decl_name% ++ `up)
down := โ mkSimpExt (decl_name% ++ `down)
squash := โ mkSimpExt (decl_name% ++ `squash)
}: NormCastExtension := โ mkSimpExt: autoParam Name _autoโ โ IO SimpExtensionmkSimpExt{
up := โ mkSimpExt (decl_name% ++ `up)
down := โ mkSimpExt (decl_name% ++ `down)
squash := โ mkSimpExt (decl_name% ++ `squash)
}: NormCastExtension (decl_name%: Namedecl_name%{
up := โ mkSimpExt (decl_name% ++ `up)
down := โ mkSimpExt (decl_name% ++ `down)
squash := โ mkSimpExt (decl_name% ++ `squash)
}: NormCastExtension ++ `up: Name`up{
up := โ mkSimpExt (decl_name% ++ `up)
down := โ mkSimpExt (decl_name% ++ `down)
squash := โ mkSimpExt (decl_name% ++ `squash)
}: NormCastExtension)
down{
up := โ mkSimpExt (decl_name% ++ `up)
down := โ mkSimpExt (decl_name% ++ `down)
squash := โ mkSimpExt (decl_name% ++ `squash)
}: NormCastExtension := โ mkSimpExt: autoParam Name _autoโ โ IO SimpExtensionmkSimpExt{
up := โ mkSimpExt (decl_name% ++ `up)
down := โ mkSimpExt (decl_name% ++ `down)
squash := โ mkSimpExt (decl_name% ++ `squash)
}: NormCastExtension (decl_name%: Namedecl_name%{
up := โ mkSimpExt (decl_name% ++ `up)
down := โ mkSimpExt (decl_name% ++ `down)
squash := โ mkSimpExt (decl_name% ++ `squash)
}: NormCastExtension ++ `down: Name`down{
up := โ mkSimpExt (decl_name% ++ `up)
down := โ mkSimpExt (decl_name% ++ `down)
squash := โ mkSimpExt (decl_name% ++ `squash)
}: NormCastExtension)
squash{
up := โ mkSimpExt (decl_name% ++ `up)
down := โ mkSimpExt (decl_name% ++ `down)
squash := โ mkSimpExt (decl_name% ++ `squash)
}: NormCastExtension := โ mkSimpExt: autoParam Name _autoโ โ IO SimpExtensionmkSimpExt{
up := โ mkSimpExt (decl_name% ++ `up)
down := โ mkSimpExt (decl_name% ++ `down)
squash := โ mkSimpExt (decl_name% ++ `squash)
}: NormCastExtension (decl_name%: Namedecl_name%{
up := โ mkSimpExt (decl_name% ++ `up)
down := โ mkSimpExt (decl_name% ++ `down)
squash := โ mkSimpExt (decl_name% ++ `squash)
}: NormCastExtension ++ `squash: Name`squash{
up := โ mkSimpExt (decl_name% ++ `up)
down := โ mkSimpExt (decl_name% ++ `down)
squash := โ mkSimpExt (decl_name% ++ `squash)
}: NormCastExtension)
}

/-- `addElim decl` adds `decl` as an `elim` lemma to the cache. -/
def addElim: Name โ optParam AttributeKind AttributeKind.global โ optParam Nat 1000 โ MetaM UnitaddElim (decl: Namedecl : Name: TypeName)
(kind: optParam AttributeKind AttributeKind.globalkind := AttributeKind.global: AttributeKindAttributeKind.global) (prio: optParam ?m.19604 1000prio := eval_prio default: ?m.19606eval_prioeval_prio default: ?m.19606 eval_prio default: ?m.19606default) : MetaM: Type โ TypeMetaM Unit: TypeUnit :=
addSimpTheorem: SimpExtension โ Name โ Bool โ Bool โ AttributeKind โ Nat โ MetaM UnitaddSimpTheorem normCastExt: NormCastExtensionnormCastExt.up: NormCastExtension โ SimpExtensionup decl: Namedecl (post := true: Booltrue) (inv := false: Boolfalse) kind: optParam AttributeKind AttributeKind.globalkind prio: optParam Nat 1000prio

/-- `addMove decl` adds `decl` as a `move` lemma to the cache. -/
def addMove: Name โ optParam AttributeKind AttributeKind.global โ optParam Nat 1000 โ MetaM UnitaddMove (decl: Namedecl : Name: TypeName)
(kind: optParam ?m.19797 AttributeKind.globalkind := AttributeKind.global: AttributeKindAttributeKind.global) (prio: optParam Nat 1000prio := eval_prio default: ?m.19803eval_prioeval_prio default: ?m.19803 eval_prio default: ?m.19803default) : MetaM: Type โ TypeMetaM Unit: TypeUnit := do
addSimpTheorem: SimpExtension โ Name โ Bool โ Bool โ AttributeKind โ Nat โ MetaM UnitaddSimpTheorem pushCastExt: SimpExtensionpushCastExt decl: Namedecl (post := true: Booltrue) (inv := false: Boolfalse) kind: optParam AttributeKind AttributeKind.globalkind prio: optParam Nat 1000prio
addSimpTheorem: SimpExtension โ Name โ Bool โ Bool โ AttributeKind โ Nat โ MetaM UnitaddSimpTheorem normCastExt: NormCastExtensionnormCastExt.up: NormCastExtension โ SimpExtensionup decl: Namedecl (post := true: Booltrue) (inv := true: Booltrue) kind: optParam AttributeKind AttributeKind.globalkind prio: optParam Nat 1000prio
addSimpTheorem: SimpExtension โ Name โ Bool โ Bool โ AttributeKind โ Nat โ MetaM UnitaddSimpTheorem normCastExt: NormCastExtensionnormCastExt.down: NormCastExtension โ SimpExtensiondown decl: Namedecl (post := true: Booltrue) (inv := false: Boolfalse) kind: optParam AttributeKind AttributeKind.globalkind prio: optParam Nat 1000prio

/-- `addSquash decl` adds `decl` as a `squash` lemma to the cache. -/
def addSquash: Name โ optParam AttributeKind AttributeKind.global โ optParam Nat 1000 โ MetaM UnitaddSquash (decl: Namedecl : Name: TypeName)
(kind: optParam AttributeKind AttributeKind.globalkind := AttributeKind.global: AttributeKindAttributeKind.global) (prio: optParam Nat 1000prio := eval_prio default: ?m.20316eval_prioeval_prio default: ?m.20316 eval_prio default: ?m.20316default) : MetaM: Type โ TypeMetaM Unit: TypeUnit := do
addSimpTheorem: SimpExtension โ Name โ Bool โ Bool โ AttributeKind โ Nat โ MetaM UnitaddSimpTheorem pushCastExt: SimpExtensionpushCastExt decl: Namedecl (post := true: Booltrue) (inv := false: Boolfalse) kind: optParam AttributeKind AttributeKind.globalkind prio: optParam Nat 1000prio
addSimpTheorem: SimpExtension โ Name โ Bool โ Bool โ AttributeKind โ Nat โ MetaM UnitaddSimpTheorem normCastExt: NormCastExtensionnormCastExt.squash: NormCastExtension โ SimpExtensionsquash decl: Namedecl (post := true: Booltrue) (inv := false: Boolfalse) kind: optParam AttributeKind AttributeKind.globalkind prio: optParam Nat 1000prio
addSimpTheorem: SimpExtension โ Name โ Bool โ Bool โ AttributeKind โ Nat โ MetaM UnitaddSimpTheorem normCastExt: NormCastExtensionnormCastExt.down: NormCastExtension โ SimpExtensiondown decl: Namedecl (post := true: Booltrue) (inv := false: Boolfalse) kind: optParam AttributeKind AttributeKind.globalkind prio: optParam Nat 1000prio

/-- `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
-/
def addInfer: Name โ optParam AttributeKind AttributeKind.global โ optParam Nat 1000 โ MetaM UnitaddInfer (decl: Namedecl : Name: TypeName)
(kind: optParam ?m.20812 AttributeKind.globalkind := AttributeKind.global: AttributeKindAttributeKind.global) (prio: optParam ?m.20816 1000prio := eval_prio default: ?m.20818eval_prioeval_prio default: ?m.20818 eval_prio default: ?m.20818default) : MetaM: Type โ TypeMetaM Unit: TypeUnit := do
let ty: ?m.21136ty := (โ getConstInfo decl): ?m.21133(โ getConstInfo: {m : Type โ Type} โ [inst : Monad m] โ [inst : MonadEnv m] โ [inst : MonadError m] โ Name โ m ConstantInfogetConstInfo(โ getConstInfo decl): ?m.21133 decl: Namedecl(โ getConstInfo decl): ?m.21133).type: ConstantInfo โ Exprtype
match โ classifyType: Expr โ MetaM LabelclassifyType ty: ?m.21136ty with
| Label.elim: LabelLabel.elim => addElim: Name โ optParam AttributeKind AttributeKind.global โ optParam Nat 1000 โ MetaM UnitaddElim decl: Namedecl kind: optParam AttributeKind AttributeKind.globalkind prio: optParam Nat 1000prio
| Label.squash: LabelLabel.squash => addSquash: Name โ optParam AttributeKind AttributeKind.global โ optParam Nat 1000 โ MetaM UnitaddSquash decl: Namedecl kind: optParam AttributeKind AttributeKind.globalkind prio: optParam Nat 1000prio
| Label.move: LabelLabel.move => addMove: Name โ optParam AttributeKind AttributeKind.global โ optParam Nat 1000 โ MetaM UnitaddMove decl: Namedecl kind: optParam AttributeKind AttributeKind.globalkind prio: optParam Nat 1000prio

namespace Attr
/-- The possible `norm_cast` kinds: `elim`, `move`, or `squash`. -/
syntax normCastLabel: ParserDescrnormCastLabel := &: String โ Bool โ ParserDescr&"elim" <|> &: String โ Bool โ ParserDescr&"move" <|> &: String โ Bool โ ParserDescr&"squash"

/--
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:
```lean
@[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.

```lean
@[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
.
-/
syntax (name := norm_cast: ParserDescrnorm_cast) "norm_cast" (ppSpace: Parser.ParserppSpace normCastLabel: ParserDescrnormCastLabel)? (ppSpace: Parser.ParserppSpace num: Parser.Parsernum)? : attr: Parser.Categoryattr
end Attr

initialize registerBuiltinAttribute: AttributeImpl โ IO UnitregisterBuiltinAttribute {
name := `norm_cast: Name`norm_cast
descr := "attribute for norm_cast": String"attribute for norm_cast"
add := fun decl: ?m.21848decl stx: ?m.21851stx kind: ?m.21854kind => MetaM.run': {ฮฑ : Type} โ
MetaM ฮฑ โ
optParam Context
{
config :=
{ foApprox := false, ctxApprox := false, quasiPatternApprox := false, constApprox := false,
isDefEqStuckEx := false, transparency := TransparencyMode.default, zetaNonDep := true, trackZeta := false,
unificationHints := true, proofIrrelevance := true, assignSyntheticOpaque := false, offsetCnstrs := true,
etaStruct := EtaStructMode.all },
lctx :=
{
fvarIdToDecl :=
{ root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 },
decls :=
{ root := PersistentArrayNode.node (Array.mkEmpty (USize.toNat PersistentArray.branching)),
tail := Array.mkEmpty (USize.toNat PersistentArray.branching), size := 0,
shift := PersistentArray.initShift, tailOff := 0 } },
localInstances := #[], defEqCtx? := none, synthPendingDepth := 0, canUnfold? := none } โ
optParam State
{
mctx :=
{ depth := 0, levelAssignDepth := 0, mvarCounter := 0,
lDepth := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 },
decls := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 },
{ root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 },
lAssignment :=
{ root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 },
eAssignment :=
{ root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 },
dAssignment :=
{ root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 } },
cache :=
{
inferType :=
{ root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 },
funInfo := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 },
synthInstance :=
{ root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 },
whnfDefault :=
{ root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 },
whnfAll := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 },
defEq := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 } },
zetaFVarIds := โ,
postponed :=
{ root := PersistentArrayNode.node (Array.mkEmpty (USize.toNat PersistentArray.branching)),
tail := Array.mkEmpty (USize.toNat PersistentArray.branching), size := 0,
shift := PersistentArray.initShift, tailOff := 0 } } โ
CoreM ฮฑMetaM.run' do
let `(attr: Parser.Categoryattr| norm_cast \$[\$label: ?m.21916 xโlabel:normCastLabel: ParserDescrnormCastLabel]? \$[\$prio: ?m.22423prio]?) := stx: ?m.21851stx | unreachable!: ?m.22454unreachable!
let prio: ?m.22556prio := (prio: ?m.22324 xโprio.bind: {ฮฑ : Type ?u.22558} โ {ฮฒ : Type ?u.22557} โ Option ฮฑ โ (ฮฑ โ Option ฮฒ) โ Option ฮฒbind (ยท.1.isNatLit?: Syntax โ Option NatisNatLit?)).getD: {ฮฑ : Type ?u.22573} โ Option ฮฑ โ ฮฑ โ ฮฑgetD (eval_prio default: ?m.22579eval_prioeval_prio default: ?m.22579 eval_prio default: ?m.22579default)
match label: ?m.21916 xโยนlabel.bind: {ฮฑ : Type ?u.22585} โ {ฮฒ : Type ?u.22584} โ Option ฮฑ โ (ฮฑ โ Option ฮฒ) โ Option ฮฒbind (ยท.1.isStrLit?: Syntax โ Option StringisStrLit?) with
| "elim" => addElim: Name โ optParam AttributeKind AttributeKind.global โ optParam Nat 1000 โ MetaM UnitaddElim decl: ?m.21848decl kind: ?m.21854kind prio: ?m.22556prio
| "move" => addMove: Name โ optParam AttributeKind AttributeKind.global โ optParam Nat 1000 โ MetaM UnitaddMove decl: ?m.21848decl kind: ?m.21854kind prio: ?m.22556prio
| "squash" => addSquash: Name โ optParam AttributeKind AttributeKind.global โ optParam Nat 1000 โ MetaM UnitaddSquash decl: ?m.21848decl kind: ?m.21854kind prio: ?m.22556prio
| none: {ฮฑ : Type ?u.21875} โ Option ฮฑnone => addInfer: Name โ optParam AttributeKind AttributeKind.global โ optParam Nat 1000 โ MetaM UnitaddInfer decl: ?m.21848decl kind: ?m.21854kind prio: ?m.22556prio
| _ => unreachable!: ?m.22848unreachable!
}
```