simp_all? suggests wrong/misleading simp_all only [...]

[JLimperg]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

Consider this simp_all? call:

example {m n k : Nat} (h₁: n = m) (h₂ : m = k) : n = 0 := by
  set_option tactic.simp.trace true in
  simp_all -- Try this: simp_all only [h₂]
  -- m n k : Nat
  -- h₁ : n = k
  -- h₂ : m = k
  -- ⊢ k = 0

The Try this suggestion is (a) wrong, since h₁ was also used; (b) misleading since simp_all only [h₂] doesn't appear to actually restrict the set of local hypotheses used. In the following example, h₁ is used despite only [h₂]:

example {m n k : Nat} (h₁: n = m) (h₂ : m = k) : n = 0 := by
  simp_all only [h₂]
  -- m n k : Nat
  -- h₁ : n = k
  -- h₂ : m = k
  -- ⊢ k = 0

I would therefore suggest that simp_all? should omit local hypotheses from the generated simp_all only list. Hence, the expected suggestion above would be simp_all only.

Are there any hypotheses whose presence in the simp_all only list does make a difference? I thought simp_all might not pick up dependent propositional hypotheses by default, but apparently it does:

example {m n : Nat} (P : ∀ {n m}, n = m → Prop) (h₁ : n = m) (h₂ : P h₁) : n = 0 := by
  simp_all
  -- m n : Nat
  -- P : {n m : Nat} → n = m → Prop
  -- h₁ : n = m
  -- h₂ : P _
  -- ⊢ m = 0

Context

Issue #1853 is somewhat related. The very old PR #1862 addresses the issue; I'll try to resurrect it.

Versions

Lean 4.3.0-rc2

Impact

Aesop currently works around this.

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