[downstream PR] Julia's instance check - #14536
Draft
datokrat wants to merge 16 commits into
Draft
Conversation
|
The adaptation PR for this PR is leanprover/downstream-lean4#16. |
github-actions
Bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
datokrat
force-pushed
the
julias-instance-check
branch
2 times, most recently
from
August 14, 2026 15:34
3801f8b to
bb2ac20
Compare
Contributor
Author
|
Note to self: No longer on downstream-green. Generally, I should migrate this to nightly-with-mathlib, so that I can get benchmarks. |
github-actions
Bot
added
the
mathlib4-nightly-available
mathlib-lean-pr-testing
Bot
added
the
breaks-mathlib
…y.instances enabled even if respectTransparency.types is disabled
datokrat
force-pushed
the
julias-instance-check
branch
from
August 18, 2026 09:22
bb2ac20 to
cc7922e
Compare
This PR makes `simp` and `dsimp` check, after they rewrite an argument of an application, the instance arguments whose types depend on that argument. When such an instance no longer has the expected type at `.instances` transparency, a replacement instance is synthesized and adopted if it is defeq to the old one at `.implicit` transparency; otherwise the rewrite of the argument is refused and a warning is logged. Previously the rewrite was applied unconditionally, leaving behind an instance argument that later lemmas mentioning that instance no longer match. The check is controlled by `dsimp.resynthInstances` (default `true`), its warning by `dsimp.resynthInstances.warning` (default `true`). Adoptions and refusals are traced under `Meta.Tactic.simp.resynthInstances`. Both entry points run the same fix-up: `simpApp` covers every argument-wise rebuild in `simp` (`simpAppUsingCongr`, `congrArgs`, and the `.fixed` branch of `tryAutoCongrTheorem?`), and standalone `dsimp` uses a new `postApp` hook of `transformWithCache`. The arguments an instance depends on carry forward dependencies, so `simp` can only ever have changed them definitionally; reverting or replacing them therefore keeps an already-built `Result.proof?` valid. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FXiCjRqcz5MmCqu6YxoBFR
…nstance check This PR adds the `@[lax_instance_defeq]` attribute, which exempts a class from the strict instance-argument discipline of `backward.isDefEq.respectTransparency.instances`: values assigned to instance metavariables of an exempt class are not required to match the metavariable's type at `.instances` transparency, and the instance-argument checks of `simp`/`dsimp` (`dsimp.resynthInstances`) and `linter.tacticCheckInstances` skip the class as well. Propositional classes are exempt by default, since proof irrelevance makes a stale instance argument harmless there. The attribute is backed by a scoped environment extension, so it supports `local`/`scoped` use and can be applied retroactively to classes from other modules. The exemption is consulted in `isInstanceMVar` (which also feeds `spineMVarsAdmissible`), in `Simp.resynthInstanceArgs`, and in `Meta.findInstanceArgMismatch?`. The `backward.isDefEq.respectTransparency.instanceSearchTypes` path is deliberately not affected. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FXiCjRqcz5MmCqu6YxoBFR
The option's default is a property of the toolchain and governs every package built with it, including dependencies such as Batteries that do not receive Mathlib's `leanOptions`. This branch (worktree `julia-instance-mvars`) keeps the backward-compatible behavior by default; the sibling branch `instance-strict-dsimp` enables the check by default. The feature test sets the option explicitly so it passes under either default. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FXiCjRqcz5MmCqu6YxoBFR
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
3 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.
No description provided.