evalPropStep simproc util can use local decidable instance

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Here are three examples:

example [inst : DecidableEq (Fin 3)] :
    (2 : Fin 3) ≠ 0 := by
  simp only [Fin.reduceNe]

example [inst : DecidableEq Int] :
    (2 : Int) ≠ 0 := by
  simp only [Int.reduceNe]

example [inst : Decidable (2 < 3)] :
    2 < 3 := by
  simp only [Nat.reduceLT]

live.lean-lang.org version, for convenience
In each of these, an error is produced when typechecking:

application type mismatch
  eq_true_of_decide (Eq.refl true)
argument has type
  true = true
but function has type
  decide ... = true → ... = True

In each, the cause appears to be decide using inst rather than the expected existing instance for each of these structures. This arises from the simprocs in question, X.reduceBinPred each using evalPropStep, which infers the instance for decide using mkAppOptM and thus picks up inst first.

While this may appear to be user error ("just don't have inst there!"), this does occur for users of mathlib, see zulip thread because of the implementation of MultilinearMap. It also appears easily solvable by adjusting the relevant simprocs to use the correct Decidable instance when they call evalPropStep, and adjusting evalPropStep itself to take an optional decidability instance rather than using typeclass inference.

Context

Lean Zulip thread where this arose

Steps to Reproduce

1. Code as above

Expected behavior: The simp only call closes the goal with no errors.

Actual behavior: The simp only call closes the goal but errors are generated on the example during typechecking.

Versions

Lean 4.19.0-nightly-2025-03-11
Target: x86_64-unknown-linux-gnu

on live.lean-lang.org (Lean nightly without mathlib)
and

Lean 4.18.0-rc1
Target: x86_64-unknown-linux-gnu

on live.lean-lang.org (Latest Mathlib)

Additional Information

None.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Reproduce the three examples from the issue and inspect the X.reduceBinPred simprocs together with evalPropStep, especially their use of mkAppOptM and the decidability instance. The work is done when the examples typecheck without generated errors while preserving the expected simp behavior.