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.cast_int_eq_mod (R : Type u_1) [Ring R] (p : ℕ) [CharP R p] (k : ℤ) : ↑k = ↑(k % ↑p)

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

def Tactic.ReduceModChar.normIntNumeral {u : Lean.Level} {α : Q(Type u)} (n : Q(ℕ)) (e : Q(«$α»)) (instRing : 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.

Equations

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

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.

Equations

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

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.

Equations

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

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 «$α»)) → Q(CharP «$α» «$n») → Tactic.ReduceModChar.TypeToCharPResult α
• failure: {u : Lean.Level} → {α : Q(Type u)} → Tactic.ReduceModChar.TypeToCharPResult α

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

Equations

• Tactic.ReduceModChar.instInhabitedTypeToCharPResult = { default := Tactic.ReduceModChar.TypeToCharPResult.failure }

partial def Tactic.ReduceModChar.typeToCharP {u : Lean.Level} (t : Q(Type u)) : Tactic.ReduceModChar.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.

def Tactic.ReduceModChar.matchAndNorm (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.

Equations

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

def Tactic.ReduceModChar.derive (e : Lean.Expr) : Lean.MetaM Lean.Meta.Simp.Result

Reduce all numeric subexpressions of e modulo their characteristic.

Equations

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

def Tactic.ReduceModChar.reduceModCharTarget : Lean.Elab.Tactic.TacticM Unit

Reduce all numeric subexpressions of the goal modulo their characteristic.

Equations

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

def Tactic.ReduceModChar.reduceModCharHyp (fvarId : Lean.FVarId) : Lean.Elab.Tactic.TacticM Unit

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

Equations

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

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.

Equations

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