-
Notifications
You must be signed in to change notification settings - Fork 462
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.
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
simp?
can still incorrectly unresolve a name to the current theorem name
#6706
Comments
Thanks for the report. Is this something that bit you “in the wild”, or a constructed corner case? |
It did happen in the wild: I have a function @[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 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 @[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 |
@nomeata This is a bug in 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
-/ |
Description
When
simp? [name]
gets replaced withsimp 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
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 fromN.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.
The text was updated successfully, but these errors were encountered: