decidability in the proof of `DFinsupp.update`

Stream: mathlib4

[Kin Yau James Wong]

This is probably a very minor thing/perhaps I am misreading, but I noticed I noticed that DFinsupp.update uses eq_or_ne instead of Decidable.eq_or_ne even though there was a DecidableEq instance in the hypothesis. When I navigate to the definition of eq_or_ne, it takes me to the classical version of it instead of the decidable one. Is there a reason to use eq_or_ne here, or am I misreading it somehow?

I've attached the version of DFinsupp.update that I have locally below (along with the hypotheses that it apparently uses):

def update {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] [DecidableEq ι] (f : Π₀ (i : ι), β i)
  (i : ι) (b : β i) : Π₀ i, β i :=
  ⟨Function.update f i b,
    f.support'.map fun s =>
      ⟨i ::ₘ s.1, fun j => by
        rcases eq_or_ne i j with (rfl | hi)
        · simp
        · obtain hj | (hj : f j = 0) := s.prop j
          · exact Or.inl (Multiset.mem_cons_of_mem hj)
          · exact Or.inr ((Function.update_of_ne hi.symm b _).trans hj)⟩⟩

[Ruben Van de Velde]

The reason is that very few people want to bother with using decidability

[Kin Yau James Wong]

But it is already included in the hypothesis anyways :thinking:

[Eric Wieser]

You should read Ruben's message as "no one previously cared about it in this case" as opposed to "this change is a bad idea, do not make it".

[Eric Wieser]

(though your subtext of "this would be a bad idea if we had to add an extra hypothesis" is also largely the community opinion)

[Ruben Van de Velde]

Well, I also mean "please don't make a PR that someone would need to review"

[Kin Yau James Wong]

Ah ok I understand - so no action required?

[Yaël Dillies]

My opinion is no action required

[Yury G. Kudryashov]

As far as I understand, the policy is: unless there is a result that someone really wants to see formalized without Classical.choice, we don't bother reducing dependencies.

[Yury G. Kudryashov]

If there is such result, the way to do it is

• recover from Zulip archives or write a linter (or an attribute) that will check that a given declaration doesn't depend on Classical.choice;
• put this tag on the theorem you really care about;
• get rid of Classical.choice in the dependencies of this theorem.

[Yury G. Kudryashov]

For all other results,

• we assume decidability in definitions, if it's required to make them computable and we want them to be computable;
• we assume decidability in theorems, if it's required to state the theorem; otherwise, we use classical in the proof.