simp_all [h], where h is a hypothesis, removes h

[JLimperg]

It seems like the simp_all logic that prevents hypotheses from self-simplifying to True does not fire if the hypothesis is given explicitly:

example (h : n = m) : n = 0 := by
  simp_all
  -- n m : ℕ
  -- h : n = m
  -- ⊢ m = 0

example (h : n = m) : n = 0 := by
  simp_all [h]
  -- n m : ℕ
  -- ⊢ m = 0

I discovered this because simp_all? suggests calls of the form simp_all only [h]:

import Mathlib

example (h : n = m) : n = 0 := by
  simp_all?
  -- Try this: simp_all only [h]

[leodemoura]

This is the intended behavior. The suggestion made by simp_all? is redundant. simp_all only already includes h. The only is instructing simp_all to not use the global simp theorem set, but it still includes all hypotheses.

[JLimperg]

Okay, then simp_all? should be changed to exclude hypotheses from the simp only list. (Including the hypotheses is not just redundant; it changes the observable behaviour.) This requires a change to traceSimpCall. I can prepare a patch.

[JLimperg]

It appears simp_all no longer self-simplifies and removes local hypotheses when they're provided explicitly:

example {m n : Nat} (h : n = m) : n = 0 := by
  simp_all [h]
  -- m n : Nat
  -- h : n = m
  -- ⊢ m = 0
  sorry

(Same result with simp_all only [h].)

As such, I'll close this issue. simp_all? still suggests the redundant (and somewhat misleading) simp_all only [h], but I'll open a separate issue for this.