Finsupp and FreeAbelianGroup

Stream: mathlib4

[Martin Dvořák]

Why does the first example work but the second doesn't?

import Mathlib

noncomputable def c : ℕ →₀ WithZero Char := fun₀
  | 5 => 'x'
  | 7 => 'y'

example : c 5 = 'x' := by
  simp [c]

noncomputable def f : FreeAbelianGroup ℤ →₀ WithZero (FreeAbelianGroup ℤ) := fun₀
  | FreeAbelianGroup.of 0 => some (FreeAbelianGroup.of 1)
  | FreeAbelianGroup.of 2 => some (FreeAbelianGroup.of 3)

example : f (FreeAbelianGroup.of 0) = some (FreeAbelianGroup.of 1) := by
  simp [f]

[Eric Wieser]

Because in the first case, lean proves 5 \ne 7 for you, but it doesn't have a simp lemma for injcetivity of FreeAbelianGroup.of

[Martin Dvořák]

[resolved]

[Martin Dvořák]

Eric Wieser said:

Because in the first case, lean proves 5 \ne 7 for you, but it doesn't have a simp lemma for injcetivity of FreeAbelianGroup.of

I thought injectivity was not the problem because then

example : f (FreeAbelianGroup.of 2) = some (FreeAbelianGroup.of 3) := by
  simp [f]

would succeed, right?

Also the following two examples fail the same way...

example : f (FreeAbelianGroup.of 0) = some (FreeAbelianGroup.of 1) := by
  simp [f, FreeAbelianGroup.of_injective]

example : f (FreeAbelianGroup.of 2) = some (FreeAbelianGroup.of 3) := by
  simp [f, FreeAbelianGroup.of_injective]

[Martin Dvořák]

I still haven't figured out what's wrong.

[Daniel Weber]

The problem is that docs#Finsupp.coe_update requires DecidableEq, this works:

import Mathlib

theorem FreeAbelianGroup.of_inj {α : Type u} (a b : α) :
  FreeAbelianGroup.of a = FreeAbelianGroup.of b ↔ a = b := ⟨fun h ↦ FreeAbelianGroup.of_injective h, congrArg _⟩

noncomputable def f : FreeAbelianGroup ℤ →₀ WithZero (FreeAbelianGroup ℤ) := fun₀
  | FreeAbelianGroup.of 0 => some (FreeAbelianGroup.of 1)
  | FreeAbelianGroup.of 2 => some (FreeAbelianGroup.of 3)

open scoped Classical in
example : f (FreeAbelianGroup.of 0) = some (FreeAbelianGroup.of 1) := by
  simp [f, FreeAbelianGroup.of_inj]

open scoped Classical in
example : f (FreeAbelianGroup.of 2) = some (FreeAbelianGroup.of 3) := by
  simp [f]

[Daniel Weber]

Or, looking it in another way, the problem is that docs#Finsupp.update doesn't require it