fix: make rw collect only new goals, occurs check#10306
Merged
kmill merged 2 commits intoleanprover:masterfrom Sep 14, 2025
Merged
fix: make rw collect only new goals, occurs check#10306kmill merged 2 commits intoleanprover:masterfrom
rw collect only new goals, occurs check#10306kmill merged 2 commits intoleanprover:masterfrom
Conversation
Collaborator
|
Reference manual CI status:
|
ghost
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Sep 9, 2025
ghost
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Sep 9, 2025
|
Mathlib CI status (docs):
|
This PR fixes a few bugs in the `rw` tactic: it could "steal" goals because they appear in the type of the rewrite, it did not do an occurs check, and new proof goals would not be synthetic opaque. This PR also lets the `rfl` tactic assign synthetic opaque metavariables so that it is equivalent to `exact rfl`. Implementation note: filtering old vs new is not sufficient. This PR partially addresses the bug where the rw tactic creates natural metavariables for each of the goals; now new proof goals are synthetic opaque. Metaprogramming API: Instead of `Lean.MVarId.rewrite` prefer `Lean.Elab.Tactic.elabRewrite` for elaborating rewrite theorems and applying rewrites to expressions.
kim-em
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Sep 15, 2025
* fix deprecations * remove upstreamed defs * two fixes * fix merge * fix merge * revert sqrt changes * ugh * fix from nightly-testing * fix merge * remove test deleted on master * fix test * note about test * . * Update lean-toolchain for leanprover/lean4#10194 * chore: bump to nightly-2025-09-02 * adjust to upstream changes * fix * fix * long line * Use Mathlib's nightly toolchain to run docgen in the nightly test * simpNF linter * whitespace * Update lean-toolchain for testing leanprover/lean4#10217 * Correct the working directory: should be 'docbuild' * Rework the grind regression report as a nightly-testing regression report It should still report the same things, but now as one message for all regression kinds * feat(Cache): download speeds & more info on errors * fix(Cache): add base download failure message * fixes * turn off linter * adaptation note * turn off linter.nightlyRegressionSet * chore: adaptations for nightly-2025-09-02 * Update lean-toolchain for testing leanprover/lean4#10059 * Update lean-toolchain for leanprover/lean4#10217 * chore: bump to nightly-2025-09-03 * Remove the erroring nightly regression report, we'll develop this on another branch. * fixes * update LibraryRewrite test * Update lean-toolchain for leanprover/lean4#10059 * chore: bump to nightly-2025-09-04 * fix * chore: bump to nightly-2025-09-05 * chore: adaptations for nightly-2025-09-05 * chore: bump to nightly-2025-09-06 * Update lean-toolchain for testing leanprover/lean4#10271 * Adapt to leanprover/lean4#10271 * Bump batteries * Update lean-toolchain for leanprover/lean4#10271 * chore: bump to nightly-2025-09-07 * nolint unusedArguments * Merge master into nightly-testing * chore: bump to nightly-2025-09-08 * fixes * chore: bump to nightly-2025-09-09 * fix thing * Update lean-toolchain for testing leanprover/lean4#10306 * temporarily remove test * adaptation note * master version of Cache/Requests.lean * chore: bump to nightly-2025-09-10 * adaptation note * chore: adaptations for nightly-2025-09-10 * merge lean-pr-testing-10059 * bump toolchain manually?? * restore test * chore: bump to nightly-2025-09-11 * lake update * fix * adaptations for leanprover/lean4#10307 * remove validateDocComment in ToAdditive * remove upstreamed Function.Injective * update assert_not_exists * oops * comment out DeriveTraversable * chore: replace some grind attibutes with grind_pattern, to be robust for future heuristic changes * suggestions from Rob23oba * lshake --fix * fix bad shake * shake --update * . * chore: adaptations for nightly-2025-09-11 * chore: bump to nightly-2025-09-12 * Revert "oops" This reverts commit 517b832. * Revert "comment out DeriveTraversable" This reverts commit 0460eb8. * fix DeriveTraversable * add `binders` fields * fix * fixes * update manifest * fixes * fixes * fixes * chore: bump to nightly-2025-09-13 * fixes * fixes * fixes * fixes * fixes * fixes * fixes * remove adaptation note * Update lean-toolchain for testing leanprover/lean4#10373 * fixes * chore: bump to nightly-2025-09-14 * Update lean-toolchain for testing leanprover/lean4#10377 * fix * fix * fix * fix emrge * update batteries * chore: adaptations for nightly-2025-09-14 * Merge master into nightly-testing * Update Mathlib/Data/List/Basic.lean * Merge master into nightly-testing * chore: adaptations for nightly-2025-09-14 * chore: bump to nightly-2025-09-15 --------- Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Mac Malone <mac@lean-fro.org> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR fixes a few bugs in the
rwtactic: it could "steal" goals because they appear in the type of the rewrite, it did not do an occurs check, and new proof goals would not be synthetic opaque. This PR also lets therfltactic assign synthetic opaque metavariables so that it is equivalent toexact rfl.Implementation note: filtering old vs new is not sufficient. This PR partially addresses the bug where the rw tactic creates natural metavariables for each of the goals; now new proof goals are synthetic opaque.
Metaprogramming API: Instead of
Lean.MVarId.rewritepreferLean.Elab.Tactic.elabRewritefor elaborating rewrite theorems and applying rewrites to expressions.Closes #10172