How to work with addition and match on ZMod

Stream: new members

[Snir Broshi]

I have a theorem which includes addition of ZMod and matching on ZMod,
but simp fails to simplify any of them:

import Mathlib.Data.ZMod.Basic

variable (MyProp : String -> Prop)

theorem foo : MyProp (
    match (1 : ZMod 4) + 1 with
    | 0 => "0 mod 4"
    | 1 => "1 mod 4"
    | 2 => "2 mod 4"
    | 3 => "3 mod 4"
) := by
  simp
  sorry

simp doesn't replace 1 + 1 with 2, and even if I manually change the matched expression to (2 : ZMod 4) it doesn't reduce the match expression to "2 mod 4".
When dealing with 0 + 1 or match 0 or match 1, simp works as expected.
I'm especially confused about match (2 : ZMod 4), since the matched expression and the branch are syntactically equal but it doesn't simplify.

If I change ZMod to Fin then simp works, even though ZMod 4 is defined to be Fin 4.

If I add an axiom:

axiom my_axiom : MyProp "2 mod 4"

and apply my_axiom then it figures everything out, but this only works when I have the exact goal as a theorem.

Thanks!

[Kenny Lau]

a bit of a hack:

import Mathlib.Data.ZMod.Basic

variable (MyProp : String -> Prop)

theorem foo : MyProp (
    match (1 : ZMod 4) + 1 with
    | 0 => "0 mod 4"
    | 1 => "1 mod 4"
    | 2 => "2 mod 4"
    | 3 => "3 mod 4"
) := by
  simp [show (1 + 1 : ZMod 4) = @OfNat.ofNat (Fin 4) 2 Fin.instOfNat from rfl]
  sorry

[Kenny Lau]

slightly less of a hack:

import Mathlib.Data.ZMod.Basic

variable (MyProp : String -> Prop)

theorem foo : MyProp (!["a", "b", "c", "d"] ((1 : Fin 4) + 1)) := by
  simp
  sorry

[Snir Broshi]

It seems that the hack can be simplified to simp [show (1 + 1 : Fin 4) = 2 from rfl]
The second solution doesn't work for me because it uses Fin only, which doesn't support casting from a Nat, as opposed to ZMod.
Why is Lean okay with doing arithmetic on Fin and then lifting it to ZMod, but it isn't capable of doing that arithmetic in simp without help?