applying simp? gives a different result from simp

[b-mehta]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Applying the code action from simp? gives a different result than simp or simp? itself. Example:

def nothing (T : Nat → Prop) : Prop := sorry
def bar (T : Nat → Prop) : Nat := sorry

def foo (x : Nat) : Prop :=
  ∃ (S : Nat → Prop) (_ : nothing S) (_ : ∀ T, (∀ x, T x → S x) → nothing T), x = bar S

theorem foo_zero (n : Nat) : foo n := by
  rw [foo]
  simp?

After the final simp or simp? call, the goal is

∃ S, (∀ (T : Nat → Prop), (∀ (x : Nat), T x → S x) → nothing T) ∧ nothing S ∧ n = bar S

However after applying the code action simp? gives me, simp is replaced with

theorem foo_zero (n : Nat) : foo n := by
  rw [foo]
  simp only [exists_prop', nonempty_prop, exists_and_left]

and after the simp only call now, the goal is

∃ S, nothing S ∧ (∀ (T : Nat → Prop), (∀ (x : Nat), T x → S x) → nothing T) ∧ n = bar S

Context

Occurred while trying to demonstrate how simp? works for teaching. Discussion here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/The.20result.20of.20simp.3F.20gives.20a.20different.20result.20to.20simp

Steps to Reproduce

1. Code as above.

Expected behavior:
The simp only command given by simp? should behave the same as simp itself.

Actual behavior: Squeezing the simp changes what it does.

Versions

4.12.0-rc1, MacOS Monterey. Also reproduces on Lean nightly at time of writing.

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

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

[nomeata]

The three lemmas listed here are non-confluent, which partially explains the issue. But as long as simp and simp only apply the same strategy, it shouldn’t matter.

My assumption (not further investigated) is that the rules come out of the DiscrTree in a different order. Maybe if there are multiple rules there, they should be sorted by some predictable way – even lemma name could help to make this more reliable.

[Kha]

Should be a duplicate of #4615