squeezing `simp` changes the goal

Stream: lean4

[llllvvuu]

Should I expect the output of simp? to guarantee the same result as simp?

 /-- info: "4.10.0-rc1" -/
#guard_msgs in
#eval Lean.versionString

/--
info: Try this: simp only [exists_prop, exists_and_left, exists_eq_right_right]
---
warning: declaration uses 'sorry'
---
info: [Meta.Tactic.simp.rewrite] exists_prop:1000, ∃ x_1, a = x ==> 1 < a ∧ a = x
[Meta.Tactic.simp.rewrite] exists_and_left:1000, ∃ x_1, 1 < a ∧ a = x ==> 1 < a ∧ ∃ x_1, a = x
[Meta.Tactic.simp.rewrite] exists_prop:1000, ∃ x_1, a = x ==> 0 < a ∧ a = x
[Meta.Tactic.simp.rewrite] exists_eq_right_right:1000, ∃ a, 1 < a ∧ 0 < a ∧ a = x ==> 1 < x ∧ 0 < x
-/
#guard_msgs in
set_option trace.Meta.Tactic.simp.rewrite true in
example (x : Nat) : ∃ (a : Nat) (_ : 0 < a) (_ : 1 < a), a = x := by
  simp?
  show 1 < x ∧ 0 < x
  sorry

example (x : Nat) : ∃ (a : Nat) (_ : 0 < a) (_ : 1 < a), a = x := by
  simp only [exists_prop, exists_and_left, exists_eq_right_right]
  show 0 < x ∧ 1 < x
  sorry

[Kim Morrison]

That's a bug! Could you please file an issue?

[llllvvuu]

Done: lean4#4615

[Michael Stoll]

There is also the problem that simp makes use of priorities, but simp only does not, so simp? may produce a list of lemmas that do not work in the same way with simp only:

example : ∀ x ∈ [1,2,3], x < 4 := by
  intro x hx
  simp at hx
  -- hx: x = 1 ∨ x = 2 ∨ x = 3
  omega

example : ∀ x ∈ [1,2,3], x < 4 := by
  intro x hx
  -- this is produced by using `simp?` above
  simp only [List.mem_cons, List.mem_singleton] at hx
  -- hx: x = 1 ∨ x = 2 ∨ x = 3 ∨ x ∈ []
  omega -- fails now

[Michael Stoll]

See here for an earlier discussion.

[Kim Morrison]

I guess ideally simp only would look up the priorities from the environment, and possibly also allow overriding them in the tactic call.

[Kim Morrison]

A lot of work for marginal improvement, however.

[Michael Stoll]

My experience is that I encounter this only rarely, and when I do, I try to figure out which lemmas to add to make simp only work (e.g., List.not_mem_nil and or_false in the example above; usually a second simp? call reveals them).
So, yes, a lot of work to fix this for not much gain.