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.

ink

def norm_num : Lean.ParserDescr

Attribute for identifying norm_num extensions.

Equations

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

ink

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

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

• The element is equal to the coercion of the integer.

  out : a = ↑n

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

Represent an integer as a typed expression.

Equations

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

ink

def Mathlib.Meta.NormNum.instAddMonoidWithOneNat : AddMonoidWithOne ℕ

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

Equations

• Mathlib.Meta.NormNum.instAddMonoidWithOneNat = inferInstance

ink

def Mathlib.Meta.NormNum.instRingInt : Ring ℤ

A shortcut (non)instance for Ring ℤ to shrink generated proofs.

Equations

• Mathlib.Meta.NormNum.instRingInt = inferInstance

ink

inductive Mathlib.Meta.NormNum.IsRat {α : Type u_1} [inst : 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.

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

Represent an integer as a typed expression.

Equations

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

ink

def Mathlib.Meta.NormNum.instRingRat : Ring ℚ

A shortcut (non)instance for Ring ℚ to shrink generated proofs.

Equations

• Mathlib.Meta.NormNum.instRingRat = inferInstance

ink

def Mathlib.Meta.NormNum.instDivisionRingRat : DivisionRing ℚ

A shortcut (non)instance for DivisionRing ℚ to shrink generated proofs.

Equations

• Mathlib.Meta.NormNum.instDivisionRingRat = inferInstance

ink

inductive Mathlib.Meta.NormNum.Result' : Type

• Untyped version of Result.isBool.

  isBool: Bool → Lean.Expr → Mathlib.Meta.NormNum.Result'

• Untyped version of Result.isNat.

  isNat: Lean.Expr → Lean.Expr → Lean.Expr → Mathlib.Meta.NormNum.Result'

• Untyped version of Result.isNegNat.

  isNegNat: Lean.Expr → Lean.Expr → Lean.Expr → Mathlib.Meta.NormNum.Result'

• Untyped version of Result.isRat.

  isRat: Lean.Expr → ℚ → Lean.Expr → Lean.Expr → Lean.Expr → Mathlib.Meta.NormNum.Result'

The result of norm_num running on an expression x of type α. Untyped version of Result.

ink

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

Equations

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

ink

def Mathlib.Meta.NormNum.Result {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (x : Qq.QQ α) : Type

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

Equations

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

ink

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

ink

@[match_pattern, inline]

def Mathlib.Meta.NormNum.Result.isTrue {x : Q(Prop)} (proof : Qq.QQ x) : Mathlib.Meta.NormNum.Result x

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

Equations

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

ink

@[match_pattern, inline]

def Mathlib.Meta.NormNum.Result.isFalse {x : Q(Prop)} (proof : Qq.QQ (Lean.Expr.app (Lean.Expr.const `Not []) x)) : Mathlib.Meta.NormNum.Result x

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

Equations

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

ink

@[match_pattern, inline]

def Mathlib.Meta.NormNum.Result.isNat {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} {x : Qq.QQ α} (inst : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const `AddMonoidWithOne [u]) α)) _auto✝) (lit : Q(ℕ)) (proof : Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Mathlib.Meta.NormNum.IsNat [u]) α) inst) x) lit)) : Mathlib.Meta.NormNum.Result x

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

Equations

• Mathlib.Meta.NormNum.Result.isNat = Mathlib.Meta.NormNum.Result'.isNat

ink

@[match_pattern, inline]

def Mathlib.Meta.NormNum.Result.isNegNat {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} {x : Qq.QQ α} (inst : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const `Ring [u]) α)) _auto✝) (lit : Q(ℕ)) (proof : Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Mathlib.Meta.NormNum.IsInt [u]) α) inst) x) (Lean.Expr.app (Lean.Expr.const `Int.negOfNat []) lit))) : Mathlib.Meta.NormNum.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 = Mathlib.Meta.NormNum.Result'.isNegNat

ink

@[match_pattern, inline]

def Mathlib.Meta.NormNum.Result.isRat {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} {x : Qq.QQ α} (inst : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const `DivisionRing [u]) α)) _auto✝) (q : ℚ) (n : Q(ℤ)) (d : Q(ℕ)) (proof : Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Mathlib.Meta.NormNum.IsRat [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `DivisionRing.toRing [u]) α) inst)) x) n) d)) : Mathlib.Meta.NormNum.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 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

ink

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

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

Equations

• Mathlib.Meta.NormNum.instAddMonoidWithOne = inferInstance

ink

def Mathlib.Meta.NormNum.Result.isInt {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} {x : Qq.QQ α} (inst : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const `Ring [u]) α)) _auto✝) (z : Q(ℤ)) (n : ℤ) (proof : Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Mathlib.Meta.NormNum.IsInt [u]) α) inst) x) z)) : Mathlib.Meta.NormNum.Result x

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

Equations

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

ink

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.

ink

def Lean.LOption.toOption {α : Type u_1} : Lean.LOption α → Option α

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

ink

def Mathlib.Meta.NormNum.inferAddMonoidWithOne {u : Lean.Level} (α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))) : Lean.MetaM (Qq.QQ (Lean.Expr.app (Lean.Expr.const `AddMonoidWithOne [u]) α))

Helper function to synthesize a typed AddMonoidWithOne α expression.

Equations

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

ink

def Mathlib.Meta.NormNum.inferSemiring {u : Lean.Level} (α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))) : Lean.MetaM (Qq.QQ (Lean.Expr.app (Lean.Expr.const `Semiring [u]) α))

Helper function to synthesize a typed Semiring α expression.

Equations

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

ink

def Mathlib.Meta.NormNum.inferRing {u : Lean.Level} (α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))) : Lean.MetaM (Qq.QQ (Lean.Expr.app (Lean.Expr.const `Ring [u]) α))

Helper function to synthesize a typed Ring α expression.

Equations

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

ink

def Mathlib.Meta.NormNum.inferDivisionRing {u : Lean.Level} (α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))) : Lean.MetaM (Qq.QQ (Lean.Expr.app (Lean.Expr.const `DivisionRing [u]) α))

Helper function to synthesize a typed DivisionRing α expression.

Equations

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

ink

def Mathlib.Meta.NormNum.inferOrderedSemiring {u : Lean.Level} (α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))) : Lean.MetaM (Qq.QQ (Lean.Expr.app (Lean.Expr.const `OrderedSemiring [u]) α))

Helper function to synthesize a typed OrderedSemiring α expression.

Equations

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

ink

def Mathlib.Meta.NormNum.inferOrderedRing {u : Lean.Level} (α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))) : Lean.MetaM (Qq.QQ (Lean.Expr.app (Lean.Expr.const `OrderedRing [u]) α))

Helper function to synthesize a typed OrderedRing α expression.

Equations

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

ink

def Mathlib.Meta.NormNum.inferLinearOrderedField {u : Lean.Level} (α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))) : Lean.MetaM (Qq.QQ (Lean.Expr.app (Lean.Expr.const `LinearOrderedField [u]) α))

Helper function to synthesize a typed LinearOrderedField α expression.

Equations

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

ink

def Mathlib.Meta.NormNum.inferCharZeroOfRing {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (_i : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const `Ring [u]) α)) _auto✝) : Lean.MetaM (Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CharZero [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `AddGroupWithOne.toAddMonoidWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Ring.toAddGroupWithOne [u]) α) _i))))

Helper function to synthesize a typed CharZero α expression given Ring α.

Equations

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

ink

def Mathlib.Meta.NormNum.inferCharZeroOfRing? {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (_i : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const `Ring [u]) α)) _auto✝) : Lean.MetaM (Option (Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CharZero [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `AddGroupWithOne.toAddMonoidWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Ring.toAddGroupWithOne [u]) α) _i)))))

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.

ink

def Mathlib.Meta.NormNum.inferCharZeroOfAddMonoidWithOne {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (_i : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const `AddMonoidWithOne [u]) α)) _auto✝) : Lean.MetaM (Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CharZero [u]) α) _i))

Helper function to synthesize a typed CharZero α expression given AddMonoidWithOne α.

Equations

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

ink

def Mathlib.Meta.NormNum.inferCharZeroOfAddMonoidWithOne? {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (_i : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const `AddMonoidWithOne [u]) α)) _auto✝) : Lean.MetaM (Option (Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CharZero [u]) α) _i)))

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.

ink

def Mathlib.Meta.NormNum.inferCharZeroOfDivisionRing {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (_i : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const `DivisionRing [u]) α)) _auto✝) : Lean.MetaM (Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CharZero [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `AddGroupWithOne.toAddMonoidWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Ring.toAddGroupWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `DivisionRing.toRing [u]) α) _i)))))

Helper function to synthesize a typed CharZero α expression given DivisionRing α.

Equations

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

ink

def Mathlib.Meta.NormNum.inferCharZeroOfDivisionRing? {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (_i : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const `DivisionRing [u]) α)) _auto✝) : Lean.MetaM (Option (Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `CharZero [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `AddGroupWithOne.toAddMonoidWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Ring.toAddGroupWithOne [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `DivisionRing.toRing [u]) α) _i))))))

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.

ink

def Mathlib.Meta.NormNum.Result.toInt {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} {e : Qq.QQ α} (_i : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const `Ring [u]) α)) _auto✝) : Mathlib.Meta.NormNum.Result e → Option (ℤ × (lit : Q(ℤ)) × Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Mathlib.Meta.NormNum.IsInt [u]) α) _i) 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

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

ink

def Mathlib.Meta.NormNum.Result.toRat' {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} {e : Qq.QQ α} (_i : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const `DivisionRing [u]) α)) _auto✝) : Mathlib.Meta.NormNum.Result e → Option (ℚ × (n : Q(ℤ)) × (d : Q(ℕ)) × Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Mathlib.Meta.NormNum.IsRat [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `DivisionRing.toRing [u]) α) _i)) 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

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

ink

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.

ink

def Mathlib.Meta.NormNum.Result.toRawEq {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} {e : Qq.QQ α} : Mathlib.Meta.NormNum.Result e → (e' : Qq.QQ α) × Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Eq [Lean.Level.succ u]) α) 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.

Equations

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

ink

def Mathlib.Meta.NormNum.Result.toRawIntEq {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} {e : Qq.QQ α} : Mathlib.Meta.NormNum.Result e → Option (ℤ × (e' : Qq.QQ α) × Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Eq [Lean.Level.succ u]) α) 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

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

ink

def Mathlib.Meta.NormNum.Result.ofRawNat {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (e : Qq.QQ α) : Mathlib.Meta.NormNum.Result e

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.

ink

def Mathlib.Meta.NormNum.Result.ofRawInt {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (n : ℤ) (e : Qq.QQ α) : Mathlib.Meta.NormNum.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.

ink

def Mathlib.Meta.NormNum.Result.ofRawRat {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (q : ℚ) (e : Qq.QQ α) (hyp : optParam (Option Lean.Expr) none) : Mathlib.Meta.NormNum.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.

ink

def Mathlib.Meta.NormNum.Result.isRat' {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} {x : Qq.QQ α} (inst : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const `DivisionRing [u]) α)) _auto✝) (q : ℚ) (n : Q(ℤ)) (d : Q(ℕ)) (proof : Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Mathlib.Meta.NormNum.IsRat [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `DivisionRing.toRing [u]) α) inst)) x) n) d)) : Mathlib.Meta.NormNum.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.

ink

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.

Equations

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

ink

def Mathlib.Meta.NormNum.mkOfNat {u : Lean.Level} (α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))) (_sα : Qq.QQ (Lean.Expr.app (Lean.Expr.const `AddMonoidWithOne [u]) α)) (lit : Q(ℕ)) : Lean.MetaM ((a' : Qq.QQ α) × Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Eq [Lean.Level.succ u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Nat.cast [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `AddMonoidWithOne.toNatCast [u]) α) _sα)) 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.

ink

def Mathlib.Meta.NormNum.Result.toSimpResult {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} {e : Qq.QQ α} : Mathlib.Meta.NormNum.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.

ink

structure Mathlib.Meta.NormNum.NormNumExt : Type

• The extension should be run in the pre phase when used as simp plugin.

  pre : Bool

• The extension should be run in the post phase when used as simp plugin.

  post : Bool

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

  name : autoParam Lean.Name _auto✝

A extension for norm_num.

ink

def Mathlib.Meta.NormNum.mkNormNumExt (n : Lean.Name) : Lean.ImportM Mathlib.Meta.NormNum.NormNumExt

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

ink

@[inline]

abbrev Mathlib.Meta.NormNum.Entry : Type

Each norm_num extension is labelled with a collection of patterns which determine the expressions to which it should be applied.

Equations

• Mathlib.Meta.NormNum.Entry = (Array (Array (Lean.Meta.DiscrTree.Key true)) × Lean.Name)

ink

structure Mathlib.Meta.NormNum.NormNums : Type

• The tree of norm_num extensions.

  tree : Lean.Meta.DiscrTree Mathlib.Meta.NormNum.NormNumExt true

• Erased norm_nums.

  erased : Lean.PHashSet Lean.Name

The state of the norm_num extension environment

ink

instance Mathlib.Meta.NormNum.instInhabitedNormNums : Inhabited Mathlib.Meta.NormNum.NormNums

Equations

• Mathlib.Meta.NormNum.instInhabitedNormNums = { default := { tree := default, erased := default } }

ink

opaque Mathlib.Meta.NormNum.normNumExt : Lean.ScopedEnvExtension Mathlib.Meta.NormNum.Entry (Mathlib.Meta.NormNum.Entry × Mathlib.Meta.NormNum.NormNumExt) Mathlib.Meta.NormNum.NormNums

Environment extensions for norm_num declarations

ink

def Mathlib.Meta.NormNum.derive {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (e : Qq.QQ α) (post : optParam Bool false) : Lean.MetaM (Mathlib.Meta.NormNum.Result e)

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.

ink

def Mathlib.Meta.NormNum.deriveNat' {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (e : Qq.QQ α) : Lean.MetaM ((_inst : Qq.QQ (Lean.Expr.app (Lean.Expr.const `AddMonoidWithOne [u]) α)) × (lit : Qq.QQ (Lean.Expr.const `Nat [])) × Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Mathlib.Meta.NormNum.IsNat [u]) α) _inst) e) lit))

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.

ink

def Mathlib.Meta.NormNum.deriveNat {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (e : Qq.QQ α) (_inst : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const `AddMonoidWithOne [u]) α)) _auto✝) : Lean.MetaM ((lit : Q(ℕ)) × Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Mathlib.Meta.NormNum.IsNat [u]) α) _inst) e) lit))

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.

ink

def Mathlib.Meta.NormNum.deriveInt {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (e : Qq.QQ α) (_inst : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const `Ring [u]) α)) _auto✝) : Lean.MetaM ((lit : Q(ℤ)) × Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Mathlib.Meta.NormNum.IsInt [u]) α) _inst) e) lit))

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.

ink

def Mathlib.Meta.NormNum.deriveRat {u : Lean.Level} {α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ u))} (e : Qq.QQ α) (_inst : autoParam (Qq.QQ (Lean.Expr.app (Lean.Expr.const `DivisionRing [u]) α)) _auto✝) : Lean.MetaM (ℚ × (n : Q(ℤ)) × (d : Q(ℕ)) × Qq.QQ (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `Mathlib.Meta.NormNum.IsRat [u]) α) (Lean.Expr.app (Lean.Expr.app (Lean.Expr.const `DivisionRing.toRing [u]) α) _inst)) e) n) d))

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.

ink

def Mathlib.Meta.NormNum.isNatLit (e : Lean.Expr) : Option ℕ

Extract the natural number n if the expression is of the form OfNat.ofNat n.

Equations

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

ink

def Mathlib.Meta.NormNum.isIntLit (e : Lean.Expr) : Option ℤ

Extract the integer i if the expression is either a natural number literal or the negation of one.

Equations

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

ink

def Mathlib.Meta.NormNum.isRatLit (e : Lean.Expr) : Option ℚ

Extract the numerator n : ℤ and denominator d : ℕ if the expression is either an integer literal, or the division of one integer literal by another.

Equations

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

ink

def Mathlib.Meta.NormNum.isNormalForm : Lean.Expr → Bool

Test if an expression represents an explicit number written in normal form.

Equations

• Mathlib.Meta.NormNum.isNormalForm (Lean.Expr.lit a) = true
• Mathlib.Meta.NormNum.isNormalForm (Lean.Expr.mdata data e) = Mathlib.Meta.NormNum.isNormalForm e
• Mathlib.Meta.NormNum.isNormalForm x = Option.isSome (Mathlib.Meta.NormNum.isRatLit x)

ink

def Mathlib.Meta.NormNum.eval (e : Lean.Expr) (post : optParam Bool false) : Lean.MetaM Lean.Meta.Simp.Result

Run each registered norm_num extension on an expression, returning a Simp.Result.

Equations

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

ink

def Mathlib.Meta.NormNum.NormNums.eraseCore (d : Mathlib.Meta.NormNum.NormNums) (declName : Lean.Name) : Mathlib.Meta.NormNum.NormNums

Erases a name marked norm_num by adding it to the state's erased field and removing it from the state's list of Entrys.

Equations

• Mathlib.Meta.NormNum.NormNums.eraseCore d declName = { tree := d.tree, erased := Lean.PersistentHashSet.insert d.erased declName }

ink

def Mathlib.Meta.NormNum.NormNums.erase {m : Type → Type} [inst : Monad m] [inst : Lean.MonadError m] (d : Mathlib.Meta.NormNum.NormNums) (declName : Lean.Name) : m Mathlib.Meta.NormNum.NormNums

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.

ink

def Mathlib.Meta.NormNum.tryNormNum? (post : optParam Bool false) (e : Lean.Expr) : Lean.Meta.SimpM (Option Lean.Meta.Simp.Step)

A simp plugin which calls NormNum.eval.

Equations

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

ink

def Lean.Meta.Simp.Result.ofTrue (r : Lean.Meta.Simp.Result) : Lean.MetaM (Option Lean.Expr)

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.

ink

partial def Mathlib.Meta.NormNum.discharge (ctx : Lean.Meta.Simp.Context) (useSimp : optParam Bool true) (e : Lean.Expr) : Lean.Meta.SimpM (Option Lean.Expr)

A discharger which calls norm_num.

ink

partial def Mathlib.Meta.NormNum.methods (ctx : Lean.Meta.Simp.Context) (useSimp : optParam Bool true) : Lean.Meta.Simp.Methods

A Methods implementation which calls norm_num.

ink

partial def Mathlib.Meta.NormNum.deriveSimp (ctx : Lean.Meta.Simp.Context) (useSimp : optParam Bool true) (e : Lean.Expr) : Lean.MetaM Lean.Meta.Simp.Result

Traverses the given expression using simp and normalises any numbers it finds.

ink

def Mathlib.Meta.NormNum.normNumAt (g : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (fvarIdsToSimp : Array Lean.FVarId) (simplifyTarget : optParam Bool true) (useSimp : optParam Bool true) : Lean.MetaM (Option (Array Lean.FVarId × Lean.MVarId))

The core of norm_num as a tactic in MetaM.

• g: The goal to simplify
• ctx: The simp context, constructed by mkSimpContext and containing any additional simp rules we want to use
• fvarIdsToSimp: The selected set of hypotheses used in the location argument
• simplifyTarget: true if the target is selected in the location argument
• useSimp: true if we used norm_num instead of norm_num1

Equations

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

ink

def Mathlib.Meta.NormNum.getSimpContext (args : Lean.Syntax) (simpOnly : optParam Bool false) : Lean.Elab.Tactic.TacticM Lean.Meta.Simp.Context

Constructs a simp context from the simp argument syntax.

Equations

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

ink

def Mathlib.Meta.NormNum.elabNormNum (args : Lean.Syntax) (loc : Lean.Syntax) (simpOnly : optParam Bool false) (useSimp : optParam Bool true) : Lean.Elab.Tactic.TacticM Unit

Elaborates a call to norm_num only? [args] or norm_num1.

• args: the (simpArgs)? syntax for simp arguments
• loc: the (location)? syntax for the optional location argument
• simpOnly: true if only was used in norm_num
• useSimp: false if norm_num1 was used, in which case only the structural parts of simp will be used, not any of the post-processing that simp only does without lemmas

Equations

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

ink

def Mathlib.Tactic.normNum : Lean.ParserDescr

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.

ink

def Mathlib.Tactic.normNum1 : Lean.ParserDescr

Basic version of norm_num that does not call simp.

Equations

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

ink

def Mathlib.Tactic.normNum1Conv : Lean.ParserDescr

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)

ink

def Mathlib.Tactic.elabNormNum1Conv : Lean.Elab.Tactic.Tactic

Elaborator for norm_num1 conv tactic.

Equations

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

ink

def Mathlib.Tactic.normNumConv : Lean.ParserDescr

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.

ink

def Mathlib.Tactic.elabNormNumConv : Lean.Elab.Tactic.Tactic

Elaborator for norm_num conv tactic.

Equations

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

ink

def Mathlib.Tactic.normNumCmd : Lean.ParserDescr

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.