Implicit decidability arguments

Stream: mathlib4

[Oliver Nash]

I recently discovered that we have a (small) number of lemmas in the library where decidability data is supplied as implicit rather than typeclass arguments.

An example is docs#Finset.sum_ite_of_false

For reasons I do not understand, it seems that such lemmas will not fire for simp but they will for rw.

[Oliver Nash]

Here is an example:

import Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
import Mathlib.Data.Real.Basic

-- Variant of `Finset.sum_ite_of_false` except `DecidablePred p` is typeclass rather than implicit
lemma Finset.sum_ite_of_false' {α β : Type*} [AddCommMonoid β] {s : Finset α} {p : α → Prop}
    [DecidablePred p] (h : ∀ x ∈ s, ¬ p x) (f g : α → β) :
    ∑ x ∈ s, (if p x then f x else g x) = ∑ x ∈ s, g x :=
  s.sum_ite_of_false h f g

example (s : Finset ℝ) (hs : ∀ x ∈ s, x ≠ 0) :
    (∑ x ∈ s, if x = 0 then 1 else 0) = 0 := by
  rw [Finset.sum_ite_of_false hs] -- succeeds
  exact Finset.sum_const_zero

example (s : Finset ℝ) (hs : ∀ x ∈ s, x ≠ 0) :
    (∑ x ∈ s, if x = 0 then 1 else 0) = 0 := by
  simp only [Finset.sum_ite_of_false hs] -- fails!
  exact Finset.sum_const_zero

example (s : Finset ℝ) (hs : ∀ x ∈ s, x ≠ 0) :
    (∑ x ∈ s, if x = 0 then 1 else 0) = 0 := by
  simp only [Finset.sum_ite_of_false' hs] -- succeeds
  exact Finset.sum_const_zero

[Oliver Nash]

Searching for the regex \{.* : Decidable.*\} in Mathlib I find only a small number of such lemmas and looking at our history it seems that a number of them arrived in https://github.com/leanprover-community/mathlib3/pull/7291 but I see no discussion of why to follow the non-standard pattern there.

[Oliver Nash]

I therefore have two questions:

1. Does anyone understand why simp fails to fire in the example I give above?
2. Should we change these lemmas to take their decidability as typeclass arguments?

[Kyle Miller]

I think rw can succeed because elaboration order for rw [thm] is

1. start elaborating thm
2. find all matches in the target by unification
3. ... do the rewrite ...
4. finish elaborating thm (that is, try to synthesize any pending instances, etc.)

In this case, it's able to pick up the Decidable instance through unification. I'd expected <- rewrites to fail.

simp has a different elaboration order, but I'm not sure why it fails.

[Oliver Nash]

Thanks, this is very helpful. Of course the next question might be how to make simp succeed but it may not matter much if #26662 goes through.