norm_num extension for integer div/mod and divides

This file adds support for the %, /, and ∣ (divisibility) operators on ℤ to the norm_num tactic.

theorem Mathlib.Meta.NormNum.isInt_ediv_zero {a : ℤ} {b : ℤ} {r : ℤ} : Mathlib.Meta.NormNum.IsInt a r → Mathlib.Meta.NormNum.IsNat b 0 → Mathlib.Meta.NormNum.IsNat (a / b) 0

theorem Mathlib.Meta.NormNum.isInt_ediv {a : ℤ} {b : ℤ} {q : ℤ} {m : ℤ} {a' : ℤ} {b' : ℕ} {r : ℕ} (ha : Mathlib.Meta.NormNum.IsInt a a') (hb : Mathlib.Meta.NormNum.IsNat b b') (hm : q * ↑b' = m) (h : ↑r + m = a') (h₂ : r.blt b' = true) : Mathlib.Meta.NormNum.IsInt (a / b) q

theorem Mathlib.Meta.NormNum.isInt_ediv_neg {a : ℤ} {b : ℤ} {q : ℤ} {q' : ℤ} (h : Mathlib.Meta.NormNum.IsInt (a / -b) q) (hq : -q = q') : Mathlib.Meta.NormNum.IsInt (a / b) q'

theorem Mathlib.Meta.NormNum.isNat_neg_of_isNegNat {a : ℤ} {b : ℕ} (h : Mathlib.Meta.NormNum.IsInt a (Int.negOfNat b)) : Mathlib.Meta.NormNum.IsNat (-a) b

def Mathlib.Meta.NormNum.evalIntDiv : Mathlib.Meta.NormNum.NormNumExt

The norm_num extension which identifies expressions of the form Int.ediv 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.evalIntDiv.core (a : Q(ℤ)) (na : Q(ℤ)) (za : ℤ) (pa : Q(Mathlib.Meta.NormNum.IsInt «$a» «$na»)) (b : Q(ℤ)) (nb : Q(ℕ)) (pb : Q(Mathlib.Meta.NormNum.IsNat «$b» «$nb»)) : ℤ × (q : Q(ℤ)) × Q(Mathlib.Meta.NormNum.IsInt («$a» / «$b») «$q»)

Given a result for evaluating a b in ℤ where b > 0, evaluate a / b.

theorem Mathlib.Meta.NormNum.isInt_emod_zero {a : ℤ} {b : ℤ} {r : ℤ} : Mathlib.Meta.NormNum.IsInt a r → Mathlib.Meta.NormNum.IsNat b 0 → Mathlib.Meta.NormNum.IsInt (a % b) r

theorem Mathlib.Meta.NormNum.isInt_emod {a : ℤ} {b : ℤ} {q : ℤ} {m : ℤ} {a' : ℤ} {b' : ℕ} {r : ℕ} (ha : Mathlib.Meta.NormNum.IsInt a a') (hb : Mathlib.Meta.NormNum.IsNat b b') (hm : q * ↑b' = m) (h : ↑r + m = a') (h₂ : r.blt b' = true) : Mathlib.Meta.NormNum.IsNat (a % b) r

theorem Mathlib.Meta.NormNum.isInt_emod_neg {a : ℤ} {b : ℤ} {r : ℕ} (h : Mathlib.Meta.NormNum.IsNat (a % -b) r) : Mathlib.Meta.NormNum.IsNat (a % b) r

def Mathlib.Meta.NormNum.evalIntMod : Mathlib.Meta.NormNum.NormNumExt

The norm_num extension which identifies expressions of the form Int.emod 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.evalIntMod.go (a : Q(ℤ)) (na : Q(ℤ)) (za : ℤ) (pa : Q(Mathlib.Meta.NormNum.IsInt «$a» «$na»)) (b : Q(ℤ)) : Mathlib.Meta.NormNum.Result b → Option (Mathlib.Meta.NormNum.Result q(«$a» % «$b»))

Given a result for evaluating a b in ℤ, evaluate a % b.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Meta.NormNum.evalIntMod.go a na za pa b x = none

def Mathlib.Meta.NormNum.evalIntMod.core (a : Q(ℤ)) (na : Q(ℤ)) (za : ℤ) (pa : Q(Mathlib.Meta.NormNum.IsInt «$a» «$na»)) (b : Q(ℤ)) (nb : Q(ℕ)) (pb : Q(Mathlib.Meta.NormNum.IsNat «$b» «$nb»)) : (r : Q(ℕ)) × Q(Mathlib.Meta.NormNum.IsNat («$a» % «$b») «$r»)

Given a result for evaluating a b in ℤ where b > 0, evaluate a % b.

theorem Mathlib.Meta.NormNum.isInt_dvd_true {a : ℤ} {b : ℤ} {a' : ℤ} {b' : ℤ} {c : ℤ} : Mathlib.Meta.NormNum.IsInt a a' → Mathlib.Meta.NormNum.IsInt b b' → a'.mul c = b' → a ∣ b

theorem Mathlib.Meta.NormNum.isInt_dvd_false {a : ℤ} {b : ℤ} {a' : ℤ} {b' : ℤ} : Mathlib.Meta.NormNum.IsInt a a' → Mathlib.Meta.NormNum.IsInt b b' → (b'.emod a' != 0) = true → ¬a ∣ b

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