simp? does not report a theorem it used

[MichaelStollBayreuth]

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

In some (probably rather specific) cases, the Try this: suggestion provided by simp? misses a relevant simp-lemma.

Context

See this Zulip thread.

The behavior seems to depend on whether other lemmas are present or not in the simp set.

Steps to Reproduce

The following code shows the problem.

def Set := Nat → Prop

namespace Set

def singleton (a : Nat) : Set := fun b ↦ b = a

def compl (s : Set) : Set := fun x ↦ ¬ s x

@[simp]
theorem compl_iff (s : Set) (x : Nat) : s.compl x ↔ ¬ s x := Iff.rfl

@[simp]
theorem singleton_iff {a b : Nat} : singleton b a ↔ a = b := Iff.rfl

open Classical

noncomputable def indicator (s : Set) (x : Nat) : Nat := if s x then 1 else 0

@[simp] -- remove `simp` attribute --> works (and the trace changes)
theorem indicator_of {s : Set} {a : Nat} (h : s a) : indicator s a = 1 := if_pos h

@[simp]
theorem indicator_of_not {s : Set} {a : Nat} (h : ¬ s a) : indicator s a = 0 := if_neg h

set_option trace.Meta.Tactic.simp.rewrite true

theorem test : indicator (compl <| singleton 0) 0 = 0 := by
  simp? -- leaves out `singleton_iff` even though it is necessary

Removing the simp attribute from indicator_of makes the problem go away.

With set_option trace.Meta.Tactic.simp.discharge true (in addition to ...rewrite true), the trace in the "bad" case is

 [Meta.Tactic.simp.discharge] @Set.indicator_of discharge ❌
      Set.compl (Set.singleton 0) 0 ▼
  [rewrite] Set.compl_iff:1000, Set.compl (Set.singleton 0) 0 ==> ¬Set.singleton 0 0
  [rewrite] @Set.singleton_iff:1000, Set.singleton 0 0 ==> 0 = 0
  [rewrite] @eq_self:1000, 0 = 0 ==> True
  [rewrite] not_true_eq_false:1000, ¬True ==> False

[Meta.Tactic.simp.discharge] @Set.indicator_of_not discharge ✅
      ¬Set.compl (Set.singleton 0) 0 ▼
  [rewrite] Set.compl_iff:1000, Set.compl (Set.singleton 0) 0 ==> ¬Set.singleton 0 0
  [rewrite] not_true_eq_false:1000, ¬True ==> False
  [rewrite] not_false_eq_true:1000, ¬False ==> True

[Meta.Tactic.simp.rewrite] @Set.indicator_of_not:1000, Set.indicator (Set.compl (Set.singleton 0)) 0 ==> 0

[Meta.Tactic.simp.rewrite] @eq_self:1000, 0 = 0 ==> True

whereas in the "good" case, it is

[Meta.Tactic.simp.discharge] @Set.indicator_of_not discharge ✅
      ¬Set.compl (Set.singleton 0) 0 ▼
  [rewrite] Set.compl_iff:1000, Set.compl (Set.singleton 0) 0 ==> ¬Set.singleton 0 0
  [rewrite] @Set.singleton_iff:1000, Set.singleton 0 0 ==> 0 = 0
  [rewrite] @eq_self:1000, 0 = 0 ==> True
  [rewrite] not_true_eq_false:1000, ¬True ==> False
  [rewrite] not_false_eq_true:1000, ¬False ==> True

[Meta.Tactic.simp.rewrite] @Set.indicator_of_not:1000, Set.indicator (Set.compl (Set.singleton 0)) 0 ==> 0

[Meta.Tactic.simp.rewrite] @eq_self:1000, 0 = 0 ==> True

Note: in the "bad" case, singleton_iff is used in the first attempt via indicator_of that ultimately fails, and is not listed again in the second (succeeding) attempt. However, it is necessary to use it there (as the "good" trace shows).

Speculation: simp caches the result obtained from singleton_iff in the first attempt and reuses that in the second one, but does not take note of it for inclusion in the lemma list.

Disclaimer: I have no actual idea how simp works internally.

Expected behavior:
simp? should suggest a simp only [...] call whose list of lemmas (and simprocs) contains all lemmas etc. that simp used.

Actual behavior:
In the specific case, one necessary lemma is missing from the suggested list.

Versions

"4.7.0-rc2" on Linux

Impact

This behavior (when it occurs) is annoying, since it necessitates a manual correction, and it is not always immediately obvious which lemma(s) is/are missing.

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