reduce_mod_char doesn't work

Stream: mathlib4

[Floris van Doorn]

I don't know how to get the tactic reduce_mod_char to do anything for me in a (variable) ring with a CharP hypothesis. @Anne Baanen

import Mathlib.Tactic

example {R} [CommRing R] [CharP R 3] (x : R) : x + x + x + x = x := by
  ring
  reduce_mod_char -- no progress

example {R} [CommRing R] [CharP R 2] (x y : R) : (x + y) ^ 2 = x ^ 2 + y ^ 2 := by
  ring
  reduce_mod_char -- no progress

example {R : Type*} [Ring R] [CharP R 2] : (2 : R) = 0 := by
  reduce_mod_char -- no progress

example {R : Type*} [Ring R] [CharP R 2] (r : R) : 2 • r = 0 := by
  reduce_mod_char -- no progress

example {R : Type*} [Ring R] [CharP R 2] (r : R) : (2 : ℤ) • r = 0 := by
  reduce_mod_char -- no progress

[Markus Himmel]

I don't think reduce_mod_char searches for a CharP instance at all. It contains a hardcoded list of supported types:

/-- 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. -/
partial def typeToCharP (t : Q(Type u)) : TypeToCharPResult t :=
match Expr.getAppFnArgs t with
| (``ZMod, #[(n : Q(ℕ))]) => .intLike n
  (q((ZMod.commRing _).toRing) : Q(Ring (ZMod $n)))
  (q(ZMod.charP _) : Q(CharP (ZMod $n) $n))
| (``Polynomial, #[(R : Q(Type u)), _]) => match typeToCharP R with
  | (.intLike n _ _) => .intLike n
    (q(Polynomial.ring) : Q(Ring (Polynomial $R)))
    (q(Polynomial.instCharP _) : Q(CharP (Polynomial $R) $n))
  | .failure => .failure
| _ => .failure

[Alex J. Best]

Huh, that seems like it should be easy to support (iirc Anne's Lean 3 version did support this, and it certainly seems coded up with that in mind also)

[Anne Baanen]

(I posted this reply a couple days ago, but I can't see it now so I'll repost. Sorry for possibly spamming the topic.)

Markus is right. The reason that this is not supported currently is that the tactic avoids searching for a CharP instance on every type of every subexpression, which saves quite a bit of time in my testcases. I suppose adding a reduce_mod_char! variant that does do the instance search would be an easy fix. (Or maybe the user can pass the type on which to operate?)

[Anne Baanen]

I tried implementing the typeclass search approach and ran into an issue: docs#CharP in CharP R n doesn't have n as an outParam, so it's not supposed to be assignable during instance search. So when we ask for an instance of CharP R ?n with [CharP R 2] in the context, the unification ?n =?= 2 fails. Is there a workaround?

[Yaël Dillies]

Try typeclass search with every possible n? :speak_no_evil:

[Anne Baanen]

(Modifying the depth of the metavariable after creating it doesn't work, because it's subsequently checked in the original depth, so the metavariable won't be assignable during that check.)

[Anne Baanen]

Here's the code I came up with:

partial def typeToCharP (expensive := false) (t : Q(Type u)) : MetaM (TypeToCharPResult t) :=
match Expr.getAppFnArgs t with
| (``ZMod, #[(n : Q(ℕ))]) =>
  return .intLike n
    (q((ZMod.commRing _).toRing) : Q(Ring (ZMod $n)))
    (q(ZMod.charP _) : Q(CharP (ZMod $n) $n))
| (``Polynomial, #[(R : Q(Type u)), _]) => do match ← typeToCharP (expensive := expensive) R with
  | (.intLike n _ _) =>
    return .intLike n
      (q(Polynomial.ring) : Q(Ring (Polynomial $R)))
      (q(Polynomial.instCharP _) : Q(CharP (Polynomial $R) $n))
  | .failure => return .failure
| _ => if ! expensive then return .failure else do
  -- Fallback: run an expensive procedures to determine a characteristic,
  -- by looking for a `CharP` instance.
  withNewMCtxDepth do
    /- If we want to support semirings, here we could implement the `natLike` fallback. -/
    let .some instRing ← trySynthInstanceQ q(Ring $t) | return .failure

    let n ← mkFreshExprMVarQ q(ℕ)
    /-
    -- Evil hack because we do want `n` to be assigned by `synthInstance`.
    modifyMCtx fun mctx => mctx.modifyExprMVarDecl n.mvarId!
      fun decl => { decl with depth := decl.depth + 1 }
    -/
    let .some instCharP ← trySynthInstanceQ q(CharP $t $n) | return .failure

    return .intLike (← instantiateMVarsQ n) instRing instCharP

[Yaël Dillies]

Can't you create a new metavariable at the correct depth, unify that one, then unify it with the old one too?

[Yaël Dillies]

The point being that both unifications can be done at different depths

[Anne Baanen]

synthInstance does both unifications internally, so I don't see how to pass in two different metavariables in one call.

[Yaël Dillies]

Do the first one using synthInstance, the second one manually?

[Anne Baanen]

No no, I mean that synthInstance unifies CharP R ?n =?= CharP R 2 twice: once inside a withNewMCtxDepth (when trying candidate instances) and once outside (when checking that the resulting instance is correct). I don't see a way to separate these out without reimplementing a large part of the instance synthesis functions.

[Alex J. Best]

Is docs#ringChar.charP the only reason we don't just make the n an out param? Maybe its time we reconsidered how this is all set up

[Anne Baanen]

Yes, I assume the problem is that we might get equal-but-not-defeq values for ?n from a CharP R ?n goal. But that shouldn't be a big issue, right?

[Anne Baanen]

Here's a PR that makes the first few examples in this thread work: #11478. The last ones require support for (n, z, ...)-smul which we can do in a separate, and hopefully easier, PR.

[Floris van Doorn]

Anne Baanen said:

(I posted this reply a couple days ago, but I can't see it now so I'll repost. Sorry for possibly spamming the topic.)

Markus is right. The reason that this is not supported currently is that the tactic avoids searching for a CharP instance on every type of every subexpression, which saves quite a bit of time in my testcases. I suppose adding a reduce_mod_char! variant that does do the instance search would be an easy fix. (Or maybe the user can pass the type on which to operate?)

Other tactics like ring and norm_num also search for a lot of type classes, so that doesn't sound like an inherent problem for a performant tactic.
The fact that the n is a metavariable during type-class search is a problem of course.
I think looking for variables in the local context is a good compromise.