simp and matching on ZMod

Stream: lean4

[Toby Cathcart Burn]

I'm updating a proof from v4.20.0-rc5 to v4.22.0-rc3 and simp is no longer always reducing match statements involving ZMod. Minimal example:

import Mathlib

noncomputable def f (rot : ZMod 4) : ℕ := match rot with
  | 0 => 1
  | 1 => 2
  | 2 => 3
  | 3 => 4

--works
example : f 0 = 1 := by
  simp [f]
example : f 1 = 2 := by
  simp [f]

--don't work
example : f 2 = 3 := by
  simp [f]
example : f 3 = 4 := by
  simp [f]
/-
unsolved goals
⊢ (match 3 with
    | 0 => 1
    | 1 => 2
    | 2 => 3
    | 3 => 4) =
    4
-/

-- works (my current fix)
example : f 2 = 3 := by
  simp [f.eq_3]
example : f 3 = 4 := by
  simp [f.eq_4]

It looks related to #mathlib4 > #eval returns `unreachable code`.

[Aaron Liu]

I don't think this is related to #mathlib4 > #eval returns `unreachable code` because that's a compiler bug and this isn't compiling anything

[Toby Cathcart Burn]

I thought both might have arisen from a change in how lean sees the connection between ZMod and Fin, but I'm not claiming to understand any details.

[Robin Arnez]

This is a problem in how match treats numerals:

set_option pp.numericTypes true

def OtherNat := Nat deriving DecidableEq

instance : OfNat OtherNat n := ⟨(n : Nat) + 1⟩

def test (x : OtherNat) : Nat :=
  match x with
  | 1 => 7
  | _ => 5

/--
info: def test : OtherNat → Nat :=
fun x =>
  match x with
  | (1 : Nat) => (7 : Nat)
  | x => (5 : Nat)
-/
#guard_msgs in
#print test

example : test 1 = 5 := rfl

[Robin Arnez]

In other words: The match equation says (2 : Fin 4) but you provide (2 : ZMod 4)