`simp?` may unresolve simp name to current theorem name, making the theorem recursive

chabulhwi commented 3 months ago

Prerequisites

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

[X] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
[X] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
[X] 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

The suggestions by simp? replace some names with the same ones in different namespaces.

Context

Kim Morrison and I used simp? to replace non-terminal simps in the proofs of several Batteries lemmas with simp onlys. Then those proofs broke down.

Prior discussion: https://leanprover.zulipchat.com/#narrow/stream/348111-batteries/topic/String.2FLemmas/near/448085384

Steps to Reproduce

def Nat.foo : Nat → Nat
  | 0 => 0
  | n+1 => foo n
decreasing_by decreasing_tactic

theorem Nat.Bar.foo : foo 2 = 0 := by
  simp? [Nat.foo]
  -- Try this: simp only [foo]
  -- What it should be: simp only [Nat.foo]

Check the suggestion by simp? in the code above.

Expected behavior: simp? should suggest simp only [Nat.foo].

Actual behavior: simp? suggests simp only [foo].

Version

4.10.0-nightly-2024-06-30

Impact

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

nomeata commented 3 months ago

Lean.Elab.Tactic.mkSimpOnly uses Lean.unresolveNameGlobal. Maybe that doesn’t take locally open namespaces into account? But Lean.PrettyPrinter.Delaborator.delabConst uses it, so that’s probably right.

It seems to be less about namespaces and more about the corner case that the currently being defined theorem isn’t in scope properly, because here we do get the properly qualified name:

def Nat.foo : Nat → Nat
  | 0 => 0
  | n+1 => foo n
decreasing_by decreasing_tactic

theorem Nat.Bar.foo : True := by trivial

theorem Nat.Bar.foo' : Nat.foo 2 = 0 := by
  simp? [Nat.foo]
  -- Try this: simp only [Nat foo]

Maybe what happens is that the following: The theorem you wrote does not “look” recursive. So Nat.Bar.foois not in scope in itself, and thussimp?will printfoo, because it resolves toNat.foo. But once you putfoointo the syntax, Lean will think that you want to define a recursive functionNat.Bar.foo, and nowfoo_does_ resolve toNat.Bar.foo`.

This may be tricky to resolve. And it’s a rather peculiar corner case, much less severe than if simp? would in general get confused by namespaces.

digama0 commented 3 months ago

Lean.Elab.Tactic.mkSimpOnly uses Lean.unresolveNameGlobal. Maybe that doesn’t take locally open namespaces into account? But Lean.PrettyPrinter.Delaborator.delabConst uses it, so that’s probably right.

I think it's not about open namespaces so much as not taking local variables into account, or possibly something even more complicated because recursive references have extra special behavior in the name resolver because unlike regular local variables they can have namespaces and participate in dot notation etc. exactly like a regular global declaration name. (And of course you have to take nonrec into account...)

leanprover / lean4