Zulip Chat Archive

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 (Dec 24 2022 at 17:04):

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 (Dec 24 2022 at 17:04):

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

Reid Barton (Dec 24 2022 at 17:05):

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