norm_num in finite characteristic

Stream: mathlib4

[Matthew Ballard]

The following makes me sad

import Mathlib.Data.ZMod.Basic

/--
error: unsolved goals
⊢ ¬0 = 1
-/
#guard_msgs in
example : (0 : ZMod 5) ≠ (1 : ZMod 5) := by norm_num

[Matthew Ballard]

One culprit is docs#Mathlib.Tactic.Normnum.evalEq L101

  | .isNat _ na pa, .isNat mα nb pb =>
    assumeInstancesCommute
    if na.natLit! = nb.natLit! then
      haveI' : $na =Q $nb := ⟨⟩
      return .isTrue q(isNat_eq_true $pa $pb)
    else if let some _ ← inferCharZeroOfAddMonoidWithOne? mα then
      let r : Q(Nat.beq $na $nb = false) := (q(Eq.refl false) : Expr)
      return .isFalse q(isNat_eq_false $pa $pb $r)
    else
      failure --TODO: nonzero characteristic ≠

[Matthew Ballard]

Correct me if I wrong but there is no simple way to return all the m such that CharP R m instance is registered right?

[Matthew Ballard]

It seems simpler to refactor to include .isNatMod

[Adam Topaz]

I think it would be relatively straightforward to obtain all m such that CharP R m is registered directly, given a particular R. E.g. in this case it should be easy to find docs#ZMod.CharP` in the environment.

[Adam Topaz]

But yeah, presumably adding a isNatMod would be more direct.

[Matthew Ballard]

Oh yeah. I guess I could just query the instance cache.