norm_num handling for expressions of the form a ^ b % m.

These expressions can often be evaluated efficiently in cases where first evaluating a ^ b and then reducing mod m is not feasible. We provide a function evalNatPowMod which is used by the reduce_mod_char tactic to efficiently evaluate powers in rings with positive characteristic.

The approach taken here is identical to (and copied from) the development in NormNum/Pow.lean.

TODO

• Adapt the norm_num extensions for Nat.mod and Int.emod to efficiently evaluate expressions of the form a ^ b % m using evalNatPowMod.

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

Represents and proves equalities of the form a^b % m = c for natural numbers.

• run' : p → (a.pow b).mod m = c

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

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

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

theorem Mathlib.Meta.NormNum.natPow_zero_natMod_zero {a : ℕ} : (a.pow 0).mod 0 = 1

theorem Mathlib.Meta.NormNum.natPow_zero_natMod_one {a : ℕ} : (a.pow 0).mod 1 = 0

theorem Mathlib.Meta.NormNum.natPow_zero_natMod_succ_succ {a : ℕ} {m : ℕ} : (a.pow 0).mod m.succ.succ = 1

theorem Mathlib.Meta.NormNum.natPow_one_natMod {a m : ℕ} : (a.pow 1).mod m = a.mod m

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

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

Evaluates and proves a^b % m for natural numbers using fast modular exponentiation.

Equations

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

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

Invariants: a ^ b₀ % m = c₀, depth > 0, b >>> depth = b₀