norm_num on Fin

Stream: mathlib4

[Yakov Pechersky]

In mathlib3, we had norm_num and norm_fin, which did reductions of expressions like (3 : Fin 3) to 0. So norm_num could solve (3 : Fin 3) = 0. I'm trying to extend mathlib4 norm_num to do the same. It seems a path would be to hardcode a branch in mkOfNat.:

def mkOfNat (α : Q(Type u)) (_sα : Q(AddMonoidWithOne $α)) (lit : Q(ℕ)) :
    MetaM ((a' : Q($α)) × Q($lit = $a')) := do
  if α.isConstOf ``Nat then
    let a' : Q(ℕ) := q(OfNat.ofNat $lit : ℕ)
    pure ⟨a', (q(Eq.refl $a') : Expr)⟩
  else if α.isConstOf ``Int then
    let a' : Q(ℤ) := q(OfNat.ofNat $lit : ℤ)
    pure ⟨a', (q(Eq.refl $a') : Expr)⟩
  else if α.isConstOf ``Rat then
    let a' : Q(ℚ) := q(OfNat.ofNat $lit : ℚ)
    pure ⟨a', (q(Eq.refl $a') : Expr)⟩
  else if α.isAppOf ``Fin then
    trace[Tactic.norm_num] "inside Fin α := {α}"
    let .app (.const `Fin _) (n : Q(ℕ)) ← whnfR α | failure
    trace[Tactic.norm_num] "inside Fin qn := {n}"
    let some n := n.natLit? | failure -- fails here; need to `deriveNat n` possibly?
    trace[Tactic.norm_num] "inside Fin n := {n}"
    let some x := lit.natLit? | failure
    trace[Tactic.norm_num] "inside Fin {x} {n}"
    match (x % n) with
    | 0 => pure ⟨q(0 : $α), (q(Nat.cast_zero (R := $α)) : Expr)⟩
    | 1 => pure ⟨q(1 : $α), (q(Nat.cast_one (R := $α)) : Expr)⟩
    | k+2 =>
      let k : Q(ℕ) := mkRawNatLit k
      let _x : Q(Nat.AtLeastTwo $lit) :=
        (q(instNatAtLeastTwo (n := $k)) : Expr)
      let a' : Q($α) := q(OfNat.ofNat $lit)
      pure ⟨a', (q(Eq.refl $a') : Expr)⟩
  else
    let some n := lit.natLit? | failure
    match n with
    | 0 => pure ⟨q(0 : $α), (q(Nat.cast_zero (R := $α)) : Expr)⟩
    | 1 => pure ⟨q(1 : $α), (q(Nat.cast_one (R := $α)) : Expr)⟩
    | k+2 =>
      let k : Q(ℕ) := mkRawNatLit k
      let _x : Q(Nat.AtLeastTwo $lit) :=
        (q(instNatAtLeastTwo (n := $k)) : Expr)
      let a' : Q($α) := q(OfNat.ofNat $lit)
      pure ⟨a', (q(Eq.refl $a') : Expr)⟩

[Yakov Pechersky]

But the n.natLit? is failing, which makes sense, it's not really a literal at that point. Somehow I have to extract the nat value from the expression -- is this where deriveNat should come in?

[Yakov Pechersky]

Or, separately, one could image writing a specific norm_num extension for Fin, but I would think it would be for catching @OfNat.ofNat (Fin _) _ _, which is already caught by the existing @[norm_num OfNat.ofNat _] def evalOfNat. How does norm_num currently handle overlapping extensions?

[Yakov Pechersky]

The motivating example here to make neater is:

import Mathlib.GroupTheory.Perm.List
import Mathlib.Tactic.FinCases
import Mathlib.Tactic.NormNum

def exercise36_hom3 : Fin 3 →+ Additive (Equiv.Perm (Fin 3)) :=
  AddMonoidHom.mk' (fun k => match k with
  | 0 => 0
  | 1 => Additive.ofMul (List.formPerm [0, 1, 2])
  | 2 => Additive.ofMul (List.formPerm [0, 2, 1])
  ) (by
    intros a b
    have h2 : (⟨2, by norm_num⟩ : Fin 3) = 2 := rfl
    have h3 : (3 : Fin 3) = ⟨0, by norm_num⟩ := rfl
    have h4 : (4 : Fin 3) = ⟨1, by norm_num⟩ := rfl
    fin_cases a <;>
    fin_cases b
    · simp
    · simp
    · simp
    · simp
    · norm_num
      simp_rw [←h2, ←ofMul_mul]
      simp [-ofMul_mul]
    · norm_num [h2]
      simp_rw [←ofMul_mul]
      rw [h3, eq_comm]
      simp [-ofMul_mul]
    · simp
    · norm_num [h2]
      simp_rw [h3, ←ofMul_mul]
      rw [eq_comm]
      simp [-ofMul_mul]
    · norm_num [h2]
      simp_rw [h4, ←ofMul_mul]
      rw [eq_comm]
      simp [-ofMul_mul])

[Yakov Pechersky]

Perhaps it is also a fin_cases concern, that it shouldn't break down a Fin into a Fin.mk expression.

[Alex J. Best]

This should hopefully be handled by #5376

[Alex J. Best]

See also https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Reducing.20mod.20n/near/387773271 if you just want the case of numerals equal to the characteristic to be reduced

[Yakov Pechersky]

In the meantime, if I wanted to match solely on FIn (instead of all char p rings), what would be the right syntax?

[Michael Stoll]

What happened to this effort? So far, norm_num still does not simplify 8 * a to zero, when a : ZMod 8...

[Alex J. Best]

I think #5376 still needs some work, it looks like it basically works, but linting fails and it gets merge conflicts sometimes. Anne is busy writing their PhD thesis so it probably isnt their first priority right now. So maybe we shoud be a bit more proactive in fixing the (seemingly minor) issues with the branch for them. It does solve your problem so there is certainly benefit to merging it even if other improvements are planned

[Anne Baanen]

I'm mostly done with my thesis now, but getting back into active work on mathlib is proving harder than expected. I'll do my best to get this PR in a good shape next week, and help is always deeply appreciated!