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

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 «$α») := by exact q(delta% inferInstance)) (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 «$α») := by exact q(delta% inferInstance)) (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 «$α») := by exact q(delta% inferInstance)) (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 subtracting two norm_num results.

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 «$α») := by exact q(delta% inferInstance)) (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.