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

.

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.

## Instances For

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.

## Instances For

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.

## Instances For

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 α

## Instances For

## Equations

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

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.

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.

## Instances For

Reduce all numeric subexpressions of `e`

modulo their characteristic.

## Equations

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

## Instances For

Reduce all numeric subexpressions of the goal modulo their characteristic.

## Equations

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

## Instances For

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

## Equations

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

## Instances For

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.