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} [Ring α] : AddMonoidWithOne α

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

Equations

• Mathlib.Meta.NormNum.instAddMonoidWithOne = inferInstance

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

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

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

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.

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.

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.

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.

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

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

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

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

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

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

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.

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

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

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

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

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

theorem Mathlib.Meta.NormNum.IsInt.neg_to_eq {α : Type u_1} [Ring α] {n : ℕ} {a a' : α} : 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 : IsInt a (Int.ofNat n)) (e : ↑n = a') : a = a'

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

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
• (Rat.rawCast n d : α) where n is a raw int literal, d is a raw nat literal, and d is not 1 or 0.

(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

• Rat.rawCast n d = ↑n / ↑d

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

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

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

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

theorem Mathlib.Meta.NormNum.IsRat.to_raw_eq {α : Type u} {n : ℤ} {d : ℕ} [DivisionRing α] {a : α} : 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' : α} : 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' : α} : 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) : IsRat (Rat.rawCast n d) n d

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

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.

• isRat (inst : Lean.Expr) (q : ℚ) (n d proof : Lean.Expr) : Result'

  Untyped version of Result.isRat.

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

Equations

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

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'

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')

@[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

@[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

@[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

@[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

@[match_pattern, inline]

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

• @Mathlib.Meta.NormNum.Result.isRat u α x = Mathlib.Meta.NormNum.Result'.isRat

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.

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

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.

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'.isRat inst q n d proof) = some q

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'.isRat inst q n d proof) = some (q, some q(⋯))

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

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'.isRat inst q n d proof) = some (q, ⟨n, ⟨d, proof⟩⟩)

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.

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'.isRat inst q n d proof) = none
• Mathlib.Meta.NormNum.Result.toRawIntEq (Mathlib.Meta.NormNum.Result'.isBool val proof) = none

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" 397 70 "not a raw nat cast").run

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.

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.

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.

@[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»)

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

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.