simp discharging

Stream: mathlib4

[Reid Barton]

When there is a side condition to a simp lemma, simp will apparently apply more simp lemmas to simplify the condition before trying to apply something passed in. It means simp [h] becomes fragile. Was it like this in Lean 3 as well?

[Reid Barton]

Contrived mwe

theorem T (a b : Nat) (h : ¬ (a < 0 + b)) : (a - b) + b = a :=
  sorry

theorem U (a b : Nat) (h : ¬ (a < 0 + b)) : (a - b) + b = a := by
  simp [T, h] -- no effect

[Reid Barton]

Here Nat.zero_add kicks in to mess up the side condition before simp tries applying h

[Reid Barton]

Obviously T is dumb here, but in practice it can show up when the side condition in a simp lemma is no longer in simp normal form after stuff gets substituted for the variables

[Reid Barton]

In Lean 3 the second simp works though I don't know if it is just luck.