Multiplicative doesn't play well with simp

Stream: mathlib4

[Yongyi Chen]

In particular, simp doesn't simplify defeqs. My MWE is a real world example, a group homomorphism $\mathbb Z/2\mathbb Z\to \text{Aut}(\mathbb Z/n\mathbb Z)$:

import Mathlib

def α' (n : ℕ) : Multiplicative (ZMod 2) →* AddAut (ZMod n) where
  toFun x := (AddEquiv.neg _) ^ x.val
  map_one' := rfl
  map_mul'
  | (0 : ZMod 2), (0 : ZMod 2) => rfl
  | (0 : ZMod 2), (1 : ZMod 2) => rfl
  | (1 : ZMod 2), (0 : ZMod 2) => rfl
  | (1 : ZMod 2), (1 : ZMod 2) => by
    ext x
    dsimp only
    simp
    -- Goal : ↑(AddEquiv.neg (ZMod n) ^ ZMod.val (1 * 1)) x = ↑(AddEquiv.neg (ZMod n) ^ ZMod.val 1) (↑(AddEquiv.neg (ZMod n) ^ ZMod.val 1) x)
    sorry

This proof works but I shouldn't need to do manual defeq conversions with conv:

import Mathlib

def α' (n : ℕ) : Multiplicative (ZMod 2) →* AddAut (ZMod n) where
  toFun x := (AddEquiv.neg _) ^ x.val
  map_one' := rfl
  map_mul'
  | (0 : ZMod 2), (0 : ZMod 2) => rfl
  | (0 : ZMod 2), (1 : ZMod 2) => rfl
  | (1 : ZMod 2), (0 : ZMod 2) => rfl
  | (1 : ZMod 2), (1 : ZMod 2) => by
    ext x
    dsimp only
    conv in ZMod.val _ => change 0
    conv in ZMod.val _ => change 1
    conv in ZMod.val _ => change 1
    simp only [pow_zero, AddAut.one_apply, pow_one, AddAut.mul_apply, AddEquiv.neg_apply, map_neg, neg_neg]

[Eric Wieser]

You're having this problem because you cheated and didn't use ofAdd and toAdd:

def α' (n : ℕ) : Multiplicative (ZMod 2) →* AddAut (ZMod n) where
  toFun x := (AddEquiv.neg _) ^ x.toAdd.val
  map_one' := rfl
  map_mul'
  | .ofAdd (0 : ZMod 2), .ofAdd (0 : ZMod 2) => rfl
  | .ofAdd (0 : ZMod 2), .ofAdd (1 : ZMod 2) => rfl
  | .ofAdd (1 : ZMod 2), .ofAdd (0 : ZMod 2) => rfl
  | .ofAdd (1 : ZMod 2), .ofAdd (1 : ZMod 2) => by
    ext x
    dsimp only
    simp

[Eric Wieser]

You were pretending that Multiplicative (ZMod 2) and ZMod 2 were the same type, but simp is not ok with you doing that

[Yongyi Chen]

Ohh actually | ofAdd (0 : ZMod 2) was one of the things I tried, and Lean didn't accept that... because I was missing the dot!

[Eric Wieser]

Without the dot it thinks you're declaring a new variable called ofAdd

[Eric Wieser]

Note I also changed .toFun

[Eric Wieser]

As an aside, I think there's probably some overlap here with docs#instModuleZModOfNatNatInstOfNatNatAdditiveUnitsIntInstMonoidIntToSemiringToDivisionSemiringToSemifieldInstFieldZModFact_prime_twoAddCommMonoidToCommMonoidInstCommGroupUnitsInstCommMonoidInt

[Yongyi Chen]

Eric Wieser said:

You're having this problem because you cheated and didn't use ofAdd and toAdd:

def α' (n : ℕ) : Multiplicative (ZMod 2) →* AddAut (ZMod n) where
  toFun x := (AddEquiv.neg _) ^ x.toAdd.val
  map_one' := rfl
  map_mul'
  | .ofAdd (0 : ZMod 2), .ofAdd (0 : ZMod 2) => rfl
  | .ofAdd (0 : ZMod 2), .ofAdd (1 : ZMod 2) => rfl
  | .ofAdd (1 : ZMod 2), .ofAdd (0 : ZMod 2) => rfl
  | .ofAdd (1 : ZMod 2), .ofAdd (1 : ZMod 2) => by
    ext x
    dsimp only
    simp

OK, I tried this code snippet. Before I got to my computer, I thought this was a valid proof, but actually there is still some stuff to do after the simp. How to finish?

The goal state is

x = ↑(AddEquiv.neg (ZMod n) ^ ZMod.val 1) (↑(AddEquiv.neg (ZMod n) ^ ZMod.val 1) x)

Obviously, for example, ZMod.val 1 is defeq to 1, but simp refuses to touch that for some reason.

[Eric Wieser]

You should write a lemma that says the thing that is obvious to you

[Eric Wieser]

And then hand it to simp

[Eric Wieser]

Is the proof easier without ext?

[Yongyi Chen]

ok this works:

def α' (n : ℕ) : Multiplicative (ZMod 2) →* AddAut (ZMod n) where
  toFun x := (AddEquiv.neg _) ^ x.toAdd.val
  map_one' := rfl
  map_mul'
  | .ofAdd (0 : ZMod 2), .ofAdd (0 : ZMod 2) => rfl
  | .ofAdd (0 : ZMod 2), .ofAdd (1 : ZMod 2) => rfl
  | .ofAdd (1 : ZMod 2), .ofAdd (0 : ZMod 2) => rfl
  | .ofAdd (1 : ZMod 2), .ofAdd (1 : ZMod 2) => by
    simp [ZMod.val]
    ext
    simp