norm_num plugin for ^.

theorem Mathlib.Meta.NormNum.natPow_zero {a : ℕ} : a.pow 0 = 1

theorem Mathlib.Meta.NormNum.natPow_one {a : ℕ} : a.pow 1 = a

theorem Mathlib.Meta.NormNum.zero_natPow {b : ℕ} : Nat.pow 0 b.succ = 0

theorem Mathlib.Meta.NormNum.one_natPow {b : ℕ} : Nat.pow 1 b = 1

structure Mathlib.Meta.NormNum.IsNatPowT (p : Prop) (a b c : ℕ) : Prop

This is an opaque wrapper around Nat.pow to prevent lean from unfolding the definition of Nat.pow on numerals. The arbitrary precondition p is actually a formula of the form Nat.pow a' b' = c' but we usually don't care to unfold this proposition so we just carry a reference to it.

• run' : p → a.pow b = c

  Unfolds the assertion.

theorem Mathlib.Meta.NormNum.IsNatPowT.run {a b c : ℕ} (p : IsNatPowT (a.pow 1 = a) a b c) : a.pow b = c

theorem Mathlib.Meta.NormNum.IsNatPowT.trans {a b c : ℕ} {p : Prop} {b' c' : ℕ} (h1 : IsNatPowT p a b c) (h2 : IsNatPowT (a.pow b = c) a b' c') : IsNatPowT p a b' c'

This is the key to making the proof proceed as a balanced tree of applications instead of a linear sequence. It is just modus ponens after unwrapping the definitions.

theorem Mathlib.Meta.NormNum.IsNatPowT.bit0 {a b c : ℕ} : IsNatPowT (a.pow b = c) a (2 * b) (c.mul c)

theorem Mathlib.Meta.NormNum.IsNatPowT.bit1 {a b c : ℕ} : IsNatPowT (a.pow b = c) a (2 * b + 1) (c.mul (c.mul a))

def Mathlib.Meta.NormNum.evalNatPow (a b : Q(ℕ)) : (c : Q(ℕ)) × Q(«$a».pow «$b» = «$c»)

Proves Nat.pow a b = c where a and b are raw nat literals. This could be done by just rfl but the kernel does not have a special case implementation for Nat.pow so this would proceed by unary recursion on b, which is too slow and also leads to deep recursion.

We instead do the proof by binary recursion, but this can still lead to deep recursion, so we use an additional trick to do binary subdivision on log2 b. As a result this produces a proof of depth log (log b) which will essentially never overflow before the numbers involved themselves exceed memory limits.

partial def Mathlib.Meta.NormNum.evalNatPow.go (depth : ℕ) (a b₀ c₀ b : Q(ℕ)) (p : Q(Prop)) (hp : «$p» =Q («$a».pow «$b₀» = «$c₀»)) : (c : Q(ℕ)) × Q(IsNatPowT «$p» «$a» «$b» «$c»)

Invariants: a ^ b₀ = c₀, depth > 0, b >>> depth = b₀, p := Nat.pow $a $b₀ = $c₀

theorem Mathlib.Meta.NormNum.intPow_ofNat {a b c : ℕ} (h1 : a.pow b = c) : (Int.ofNat a).pow b = Int.ofNat c

theorem Mathlib.Meta.NormNum.intPow_negOfNat_bit0 {a b c b' c' : ℕ} (h1 : a.pow b' = c') (hb : 2 * b' = b) (hc : c' * c' = c) : (Int.negOfNat a).pow b = Int.ofNat c

theorem Mathlib.Meta.NormNum.intPow_negOfNat_bit1 {a b c b' c' : ℕ} (h1 : a.pow b' = c') (hb : 2 * b' + 1 = b) (hc : c' * (c' * a) = c) : (Int.negOfNat a).pow b = Int.negOfNat c

def Mathlib.Meta.NormNum.evalIntPow (za : ℤ) (a : Q(ℤ)) (b : Q(ℕ)) : ℤ × (c : Q(ℤ)) × Q(«$a».pow «$b» = «$c»)

Evaluates Int.pow a b = c where a and b are raw integer literals.

theorem Mathlib.Meta.NormNum.isNat_pow {α : Type u_1} [Semiring α] {f : α → ℕ → α} {a : α} {b a' b' c : ℕ} : f = HPow.hPow → IsNat a a' → IsNat b b' → a'.pow b' = c → IsNat (f a b) c

theorem Mathlib.Meta.NormNum.isInt_pow {α : Type u_1} [Ring α] {f : α → ℕ → α} {a : α} {b : ℕ} {a' : ℤ} {b' : ℕ} {c : ℤ} : f = HPow.hPow → IsInt a a' → IsNat b b' → a'.pow b' = c → IsInt (f a b) c

theorem Mathlib.Meta.NormNum.isRat_pow {α : Type u_1} [Ring α] {f : α → ℕ → α} {a : α} {an cn : ℤ} {ad b b' cd : ℕ} : f = HPow.hPow → IsRat a an ad → IsNat b b' → an.pow b' = cn → ad.pow b' = cd → IsRat (f a b) cn cd

def Mathlib.Meta.NormNum.evalPow : NormNumExt

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

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

Main part of evalPow.

theorem Mathlib.Meta.NormNum.isNat_zpow_pos {α : Type u_1} [DivisionSemiring α] {a : α} {b : ℤ} {nb ne : ℕ} (pb : IsNat b nb) (pe' : IsNat (a ^ nb) ne) : IsNat (a ^ b) ne

theorem Mathlib.Meta.NormNum.isNat_zpow_neg {α : Type u_1} [DivisionSemiring α] {a : α} {b : ℤ} {nb ne : ℕ} (pb : IsInt b (Int.negOfNat nb)) (pe' : IsNat (a ^ nb)⁻¹ ne) : IsNat (a ^ b) ne

theorem Mathlib.Meta.NormNum.isInt_zpow_pos {α : Type u_1} [DivisionRing α] {a : α} {b : ℤ} {nb ne : ℕ} (pb : IsNat b nb) (pe' : IsInt (a ^ nb) (Int.negOfNat ne)) : IsInt (a ^ b) (Int.negOfNat ne)

theorem Mathlib.Meta.NormNum.isInt_zpow_neg {α : Type u_1} [DivisionRing α] {a : α} {b : ℤ} {nb ne : ℕ} (pb : IsInt b (Int.negOfNat nb)) (pe' : IsInt (a ^ nb)⁻¹ (Int.negOfNat ne)) : IsInt (a ^ b) (Int.negOfNat ne)

theorem Mathlib.Meta.NormNum.isRat_zpow_pos {α : Type u_1} [DivisionRing α] {a : α} {b : ℤ} {nb : ℕ} {num : ℤ} {den : ℕ} (pb : IsNat b nb) (pe' : IsRat (a ^ nb) num den) : IsRat (a ^ b) num den

theorem Mathlib.Meta.NormNum.isRat_zpow_neg {α : Type u_1} [DivisionRing α] {a : α} {b : ℤ} {nb : ℕ} {num : ℤ} {den : ℕ} (pb : IsInt b (Int.negOfNat nb)) (pe' : IsRat (a ^ nb)⁻¹ num den) : IsRat (a ^ b) num den

def Mathlib.Meta.NormNum.evalZPow : NormNumExt

The norm_num extension which identifies expressions of the form a ^ b, such that norm_num successfully recognises both a and b, with b : ℤ.