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.
/-
Copyright (c) 2019 Paul-Nicolas Madelaine. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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.1
Label
/-- elim lemma: LHS has 0 head coes and β‰₯ 1 internal coe -/ |
elim: Label
elim
/-- move lemma: LHS has 1 head coe and 0 internal coes, RHS has 0 head coes and β‰₯ 1 internal coes -/ |
move: Label
move
/-- squash lemma: LHS has β‰₯ 1 head coes and 0 internal coes, RHS has fewer head coes -/ |
squash: Label
squash
deriving
DecidableEq: Sort u β†’ Sort (max1u)
DecidableEq
,
Repr: Type u β†’ Type u
Repr
,
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: Expr
e
:
Expr: Type
Expr
) :
MetaM: Type β†’ Type
MetaM
(
Array: Type ?u.1007 β†’ Type ?u.1007
Array
Expr: Type
Expr
) := do match ←
mkCongrSimp?: Expr β†’ optParam Bool true β†’ MetaM (Option CongrTheorem)
mkCongrSimp?
e: Expr
e
.
getAppFn: Expr β†’ Expr
getAppFn
with |
none: {Ξ± : Type ?u.1031} β†’ Option Ξ±
none
=> return
e: Expr
e
.
getAppArgs: Expr β†’ Array Expr
getAppArgs
|
some: {Ξ± : Type ?u.1184} β†’ Ξ± β†’ Option Ξ±
some
{argKinds, ..} => let mut
args: ?m.1352
args
:=
#[]: Array ?m.1210
#[]
for
a: ?m.1340
a
in
e: Expr
e
.
getAppArgs: Expr β†’ Array Expr
getAppArgs
, k in argKinds do if k matches .eq then
args: ?m.1352
args
:=
args: ?m.1352
args
.
push: {Ξ± : Type ?u.1667} β†’ Array Ξ± β†’ Ξ± β†’ Array Ξ±
push
a: ?m.1340
a
return
args: Array Expr
args
/-- Count how many coercions are at the top of the expression. -/ partial def
countHeadCoes: Expr β†’ MetaM Nat
countHeadCoes
(
e: Expr
e
:
Expr: Type
Expr
) :
MetaM: Type β†’ Type
MetaM
Nat: Type
Nat
:= do if let
Expr.const: Name β†’ List Level β†’ Expr
Expr.const
fn: Name
fn
.. :=
e: Expr
e
.
getAppFn: Expr β†’ Expr
getAppFn
then if let
some: {Ξ± : Type ?u.5052} β†’ Ξ± β†’ Option Ξ±
some
info: CoeFnInfo
info
←
getCoeFnInfo?: Name β†’ CoreM (Option CoeFnInfo)
getCoeFnInfo?
fn: Name
fn
then if
e: Expr
e
.
getAppNumArgs: Expr β†’ Nat
getAppNumArgs
>=
info: CoeFnInfo
info
.
numArgs: CoeFnInfo β†’ Nat
numArgs
then return (←
countHeadCoes: Expr β†’ MetaM Nat
countHeadCoes
(
e: Expr
e
.
getArg!: (e : Expr) β†’ Nat β†’ optParam Nat (Expr.getAppNumArgs e) β†’ Expr
getArg!
info: CoeFnInfo
info
.
coercee: CoeFnInfo β†’ Nat
coercee
)) +
1: ?m.5169
1
return
0: ?m.5946
0
/-- Count how many coercions are inside the expression, including the top ones. -/ partial def
countCoes: Expr β†’ MetaM Nat
countCoes
(
e: Expr
e
:
Expr: Type
Expr
) :
MetaM: Type β†’ Type
MetaM
Nat: Type
Nat
:=
lambdaTelescope: {n : Type β†’ Type ?u.7417} β†’ [inst : MonadControlT MetaM n] β†’ [inst : Monad n] β†’ {Ξ± : Type} β†’ Expr β†’ (Array Expr β†’ Expr β†’ n Ξ±) β†’ n Ξ±
lambdaTelescope
e: Expr
e
fun
_: ?m.7458
_
e: ?m.7461
e
=> do if let
Expr.const: Name β†’ List Level β†’ Expr
Expr.const
fn: Name
fn
.. :=
e: ?m.7461
e
.
getAppFn: Expr β†’ Expr
getAppFn
then if let
some: {Ξ± : Type ?u.7484} β†’ Ξ± β†’ Option Ξ±
some
info: CoeFnInfo
info
←
getCoeFnInfo?: Name β†’ CoreM (Option CoeFnInfo)
getCoeFnInfo?
fn: Name
fn
then if
e: ?m.7461
e
.
getAppNumArgs: Expr β†’ Nat
getAppNumArgs
>=
info: CoeFnInfo
info
.
numArgs: CoeFnInfo β†’ Nat
numArgs
then let mut
coes: ?m.7898
coes
:= (←
countHeadCoes: Expr β†’ MetaM Nat
countHeadCoes
(
e: ?m.7461
e
.
getArg!: (e : Expr) β†’ Nat β†’ optParam Nat (Expr.getAppNumArgs e) β†’ Expr
getArg!
info: CoeFnInfo
info
.
coercee: CoeFnInfo β†’ Nat
coercee
)) +
1: ?m.7760
1
for
i: ?m.7892
i
in [
info: CoeFnInfo
info
.
numArgs: CoeFnInfo β†’ Nat
numArgs
:
e: ?m.7461
e
.
getAppNumArgs: Expr β†’ Nat
getAppNumArgs
] do
coes: ?m.7953
coes
:=
coes: ?m.7898
coes
+ (←
countCoes: Expr β†’ MetaM Nat
countCoes
(
e: ?m.7461
e
.
getArg!: (e : Expr) β†’ Nat β†’ optParam Nat (Expr.getAppNumArgs e) β†’ Expr
getArg!
i: ?m.7892
i
)) return
coes: ?m.8157
coes
return
(← (← getSimpArgs e).mapM countCoes): ?m.8940
(←
(← getSimpArgs e): ?m.8850
(←
getSimpArgs: Expr β†’ MetaM (Array Expr)
getSimpArgs
(← getSimpArgs e): ?m.8850
e: ?m.7461
e
(← 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 Nat
countCoes
(← (← 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.9010
0
/-- Count how many coercions are inside the expression, excluding the top ones. -/ def
countInternalCoes: Expr β†’ MetaM Nat
countInternalCoes
(
e: Expr
e
:
Expr: Type
Expr
) :
MetaM: Type β†’ Type
MetaM
Nat: Type
Nat
:= return
(← countCoes e) - (← countHeadCoes e): ?m.11955
(←
countCoes: Expr β†’ MetaM Nat
countCoes
(← countCoes e) - (← countHeadCoes e): ?m.11955
e: Expr
e
(← countCoes e) - (← countHeadCoes e): ?m.11955
) - (←
countHeadCoes: Expr β†’ MetaM Nat
countHeadCoes
(← countCoes e) - (← countHeadCoes e): ?m.11955
e: Expr
e
(← countCoes e) - (← countHeadCoes e): ?m.11955
)
/-- Classifies a declaration of type `ty` as a `norm_cast` rule. -/ def
classifyType: Expr β†’ MetaM Label
classifyType
(
ty: Expr
ty
:
Expr: Type
Expr
) :
MetaM: Type β†’ Type
MetaM
Label: Type
Label
:=
forallTelescopeReducing: {n : Type β†’ Type ?u.12346} β†’ [inst : MonadControlT MetaM n] β†’ [inst : Monad n] β†’ {Ξ± : Type} β†’ Expr β†’ (Array Expr β†’ Expr β†’ n Ξ±) β†’ n Ξ±
forallTelescopeReducing
ty: Expr
ty
fun
_: ?m.12387
_
ty: ?m.12390
ty
=> do let
ty: ?m.12465
ty
←
whnf: Expr β†’ MetaM Expr
whnf
ty: ?m.12390
ty
let (
lhs: Expr
lhs
,
rhs: Expr
rhs
) ← if
ty: ?m.12465
ty
.
isAppOfArity: Expr β†’ Name β†’ Nat β†’ Bool
isAppOfArity
``
Eq: {Ξ± : Sort u_1} β†’ Ξ± β†’ Ξ± β†’ Prop
Eq
3: ?m.12480
3
then
pure: {f : Type ?u.12615 β†’ Type ?u.12614} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.12615} β†’ Ξ± β†’ f Ξ±
pure
pure (ty.getArg! 1, ty.getArg! 2): MetaM (?m.12472 y✝)
(
ty: ?m.12465
ty
pure (ty.getArg! 1, ty.getArg! 2): MetaM (?m.12472 y✝)
.
getArg!: (e : Expr) β†’ Nat β†’ optParam Nat (Expr.getAppNumArgs e) β†’ Expr
getArg!
pure (ty.getArg! 1, ty.getArg! 2): MetaM (?m.12472 y✝)
1: ?m.12647
1
pure (ty.getArg! 1, ty.getArg! 2): MetaM (?m.12472 y✝)
,
ty: ?m.12465
ty
pure (ty.getArg! 1, ty.getArg! 2): MetaM (?m.12472 y✝)
.
getArg!: (e : Expr) β†’ Nat β†’ optParam Nat (Expr.getAppNumArgs e) β†’ Expr
getArg!
pure (ty.getArg! 1, ty.getArg! 2): MetaM (?m.12472 y✝)
2: ?m.12655
2
pure (ty.getArg! 1, ty.getArg! 2): MetaM (?m.12472 y✝)
)
else if
ty: ?m.12465
ty
.
isAppOfArity: Expr β†’ Name β†’ Nat β†’ Bool
isAppOfArity
``
Iff: Prop β†’ Prop β†’ Prop
Iff
2: ?m.12728
2
then
pure: {f : Type ?u.12830 β†’ Type ?u.12829} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.12830} β†’ Ξ± β†’ f Ξ±
pure
pure (ty.getArg! 0, ty.getArg! 1): MetaM (?m.12472 y✝)
(
ty: ?m.12465
ty
pure (ty.getArg! 0, ty.getArg! 1): MetaM (?m.12472 y✝)
.
getArg!: (e : Expr) β†’ Nat β†’ optParam Nat (Expr.getAppNumArgs e) β†’ Expr
getArg!
pure (ty.getArg! 0, ty.getArg! 1): MetaM (?m.12472 y✝)
0: ?m.12862
0
pure (ty.getArg! 0, ty.getArg! 1): MetaM (?m.12472 y✝)
,
ty: ?m.12465
ty
pure (ty.getArg! 0, ty.getArg! 1): MetaM (?m.12472 y✝)
.
getArg!: (e : Expr) β†’ Nat β†’ optParam Nat (Expr.getAppNumArgs e) β†’ Expr
getArg!
pure (ty.getArg! 0, ty.getArg! 1): MetaM (?m.12472 y✝)
1: ?m.12870
1
pure (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✝)
throwError
throwError "norm_cast: lemma must be = or ↔, but is{indentExpr ty}": MetaM (?m.12472 y✝)
"norm_cast: lemma must be = or ↔, but is{
indentExpr: Expr β†’ MessageData
indentExpr
throwError "norm_cast: lemma must be = or ↔, but is{indentExpr ty}": MetaM (?m.12472 y✝)
ty: ?m.12465
ty
throwError "norm_cast: lemma must be = or ↔, but is{indentExpr ty}": MetaM (?m.12472 y✝)
}"
let
lhsCoes: ?m.13319
lhsCoes
←
countCoes: Expr β†’ MetaM Nat
countCoes
lhs: Expr
lhs
if
lhsCoes: ?m.13319
lhsCoes
=
0: ?m.13332
0
then
throwError "norm_cast: badly shaped lemma, lhs must contain at least one coe{indentExpr lhs}": MetaM (?m.13326 y✝)
throwError
throwError "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 β†’ MessageData
indentExpr
throwError "norm_cast: badly shaped lemma, lhs must contain at least one coe{indentExpr lhs}": MetaM (?m.13326 y✝)
lhs: Expr
lhs
throwError "norm_cast: badly shaped lemma, lhs must contain at least one coe{indentExpr lhs}": MetaM (?m.13326 y✝)
}"
let
lhsHeadCoes: ?m.13650
lhsHeadCoes
←
countHeadCoes: Expr β†’ MetaM Nat
countHeadCoes
lhs: Expr
lhs
let
rhsHeadCoes: ?m.13699
rhsHeadCoes
←
countHeadCoes: Expr β†’ MetaM Nat
countHeadCoes
rhs: Expr
rhs
let
rhsInternalCoes: ?m.13748
rhsInternalCoes
←
countInternalCoes: Expr β†’ MetaM Nat
countInternalCoes
rhs: Expr
rhs
if
lhsHeadCoes: ?m.13650
lhsHeadCoes
=
0: ?m.13752
0
then return
Label.elim: Label
Label.elim
else if
lhsHeadCoes: ?m.13650
lhsHeadCoes
=
1: ?m.13803
1
then do unless
rhsHeadCoes: ?m.13699
rhsHeadCoes
=
0: ?m.13833
0
do
throwError "norm_cast: badly shaped lemma, rhs can't start with coe{indentExpr rhs}": MetaM (?m.13827 y✝)
throwError
throwError "norm_cast: badly shaped lemma, rhs can't start with coe{indentExpr rhs}": MetaM (?m.13827 y✝)
"norm_cast: badly shaped lemma, rhs can't start with coe{
indentExpr: Expr β†’ MessageData
indentExpr
throwError "norm_cast: badly shaped lemma, rhs can't start with coe{indentExpr rhs}": MetaM (?m.13827 y✝)
rhs: Expr
rhs
throwError "norm_cast: badly shaped lemma, rhs can't start with coe{indentExpr rhs}": MetaM (?m.13827 y✝)
}"
if
rhsInternalCoes: ?m.13748
rhsInternalCoes
=
0: ?m.14104
0
then return
Label.squash: Label
Label.squash
else return
Label.move: Label
Label.move
else if
rhsHeadCoes: ?m.13699
rhsHeadCoes
<
lhsHeadCoes: ?m.13650
lhsHeadCoes
then do return
Label.squash: Label
Label.squash
else do throwError "norm_cast: badly shaped shaped squash lemma, rhs must have fewer head coes than lhs{
indentExpr: Expr β†’ MessageData
indentExpr
ty: ?m.12465
ty
}" /-- The `push_cast` simp attribute. -/ initialize
pushCastExt: SimpExtension
pushCastExt
:
SimpExtension: Type
SimpExtension
←
registerSimpAttr: Name β†’ String β†’ autoParam Name _auto✝ β†’ IO SimpExtension
registerSimpAttr
`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 β†’ NormCastExtension
NormCastExtension
where /-- A simp set which lifts coercion arrows to the top level. -/ up :
SimpExtension: Type
SimpExtension
/-- A simp set which pushes coercion arrows to the leaves. -/ down :
SimpExtension: Type
SimpExtension
/-- A simp set which simplifies transitive coercions. -/ squash :
SimpExtension: Type
SimpExtension
deriving
Inhabited: Sort u β†’ Sort (max1u)
Inhabited
/-- The `norm_cast` extension data. -/ initialize
normCastExt: NormCastExtension
normCastExt
:
NormCastExtension: Type
NormCastExtension
←
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
{ up := ← mkSimpExt (decl_name% ++ `up) down := ← mkSimpExt (decl_name% ++ `down) squash := ← mkSimpExt (decl_name% ++ `squash) }: NormCastExtension
(
decl_name%: Name
decl_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
{ up := ← mkSimpExt (decl_name% ++ `up) down := ← mkSimpExt (decl_name% ++ `down) squash := ← mkSimpExt (decl_name% ++ `squash) }: NormCastExtension
(
decl_name%: Name
decl_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
{ up := ← mkSimpExt (decl_name% ++ `up) down := ← mkSimpExt (decl_name% ++ `down) squash := ← mkSimpExt (decl_name% ++ `squash) }: NormCastExtension
(
decl_name%: Name
decl_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 (
decl: Name
decl
:
Name: Type
Name
) (kind :=
AttributeKind.global: AttributeKind
AttributeKind.global
) (
prio: optParam ?m.19604 1000
prio
:=
eval_prio default: ?m.19606
eval_prio
eval_prio default: ?m.19606
eval_prio default: ?m.19606
default
) :
MetaM: Type β†’ Type
MetaM
Unit: Type
Unit
:=
addSimpTheorem: SimpExtension β†’ Name β†’ Bool β†’ Bool β†’ AttributeKind β†’ Nat β†’ MetaM Unit
addSimpTheorem
normCastExt: NormCastExtension
normCastExt
.up
decl: Name
decl
(post :=
true: Bool
true
) (inv :=
false: Bool
false
) kind
prio: optParam Nat 1000
prio
/-- `addMove decl` adds `decl` as a `move` lemma to the cache. -/ def addMove (
decl: Name
decl
:
Name: Type
Name
) (kind :=
AttributeKind.global: AttributeKind
AttributeKind.global
) (
prio: optParam Nat 1000
prio
:=
eval_prio default: ?m.19803
eval_prio
eval_prio default: ?m.19803
eval_prio default: ?m.19803
default
) :
MetaM: Type β†’ Type
MetaM
Unit: Type
Unit
:= do
addSimpTheorem: SimpExtension β†’ Name β†’ Bool β†’ Bool β†’ AttributeKind β†’ Nat β†’ MetaM Unit
addSimpTheorem
pushCastExt: SimpExtension
pushCastExt
decl: Name
decl
(post :=
true: Bool
true
) (inv :=
false: Bool
false
) kind
prio: optParam Nat 1000
prio
addSimpTheorem: SimpExtension β†’ Name β†’ Bool β†’ Bool β†’ AttributeKind β†’ Nat β†’ MetaM Unit
addSimpTheorem
normCastExt: NormCastExtension
normCastExt
.up
decl: Name
decl
(post :=
true: Bool
true
) (inv :=
true: Bool
true
) kind
prio: optParam Nat 1000
prio
addSimpTheorem: SimpExtension β†’ Name β†’ Bool β†’ Bool β†’ AttributeKind β†’ Nat β†’ MetaM Unit
addSimpTheorem
normCastExt: NormCastExtension
normCastExt
.down
decl: Name
decl
(post :=
true: Bool
true
) (inv :=
false: Bool
false
) kind
prio: optParam Nat 1000
prio
/-- `addSquash decl` adds `decl` as a `squash` lemma to the cache. -/ def
addSquash: Name β†’ optParam AttributeKind AttributeKind.global β†’ optParam Nat 1000 β†’ MetaM Unit
addSquash
(
decl: Name
decl
:
Name: Type
Name
) (kind :=
AttributeKind.global: AttributeKind
AttributeKind.global
) (
prio: optParam Nat 1000
prio
:=
eval_prio default: ?m.20316
eval_prio
eval_prio default: ?m.20316
eval_prio default: ?m.20316
default
) :
MetaM: Type β†’ Type
MetaM
Unit: Type
Unit
:= do
addSimpTheorem: SimpExtension β†’ Name β†’ Bool β†’ Bool β†’ AttributeKind β†’ Nat β†’ MetaM Unit
addSimpTheorem
pushCastExt: SimpExtension
pushCastExt
decl: Name
decl
(post :=
true: Bool
true
) (inv :=
false: Bool
false
) kind
prio: optParam Nat 1000
prio
addSimpTheorem: SimpExtension β†’ Name β†’ Bool β†’ Bool β†’ AttributeKind β†’ Nat β†’ MetaM Unit
addSimpTheorem
normCastExt: NormCastExtension
normCastExt
.squash
decl: Name
decl
(post :=
true: Bool
true
) (inv :=
false: Bool
false
) kind
prio: optParam Nat 1000
prio
addSimpTheorem: SimpExtension β†’ Name β†’ Bool β†’ Bool β†’ AttributeKind β†’ Nat β†’ MetaM Unit
addSimpTheorem
normCastExt: NormCastExtension
normCastExt
.down
decl: Name
decl
(post :=
true: Bool
true
) (inv :=
false: Bool
false
) kind
prio: optParam Nat 1000
prio
/-- `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 (
decl: Name
decl
:
Name: Type
Name
) (kind :=
AttributeKind.global: AttributeKind
AttributeKind.global
) (
prio: optParam ?m.20816 1000
prio
:=
eval_prio default: ?m.20818
eval_prio
eval_prio default: ?m.20818
eval_prio default: ?m.20818
default
) :
MetaM: Type β†’ Type
MetaM
Unit: Type
Unit
:= do let
ty: ?m.21136
ty
:=
(← getConstInfo decl): ?m.21133
(←
getConstInfo: {m : Type β†’ Type} β†’ [inst : Monad m] β†’ [inst : MonadEnv m] β†’ [inst : MonadError m] β†’ Name β†’ m ConstantInfo
getConstInfo
(← getConstInfo decl): ?m.21133
decl: Name
decl
(← getConstInfo decl): ?m.21133
)
.
type: ConstantInfo β†’ Expr
type
match ←
classifyType: Expr β†’ MetaM Label
classifyType
ty: ?m.21136
ty
with |
Label.elim: Label
Label.elim
=> addElim
decl: Name
decl
kind
prio: optParam Nat 1000
prio
|
Label.squash: Label
Label.squash
=>
addSquash: Name β†’ optParam AttributeKind AttributeKind.global β†’ optParam Nat 1000 β†’ MetaM Unit
addSquash
decl: Name
decl
kind
prio: optParam Nat 1000
prio
|
Label.move: Label
Label.move
=> addMove
decl: Name
decl
kind
prio: optParam Nat 1000
prio
namespace Attr /-- The possible `norm_cast` kinds: `elim`, `move`, or `squash`. -/ syntax
normCastLabel: ParserDescr
normCastLabel
:=
&: 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: ParserDescr
norm_cast
) "norm_cast" (
ppSpace: Parser.Parser
ppSpace
normCastLabel: ParserDescr
normCastLabel
)? (
ppSpace: Parser.Parser
ppSpace
num)? : attr end Attr initialize
registerBuiltinAttribute: AttributeImpl β†’ IO Unit
registerBuiltinAttribute
{ name :=
`norm_cast: Name
`norm_cast
descr :=
"attribute for norm_cast": String
"attribute for norm_cast"
add := fun
decl: ?m.21848
decl
stx: ?m.21851
stx
kind: ?m.21854
kind
=>
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 }, userNames := { 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| norm_cast $[$
label: ?m.21916 x✝
label
:
normCastLabel: ParserDescr
normCastLabel
]? $[$
prio: ?m.22423
prio
]?) :=
stx: ?m.21851
stx
|
unreachable!: ?m.22454
unreachable!
let
prio: ?m.22556
prio
:= (
prio: ?m.22324 x✝
prio
.
bind: {Ξ± : Type ?u.22558} β†’ {Ξ² : Type ?u.22557} β†’ Option Ξ± β†’ (Ξ± β†’ Option Ξ²) β†’ Option Ξ²
bind
(Β·.1.
isNatLit?: Syntax β†’ Option Nat
isNatLit?
)).
getD: {Ξ± : Type ?u.22573} β†’ Option Ξ± β†’ Ξ± β†’ Ξ±
getD
(
eval_prio default: ?m.22579
eval_prio
eval_prio default: ?m.22579
eval_prio default: ?m.22579
default
) match
label: ?m.21916 x✝¹
label
.
bind: {Ξ± : Type ?u.22585} β†’ {Ξ² : Type ?u.22584} β†’ Option Ξ± β†’ (Ξ± β†’ Option Ξ²) β†’ Option Ξ²
bind
(Β·.1.
isStrLit?: Syntax β†’ Option String
isStrLit?
) with | "elim" => addElim
decl: ?m.21848
decl
kind: ?m.21854
kind
prio: ?m.22556
prio
| "move" => addMove
decl: ?m.21848
decl
kind: ?m.21854
kind
prio: ?m.22556
prio
| "squash" =>
addSquash: Name β†’ optParam AttributeKind AttributeKind.global β†’ optParam Nat 1000 β†’ MetaM Unit
addSquash
decl: ?m.21848
decl
kind: ?m.21854
kind
prio: ?m.22556
prio
|
none: {Ξ± : Type ?u.21875} β†’ Option Ξ±
none
=> addInfer
decl: ?m.21848
decl
kind: ?m.21854
kind
prio: ?m.22556
prio
| _ =>
unreachable!: ?m.22848
unreachable!
}