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.

def Mathlib.Meta.NormNum.instAddMonoidWithOneNat : AddMonoidWithOne ℕ

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

Equations

• Mathlib.Meta.NormNum.instAddMonoidWithOneNat = inferInstance

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

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

Equations

• Mathlib.Meta.NormNum.instAddMonoidWithOne = inferInstance

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

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.

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

• out : a = ↑n

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

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

theorem Mathlib.Meta.NormNum.IsNat.raw_refl (n : ℕ) : Mathlib.Meta.NormNum.IsNat n n

def Nat.rawCast {α : Type u_1} [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

• Nat.rawCast n = ↑n

theorem Mathlib.Meta.NormNum.IsNat.to_eq {α : Type u_1} [AddMonoidWithOne α] {n : ℕ} {a : α} {a' : α} : Mathlib.Meta.NormNum.IsNat a n → ↑n = a' → a = a'

theorem Mathlib.Meta.NormNum.IsNat.to_raw_eq {α : Type u_1} {a : α} {n : ℕ} [AddMonoidWithOne α] : Mathlib.Meta.NormNum.IsNat a n → a = Nat.rawCast n

theorem Mathlib.Meta.NormNum.IsNat.of_raw (α : Type u_1) [AddMonoidWithOne α] (n : ℕ) : Mathlib.Meta.NormNum.IsNat (Nat.rawCast n) n

theorem Mathlib.Meta.NormNum.isNat.natElim {p : ℕ → Prop} {n : ℕ} {n' : ℕ} : Mathlib.Meta.NormNum.IsNat n n' → p n' → p n

structure Mathlib.Meta.NormNum.IsInt {α : Type u_1} [Ring α] (a : α) (n : ℤ) : Prop

• out : a = ↑n

  The element is equal to the coercion of the integer.

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

def Int.rawCast {α : Type u_1} [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

• Int.rawCast n = ↑n

theorem Mathlib.Meta.NormNum.IsInt.to_isNat {α : Type u_1} [Ring α] {a : α} {n : ℕ} : Mathlib.Meta.NormNum.IsInt a (Int.ofNat n) → Mathlib.Meta.NormNum.IsNat a n

theorem Mathlib.Meta.NormNum.IsNat.to_isInt {α : Type u_1} [Ring α] {a : α} {n : ℕ} : Mathlib.Meta.NormNum.IsNat a n → Mathlib.Meta.NormNum.IsInt a (Int.ofNat n)

theorem Mathlib.Meta.NormNum.IsInt.to_raw_eq {α : Type u_1} {a : α} {n : ℤ} [Ring α] : Mathlib.Meta.NormNum.IsInt a n → a = Int.rawCast n

theorem Mathlib.Meta.NormNum.IsInt.of_raw (α : Type u_1) [Ring α] (n : ℤ) : Mathlib.Meta.NormNum.IsInt (Int.rawCast n) n

theorem Mathlib.Meta.NormNum.IsInt.neg_to_eq {α : Type u_1} [Ring α] {n : ℕ} {a : α} {a' : α} : Mathlib.Meta.NormNum.IsInt a (Int.negOfNat n) → ↑n = a' → a = -a'

theorem Mathlib.Meta.NormNum.IsInt.nonneg_to_eq {α : Type u_1} [Ring α] {n : ℕ} {a : α} {a' : α} (h : Mathlib.Meta.NormNum.IsInt a (Int.ofNat n)) (e : ↑n = a') : a = a'

inductive Mathlib.Meta.NormNum.IsRat {α : Type u_1} [Ring α] (a : α) (num : ℤ) (denom : ℕ) : Prop

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

def Rat.rawCast {α : Type u_1} [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
• (Rat.rawCast n d : α) where n is a raw int cast, d is a raw nat cast, 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

theorem Mathlib.Meta.NormNum.IsRat.to_isNat {α : Type u_1} [Ring α] {a : α} {n : ℕ} : Mathlib.Meta.NormNum.IsRat a (Int.ofNat n) 1 → Mathlib.Meta.NormNum.IsNat a n

theorem Mathlib.Meta.NormNum.IsNat.to_isRat {α : Type u_1} [Ring α] {a : α} {n : ℕ} : Mathlib.Meta.NormNum.IsNat a n → Mathlib.Meta.NormNum.IsRat a (Int.ofNat n) 1

theorem Mathlib.Meta.NormNum.IsRat.to_isInt {α : Type u_1} [Ring α] {a : α} {n : ℤ} : Mathlib.Meta.NormNum.IsRat a n 1 → Mathlib.Meta.NormNum.IsInt a n

theorem Mathlib.Meta.NormNum.IsInt.to_isRat {α : Type u_1} [Ring α] {a : α} {n : ℤ} : Mathlib.Meta.NormNum.IsInt a n → Mathlib.Meta.NormNum.IsRat a n 1

theorem Mathlib.Meta.NormNum.IsRat.to_raw_eq {α : Type u_1} {n : ℤ} {d : ℕ} [DivisionRing α] {a : α} : Mathlib.Meta.NormNum.IsRat a n d → a = Rat.rawCast n d

theorem Mathlib.Meta.NormNum.IsRat.neg_to_eq {α : Type u_1} [DivisionRing α] {n : ℕ} {d : ℕ} {a : α} {n' : α} {d' : α} : Mathlib.Meta.NormNum.IsRat a (Int.negOfNat n) d → ↑n = n' → ↑d = d' → a = -(n' / d')

theorem Mathlib.Meta.NormNum.IsRat.nonneg_to_eq {α : Type u_1} [DivisionRing α] {n : ℕ} {d : ℕ} {a : α} {n' : α} {d' : α} : Mathlib.Meta.NormNum.IsRat a (Int.ofNat n) d → ↑n = n' → ↑d = d' → a = n' / d'

theorem Mathlib.Meta.NormNum.IsRat.of_raw (α : Type u_1) [DivisionRing α] (n : ℤ) (d : ℕ) (h : ↑d ≠ 0) : Mathlib.Meta.NormNum.IsRat (Rat.rawCast n d) n d

theorem Mathlib.Meta.NormNum.IsRat.den_nz {α : Type u_1} [DivisionRing α] {a : α} {n : ℤ} {d : ℕ} : Mathlib.Meta.NormNum.IsRat a n d → ↑d ≠ 0

inductive Mathlib.Meta.NormNum.Result' : Type

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

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

Equations

• Mathlib.Meta.NormNum.instInhabitedResult' = { default := Mathlib.Meta.NormNum.Result'.isBool default default }

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

Equations

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

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

Equations

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

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

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.

def Mathlib.Meta.NormNum.Result.toRatNZ : {a : Lean.Level} → {α : Q(Type a)} → {e : Q(«$α»)} → Mathlib.Meta.NormNum.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.

@[reducible]

def 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).

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

Obtain a Result from a BoolResult.

Equations

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