## 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`.

source
def Mathlib.Meta.NormNum.instAddMonoidWithOneNat :
AddMonoidWithOne ℕ

A shortcut (non)instance for `AddMonoidWithOne ℕ` to shrink generated proofs.

Equations

- Mathlib.Meta.NormNum.instAddMonoidWithOneNat = inferInstance

Instances For

source
def Mathlib.Meta.NormNum.instAddMonoidWithOne' {α : Type u} [Semiring α] :
AddMonoidWithOne α

A shortcut (non)instance for `AddMonoidWithOne α` from `Semiring α` to shrink generated proofs.

Equations

- Mathlib.Meta.NormNum.instAddMonoidWithOne' = inferInstance

Instances For

source
def Mathlib.Meta.NormNum.instAddMonoidWithOne {α : Type u} [Ring α] :
AddMonoidWithOne α

A shortcut (non)instance for `AddMonoidWithOne α` from `Ring α` to shrink generated proofs.

Equations

- Mathlib.Meta.NormNum.instAddMonoidWithOne = inferInstance

Instances For

source
theorem Mathlib.Meta.NormNum.instAtLeastTwo (n : ℕ) :
(n + 2).AtLeastTwo

A shortcut (non)instance for `Nat.AtLeastTwo (n + 2)` to shrink generated proofs.

source
def Mathlib.Meta.NormNum.inferAddMonoidWithOne {u : Lean.Level} (α : Q(Type u)) :
Lean.MetaM Q(AddMonoidWithOne «$α»)

Helper function to synthesize a typed `AddMonoidWithOne α` expression.

Equations

- Mathlib.Meta.NormNum.inferAddMonoidWithOne α = do let __do_lift ← Qq.synthInstanceQ q(AddMonoidWithOne «$α») <|> Lean.throwError (Lean.toMessageData "not an AddMonoidWithOne") pure __do_lift

Instances For

source
def Mathlib.Meta.NormNum.inferSemiring {u : Lean.Level} (α : Q(Type u)) :
Lean.MetaM Q(Semiring «$α»)

Helper function to synthesize a typed `Semiring α` expression.

Equations

- Mathlib.Meta.NormNum.inferSemiring α = do let __do_lift ← Qq.synthInstanceQ q(Semiring «$α») <|> Lean.throwError (Lean.toMessageData "not a semiring") pure __do_lift

Instances For

source
def Mathlib.Meta.NormNum.inferRing {u : Lean.Level} (α : Q(Type u)) :
Lean.MetaM Q(Ring «$α»)

Helper function to synthesize a typed `Ring α` expression.

Equations

- Mathlib.Meta.NormNum.inferRing α = do let __do_lift ← Qq.synthInstanceQ q(Ring «$α») <|> Lean.throwError (Lean.toMessageData "not a ring") pure __do_lift

Instances For

source
def Mathlib.Meta.NormNum.mkRawIntLit (n : ℤ) :
Q(ℤ)

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!`.

Instances For

source
def Mathlib.Meta.NormNum.mkRawRatLit (q : ℚ) :
Q(ℚ)

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.

Instances For

source
def Mathlib.Meta.NormNum.rawIntLitNatAbs (n : Q(ℤ)) :
(m : Q(ℕ)) × Q(«$n».natAbs = «$m»)

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

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Meta.NormNum.mkOfNat {u : Lean.Level} (α : Q(Type u)) (_sα : Q(AddMonoidWithOne «$α»)) (lit : Q(ℕ)) :
Lean.MetaM ((a' : Q(«$α»)) × Q(↑«$lit» = «$a'»))

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.

Instances For

source
structure Mathlib.Meta.NormNum.IsNat {α : Type u} [AddMonoidWithOne α] (a : α) (n : ℕ) :
Prop

Assert that an element of a semiring is equal to the coercion of some natural number.

- out : a = ↑n

  The element is equal to the coercion of the natural number.

Instances For

source
theorem Mathlib.Meta.NormNum.IsNat.raw_refl (n : ℕ) :
IsNat n n
source
def Nat.rawCast {α : Type u} [AddMonoidWithOne α] (n : ℕ) :
α

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

- n.rawCast = ↑n

Instances For

source
theorem Mathlib.Meta.NormNum.IsNat.to_eq {α : Type u} [AddMonoidWithOne α] {n : ℕ} {a a' : α} :
IsNat a n → ↑n = a' → a = a'
source
theorem Mathlib.Meta.NormNum.IsNat.to_raw_eq {α : Type u} {a : α} {n : ℕ} [AddMonoidWithOne α] :
IsNat a n → a = n.rawCast
source
theorem Mathlib.Meta.NormNum.IsNat.of_raw (α : Type u_1) [AddMonoidWithOne α] (n : ℕ) :
IsNat n.rawCast n
source
theorem Mathlib.Meta.NormNum.isNat.natElim {p : ℕ → Prop} {n n' : ℕ} :
IsNat n n' → p n' → p n
source
structure Mathlib.Meta.NormNum.IsInt {α : Type u} [Ring α] (a : α) (n : ℤ) :
Prop

Assert that an element of a ring is equal to the coercion of some integer.

- out : a = ↑n

  The element is equal to the coercion of the integer.

Instances For

source
def Int.rawCast {α : Type u} [Ring α] (n : ℤ) :
α

A "raw int cast" is an expression of the form:

- `(Nat.rawCast lit : α)` where `lit` is a raw natural number literal
- `(Int.rawCast (Int.negOfNat lit) : α)` where `lit` 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

- n.rawCast = ↑n

Instances For

source
theorem Mathlib.Meta.NormNum.IsInt.to_isNat {α : Type u_1} [Ring α] {a : α} {n : ℕ} :
IsInt a (Int.ofNat n) → IsNat a n
source
theorem Mathlib.Meta.NormNum.IsNat.to_isInt {α : Type u_1} [Ring α] {a : α} {n : ℕ} :
IsNat a n → IsInt a (Int.ofNat n)
source
theorem Mathlib.Meta.NormNum.IsInt.to_raw_eq {α : Type u} {a : α} {n : ℤ} [Ring α] :
IsInt a n → a = n.rawCast
source
theorem Mathlib.Meta.NormNum.IsInt.of_raw (α : Type u_1) [Ring α] (n : ℤ) :
IsInt n.rawCast n
source
theorem Mathlib.Meta.NormNum.IsInt.neg_to_eq {α : Type u_1} [Ring α] {n : ℕ} {a a' : α} :
IsInt a (Int.negOfNat n) → ↑n = a' → a = -a'
source
theorem Mathlib.Meta.NormNum.IsInt.nonneg_to_eq {α : Type u_1} [Ring α] {n : ℕ} {a a' : α} (h : IsInt a (Int.ofNat n)) (e : ↑n = a') :
a = a'
source
inductive Mathlib.Meta.NormNum.IsRat {α : Type u} [Ring α] (a : α) (num : ℤ) (denom : ℕ) :
Prop

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

source
inductive Mathlib.Meta.NormNum.IsNNRat {α : Type u} [Semiring α] (a : α) (num denom : ℕ) :
Prop

Assert that an element of a semiring 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} [Semiring α] {a : α} {num denom : ℕ} (inv : Invertible ↑denom) (eq : a = ↑num * ⅟↑denom) : IsNNRat a num denom

Instances For

source
def NNRat.rawCast {α : Type u} [DivisionSemiring α] (n d : ℕ) :
α

A "raw nnrat cast" is an expression of the form:

- `(Nat.rawCast lit : α)` where `lit` is a raw natural number literal
- `(NNRat.rawCast n d : α)` where `n` is a raw nat literal, `d` is a raw nat literal, and `d` 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

- NNRat.rawCast n d = ↑n / ↑d

Instances For

source
def Rat.rawCast {α : Type u} [DivisionRing α] (n : ℤ) (d : ℕ) :
α

A "raw rat cast" is an expression of the form:

- `(Nat.rawCast lit : α)` where `lit` is a raw natural number literal
- `(Int.rawCast (Int.negOfNat lit) : α)` where `lit` is a nonzero raw natural number literal
- `(NNRat.rawCast n d : α)` where `n` is a raw nat literal, `d` is a raw nat literal, and `d` is not `1` or `0`.
- `(Rat.rawCast (Int.negOfNat n) d : α)` where `n` is a raw nat literal, `d` is a raw nat literal, `n` is not `0`, and `d` 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

Instances For

source
theorem Mathlib.Meta.NormNum.IsNNRat.to_isNat {α : Type u_1} [Semiring α] {a : α} {n : ℕ} :
IsNNRat a n 1 → IsNat a n
source
theorem Mathlib.Meta.NormNum.IsRat.to_isNNRat {α : Type u_1} [Ring α] {a : α} {n d : ℕ} :
IsRat a (Int.ofNat n) d → IsNNRat a n d
source
theorem Mathlib.Meta.NormNum.IsNat.to_isNNRat {α : Type u_1} [Semiring α] {a : α} {n : ℕ} :
IsNat a n → IsNNRat a n 1
source
theorem Mathlib.Meta.NormNum.IsNNRat.to_isRat {α : Type u_1} [Ring α] {a : α} {n d : ℕ} :
IsNNRat a n d → IsRat a (Int.ofNat n) d
source
theorem Mathlib.Meta.NormNum.IsRat.to_isInt {α : Type u_1} [Ring α] {a : α} {n : ℤ} :
IsRat a n 1 → IsInt a n
source
theorem Mathlib.Meta.NormNum.IsInt.to_isRat {α : Type u_1} [Ring α] {a : α} {n : ℤ} :
IsInt a n → IsRat a n 1
source
theorem Mathlib.Meta.NormNum.IsNNRat.to_raw_eq {α : Type u} {n d : ℕ} [DivisionSemiring α] {a : α} :
IsNNRat a n d → a = NNRat.rawCast n d
source
theorem Mathlib.Meta.NormNum.IsRat.to_raw_eq {α : Type u} {n : ℤ} {d : ℕ} [DivisionRing α] {a : α} :
IsRat a n d → a = Rat.rawCast n d
source
theorem Mathlib.Meta.NormNum.IsRat.neg_to_eq {α : Type u_1} [DivisionRing α] {n d : ℕ} {a n' d' : α} :
IsRat a (Int.negOfNat n) d → ↑n = n' → ↑d = d' → a = -(n' / d')
source
theorem Mathlib.Meta.NormNum.IsNNRat.to_eq {α : Type u_1} [DivisionSemiring α] {n d : ℕ} {a n' d' : α} :
IsNNRat a n d → ↑n = n' → ↑d = d' → a = n' / d'
source
theorem Mathlib.Meta.NormNum.IsNNRat.of_raw (α : Type u_1) [DivisionSemiring α] (n d : ℕ) (h : ↑d ≠ 0) :
IsNNRat (NNRat.rawCast n d) n d
source
theorem Mathlib.Meta.NormNum.IsRat.of_raw (α : Type u_1) [DivisionRing α] (n : ℤ) (d : ℕ) (h : ↑d ≠ 0) :
IsRat (Rat.rawCast n d) n d
source
theorem Mathlib.Meta.NormNum.IsNNRat.den_nz {α : Type u_1} [DivisionSemiring α] {a : α} {n d : ℕ} :
IsNNRat a n d → ↑d ≠ 0
source
theorem Mathlib.Meta.NormNum.IsRat.den_nz {α : Type u_1} [DivisionRing α] {a : α} {n : ℤ} {d : ℕ} :
IsRat a n d → ↑d ≠ 0
source
inductive Mathlib.Meta.NormNum.Result' :
Type

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`.

- isNNRat (inst : Lean.Expr) (q : ℚ) (n d proof : Lean.Expr) : Result'

  Untyped version of `Result.isNNRat`.

- isNegNNRat (inst : Lean.Expr) (q : ℚ) (n d proof : Lean.Expr) : Result'

  Untyped version of `Result.isNegNNRat`.

Instances For

source
def Mathlib.Meta.NormNum.instInhabitedResult'.default :
Result'
Equations

- Mathlib.Meta.NormNum.instInhabitedResult'.default = Mathlib.Meta.NormNum.Result'.isBool default default

Instances For

source
instance Mathlib.Meta.NormNum.instInhabitedResult' :
Inhabited Result'
Equations

- Mathlib.Meta.NormNum.instInhabitedResult' = { default := Mathlib.Meta.NormNum.instInhabitedResult'.default }

source
def Mathlib.Meta.NormNum.Result {u : Lean.Level} {α : Q(Type u)} (x : Q(«$α»)) :
Type

The result of `norm_num` running on an expression `x` of type `α`.

Equations

- Mathlib.Meta.NormNum.Result x = Mathlib.Meta.NormNum.Result'

Instances For

source
instance Mathlib.Meta.NormNum.instInhabitedResult {u : Lean.Level} {α : Q(Type u)} {x : Q(«$α»)} :
Inhabited (Result x)
Equations

- Mathlib.Meta.NormNum.instInhabitedResult = inferInstanceAs (Inhabited Mathlib.Meta.NormNum.Result')

source
@[match_pattern, inline]
def Mathlib.Meta.NormNum.Result.isTrue {x : Q(Prop)} (proof : Q(«$x»)) :
Result q(«$x»)

The result is `proof : x`, where `x` is a (true) proposition.

Equations

- Mathlib.Meta.NormNum.Result.isTrue = Mathlib.Meta.NormNum.Result'.isBool true

Instances For

source
@[match_pattern, inline]
def Mathlib.Meta.NormNum.Result.isFalse {x : Q(Prop)} (proof : Q(¬«$x»)) :
Result q(«$x»)

The result is `proof : ¬x`, where `x` is a (false) proposition.

Equations

- Mathlib.Meta.NormNum.Result.isFalse = Mathlib.Meta.NormNum.Result'.isBool false

Instances For

source
@[match_pattern, inline]
def Mathlib.Meta.NormNum.Result.isNat {u : Lean.Level} {α : Q(Type u)} {x : Q(«$α»)} (inst : Q(AddMonoidWithOne «$α») := by assumption) (lit : Q(ℕ)) (proof : Q(IsNat «$x» «$lit»)) :
Result x

The result is `lit : ℕ` (a raw nat literal) and `proof : isNat x lit`.

Equations

- @Mathlib.Meta.NormNum.Result.isNat u α x = Mathlib.Meta.NormNum.Result'.isNat

Instances For

source
@[match_pattern, inline]
def Mathlib.Meta.NormNum.Result.isNegNat {u : Lean.Level} {α : Q(Type u)} {x : Q(«$α»)} (inst : Q(Ring «$α») := by assumption) (lit : Q(ℕ)) (proof : Q(IsInt «$x» (Int.negOfNat «$lit»))) :
Result x

The result is `-lit` where `lit` is a raw nat literal and `proof : isInt x (.negOfNat lit)`.

Equations

- @Mathlib.Meta.NormNum.Result.isNegNat u α x = Mathlib.Meta.NormNum.Result'.isNegNat

Instances For

source
@[match_pattern, inline]
def Mathlib.Meta.NormNum.Result.isNNRat {u : Lean.Level} {α : Q(Type u)} {x : Q(«$α»)} (inst : Q(DivisionSemiring «$α») := by assumption) (q : ℚ) (n d : Q(ℕ)) (proof : Q(IsNNRat «$x» «$n» «$d»)) :
Result x

The result is `proof : IsNNRat x n d`, where `n` 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

- @Mathlib.Meta.NormNum.Result.isNNRat u α x = Mathlib.Meta.NormNum.Result'.isNNRat

Instances For

source
@[match_pattern, inline]
def Mathlib.Meta.NormNum.Result.isNegNNRat {u : Lean.Level} {α : Q(Type u)} {x : Q(«$α»)} (inst : Q(DivisionRing «$α») := by assumption) (q : ℚ) (n d : Q(ℕ)) (proof : Q(IsRat «$x» (Int.negOfNat «$n») «$d»)) :
Result x

The result is `proof : IsRat x n d`, where `n` is `.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

- @Mathlib.Meta.NormNum.Result.isNegNNRat u α x = Mathlib.Meta.NormNum.Result'.isNegNNRat

Instances For

source
def Mathlib.Meta.NormNum.Result.isInt {u : Lean.Level} {α : Q(Type u)} {x : Q(«$α»)} (inst : Q(Ring «$α») := by assumption) (z : Q(ℤ)) (n : ℤ) (proof : Q(IsInt «$x» «$z»)) :
Result x

The result is `z : ℤ` and `proof : isNat x z`.

Instances For

source
def Mathlib.Meta.NormNum.Result.isNNRat' {u : Lean.Level} {α : Q(Type u)} {x : Q(«$α»)} (inst : Q(DivisionSemiring «$α») := by assumption) (q : ℚ) (n d : Q(ℕ)) (proof : Q(IsNNRat «$x» «$n» «$d»)) :
Result x

The result is `q : NNRat` and `proof : isNNRat x q`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Meta.NormNum.Result.isRat {u : Lean.Level} {α : Q(Type u)} {x : Q(«$α»)} (inst : Q(DivisionRing «$α») := by assumption) (q : ℚ) (n : Q(ℤ)) (d : Q(ℕ)) (proof : Q(IsRat «$x» «$n» «$d»)) :
Result x

The result is `q : ℚ` and `proof : isRat x q`.

Instances For

source
instance Mathlib.Meta.NormNum.instToMessageDataResult {u : Lean.Level} {α : Q(Type u)} {x : Q(«$α»)} :
Lean.ToMessageData (Result x)
Equations

- One or more equations did not get rendered due to their size.

source
def Mathlib.Meta.NormNum.Result.toRat {u : Lean.Level} {α : Q(Type u)} {e : Q(«$α»)} :
Result e → Option ℚ

Returns the rational number that is the result of `norm_num` evaluation.

Equations

- Mathlib.Meta.NormNum.Result.toRat (Mathlib.Meta.NormNum.Result'.isBool val proof) = none
- Mathlib.Meta.NormNum.Result.toRat (Mathlib.Meta.NormNum.Result'.isNat inst lit proof) = some ↑(Lean.Expr.natLit! lit)
- Mathlib.Meta.NormNum.Result.toRat (Mathlib.Meta.NormNum.Result'.isNegNat inst lit proof) = some (-↑(Lean.Expr.natLit! lit))
- Mathlib.Meta.NormNum.Result.toRat (Mathlib.Meta.NormNum.Result'.isNNRat inst q n d proof) = some q
- Mathlib.Meta.NormNum.Result.toRat (Mathlib.Meta.NormNum.Result'.isNegNNRat inst q n d proof) = some q

Instances For

source
def Mathlib.Meta.NormNum.Result.toRatNZ {u : Lean.Level} {α : Q(Type u)} {e : Q(«$α»)} :
Result e → Option (ℚ × Option Lean.Expr)

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

- Mathlib.Meta.NormNum.Result.toRatNZ (Mathlib.Meta.NormNum.Result'.isBool val proof) = none
- Mathlib.Meta.NormNum.Result.toRatNZ (Mathlib.Meta.NormNum.Result'.isNat inst lit proof) = some (↑(Lean.Expr.natLit! lit), none)
- Mathlib.Meta.NormNum.Result.toRatNZ (Mathlib.Meta.NormNum.Result'.isNegNat inst lit proof) = some (-↑(Lean.Expr.natLit! lit), none)
- Mathlib.Meta.NormNum.Result.toRatNZ (Mathlib.Meta.NormNum.Result'.isNNRat inst q n d proof) = some (q, some q(⋯))
- Mathlib.Meta.NormNum.Result.toRatNZ (Mathlib.Meta.NormNum.Result'.isNegNNRat inst q n d proof) = some (q, some q(⋯))

Instances For

source
def Mathlib.Meta.NormNum.Result.toInt {u : Lean.Level} {α : Q(Type u)} {e : Q(«$α»)} (_i : Q(Ring «$α») := by with_reducible assumption) :
Result e → Option (ℤ × (lit : Q(ℤ)) × Q(IsInt «$e» «$lit»))

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

- Mathlib.Meta.NormNum.Result.toInt _i (Mathlib.Meta.NormNum.Result'.isNat inst lit proof) = pure (↑(Lean.Expr.natLit! lit), ⟨q(Int.ofNat «$lit»), q(⋯)⟩)
- Mathlib.Meta.NormNum.Result.toInt _i (Mathlib.Meta.NormNum.Result'.isNegNat inst lit proof) = pure (-↑(Lean.Expr.natLit! lit), ⟨q(Int.negOfNat «$lit»), proof⟩)
- Mathlib.Meta.NormNum.Result.toInt _i x✝ = failure

Instances For

source
def Mathlib.Meta.NormNum.Result.toNNRat' {u : Lean.Level} {α : Q(Type u)} {e : Q(«$α»)} (_i : Q(DivisionSemiring «$α») := by with_reducible assumption) :
Result e → Option (ℚ × (n : Q(ℕ)) × (d : Q(ℕ)) × Q(IsNNRat «$e» «$n» «$d»))

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

- Mathlib.Meta.NormNum.Result.toNNRat' _i (Mathlib.Meta.NormNum.Result'.isNat inst lit proof) = some (↑(Lean.Expr.natLit! lit), ⟨q(«$lit»), ⟨q(1), q(⋯)⟩⟩)
- Mathlib.Meta.NormNum.Result.toNNRat' _i (Mathlib.Meta.NormNum.Result'.isNNRat inst q n d proof) = some (q, ⟨n, ⟨d, proof⟩⟩)
- Mathlib.Meta.NormNum.Result.toNNRat' _i x✝ = none

Instances For

source
def Mathlib.Meta.NormNum.Result.toRat' {u : Lean.Level} {α : Q(Type u)} {e : Q(«$α»)} (_i : Q(DivisionRing «$α») := by with_reducible assumption) :
Result e → Option (ℚ × (n : Q(ℤ)) × (d : Q(ℕ)) × Q(IsRat «$e» «$n» «$d»))

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

- Mathlib.Meta.NormNum.Result.toRat' _i (Mathlib.Meta.NormNum.Result'.isBool val proof) = none
- Mathlib.Meta.NormNum.Result.toRat' _i (Mathlib.Meta.NormNum.Result'.isNat inst lit proof) = some (↑(Lean.Expr.natLit! lit), ⟨q(Int.ofNat «$lit»), ⟨q(1), q(⋯)⟩⟩)
- Mathlib.Meta.NormNum.Result.toRat' _i (Mathlib.Meta.NormNum.Result'.isNegNat inst lit proof) = some (-↑(Lean.Expr.natLit! lit), ⟨q(Int.negOfNat «$lit»), ⟨q(1), q(⋯)⟩⟩)
- Mathlib.Meta.NormNum.Result.toRat' _i (Mathlib.Meta.NormNum.Result'.isNNRat inst q n d proof) = some (q, ⟨q(Int.ofNat «$n»), ⟨d, q(⋯)⟩⟩)
- Mathlib.Meta.NormNum.Result.toRat' _i (Mathlib.Meta.NormNum.Result'.isNegNNRat inst q n d proof) = some (q, ⟨q(Int.negOfNat «$n»), ⟨d, proof⟩⟩)

Instances For

source
def Mathlib.Meta.NormNum.Result.toRawEq {u : Lean.Level} {α : Q(Type u)} {e : Q(«$α»)} :
Result e → (e' : Q(«$α»)) × Q(«$e» = «$e'»)

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.

Instances For

source
def Mathlib.Meta.NormNum.Result.toRawIntEq {u : Lean.Level} {α : Q(Type u)} {e : Q(«$α»)} :
Result e → Option (ℤ × (e' : Q(«$α»)) × Q(«$e» = «$e'»))

`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

- Mathlib.Meta.NormNum.Result.toRawIntEq (Mathlib.Meta.NormNum.Result'.isNat inst lit p) = some (↑(Lean.Expr.natLit! lit), ⟨q(«$lit».rawCast), q(⋯)⟩)
- Mathlib.Meta.NormNum.Result.toRawIntEq (Mathlib.Meta.NormNum.Result'.isNegNat inst lit p) = some (-↑(Lean.Expr.natLit! lit), ⟨q((Int.negOfNat «$lit»).rawCast), q(⋯)⟩)
- Mathlib.Meta.NormNum.Result.toRawIntEq (Mathlib.Meta.NormNum.Result'.isNNRat inst q n d proof) = none
- Mathlib.Meta.NormNum.Result.toRawIntEq (Mathlib.Meta.NormNum.Result'.isNegNNRat inst q n d proof) = none
- Mathlib.Meta.NormNum.Result.toRawIntEq (Mathlib.Meta.NormNum.Result'.isBool val proof) = none

Instances For

source
def Mathlib.Meta.NormNum.Result.ofRawNat {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) :
Result e

Constructs a `Result` out of a raw nat cast. Assumes `e` is a raw nat cast expression.

Equations

- Mathlib.Meta.NormNum.Result.ofRawNat ((fn.app sα).app lit) = Id.run (Mathlib.Meta.NormNum.Result.isNat sα lit q(⋯))
- Mathlib.Meta.NormNum.Result.ofRawNat e = (panicWithPosWithDecl "Mathlib.Tactic.NormNum.Result" "Mathlib.Meta.NormNum.Result.ofRawNat" 489 70 "not a raw nat cast").run

Instances For

source
def Mathlib.Meta.NormNum.Result.ofRawInt {u : Lean.Level} {α : Q(Type u)} (n : ℤ) (e : Q(«$α»)) :
Result e

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.

Instances For

source
def Mathlib.Meta.NormNum.Result.ofRawNNRat {u : Lean.Level} {α : Q(Type u)} (q : ℚ) (e : Q(«$α»)) (hyp : Option Lean.Expr := none) :
Result e

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.

Instances For

source
def Mathlib.Meta.NormNum.Result.ofRawRat {u : Lean.Level} {α : Q(Type u)} (q : ℚ) (e : Q(«$α»)) (hyp : Option Lean.Expr := none) :
Result e

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.

Instances For

source
def Mathlib.Meta.NormNum.Result.toSimpResult {u : Lean.Level} {α : Q(Type u)} {e : Q(«$α»)} :
Result e → Lean.MetaM Lean.Meta.Simp.Result

Convert a `Result` to a `Simp.Result`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[reducible, inline]
abbrev Mathlib.Meta.NormNum.BoolResult (p : Q(Prop)) (b : Bool) :
Type

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

- Mathlib.Meta.NormNum.BoolResult p b = Q(Bool.rec (¬«$p») «$p» «$b»)

Instances For

source
def Mathlib.Meta.NormNum.Result.ofBoolResult {p : Q(Prop)} {b : Bool} (prf : BoolResult p b) :
Result q(Prop)

Obtain a `Result` from a `BoolResult`.

Equations

- Mathlib.Meta.NormNum.Result.ofBoolResult prf = Mathlib.Meta.NormNum.Result'.isBool b prf

Instances For

source
def Mathlib.Meta.NormNum.Result.eqTrans {u : Lean.Level} {α : Q(Type u)} {a b : Q(«$α»)} (eq : Q(«$a» = «$b»)) :
Result b → Result a

If `a = b` and we can evaluate `b`, then we can evaluate `a`.

Instances For