matching on an if _ then _ else _ gets reduced to Decidable.rec by simp only, which it then can't further simplify

[alexkeizer]

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

See the following MWE:

example (k : Prop)  (h : k) [Decidable k] : 
    let ⟨a, b⟩ := if k then (1, 0) else (0, 1)
    a = 1 := by
  simp [h]
  /-
  unsolved goals
  k : Prop
  h : k
  inst✝ : Decidable k
  ⊢ (Decidable.rec (fun h => (0, 1)) (fun h => (1, 0)) inst✝).fst = 1
  -/

When we match on the result of an if _ then _ else _ (recalling that let ⟨a, b⟩ := foo; ... desugars to match foo with | ⟨a, b⟩ => ...), then even simp only will already reduce this to an application of Decidable.rec.

This is unfortunate, because our simpset is not equiped to simplify Decidable.rec, even if the if-condition is known (as it is in the example), and even if we include a proof that the if-condition is true, this reduction seems to happen first, blocking any further simplification and preventing a seemingly trivial goal from being closed.

Context

This showed up in LNSym, for example, in our semantics for a sub instruction

Steps to Reproduce

MWE:

example (k : Prop)  (h : k) [Decidable k] : 
    let ⟨a, b⟩ := if k then (1, 0) else (0, 1)
    a = 1 := by
  simp [h]
  /-
  unsolved goals
  k : Prop
  h : k
  inst✝ : Decidable k
  ⊢ (Decidable.rec (fun h => (0, 1)) (fun h => (1, 0)) inst✝).fst = 1
  -/

Expected behavior: I would've expected the goal to be automatically closed by simp, seeing that we gave it a proof that the condition of the if is true

Actual behavior: simp is unable to close the goal, getting stuck with

/-
  unsolved goals
  k : Prop
  h : k
  inst✝ : Decidable k
  ⊢ (Decidable.rec (fun h => (0, 1)) (fun h => (1, 0)) inst✝).fst = 1
  -/

Versions

4.12.0-nightly-2024-09-18, at https://live.lean-lang.org/#project=lean-nightly&codez=KYDwhgtgDgNsAEAKA1vAXPACgJwPZQEp4kALdeZIgbQBFgBjASwBMwAjOCgXXIChjicAC7xAF+RgANPDaBL8nQBeeIwBmFeEJLAAdkgCMUgAxFgMAM4JEBqboL8BYeIt0LpATzunG0eFRJc7APQAtHYArlqmuDAAbsDM8ADmuGBmdqgYOPh2ZBjIdowRQoC45OR0TKwcCHnEgEVESGUs7HAAdNgMSMrh8GTyAHxIVvA2RIidOj39iPrwRkQFpsUEzcoLjkN2QQG8dgDEwNEp8AAywGBazbHYnrhaAMpC2AUJQA

Impact

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

[alexkeizer]

Thanks for the quick fix!