`split` tactic does not eliminate impossible cases, leading to confusing behavior

Description

If split is used on if h then x else y where h is true in the local context, then there are two cases, and in both cases the ite reduces to x, which is confusing.

Context

Zulip

Related issue: #3245 (Using split on if-then-else simplifies unrelated nested if-then-else)

Steps to Reproduce

In the following, notice that in both cases the goal is x = 0.

example (p : Prop) [Decidable p] (hp : p) (x y : Nat) :
    (if p then x else y) = 0 := by
  split
  /-
  case isTrue
  p : Prop
  inst✝ : Decidable p
  hp : p
  x y : ℕ
  h✝ : p
  ⊢ x = 0

  case isFalse
  p : Prop
  inst✝ : Decidable p
  hp : p
  x y : ℕ
  h✝ : ¬p
  ⊢ x = 0
  -/

Changing the hypothesis to (hp : ¬ p) yields no confusion.

Expected behavior: Either split should check the local context for a proof or disproof of the condition and creates a single goal, or it should ensure that it reduces the if using the correct case under consideration.

Versions

4.9.0-rc2

Additional Information

This is related to #3245 since in both cases the local context is being used to simplify if expressions in unexpected ways.

The mathlib split_ifs tactic uses the local context to eliminate cases. (This is a port of a Lean 3 tactic.)

Impact

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

Start by running the provided Lean reproduction and compare it with the behavior when the hypothesis is negated. Read the split tactic implementation and mathlib's Mathlib/Tactic/SplitIfs.lean, along with related issue #3245. Done means the impossible branch is eliminated or each branch reduces the if correctly, with a regression test.