The Result
type for norm_num
#
We set up predicates IsNat
, IsInt
, and IsRat
,
stating that an element of a ring is equal to the "normal form" of a natural number, integer,
or rational number coerced into that ring.
We then define Result e
, which contains a proof that a typed expression e : Q($α)
is equal to the coercion of an explicit natural number, integer, or rational number,
or is either true
or false
.
A shortcut (non)instance for AddMonoidWithOne α
from Ring α
to shrink generated proofs.
Equations
Instances For
Helper function to synthesize a typed AddMonoidWithOne α
expression.
Equations
Instances For
Helper function to synthesize a typed Semiring α
expression.
Equations
Instances For
Represent an integer as a "raw" typed expression.
This uses .lit (.natVal n)
internally to represent a natural number,
rather than the preferred OfNat.ofNat
form.
We use this internally to avoid unnecessary typeclass searches.
This function is the inverse of Expr.intLit!
.
Equations
Instances For
Represent an integer as a "raw" typed expression.
This .lit (.natVal n)
internally to represent a natural number,
rather than the preferred OfNat.ofNat
form.
We use this internally to avoid unnecessary typeclass searches.
Equations
Instances For
Extract the raw natlit representing the absolute value of a raw integer literal
(of the type produced by Mathlib.Meta.NormNum.mkRawIntLit
) along with an equality proof.
Equations
Instances For
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
Instances For
Assert that an element of a semiring is equal to the coercion of some natural number.
The element is equal to the coercion of the 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
Instances For
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
Instances For
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.
- mk {α : Type u} [Ring α] {a : α} {num : ℤ} {denom : ℕ} (inv : Invertible ↑denom) (eq : a = ↑num * ⅟ ↑denom) : IsRat a num denom
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 literal,d
is a raw nat literal, andd
is not1
or0
.
(where a raw int literal is of the form Int.ofNat lit
or Int.negOfNat nzlit
where lit
is a raw
nat literal)
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
Instances For
The result of norm_num
running on an expression x
of type α
.
Untyped version of Result
.
- isBool
(val : Bool)
(proof : Lean.Expr)
: Result'
Untyped version of
Result.isBool
. - isNat
(inst lit proof : Lean.Expr)
: Result'
Untyped version of
Result.isNat
. - isNegNat
(inst lit proof : Lean.Expr)
: Result'
Untyped version of
Result.isNegNat
. - isRat
(inst : Lean.Expr)
(q : ℚ)
(n d proof : Lean.Expr)
: Result'
Untyped version of
Result.isRat
.
Instances For
The result of norm_num
running on an expression x
of type α
.
Equations
Instances For
Equations
The result is proof : x
, where x
is a (true) proposition.
Equations
Instances For
The result is proof : ¬x
, where x
is a (false) proposition.
Equations
Instances For
The result is lit : ℕ
(a raw nat literal) and proof : isNat x lit
.
Equations
Instances For
The result is -lit
where lit
is a raw nat literal
and proof : isInt x (.negOfNat lit)
.
Equations
Instances For
The result is proof : isRat x n d
,
where n
is either .ofNat lit
or .negOfNat lit
with lit
a raw nat literal,
d
is a raw nat literal (not 0 or 1),
n
and d
are coprime, and q
is the value of n / d
.
Equations
Instances For
The result is z : ℤ
and proof : isNat x z
.
Equations
Instances For
The result depends on whether q : ℚ
happens to be an integer, in which case the result is
.isInt ..
whereas otherwise it's .isRat ..
.
Equations
Instances For
Equations
Returns the rational number that is the result of norm_num
evaluation.
Equations
Instances For
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
Instances For
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
Instances For
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
Instances For
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
Instances For
Constructs a Result
out of a raw nat cast. Assumes e
is a raw nat cast expression.
Equations
Instances For
Constructs a Result
out of a raw int cast.
Assumes e
is a raw int cast expression denoting n
.
Equations
Instances For
Constructs a Result
out of a raw rat cast.
Assumes e
is a raw rat cast expression denoting n
.
Equations
Instances For
Convert a Result
to a Simp.Result
.
Equations
Instances For
Given Mathlib.Meta.NormNum.Result.isBool p b
, this is the type of p
.
Note that BoolResult p b
is definitionally equal to Expr
, and if you write match b with ...
,
then in the true
branch BoolResult p true
is reducibly equal to Q($p)
and
in the false
branch it is reducibly equal to Q(¬ $p)
.
Equations
Instances For
Obtain a Result
from a BoolResult
.
Equations
Instances For
If a = b
and we can evaluate b
, then we can evaluate a
.