Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

simp? can still incorrectly unresolve a name to the current theorem name #6706

Open
mniip opened this issue Jan 20, 2025 · 3 comments · May be fixed by #6938
Open

simp? can still incorrectly unresolve a name to the current theorem name #6706

mniip opened this issue Jan 20, 2025 · 3 comments · May be fixed by #6938
Labels
bug Something isn't working P-medium We may work on this issue if we find the time

Comments

@mniip
Copy link

mniip commented Jan 20, 2025

Description

When simp? [name] gets replaced with simp only [name'], it can still sometimes alias the current theorem name due to incorrect manipulation of namespaces.

Context

This has been previously filed and resolved in #4591, but the issue still persists.

Steps to Reproduce

def P := True
theorem N.A.B : P := by constructor
theorem N.X.A.B : P := by simp? [N.A.B]
-- Try this: simp only [A.B]

Expected behavior: Lean offers to replace with simp only [N.A.B].

Actual behavior: Lean offers to replace with simp only [A.B], which in this context is a different name from N.A.B, making the theorem recursive.

Versions

4.13.0, 4.16.0-rc2

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
@mniip mniip added the bug Something isn't working label Jan 20, 2025
@nomeata
Copy link
Collaborator

nomeata commented Jan 20, 2025

Thanks for the report. Is this something that bit you “in the wild”, or a constructed corner case?

@mniip
Copy link
Author

mniip commented Jan 20, 2025

It did happen in the wild: I have a function NFA.kleene.ε whose behavior on a certain subset of the inputs is characterized by

@[simp] theorem NFA.kleene.ε.some_none
  : ReflTransGen (ε E I F) (some q) none ↔ ∃ f ∈ F, ReflTransGen E q f

Then I have a construction on top of it, with a function NFA.Triple.kleene.ε, and a theorem that characterizes the new construction in terms of the previous:

theorem NFA.Triple.kleene.ε.gen
  : ReflTransGen (ε E I F) (p, q, s) (p', q', s')
    ↔ p = p' ∧ s = s'
      ∧ ReflTransGen (NFA.kleene.ε E (Rel.image I p) (Rel.preimage F s)) q q'

So a similar proof about NFA.Triple.kleene.ε on a subset of inputs proceeds by simply invoking the two aforementioned theorems:

@[simp] theorem NFA.Triple.kleene.ε.some_none
  : ReflTransGen (ε E I F) (p, some q, s) (p', none, s')
    ↔ p = p' ∧ s = s' ∧ (∃ f ∈ Rel.preimage F s, ReflTransGen E q f)
  := by simp only [gen, NFA.kleene.ε.some_none]

Which is where Lean purports to instead use simp only [gen, kleene.ε.none_some] and thus make a cyclic proof.

@leodemoura
Copy link
Member

@nomeata This is a bug in unresolveNameGlobalAvoidingLocals. It is not taking the auxiliary declarations in the local context into account. Here is a repro without simp?

import Lean

def N.A.B := 10

theorem N.X.A.B : True := by
  open Lean Meta Elab Tactic in
  run_tac do
    for decl in (← getLCtx) do
      if decl.isAuxDecl then
        IO.println s!"current namespace: {← getCurrNamespace}\nauxiliary declaration: {decl.userName}"
    IO.println s!"{``N.A.B} ===> {← unresolveNameGlobalAvoidingLocals ``N.A.B}"
  sorry
/-
current namespace: N.X.A
auxiliary declaration: B
N.A.B ===> A.B
-/

@leanprover-bot leanprover-bot added the P-medium We may work on this issue if we find the time label Jan 28, 2025
@jrr6 jrr6 linked a pull request Feb 4, 2025 that will close this issue
Draft
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug Something isn't working P-medium We may work on this issue if we find the time
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

fix: make name unresolution consistent and avoid auxiliary names jrr6/lean4
4 participants
@nomeata @mniip @leodemoura @leanprover-bot