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 : ℤ) : Mathlib.Meta.NormNum.IsInt n n

Constructors and constants

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

def Mathlib.Meta.NormNum.evalZero : Mathlib.Meta.NormNum.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 α] : Mathlib.Meta.NormNum.IsNat One.one 1

def Mathlib.Meta.NormNum.evalOne : Mathlib.Meta.NormNum.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_1) [AddMonoidWithOne α] {a : α} {n : ℕ} (h : ↑n = a) : Mathlib.Meta.NormNum.IsNat a n

def Mathlib.Meta.NormNum.evalOfNat : Mathlib.Meta.NormNum.NormNumExt

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

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

def Mathlib.Meta.NormNum.evalIntOfNat : Mathlib.Meta.NormNum.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 : ℕ} : Mathlib.Meta.NormNum.IsNat n a → Mathlib.Meta.NormNum.IsNat (Int.natAbs n) a

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

def Mathlib.Meta.NormNum.evalIntNatAbs : Mathlib.Meta.NormNum.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_cast {R : Type u_1} [AddMonoidWithOne R] (n : ℕ) (m : ℕ) : Mathlib.Meta.NormNum.IsNat n m → Mathlib.Meta.NormNum.IsNat (↑n) m

def Mathlib.Meta.NormNum.evalNatCast : Mathlib.Meta.NormNum.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_int_cast {R : Type u_1} [Ring R] (n : ℤ) (m : ℕ) : Mathlib.Meta.NormNum.IsNat n m → Mathlib.Meta.NormNum.IsNat (↑n) m

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

def Mathlib.Meta.NormNum.evalIntCast : Mathlib.Meta.NormNum.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

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

theorem Mathlib.Meta.NormNum.isInt_add {α : Type u_1} [Ring α] {f : α → α → α} {a : α} {b : α} {a' : ℤ} {b' : ℤ} {c : ℤ} : f = HAdd.hAdd → Mathlib.Meta.NormNum.IsInt a a' → Mathlib.Meta.NormNum.IsInt b b' → Int.add a' b' = c → Mathlib.Meta.NormNum.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

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

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 (_ : ↑a = ↑k * ↑b)

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

instance Mathlib.Meta.NormNum.instMonadLiftOptionMetaM : MonadLift Option Lean.MetaM

Equations

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

def Mathlib.Meta.NormNum.evalAdd : Mathlib.Meta.NormNum.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.

def Mathlib.Meta.NormNum.evalAdd.core {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) (f : Q(«$α» → «$α» → «$α»)) (a : Q(«$α»)) (b : Q(«$α»)) (ra : Mathlib.Meta.NormNum.Result a) (rb : Mathlib.Meta.NormNum.Result b) : Option (Mathlib.Meta.NormNum.Result e)

Main part of evalAdd.

Equations

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

def Mathlib.Meta.NormNum.evalAdd.core.intArm {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) (f : Q(«$α» → «$α» → «$α»)) (a : Q(«$α»)) (b : Q(«$α»)) (ra : Mathlib.Meta.NormNum.Result a) (rb : Mathlib.Meta.NormNum.Result b) (rα : Q(Ring «$α»)) : Option (Mathlib.Meta.NormNum.Result e)

Equations

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

def Mathlib.Meta.NormNum.evalAdd.core.ratArm {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) (f : Q(«$α» → «$α» → «$α»)) (a : Q(«$α»)) (b : Q(«$α»)) (ra : Mathlib.Meta.NormNum.Result a) (rb : Mathlib.Meta.NormNum.Result b) (dα : Q(DivisionRing «$α»)) : Option (Mathlib.Meta.NormNum.Result e)

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 → Mathlib.Meta.NormNum.IsInt a a' → Int.neg a' = b → Mathlib.Meta.NormNum.IsInt (-a) b

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

def Mathlib.Meta.NormNum.evalNeg : Mathlib.Meta.NormNum.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.

def Mathlib.Meta.NormNum.evalNeg.core {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) (f : Q(«$α» → «$α»)) (a : Q(«$α»)) (ra : Mathlib.Meta.NormNum.Result a) (rα : Q(Ring «$α»)) : Option (Mathlib.Meta.NormNum.Result e)

Main part of evalNeg.

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 → Mathlib.Meta.NormNum.IsInt a a' → Mathlib.Meta.NormNum.IsInt b b' → Int.sub a' b' = c → Mathlib.Meta.NormNum.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 : Mathlib.Meta.NormNum.IsRat a na da) (rb : Mathlib.Meta.NormNum.IsRat b nb db) (h₁ : Int.sub (Int.mul na ↑db) (Int.mul nb ↑da) = Int.mul (↑k) nc) (h₂ : Nat.mul da db = Nat.mul k dc) : Mathlib.Meta.NormNum.IsRat (f a b) nc dc

def Mathlib.Meta.NormNum.evalSub : Mathlib.Meta.NormNum.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.

def Mathlib.Meta.NormNum.evalSub.core {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) (f : Q(«$α» → «$α» → «$α»)) (a : Q(«$α»)) (b : Q(«$α»)) (rα : Q(Ring «$α»)) (ra : Mathlib.Meta.NormNum.Result a) (rb : Mathlib.Meta.NormNum.Result b) : Option (Mathlib.Meta.NormNum.Result e)

Main part of evalAdd.

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 → Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → Nat.mul a' b' = c → Mathlib.Meta.NormNum.IsNat (a * b) c

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

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

def Mathlib.Meta.NormNum.evalMul : Mathlib.Meta.NormNum.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.

def Mathlib.Meta.NormNum.evalMul.core {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) (f : Q(«$α» → «$α» → «$α»)) (a : Q(«$α»)) (b : Q(«$α»)) (sα : Q(Semiring «$α»)) (ra : Mathlib.Meta.NormNum.Result a) (rb : Mathlib.Meta.NormNum.Result b) : Option (Mathlib.Meta.NormNum.Result e)

Main part of evalMul.

Equations

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

def Mathlib.Meta.NormNum.evalMul.core.intArm {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) (f : Q(«$α» → «$α» → «$α»)) (a : Q(«$α»)) (b : Q(«$α»)) (sα : Q(Semiring «$α»)) (ra : Mathlib.Meta.NormNum.Result a) (rb : Mathlib.Meta.NormNum.Result b) (rα : Q(Ring «$α»)) : Option (Mathlib.Meta.NormNum.Result e)

Equations

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

def Mathlib.Meta.NormNum.evalMul.core.ratArm {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) (f : Q(«$α» → «$α» → «$α»)) (a : Q(«$α»)) (b : Q(«$α»)) (sα : Q(Semiring «$α»)) (ra : Mathlib.Meta.NormNum.Result a) (rb : Mathlib.Meta.NormNum.Result b) (dα : Q(DivisionRing «$α»)) : Option (Mathlib.Meta.NormNum.Result e)

Equations

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

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

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

Helper function to synthesize a typed DivisionRing α expression.

Equations

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

def Mathlib.Meta.NormNum.evalDiv : Mathlib.Meta.NormNum.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 : Mathlib.Meta.NormNum.NormNumExt

The norm_num extension which identifies True.

Equations

• Mathlib.Meta.NormNum.evalTrue = Mathlib.Meta.NormNum.NormNumExt.mk true true fun {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) => pure (Mathlib.Meta.NormNum.Result.isTrue q(True.intro))

def Mathlib.Meta.NormNum.evalFalse : Mathlib.Meta.NormNum.NormNumExt

The norm_num extension which identifies False.

Equations

• Mathlib.Meta.NormNum.evalFalse = Mathlib.Meta.NormNum.NormNumExt.mk true true fun {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) => pure (Mathlib.Meta.NormNum.Result.isFalse q(not_false))

def Mathlib.Meta.NormNum.evalNot : Mathlib.Meta.NormNum.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_1} [AddMonoidWithOne α] {a : α} {b : α} {c : ℕ} : Mathlib.Meta.NormNum.IsNat a c → Mathlib.Meta.NormNum.IsNat b c → a = b

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

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

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

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

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

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

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

Nat operations

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

def Mathlib.Meta.NormNum.evalNatSucc : Mathlib.Meta.NormNum.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 : ℕ} : Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → Nat.sub a' b' = c → Mathlib.Meta.NormNum.IsNat (a - b) c

def Mathlib.Meta.NormNum.evalNatSub : Mathlib.Meta.NormNum.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 : ℕ} : Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → Nat.mod a' b' = c → Mathlib.Meta.NormNum.IsNat (a % b) c

def Mathlib.Meta.NormNum.evalNatMod : Mathlib.Meta.NormNum.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 : ℕ} : Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → Nat.div a' b' = c → Mathlib.Meta.NormNum.IsNat (a / b) c

def Mathlib.Meta.NormNum.evalNatDiv : Mathlib.Meta.NormNum.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' : ℕ} : Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → Nat.mod b' a' = 0 → a ∣ b

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

def Mathlib.Meta.NormNum.evalNatDvd : Mathlib.Meta.NormNum.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.