reduce_mod_char tactic

Define the reduce_mod_char tactic, which traverses expressions looking for numerals n, such that the type of n is a ring of (positive) characteristic p, and reduces these numerals modulo p, to lie between 0 and p.

Implementation

The main entry point is ReduceModChar.derive, which uses simp to traverse expressions and calls matchAndNorm on each subexpression. The type of each subexpression is matched syntactically to determine if it is a ring with positive characteristic in typeToCharP. Using syntactic matching should be faster than trying to infer a CharP instance on each subexpression. The actual reduction happens in normIntNumeral. This is written to be compatible with norm_num so it can serve as a drop-in replacement for some norm_num-based routines (specifically, the intended use is as an option for the ring tactic).

In addition to the main functionality, we call normNeg and normNegCoeffMul to replace negation with multiplication by p - 1, and simp lemmas tagged @[reduce_mod_char] to clean up the resulting expression: e.g. 1 * X + 0 becomes X.

theorem Tactic.ReduceModChar.CharP.isInt_of_mod {e' r : ℤ} {α : Type u_1} [Ring α] {n n' : ℕ} (inst : CharP α n) {e : α} (he : Mathlib.Meta.NormNum.IsInt e e') (hn : Mathlib.Meta.NormNum.IsNat n n') (h₂ : Mathlib.Meta.NormNum.IsInt (e' % ↑n') r) : Mathlib.Meta.NormNum.IsInt e r

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

def Tactic.ReduceModChar.normBareNumeral {u : Lean.Level} {α : Q(Type u)} (n n' : Q(ℕ)) (pn : Q(Mathlib.Meta.NormNum.IsNat «$n» «$n'»)) (e : Q(«$α»)) (x✝ : Q(Ring «$α»)) (instCharP : Q(CharP «$α» «$n»)) : Lean.MetaM (Mathlib.Meta.NormNum.Result e)

Evaluates e to an integer using norm_num and reduces the result modulo n.

partial def Tactic.ReduceModChar.normPow {u : Lean.Level} {α : Q(Type u)} (n n' : Q(ℕ)) (pn : Q(Mathlib.Meta.NormNum.IsNat «$n» «$n'»)) (e : Q(«$α»)) (x✝ : Q(Ring «$α»)) (instCharP : Q(CharP «$α» «$n»)) : Lean.MetaM (Mathlib.Meta.NormNum.Result e)

Given an expression of the form a ^ b in a ring of characteristic n, reduces a modulo n recursively and then calculates a ^ b using fast modular exponentiation.

partial def Tactic.ReduceModChar.normIntNumeral' {u : Lean.Level} {α : Q(Type u)} (n n' : Q(ℕ)) (pn : Q(Mathlib.Meta.NormNum.IsNat «$n» «$n'»)) (e : Q(«$α»)) (x✝ : Q(Ring «$α»)) (instCharP : Q(CharP «$α» «$n»)) : Lean.MetaM (Mathlib.Meta.NormNum.Result e)

If e is of the form a ^ b, reduce it using fast modular exponentiation, otherwise reduce it using norm_num.

theorem Tactic.ReduceModChar.CharP.intCast_eq_mod (R : Type u_1) [Ring R] (p : ℕ) [CharP R p] (k : ℤ) : ↑k = ↑(k % ↑p)

def Tactic.ReduceModChar.normIntNumeral {u : Lean.Level} {α : Q(Type u)} (n : Q(ℕ)) (e : Q(«$α»)) (x✝ : Q(Ring «$α»)) (instCharP : Q(CharP «$α» «$n»)) : Lean.MetaM (Mathlib.Meta.NormNum.Result e)

Given an integral expression e : t such that t is a ring of characteristic n, reduce e modulo n.

theorem Tactic.ReduceModChar.CharP.neg_eq_sub_one_mul {α : Type u_1} [Ring α] (n : ℕ) (inst : CharP α n) (b : α) (a : ℕ) (a' : α) (p : Mathlib.Meta.NormNum.IsNat (↑n - 1) a) (pa : ↑a = a') : -b = a' * b

def Tactic.ReduceModChar.normNeg {u : Lean.Level} {α : Q(Type u)} (n : Q(ℕ)) (e : Q(«$α»)) (_instRing : Q(Ring «$α»)) (instCharP : Q(CharP «$α» «$n»)) : Lean.MetaM Lean.Meta.Simp.Result

Given an expression (-e) : t such that t is a ring of characteristic n, simplify this to (n - 1) * e.

This should be called only when normIntNumeral fails, because normIntNumeral would otherwise be more useful by evaluating -e mod n to an actual numeral.

theorem Tactic.ReduceModChar.CharP.neg_mul_eq_sub_one_mul {α : Type u_1} [Ring α] (n : ℕ) (inst : CharP α n) (a b : α) (na : ℕ) (na' : α) (p : Mathlib.Meta.NormNum.IsNat ((↑n - 1) * a) na) (pa : ↑na = na') : -(a * b) = na' * b

def Tactic.ReduceModChar.normNegCoeffMul {u : Lean.Level} {α : Q(Type u)} (n : Q(ℕ)) (e : Q(«$α»)) (_instRing : Q(Ring «$α»)) (instCharP : Q(CharP «$α» «$n»)) : Lean.MetaM Lean.Meta.Simp.Result

Given an expression -(a * b) : t such that t is a ring of characteristic n, and a is a numeral, simplify this to ((n - 1) * a) * b.

inductive Tactic.ReduceModChar.TypeToCharPResult {u : Lean.Level} (α : Q(Type u)) : Type

A TypeToCharPResult α indicates if α can be determined to be a ring of characteristic p.

• intLike {u : Lean.Level} {α : Q(Type u)} (n : Q(ℕ)) (instRing : Q(Ring «$α»)) (instCharP : Q(CharP «$α» «$n»)) : TypeToCharPResult α
• failure {u : Lean.Level} {α : Q(Type u)} : TypeToCharPResult α

instance Tactic.ReduceModChar.instInhabitedTypeToCharPResult {u : Lean.Level} {α : Q(Type u)} : Inhabited (TypeToCharPResult α)

partial def Tactic.ReduceModChar.typeToCharP {u : Lean.Level} (expensive : Bool := false) (t : Q(Type u)) : Lean.MetaM (TypeToCharPResult t)

Determine the characteristic of a ring from the type. This should be fast, so this pattern-matches on the type, rather than searching for a CharP instance. Use typeToCharP (expensive := true) to do more work in finding the characteristic, in particular it will search for a CharP instance in the context.

def Tactic.ReduceModChar.matchAndNorm (expensive : Bool := false) (e : Lean.Expr) : Lean.MetaM Lean.Meta.Simp.Result

Given an expression e, determine whether it is a numeric expression in characteristic n, and if so, reduce e modulo n.

This is not a norm_num plugin because it does not match on the syntax of e, rather it matches on the type of e.

Use matchAndNorm (expensive := true) to do more work in finding the characteristic of the type of e.

def Tactic.ReduceModChar.derive (expensive : Bool := false) (e : Lean.Expr) : Lean.MetaM Lean.Meta.Simp.Result

Reduce all numeric subexpressions of e modulo their characteristic.

Use derive (expensive := true) to do more work in finding the characteristic of the type of e.

def Tactic.ReduceModChar.reduceModCharTarget (expensive : Bool := false) : Lean.Elab.Tactic.TacticM Unit

Reduce all numeric subexpressions of the goal modulo their characteristic.

def Tactic.ReduceModChar.reduceModCharHyp (expensive : Bool := false) (fvarId : Lean.FVarId) : Lean.Elab.Tactic.TacticM Unit

Reduce all numeric subexpressions of the given hypothesis modulo their characteristic.

def Tactic.ReduceModChar.reduce_mod_char : Lean.ParserDescr

The tactic reduce_mod_char looks for numeric expressions in characteristic p and reduces these to lie between 0 and p.

For example:

example : (5 : ZMod 4) = 1 := by reduce_mod_char
example : (X ^ 2 - 3 * X + 4 : (ZMod 4)[X]) = X ^ 2 + X := by reduce_mod_char

It also handles negation, turning it into multiplication by p - 1, and similarly subtraction.

This tactic uses the type of the subexpression to figure out if it is indeed of positive characteristic, for improved performance compared to trying to synthesise a CharP instance. The variant reduce_mod_char! also tries to use CharP R n hypotheses in the context. (Limitations of the typeclass system mean the tactic can't search for a CharP R n instance if n is not yet known; use have : CharP R n := inferInstance; reduce_mod_char! as a workaround.)

def Tactic.ReduceModChar.reduce_mod_char! : Lean.ParserDescr

The tactic reduce_mod_char looks for numeric expressions in characteristic p and reduces these to lie between 0 and p.

For example:

example : (5 : ZMod 4) = 1 := by reduce_mod_char
example : (X ^ 2 - 3 * X + 4 : (ZMod 4)[X]) = X ^ 2 + X := by reduce_mod_char

It also handles negation, turning it into multiplication by p - 1, and similarly subtraction.

This tactic uses the type of the subexpression to figure out if it is indeed of positive characteristic, for improved performance compared to trying to synthesise a CharP instance. The variant reduce_mod_char! also tries to use CharP R n hypotheses in the context. (Limitations of the typeclass system mean the tactic can't search for a CharP R n instance if n is not yet known; use have : CharP R n := inferInstance; reduce_mod_char! as a workaround.)