norm_num
core functionality #
This file sets up the norm_num
tactic and the @[norm_num]
attribute,
which allow for plugging in new normalization functionality around a simp-based driver.
The actual behavior is in @[norm_num]
-tagged definitions in Tactic.NormNum.Basic
and elsewhere.
Attribute for identifying norm_num
extensions.
Equations
- One or more equations did not get rendered due to their size.
The element is equal to the coercion of the natural number.
out : a = ↑n
Assert that an element of a semiring is equal to the coercion of some natural number.
Instances For
A "raw nat cast" is an expression of the form (Nat.rawCast lit : α)
where lit
is a raw
natural number literal. These expressions are used by tactics like ring
to decrease the number
of typeclass arguments required in each use of a number literal at type α
.
Equations
- Nat.rawCast n = ↑n
A "raw int cast" is an expression of the form:
(Nat.rawCast lit : α)
wherelit
is a raw natural number literal(Int.rawCast (Int.negOfNat lit) : α)
wherelit
is a nonzero raw natural number literal
(That is, we only actually use this function for negative integers.) This representation is used by
tactics like ring
to decrease the number of typeclass arguments required in each use of a number
literal at type α
.
Equations
- Int.rawCast n = ↑n
Represent an integer as a typed expression.
Equations
- One or more equations did not get rendered due to their size.
A shortcut (non)instance for AddMonoidWithOne ℕ
to shrink generated proofs.
Equations
- Mathlib.Meta.NormNum.instAddMonoidWithOneNat = inferInstance
A shortcut (non)instance for Ring ℤ
to shrink generated proofs.
Equations
- Mathlib.Meta.NormNum.instRingInt = inferInstance
- mk: ∀ {α : Type u_1} [inst : Ring α] {a : α} {num : ℤ} {denom : ℕ} (inv : Invertible ↑denom), a = ↑num * ⅟↑denom → Mathlib.Meta.NormNum.IsRat a num denom
Assert that an element of a ring is equal to num / denom
(and denom
is invertible so that this makes sense).
We will usually also have num
and denom
coprime,
although this is not part of the definition.
Instances For
A "raw rat cast" is an expression of the form:
(Nat.rawCast lit : α)
wherelit
is a raw natural number literal(Int.rawCast (Int.negOfNat lit) : α)
wherelit
is a nonzero raw natural number literal(Rat.rawCast n d : α)
wheren
is a raw int cast,d
is a raw nat cast, andd
is not 1 or 0.
This representation is used by tactics like ring
to decrease the number of typeclass arguments
required in each use of a number literal at type α
.
Equations
- Rat.rawCast n d = ↑n / ↑d
Represent an integer as a typed expression.
Equations
- One or more equations did not get rendered due to their size.
A shortcut (non)instance for Ring ℚ
to shrink generated proofs.
Equations
- Mathlib.Meta.NormNum.instRingRat = inferInstance
A shortcut (non)instance for DivisionRing ℚ
to shrink generated proofs.
Equations
- Mathlib.Meta.NormNum.instDivisionRingRat = inferInstance
- isBool: Bool → Lean.Expr → Mathlib.Meta.NormNum.Result'
Untyped version of
Result.isBool
. - isNat: Lean.Expr → Lean.Expr → Lean.Expr → Mathlib.Meta.NormNum.Result'
Untyped version of
Result.isNat
. - isNegNat: Lean.Expr → Lean.Expr → Lean.Expr → Mathlib.Meta.NormNum.Result'
Untyped version of
Result.isNegNat
. - isRat: Lean.Expr → ℚ → Lean.Expr → Lean.Expr → Lean.Expr → Mathlib.Meta.NormNum.Result'
Untyped version of
Result.isRat
.
The result of norm_num
running on an expression x
of type α
.
Untyped version of Result
.
Instances For
Equations
- Mathlib.Meta.NormNum.instInhabitedResult' = { default := Mathlib.Meta.NormNum.Result'.isBool default default }
The result of norm_num
running on an expression x
of type α
.
Equations
- Mathlib.Meta.NormNum.instInhabitedResult = inferInstanceAs (Inhabited Mathlib.Meta.NormNum.Result')
The result is proof : x
, where x
is a (true) proposition.
Equations
- Mathlib.Meta.NormNum.Result.isTrue = Mathlib.Meta.NormNum.Result'.isBool true
The result is proof : ¬x¬x
, where x
is a (false) proposition.
Equations
- Mathlib.Meta.NormNum.Result.isFalse = Mathlib.Meta.NormNum.Result'.isBool false
The result is lit : ℕ
(a raw nat literal) and proof : isNat x lit
.
Equations
- Mathlib.Meta.NormNum.Result.isNat = Mathlib.Meta.NormNum.Result'.isNat
The result is -lit
where lit
is a raw nat literal
and proof : isInt x (.negOfNat lit)
.
Equations
- Mathlib.Meta.NormNum.Result.isNegNat = Mathlib.Meta.NormNum.Result'.isNegNat
The result is proof : isRat x n d
, where n
is either .ofNat lit
or .negOfNat lit
with lit
a raw nat literal and d
is a raw nat literal (not 0 or 1),
and q
is the value of n / d
.
Equations
- Mathlib.Meta.NormNum.Result.isRat = Mathlib.Meta.NormNum.Result'.isRat
A shortcut (non)instance for AddMonoidWithOne α
from Ring α
to shrink generated proofs.
Equations
- Mathlib.Meta.NormNum.instAddMonoidWithOne = inferInstance
The result is z : ℤ
and proof : isNat x z
.
Equations
- One or more equations did not get rendered due to their size.
Returns the rational number that is the result of norm_num
evaluation.
Equations
- One or more equations did not get rendered due to their size.
Convert undef
to none
to make an LOption
into an Option
.
Equations
- Lean.LOption.toOption x = match x with | Lean.LOption.some a => some a | x => none
Helper function to synthesize a typed AddMonoidWithOne α
expression.
Equations
- One or more equations did not get rendered due to their size.
Helper function to synthesize a typed Semiring α
expression.
Equations
- One or more equations did not get rendered due to their size.
Helper function to synthesize a typed Ring α
expression.
Equations
- One or more equations did not get rendered due to their size.
Helper function to synthesize a typed DivisionRing α
expression.
Equations
- One or more equations did not get rendered due to their size.
Helper function to synthesize a typed OrderedSemiring α
expression.
Equations
- One or more equations did not get rendered due to their size.
Helper function to synthesize a typed OrderedRing α
expression.
Equations
- One or more equations did not get rendered due to their size.
Helper function to synthesize a typed LinearOrderedField α
expression.
Equations
- One or more equations did not get rendered due to their size.
Helper function to synthesize a typed CharZero α
expression given Ring α
.
Equations
- One or more equations did not get rendered due to their size.
Helper function to synthesize a typed CharZero α
expression given Ring α
, if it exists.
Equations
- One or more equations did not get rendered due to their size.
Helper function to synthesize a typed CharZero α
expression given AddMonoidWithOne α
.
Equations
- One or more equations did not get rendered due to their size.
Helper function to synthesize a typed CharZero α
expression given AddMonoidWithOne α
, if it
exists.
Equations
- One or more equations did not get rendered due to their size.
Helper function to synthesize a typed CharZero α
expression given DivisionRing α
.
Equations
- One or more equations did not get rendered due to their size.
Helper function to synthesize a typed CharZero α
expression given DivisionRing α
, if it
exists.
Equations
- One or more equations did not get rendered due to their size.
Extract from a Result
the integer value (as both a term and an expression),
and the proof that the original expression is equal to this integer.
Equations
- One or more equations did not get rendered due to their size.
Extract from a Result
the rational value (as both a term and an expression),
and the proof that the original expression is equal to this rational number.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Given a NormNum.Result e
(which uses IsNat
, IsInt
, IsRat
to express equality to a rational
numeral), converts it to an equality e = Nat.rawCast n
, e = Int.rawCast n
, or
e = Rat.rawCast n d
to a raw cast expression, so it can be used for rewriting.
Equations
- One or more equations did not get rendered due to their size.
Result.toRawEq
but providing an integer. Given a NormNum.Result e
for something known to be an
integer (which uses IsNat
or IsInt
to express equality to an integer numeral), converts it to
an equality e = Nat.rawCast n
or e = Int.rawCast n
to a raw cast expression, so it can be used
for rewriting. Gives none
if not an integer.
Equations
- One or more equations did not get rendered due to their size.
Constructs a Result
out of a raw nat cast. Assumes e
is a raw nat cast expression.
Equations
- One or more equations did not get rendered due to their size.
Constructs a Result
out of a raw int cast.
Assumes e
is a raw int cast expression denoting n
.
Equations
- One or more equations did not get rendered due to their size.
Constructs a Result
out of a raw rat cast.
Assumes e
is a raw rat cast expression denoting n
.
Equations
- One or more equations did not get rendered due to their size.
The result depends on whether q : ℚ
happens to be an integer, in which case the result is
.isInt ..
whereas otherwise it's .isRat ..
.
Equations
- One or more equations did not get rendered due to their size.
Returns the rational number that is the result of norm_num
evaluation, along with a proof
that the denominator is nonzero in the isRat
case.
Equations
- One or more equations did not get rendered due to their size.
Constructs an ofNat
application a'
with the canonical instance, together with a proof that
the instance is equal to the result of Nat.cast
on the given AddMonoidWithOne
instance.
This function is performance-critical, as many higher level tactics have to construct numerals. So rather than using typeclass search we hardcode the (relatively small) set of solutions to the typeclass problem.
Equations
- One or more equations did not get rendered due to their size.
Convert a Result
to a Simp.Result
.
Equations
- One or more equations did not get rendered due to their size.
The extension should be run in the
pre
phase when used as simp plugin.pre : BoolThe extension should be run in the
post
phase when used as simp plugin.post : BoolAttempts to prove an expression is equal to some explicit number of the relevant type.
eval : {u : Lean.Level} → {α : Q(Type u)} → (e : Q(«$α»)) → Lean.MetaM (Mathlib.Meta.NormNum.Result e)The name of the
norm_num
extension.
A extension for norm_num
.
Instances For
Read a norm_num
extension from a declaration of the right type.
Equations
- Mathlib.Meta.NormNum.mkNormNumExt n = do let __discr ← read match __discr with | { env := env, opts := opts } => liftM (IO.ofExcept (Mathlib.Meta.NormNum.mkNormNumExt.impl✝ n env opts))
Each norm_num
extension is labelled with a collection of patterns
which determine the expressions to which it should be applied.
Equations
The tree of
norm_num
extensions.Erased
norm_num
s.erased : Lean.PHashSet Lean.Name
The state of the norm_num
extension environment
Instances For
Equations
- Mathlib.Meta.NormNum.instInhabitedNormNums = { default := { tree := default, erased := default } }
Environment extensions for norm_num
declarations
Run each registered norm_num
extension on an expression, returning a NormNum.Result
.
Equations
- One or more equations did not get rendered due to their size.
Run each registered norm_num
extension on a typed expression e : α
,
returning a typed expression lit : ℕ
, and a proof of isNat e lit
.
Equations
- One or more equations did not get rendered due to their size.
Run each registered norm_num
extension on a typed expression e : α
,
returning a typed expression lit : ℕ
, and a proof of isNat e lit
.
Equations
- One or more equations did not get rendered due to their size.
Run each registered norm_num
extension on a typed expression e : α
,
returning a typed expression lit : ℤ
, and a proof of IsInt e lit
in expression form.
Equations
- One or more equations did not get rendered due to their size.
Run each registered norm_num
extension on a typed expression e : α
,
returning a rational number, typed expressions n : ℚ
and d : ℚ
for the numerator and
denominator, and a proof of IsRat e n d
in expression form.
Equations
- One or more equations did not get rendered due to their size.
Test if an expression represents an explicit number written in normal form.
Erases a name marked norm_num
by adding it to the state's erased
field and
removing it from the state's list of Entry
s.
Equations
- Mathlib.Meta.NormNum.NormNums.eraseCore d declName = { tree := d.tree, erased := Lean.PersistentHashSet.insert d.erased declName }
Erase a name marked as a norm_num
attribute.
Check that it does in fact have the norm_num
attribute by making sure it names a NormNumExt
found somewhere in the state's tree, and is not erased.
Equations
- One or more equations did not get rendered due to their size.
A simp plugin which calls NormNum.eval
.
Equations
- One or more equations did not get rendered due to their size.
Constructs a proof that the original expression is true
given a simp result which simplifies the target to True
.
Equations
- One or more equations did not get rendered due to their size.
A discharger which calls norm_num
.
A Methods
implementation which calls norm_num
.
Traverses the given expression using simp and normalises any numbers it finds.
The core of norm_num
as a tactic in MetaM
.
g
: The goal to simplifyctx
: The simp context, constructed bymkSimpContext
and containing any additional simp rules we want to usefvarIdsToSimp
: The selected set of hypotheses used in the location argumentsimplifyTarget
: true if the target is selected in the location argumentuseSimp
: true if we usednorm_num
instead ofnorm_num1
Equations
- One or more equations did not get rendered due to their size.
Constructs a simp context from the simp argument syntax.
Equations
- One or more equations did not get rendered due to their size.
Elaborates a call to norm_num only? [args]
or norm_num1
.
args
: the(simpArgs)?
syntax for simp argumentsloc
: the(location)?
syntax for the optional location argumentsimpOnly
: true ifonly
was used innorm_num
useSimp
: false ifnorm_num1
was used, in which case only the structural parts ofsimp
will be used, not any of the post-processing thatsimp only
does without lemmas
Equations
- One or more equations did not get rendered due to their size.
Normalize numerical expressions. Supports the operations +
-
*
/
⁻¹⁻¹
^
and %
over numerical types such as ℕ
, ℤ
, ℚ
, ℝ
, ℂ
and some general algebraic types,
and can prove goals of the form A = B
, A ≠ B≠ B
, A < B
and A ≤ B≤ B
, where A
and B
are
numerical expressions. It also has a relatively simple primality prover.
Equations
- One or more equations did not get rendered due to their size.
Basic version of norm_num
that does not call simp
.
Equations
- One or more equations did not get rendered due to their size.
Basic version of norm_num
that does not call simp
.
Equations
- Mathlib.Tactic.normNum1Conv = Lean.ParserDescr.node `Mathlib.Tactic.normNum1Conv 1024 (Lean.ParserDescr.nonReservedSymbol "norm_num1" false)
Elaborator for norm_num1
conv tactic.
Equations
- One or more equations did not get rendered due to their size.
Normalize numerical expressions. Supports the operations +
-
*
/
⁻¹⁻¹
^
and %
over numerical types such as ℕ
, ℤ
, ℚ
, ℝ
, ℂ
and some general algebraic types,
and can prove goals of the form A = B
, A ≠ B≠ B
, A < B
and A ≤ B≤ B
, where A
and B
are
numerical expressions. It also has a relatively simple primality prover.
Equations
- One or more equations did not get rendered due to their size.
Elaborator for norm_num
conv tactic.
Equations
- One or more equations did not get rendered due to their size.
The basic usage is #norm_num e
, where e
is an expression,
which will print the norm_num
form of e
.
Syntax: #norm_num
(only
)? ([
simp lemma list ]
)? :
? expression
This accepts the same options as the #simp
command.
You can specify additional simp lemmas as usual, for example using #norm_num [f, g] : e
.
(The colon is optional but helpful for the parser.)
The only
restricts norm_num
to using only the provided lemmas, and so
#norm_num only : e
behaves similarly to norm_num1
.
Unlike norm_num
, this command does not fail when no simplifications are made.
#norm_num
understands local variables, so you can use them to introduce parameters.
Equations
- One or more equations did not get rendered due to their size.