Documentation

Mathlib.Tactic.NormNum.PowMod

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 #

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 : Mathlib.Meta.NormNum.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 : Mathlib.Meta.NormNum.IsNatPowModT p a b m c) (h2 : Mathlib.Meta.NormNum.IsNatPowModT ((a.pow b).mod m = c) a b' m c') :
    Mathlib.Meta.NormNum.IsNatPowModT p a b' m c'
    source
    theorem Mathlib.Meta.NormNum.IsNatPowModT.bit0 {a b m : ℕ} {c : ℕ} :
    Mathlib.Meta.NormNum.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 : ℕ} :
    Mathlib.Meta.NormNum.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(Mathlib.Meta.NormNum.IsNatPowModT «$p» «$a» «$b» «$m» «$c»)

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