simp? generates irrelevant lemmas

Stream: general

[MohanadAhmed]

In the Mathematics in Lean book chapter 3 section 1 see Here if I run simp? it produces lemmas that are not applicable. Accepting simp? suggestion of Try this will not change the goal in any way as far as I can tell. I believe this is a bug. simp? if it cannot apply the lemmas in question should give the usual simp only but not emit unusable lemmas.

Is that right or am I missing something?

Here is the relevant part extracted into a mwe.

import Mathlib

example (x y ε: ℝ)
  (hx: 0 < ε)(h1: ε < 1)
  (hx: |x| < ε)(hy: |y| < ε):
  |x| * |y| ≤ |x| * ε := by
  -- Run simp? here and you get
  -- simp only [gt_iff_lt, abs_pos, ne_eq]
  refine (mul_le_mul (le_refl _) (le_of_lt hy) (abs_nonneg _) (abs_nonneg _))

 ```

[Yury G. Kudryashov]

Offtopic: you can use gcongr here.

[Kyle Miller]

Looking at the output of simp when you set set_option trace.Meta.Tactic.simp true, it seems like what's going on is that simp is trying to apply mul_le_mul_left, which requires proving 0 < |x| to apply, and then simp applies those three theorems to simplify this to x ≠ 0. It fails to prove this so it doesn't end up being able to apply mul_le_mul_left.

If you have that hypotheses available, you can see that simp uses these three lemmas for real

example (x y ε: ℝ)
  (hx: 0 < ε)(h1: ε < 1) (h' : x ≠ 0)
  (hx: |x| < ε)(hy: |y| < ε):
  |x| * |y| ≤ |x| * ε := by
  simp? [h']
  -- Try this: simp only [gt_iff_lt, abs_pos, ne_eq, h', not_false_eq_true, mul_le_mul_left]
  -- ⊢ |y| ≤ ε

[Kyle Miller]

It seems like a bug that simp? isn't discarding these lemmas when it fails to prove x ≠ 0

[Yury G. Kudryashov]

Why does it need docs#gt_iff_lt ? Do we have gt in one of these lemmas?

[Yury G. Kudryashov]

And why do we need gt_iff_lt as a simp lemma? gt is reducible.

[Kyle Miller]

Yeah, I noticed that. In the simp trace, gt_iff_lt doesn't seem to do anything

[Kyle Miller]

[Meta.Tactic.simp.rewrite] @gt_iff_lt:1000, 0 < |x| ==> 0 < |x|

[Kyle Miller]

I've noticed gt_iff_lt appear unnecessarily in simp? results before

[MohanadAhmed]

Kyle Miller said:

It seems like a bug that simp? isn't discarding these lemmas when it fails to prove x ≠ 0

FWIW it seems @Mario Carneiro also has a similar idea. He suspects the simp? is trying the lemmas, figuring out they are not useful, but whatever part is backtracking is not clearing the failed lemmas, thus they appear in the output of simp?.

[Mario Carneiro]

gt_iff_lt is a bad lean 4 simp lemma

[Mario Carneiro]

I'm surprised it doesn't loop

[Mario Carneiro]

MohanadAhmed said:

Kyle Miller said:

It seems like a bug that simp? isn't discarding these lemmas when it fails to prove x ≠ 0

FWIW it seems Mario Carneiro also has a similar idea. He suspects the simp? is trying the lemmas, figuring out they are not useful, but whatever part is backtracking is not clearing the failed lemmas, thus they appear in the output of simp?.

More precisely, it is trying and succeeding to apply them within a nested context of proving the side goal for another simp lemma, most likely mul_le_mul_left, but there is a try block somewhere which discards the whole subproof because it couldn't finish the job and the simp lemma tracking is not similarly rolled back