Proof-producing evaluation of a ^ b % n

Note that Mathlib.Tactic.NormNum.PowMod contains a similar tactic, but that runs significantly slower and less efficiently than the one here.

def powMod (a b n : ℕ) : ℕ

The pow-mod function, named explicitly to allow more precise control of reduction.

Equations

• powMod a b n = a ^ b % n

def powModAux (a b c n : ℕ) : ℕ

The pow-mod auxiliary function, named explicitly to allow more precise control of reduction.

Equations

• powModAux a b c n = a ^ b * c % n

def Nat.eager (k : ℕ → ℕ) (n : ℕ) : ℕ

Equations

• Nat.eager k n = k (eagerReduce n)

noncomputable def powModTR (a b n : ℕ) : ℕ

Kernel-reducible tail-recursive modular exponentiation: computes a ^ b % n. Uses Nat.rec with bounded fuel so the kernel can reduce it via eagerReduce.

Equations

• powModTR a b n = powModTR.aux n b.succ (a.mod n) b 1

noncomputable def powModTR.aux (n : ℕ) : ℕ → (a b c : ℕ) → ℕ

Equations

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

def powModTR' (a b n : ℕ) : ℕ

Computable version of powModTR using partial_fixpoint. Used at elaboration time (e.g. in mkPowModEq') where we need actual computation, not kernel reduction.

Equations

• powModTR' a b n = powModTR'.aux n (a % n) b 1

@[irreducible]

def powModTR'.aux (n a b c : ℕ) : ℕ

Equations

• powModTR'.aux n a b c = if b = 0 then c % n else if b = 1 then a * c % n else if b % 2 = 0 then powModTR'.aux n (a * a % n) (b / 2) c else powModTR'.aux n (a * a % n) (b / 2) (a * c % n)

theorem Bool.rec_eq_ite {α : Type u_1} {b : Bool} {t f : α} : rec f t b = if b = true then t else f

@[simp]

theorem Nat.mod_eq_mod {a b : ℕ} : a.mod b = a % b

@[simp]

theorem Nat.div_eq_div {a b : ℕ} : a.div b = a / b

@[simp]

theorem Nat.land_eq_land {a b : ℕ} : a.land b = a &&& b

@[simp]

theorem powModTR_aux_zero_eq {n a b c : ℕ} : powModTR.aux n 0 a b c = 0

theorem powModTR_aux_succ_eq {n a b c fuel : ℕ} : powModTR.aux n (fuel + 1) a b c = Bool.rec (Bool.rec (powModTR.aux n fuel (a * a % n) (b / 2) (a * c % n)) (powModTR.aux n fuel (a * a % n) (b / 2) c) ((b % 2).beq 0)) (c % n) (b.beq 0)

theorem powModTR_aux_succ_eq' {n a b c fuel : ℕ} : powModTR.aux n (fuel + 1) a b c = if b = 0 then c % n else if b % 2 = 0 then powModTR.aux n fuel (a * a % n) (b / 2) c else powModTR.aux n fuel (a * a % n) (b / 2) (a * c % n)

theorem powModTR_aux_eq (n a b c fuel : ℕ) (hfuel : b < fuel) : powModTR.aux n fuel a b c = powModAux a b c n

theorem powModTR_eq (a b n : ℕ) : powModTR a b n = powMod a b n

theorem powMod_eq_of_powModTR (a b n m : ℕ) (h : (powModTR a b n).beq m = true) : powMod a b n = m

theorem powMod_ne_of_powModTR (a b n m : ℕ) (h : (powModTR a b n).beq m = false) : powMod a b n ≠ m

def Tactic.powMod.mkPowModEq' (a b n : ℕ) (aE bE nE : Lean.Expr) : Lean.MetaM (ℕ × Lean.Expr × Lean.Expr)

Given a, b, n : ℕ, return (m, ⊢ powMod a b n = m).

Equations

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

def Tactic.powMod.provePowModEq' (a b n m : ℕ) (aE bE nE : Lean.Expr) : Lean.MetaM Lean.Expr

Given a, b, n, m : ℕ, if powMod a b n = m then return a proof of that fact.

Equations

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

def Tactic.powMod.provePowModNe' (a b n m : ℕ) (aE bE nE mE : Lean.Expr) : Lean.MetaM Lean.Expr

Given a, b, n, m : ℕ, if powMod a b n ≠ m then return a proof of that fact.

Equations

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

def Tactic.powMod.prove_pow_mod_tac (g : Lean.MVarId) : Lean.MetaM Unit

Equations

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

def Tactic.powMod.tacticProve_pow_mod : Lean.ParserDescr

Tactic to close goals about modular exponentiation. Handles two goal shapes:

• powMod a b n = m — proves the equality by computing a ^ b % n at elaboration time
• powMod a b n ≠ m — proves the disequality similarly

All of a, b, n, m must be numeric literals. The computation uses powModTR' (the partial_fixpoint version) at elaboration time, then produces a kernel proof via powModTR and eagerReduce.

example : powMod 11 100002 100003 = 1 := by prove_pow_mod
example : powMod 2 100002 100003 ≠ 1 := by prove_pow_mod

Equations

• Tactic.powMod.tacticProve_pow_mod = Lean.ParserDescr.node `Tactic.powMod.tacticProve_pow_mod 1024 (Lean.ParserDescr.nonReservedSymbol "prove_pow_mod" false)