# `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`.

source
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

Instances For

source
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
source
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'
source
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)
source
theorem Mathlib.Meta.NormNum.natPow_zero_natMod_zero {a : ℕ} :
(a.pow 0).mod 0 = 1
source
theorem Mathlib.Meta.NormNum.natPow_zero_natMod_one {a : ℕ} :
(a.pow 0).mod 1 = 0
source
theorem Mathlib.Meta.NormNum.natPow_zero_natMod_succ_succ {a : ℕ} {m : ℕ} :
(a.pow 0).mod m.succ.succ = 1
source
theorem Mathlib.Meta.NormNum.natPow_one_natMod {a m : ℕ} :
(a.pow 1).mod m = a.mod m
source
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)
source
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.

Instances For

source
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₀`