norm_num basic plugins

This file adds norm_num plugins for

• constructors and constants
• Nat.cast, Int.cast, and mkRat
• +, -, *, and /
• Nat.succ, Nat.sub, Nat.mod, and Nat.div.

See other files in this directory for many more plugins.

@[implicit_reducible]

def Mathlib.Meta.NormNum.invertibleOfMul {α : Type u_1} [Semiring α] (k : ℕ) (b a : α) [Invertible a] : a = ↑k * b → Invertible b

If b divides a and a is invertible, then b is invertible.

@[implicit_reducible]

def Mathlib.Meta.NormNum.invertibleOfMul' {α : Type u_1} [Semiring α] {a k b : ℕ} [Invertible ↑a] (h : a = k * b) : Invertible ↑b

If b divides a and a is invertible, then b is invertible.

theorem Mathlib.Meta.NormNum.IsInt.raw_refl (n : ℤ) : IsInt n n

Constructors and constants

theorem Mathlib.Meta.NormNum.isNat_zero (α : Type u_1) [AddMonoidWithOne α] : IsNat Zero.zero 0

def Mathlib.Meta.NormNum.evalZero : NormNumExt

The norm_num extension which identifies the expression Zero.zero, returning 0.

theorem Mathlib.Meta.NormNum.isNat_one (α : Type u_1) [AddMonoidWithOne α] : IsNat One.one 1

def Mathlib.Meta.NormNum.evalOne : NormNumExt

The norm_num extension which identifies the expression One.one, returning 1.

theorem Mathlib.Meta.NormNum.isNat_ofNat (α : Type u) [AddMonoidWithOne α] {a : α} {n : ℕ} (h : ↑n = a) : IsNat a n

def Mathlib.Meta.NormNum.evalOfNat : NormNumExt

The norm_num extension which identifies an expression OfNat.ofNat n, returning n.

theorem Mathlib.Meta.NormNum.isNat_intOfNat {n n' : ℕ} : IsNat n n' → IsNat (Int.ofNat n) n'

def Mathlib.Meta.NormNum.evalIntOfNat : NormNumExt

The norm_num extension which identifies the constructor application Int.ofNat n such that norm_num successfully recognizes n, returning n.

theorem Mathlib.Meta.NormNum.isInt_negOfNat (m n : ℕ) (h : IsNat m n) : IsInt (Int.negOfNat m) (Int.negOfNat n)

def Mathlib.Meta.NormNum.evalNegOfNat : NormNumExt

norm_num extension for Int.negOfNat.

It's useful for calling derive with the numerator of an .isNegNNRat branch.

theorem Mathlib.Meta.NormNum.isNat_natAbs_pos {n : ℤ} {a : ℕ} : IsNat n a → IsNat n.natAbs a

theorem Mathlib.Meta.NormNum.isNat_natAbs_neg {n : ℤ} {a : ℕ} : IsInt n (Int.negOfNat a) → IsNat n.natAbs a

def Mathlib.Meta.NormNum.evalIntNatAbs : NormNumExt

The norm_num extension which identifies the expression Int.natAbs n such that norm_num successfully recognizes n.

Casts

theorem Mathlib.Meta.NormNum.isNat_natCast {R : Type u_1} [AddMonoidWithOne R] (n m : ℕ) : IsNat n m → IsNat (↑n) m

def Mathlib.Meta.NormNum.evalNatCast : NormNumExt

The norm_num extension which identifies an expression Nat.cast n, returning n.

theorem Mathlib.Meta.NormNum.isNat_intCast {R : Type u_1} [Ring R] (n : ℤ) (m : ℕ) : IsNat n m → IsNat (↑n) m

theorem Mathlib.Meta.NormNum.isintCast {R : Type u_1} [Ring R] (n m : ℤ) : IsInt n m → IsInt (↑n) m

def Mathlib.Meta.NormNum.evalIntCast : NormNumExt

The norm_num extension which identifies an expression Int.cast n, returning n.

Arithmetic

def LibraryNote.norm_num_lemma_function_equality : Batteries.Util.LibraryNote

Note: Many of the lemmas in this file use a function equality hypothesis like f = HAdd.hAdd below. The reason for this is that when this is applied, to prove e.g. 100 + 200 = 300, the + here is HAdd.hAdd with an instance that may not be syntactically equal to the one supplied by the AddMonoidWithOne instance, and rather than attempting to prove the instances equal lean will sometimes decide to evaluate 100 + 200 directly (into whatever + is defined to do in this ring), which is definitely not what we want; if the subterms are expensive to kernel-reduce then this could cause a (kernel) deep recursion detected error (see https://github.com/leanprover/lean4/issues/2171, https://github.com/leanprover-community/mathlib4/pull/4048).

By using an equality for the unapplied + function and proving it by rfl we take away the opportunity for lean to unfold the numerals (and the instance defeq problem is usually comparatively easy).

theorem Mathlib.Meta.NormNum.isNat_add {α : Type u_1} [AddMonoidWithOne α] {f : α → α → α} {a b : α} {a' b' c : ℕ} : f = HAdd.hAdd → IsNat a a' → IsNat b b' → a'.add b' = c → IsNat (f a b) c

theorem Mathlib.Meta.NormNum.isInt_add {α : Type u_1} [Ring α] {f : α → α → α} {a b : α} {a' b' c : ℤ} : f = HAdd.hAdd → IsInt a a' → IsInt b b' → a'.add b' = c → IsInt (f a b) c

theorem Mathlib.Meta.NormNum.isNNRat_add {α : Type u_1} [Semiring α] {f : α → α → α} {a b : α} {na nb nc da db dc k : ℕ} : f = HAdd.hAdd → IsNNRat a na da → IsNNRat b nb db → (na.mul db).add (nb.mul da) = k.mul nc → da.mul db = k.mul dc → IsNNRat (f a b) nc dc

theorem Mathlib.Meta.NormNum.isRat_add {α : Type u_1} [Ring α] {f : α → α → α} {a b : α} {na nb nc : ℤ} {da db dc k : ℕ} : f = HAdd.hAdd → IsRat a na da → IsRat b nb db → (na.mul ↑db).add (nb.mul ↑da) = (↑k).mul nc → da.mul db = k.mul dc → IsRat (f a b) nc dc

@[implicit_reducible]

def Mathlib.Meta.monadLiftOptionMetaM : MonadLift Option Lean.MetaM

Consider an Option as an object in the MetaM monad, by throwing an error on none.

def Mathlib.Meta.NormNum.Result.add {u : Lean.Level} {α : Q(Type u)} {a b : Q(«$α»)} (ra : Result q(«$a»)) (rb : Result q(«$b»)) (inst : Q(Add «$α») := by exact q(delta% inferInstance)) : Lean.MetaM (Result q(«$a» + «$b»))

The result of adding two norm_num results.

def Mathlib.Meta.NormNum.evalAdd : NormNumExt

The norm_num extension which identifies expressions of the form a + b, such that norm_num successfully recognises both a and b.

theorem Mathlib.Meta.NormNum.isInt_neg {α : Type u_1} [Ring α] {f : α → α} {a : α} {a' b : ℤ} : f = Neg.neg → IsInt a a' → a'.neg = b → IsInt (-a) b

theorem Mathlib.Meta.NormNum.isRat_neg {α : Type u_1} [Ring α] {f : α → α} {a : α} {n n' : ℤ} {d : ℕ} : f = Neg.neg → IsRat a n d → n.neg = n' → IsRat (-a) n' d

def Mathlib.Meta.NormNum.Result.neg {u : Lean.Level} {α : Q(Type u)} {a : Q(«$α»)} (ra : Result q(«$a»)) (rα : Q(Ring «$α») := by exact q(delta% inferInstance)) : Lean.MetaM (Result q(-«$a»))

The result of negating a norm_num result.

def Mathlib.Meta.NormNum.evalNeg : NormNumExt

The norm_num extension which identifies expressions of the form -a, such that norm_num successfully recognises a.

theorem Mathlib.Meta.NormNum.isInt_sub {α : Type u_1} [Ring α] {f : α → α → α} {a b : α} {a' b' c : ℤ} : f = HSub.hSub → IsInt a a' → IsInt b b' → a'.sub b' = c → IsInt (f a b) c

theorem Mathlib.Meta.NormNum.isRat_sub {α : Type u_1} [Ring α] {f : α → α → α} {a b : α} {na nb nc : ℤ} {da db dc k : ℕ} (hf : f = HSub.hSub) (ra : IsRat a na da) (rb : IsRat b nb db) (h₁ : (na.mul ↑db).sub (nb.mul ↑da) = (↑k).mul nc) (h₂ : da.mul db = k.mul dc) : IsRat (f a b) nc dc

def Mathlib.Meta.NormNum.Result.sub {u : Lean.Level} {α : Q(Type u)} {a b : Q(«$α»)} (ra : Result q(«$a»)) (rb : Result q(«$b»)) (inst : Q(Ring «$α») := by exact q(delta% inferInstance)) : Lean.MetaM (Result q(«$a» - «$b»))

The result of subtracting two norm_num results.

def Mathlib.Meta.NormNum.evalSub : NormNumExt

The norm_num extension which identifies expressions of the form a - b in a ring, such that norm_num successfully recognises both a and b.

theorem Mathlib.Meta.NormNum.isNat_mul {α : Type u_1} [Semiring α] {f : α → α → α} {a b : α} {a' b' c : ℕ} : f = HMul.hMul → IsNat a a' → IsNat b b' → a'.mul b' = c → IsNat (a * b) c

theorem Mathlib.Meta.NormNum.isInt_mul {α : Type u_1} [Ring α] {f : α → α → α} {a b : α} {a' b' c : ℤ} : f = HMul.hMul → IsInt a a' → IsInt b b' → a'.mul b' = c → IsInt (a * b) c

theorem Mathlib.Meta.NormNum.isNNRat_mul {α : Type u_1} [Semiring α] {f : α → α → α} {a b : α} {na nb nc da db dc k : ℕ} : f = HMul.hMul → IsNNRat a na da → IsNNRat b nb db → na.mul nb = k.mul nc → da.mul db = k.mul dc → IsNNRat (f a b) nc dc

theorem Mathlib.Meta.NormNum.isRat_mul {α : Type u_1} [Ring α] {f : α → α → α} {a b : α} {na nb nc : ℤ} {da db dc k : ℕ} : f = HMul.hMul → IsRat a na da → IsRat b nb db → na.mul nb = (↑k).mul nc → da.mul db = k.mul dc → IsRat (f a b) nc dc

def Mathlib.Meta.NormNum.Result.mul {u : Lean.Level} {α : Q(Type u)} {a b : Q(«$α»)} (ra : Result q(«$a»)) (rb : Result q(«$b»)) (inst : Q(Semiring «$α») := by exact q(delta% inferInstance)) : Lean.MetaM (Result q(«$a» * «$b»))

The result of multiplying two norm_num results.

def Mathlib.Meta.NormNum.evalMul : NormNumExt

The norm_num extension which identifies expressions of the form a * b, such that norm_num successfully recognises both a and b.

theorem Mathlib.Meta.NormNum.isNNRat_div {α : Type u} [DivisionSemiring α] {a b : α} {cn cd : ℕ} : IsNNRat (a * b⁻¹) cn cd → IsNNRat (a / b) cn cd

theorem Mathlib.Meta.NormNum.isRat_div {α : Type u} [DivisionRing α] {a b : α} {cn : ℤ} {cd : ℕ} : IsRat (a * b⁻¹) cn cd → IsRat (a / b) cn cd

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

Helper function to synthesize a typed DivisionSemiring α expression.

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

Helper function to synthesize a typed DivisionRing α expression.

def Mathlib.Meta.NormNum.evalDiv : NormNumExt

The norm_num extension which identifies expressions of the form a / b, such that norm_num successfully recognises both a and b.

Logic

def Mathlib.Meta.NormNum.evalTrue : NormNumExt

The norm_num extension which identifies True.

def Mathlib.Meta.NormNum.evalFalse : NormNumExt

The norm_num extension which identifies False.

def Mathlib.Meta.NormNum.evalNot : NormNumExt

The norm_num extension which identifies expressions of the form ¬a, such that norm_num successfully recognises a.

(In)equalities

theorem Mathlib.Meta.NormNum.isNat_eq_true {α : Type u} [AddMonoidWithOne α] {a b : α} {c : ℕ} : IsNat a c → IsNat b c → a = b

theorem Mathlib.Meta.NormNum.ble_eq_false {x y : ℕ} : x.ble y = false ↔ y < x

theorem Mathlib.Meta.NormNum.isInt_eq_true {α : Type u} [Ring α] {a b : α} {z : ℤ} : IsInt a z → IsInt b z → a = b

theorem Mathlib.Meta.NormNum.isNNRat_eq_true {α : Type u} [Semiring α] {a b : α} {n d : ℕ} : IsNNRat a n d → IsNNRat b n d → a = b

theorem Mathlib.Meta.NormNum.isRat_eq_true {α : Type u} [Ring α] {a b : α} {n : ℤ} {d : ℕ} : IsRat a n d → IsRat b n d → a = b

theorem Mathlib.Meta.NormNum.eq_of_true {a b : Prop} (ha : a) (hb : b) : a = b

theorem Mathlib.Meta.NormNum.ne_of_false_of_true {a b : Prop} (ha : ¬a) (hb : b) : a ≠ b

theorem Mathlib.Meta.NormNum.ne_of_true_of_false {a b : Prop} (ha : a) (hb : ¬b) : a ≠ b

theorem Mathlib.Meta.NormNum.eq_of_false {a b : Prop} (ha : ¬a) (hb : ¬b) : a = b

Nat operations

theorem Mathlib.Meta.NormNum.isNat_natSucc {a a' c : ℕ} : IsNat a a' → a'.succ = c → IsNat a.succ c

def Mathlib.Meta.NormNum.evalNatSucc : NormNumExt

The norm_num extension which identifies expressions of the form Nat.succ a, such that norm_num successfully recognises a.

theorem Mathlib.Meta.NormNum.isNat_natSub {a b a' b' c : ℕ} : IsNat a a' → IsNat b b' → a'.sub b' = c → IsNat (a - b) c

def Mathlib.Meta.NormNum.evalNatSub : NormNumExt

The norm_num extension which identifies expressions of the form Nat.sub a b, such that norm_num successfully recognises both a and b.

theorem Mathlib.Meta.NormNum.isNat_natMod {a b a' b' c : ℕ} : IsNat a a' → IsNat b b' → a'.mod b' = c → IsNat (a % b) c

def Mathlib.Meta.NormNum.evalNatMod : NormNumExt

The norm_num extension which identifies expressions of the form Nat.mod a b, such that norm_num successfully recognises both a and b.

theorem Mathlib.Meta.NormNum.isNat_natDiv {a b a' b' c : ℕ} : IsNat a a' → IsNat b b' → a'.div b' = c → IsNat (a / b) c

def Mathlib.Meta.NormNum.evalNatDiv : NormNumExt

The norm_num extension which identifies expressions of the form Nat.div a b, such that norm_num successfully recognises both a and b.

theorem Mathlib.Meta.NormNum.isNat_dvd_true {a b a' b' : ℕ} : IsNat a a' → IsNat b b' → b'.mod a' = 0 → a ∣ b

theorem Mathlib.Meta.NormNum.isNat_dvd_false {a b a' b' c : ℕ} : IsNat a a' → IsNat b b' → b'.mod a' = c.succ → ¬a ∣ b

def Mathlib.Meta.NormNum.evalNatDvd : NormNumExt

The norm_num extension which identifies expressions of the form (a : ℕ) | b, such that norm_num successfully recognises both a and b.