feat(Tactic): `ring` modulo a given characteristic

[Vierkantor]

trafficstars

This PR extends the ring tactic with a new config argument char which will try to reduce all constant terms modulo the given characteristic. This allows ring to prove e.g. (x + y)^3 = x^3 + y^3 in characteristic 3. This is a simpler and faster way to do so than what we had before: repeat { ring; reduce_mod_char } becomes ring (config := { char := 3 }).

The first step is to split off the required CharP definitions, since Mathlib.Algebra.CharP.Basic already requires the ring tactic.

To perform the reduction modulo the given characteristic, I implemented reduceCast which reduces a raw integer, and wrapped it in reduceResult that takes a NormNum.Result for easy use. We need to pass through quite a few parameters into reduceResult so maybe it's worth defining a structure, or reusing Cache for this.

Then it's basically a case of replacing every place where ring constructs a numeral with a call to reduceResult.

Limitations:

• ring doesn't attempt to detect the characteristic by itself, you need to pass it in explicitly. Trying to infer a CharP instance at each point sounds quite expensive.
• Since the support for % in NormNum only exists for integers, I implemented the reduction only when a Ring instance is available. It is still sound in the semiring case, just not complete.
• We could optimize exponentiation in the specific case where the characteristic p is a prime that divides the exponent n: (x + y)^n = x^n + y^n. I'll leave that to future work.

---

• [ ] depends on: #12907

[YaelDillies]

Stupid question: Can we hardcode a few common rings of known characteristic to avoid the user having to provide the characteristic in most cases?

[Vierkantor]

Stupid question: Can we hardcode a few common rings of known characteristic to avoid the user having to provide the characteristic in most cases?

That was indeed the original plan (see also reduce_mod_char). It turns out the application of this tactic in the current project is over a generic, free variable, ring. Therefore, for this initial version the characteristic will need to be supplied. The addition of autodetection of characteristic may be done in a follow-up pull request.

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#12907~~ By Dependent Issues (🤖). Happy coding!

[github-actions[bot]]

PR summary c97f1a6bda

Import changes

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.Ring.Basic	489	519	+30 (+6.13%)
Mathlib.Tactic.Ring.RingNF	491	520	+29 (+5.91%)
Mathlib.Tactic.Polyrith	497	526	+29 (+5.84%)

---

Declarations diff

+ CharP.isInt_of_mod + RingConfig + evalCastReduced

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[joneugster]

@Vierkantor do you think you have time update this PR again, so we can get it merged?

I'll add "help-wanted" if anybody is inclined:

• merge master
• fix conflicts
• address 2 comments above
• have a final look over the PR