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.

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

cannot use ax_aux_lemma or native_decide in simp discharger #7318

Closed
nomeata opened this issue Mar 4, 2025 · 1 comment · Fixed by #7362
Closed

cannot use ax_aux_lemma or native_decide in simp discharger #7318

nomeata opened this issue Mar 4, 2025 · 1 comment · Fixed by #7362
Labels
bug Something isn't working P-high We will work on this issue

Comments

@nomeata
Copy link
Collaborator

nomeata commented Mar 4, 2025

It seems that simp doesn’t like dischargers that add auxillary lemmas to the environment:

inductive P : Prop where
  | mk : P

def Q : Prop := P

theorem Q_of_P : P → Q := fun x => x

-- works
theorem foo : Q := by
  simp (discharger := exact P.mk) [Q_of_P]


/-- error: unknown constant 'Lean.Elab.Tactic.AsAuxLemma.auxLemma✝' -/
#guard_msgs in
theorem bar : Q := by
  simp (discharger := as_aux_lemma => exact P.mk) [Q_of_P]

theorem Q_of_decide : (1 + 1 = 2) → Q := fun _ => P.mk

/-- error: unknown constant 'lean.run.issue7318._auxLemma.3' -/
#guard_msgs in
theorem bar_decide : Q := by
  simp (discharger := native_decide) [Q_of_decide]

No immediate super blocking use-case, but fixing this would help with experiments like
https://github.com/leanprover/lean4/pull/5998/files

@nomeata nomeata added the bug Something isn't working label Mar 4, 2025
@nomeata nomeata changed the title cannot use ax_aux_lemma in simp discharger cannot use ax_aux_lemma or native_decide in simp discharger Mar 4, 2025
@nomeata
Copy link
Collaborator Author

nomeata commented Mar 4, 2025

The issue is due to the use of withoutModifyingStateWithInfoAndMessages in tacticToDischarge. Maybe reverting all of Core.state is too much? But there must be a reason not to use just withoutModifyingElabMetaStateWithInfo?

@leanprover-bot leanprover-bot added the P-high We will work on this issue label Mar 6, 2025
github-merge-queue bot pushed a commit that referenced this issue Mar 6, 2025
This PR allows simp dischargers to add aux decls to the environment.
This enables tactics like `native_decide` to be used here, and unblocks
improvements to omega in #5998.

Fixes #7318
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working P-high We will work on this issue
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants