Always provide primitive eta when check_eliminations is disabled#21952
Open
ebmoon wants to merge 4 commits intorocq-prover:masterfrom
Open
Always provide primitive eta when check_eliminations is disabled#21952ebmoon wants to merge 4 commits intorocq-prover:masterfrom
check_eliminations is disabled#21952ebmoon wants to merge 4 commits intorocq-prover:masterfrom
Conversation
…nations is disabled When check_eliminations is false, primitive records with no relevant arguments now get AlwaysEta instead of NoEta. This allows definitional eta expansion for such records without unconditionally changing the default behavior. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
- Add bypass_check(eliminations) attribute for inductive declarations - Add Set/Unset Elimination Checking vernacular option - Add set_check_eliminations in safe_typing and Global - Add test suite covering eta behavior with and without the flag, including a Rocq translation of the Lean Inhabited' example Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
coqbot-app
Bot
added
the
needs: full CI
Contributor
|
Note that it's possible that lean still accepts some definitional equalities that rocq doesn't even with this patch, because the rocq conversion checker is not expected to be particularly complete when check_eliminations is off. |
Member
|
@coqbot run full ci |
SkySkimmer
reviewed
Apr 23, 2026
JasonGross
added
the
request: full CI
…bute only The check_eliminations flag is not meant to be exposed as a global Set/Unset option. It should only be used per-definition via the #[bypass_check(eliminations)] attribute (e.g. by the Lean importer plugin). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
coqbot-app
Bot
removed
request: full CI
SkySkimmer
reviewed
Apr 23, 2026
Contributor
|
How important is eta for such structures? In any case, Lean will be able to combine eta and irrelevance in a way Rocq won't (and there's also eta for unit that won't happen in Rocq). |
coqbot-app
Bot
added
the
needs: full CI
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
4 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.
Summary
When
Unset Elimination Checkingis active, records with irrelevant (SProp) fields in relevant sorts (Prop, Type, Set) are now given primitive eta, bypassing the usual elimination restriction checks.This is motivated by the Lean-to-Rocq import pipeline, where Lean structures unconditionally have eta regardless of field relevance. Without this change, imported records with irrelevant fields lose eta, causing definitional equalities that hold in Lean to fail in Rocq.
Related issue: rocq-community/rocq-lean-import#63