Using split on if-then-else simplifies unrelated nested if-then-else

This is rather minor, but I stumbled over this while debugging #3229, and I’d like to record it as an instance of a non-finishing tactic doing possibly unexpected things on the side.

Consider this example:

example (b1 b2 : Bool) :
  (match b1 with
  | true => 0
  | false => (if b2 then 0 else if b2 then 42 else 0)) = 0 := by
  split
  rfl

Now the goal is, as expected

b2 b1✝: Bool
⊢ (if b2 = true then 0 else if b2 = true then 42 else 0) = 0

The split tactic split the match, and leaves the branch in place.

Using if-then-else however:

example (b1 b2 : Bool) :
  (if b1
  then 0
  else (if b2 then 0 else if b2 then 42 else 0)) = 0 := by
  split
  rfl

the goal becomes

b1b2: Bool
h✝: ¬b1 = true
⊢ (if b2 = true then 0 else 0) = 0

Note that suddenly, the totally unrelated nested if b2 was reduced.

The problem lies is with Lean.Meta.simpIfTarget, which

• uses the if-then-else congruence theorems and
• a discharger that looks into the hypotheses.

I wonder if it really needs to enable ite_congr – after all, for the if-then-else that was split the condition is already in the context, so no need for the “better” congruence rule and the standard rule should suffice?

Versions

v4.5.0

Impact

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

Start with Lean.Meta.simpIfTarget, identified in the report as the source of the behavior, and reproduce both split examples from the issue. Compare how the discharger and if-then-else congruence affect unrelated nested conditions; done means the nested if b2 is not simplified when splitting the unrelated condition.