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.

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

Arithmetic

def Mathlib.Meta.NormNum.Mathlib.LibraryNote.«norm_num lemma function equality» : 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).

Equations

• Mathlib.Meta.NormNum.Mathlib.LibraryNote.«norm_num lemma function equality» = ()

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

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.

Equations

• Mathlib.Meta.NormNum.invertibleOfMul k b (↑k * b) ⋯ = { invOf := c * ↑k, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

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.

Equations

• Mathlib.Meta.NormNum.invertibleOfMul' h = Mathlib.Meta.NormNum.invertibleOfMul k ↑b ↑a ⋯

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

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

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

Equations

• Mathlib.Meta.monadLiftOptionMetaM = { monadLift := fun {α : Type} (x : Option α) => match x with | none => failure | some e => pure e }

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.Result.add.intArm {u : Lean.Level} {α : Q(Type u)} {a b : Q(«$α»)} (ra : Result q(«$a»)) (rb : Result q(«$b»)) (inst : Q(Add «$α»)) (rα : Q(Ring «$α»)) : Lean.MetaM (Result q(«$a» + «$b»))

Equations

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

def Mathlib.Meta.NormNum.Result.add.nnratArm {u : Lean.Level} {α : Q(Type u)} {a b : Q(«$α»)} (ra : Result q(«$a»)) (rb : Result q(«$b»)) (inst : Q(Add «$α»)) (dsα : Q(DivisionSemiring «$α»)) : Lean.MetaM (Result q(«$a» + «$b»))

Equations

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

def Mathlib.Meta.NormNum.Result.add.ratArm {u : Lean.Level} {α : Q(Type u)} {a b : Q(«$α»)} (ra : Result q(«$a»)) (rb : Result q(«$b»)) (inst : Q(Add «$α»)) (dα : Q(DivisionRing «$α»)) : Lean.MetaM (Result q(«$a» + «$b»))

Equations

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

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.

Equations

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

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.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Meta.NormNum.Result.neg (Mathlib.Meta.NormNum.Result'.isBool val proof) rα = failure

def Mathlib.Meta.NormNum.evalNeg : NormNumExt

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

Equations

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

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.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Meta.NormNum.Result.sub (Mathlib.Meta.NormNum.Result'.isBool val proof) rb inst = failure
• ra.sub (Mathlib.Meta.NormNum.Result'.isBool val proof) inst = failure

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.

Equations

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

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.Result.mul.ratArm {u : Lean.Level} {α : Q(Type u)} {a b : Q(«$α»)} (ra : Result q(«$a»)) (rb : Result q(«$b»)) (inst : Q(Semiring «$α»)) (dα : Q(DivisionRing «$α»)) : Option (Result q(«$a» * «$b»))

Equations

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

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.

Equations

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

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.

Equations

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

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

Helper function to synthesize a typed DivisionRing α expression.

Equations

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

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.

Equations

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

Logic

def Mathlib.Meta.NormNum.evalTrue : NormNumExt

The norm_num extension which identifies True.

Equations

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

def Mathlib.Meta.NormNum.evalFalse : NormNumExt

The norm_num extension which identifies False.

Equations

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

def Mathlib.Meta.NormNum.evalNot : NormNumExt

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

Equations

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

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

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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