Skip to content

feat: eta-expand recursor major for subsingleton structures - #15371

Merged
nomeata merged 10 commits into
leanprover:masterfrom
arthur-adjedj:eta-singleton-major
Oct 20, 2026
Merged

feat: eta-expand recursor major for subsingleton structures#15371
nomeata merged 10 commits into
leanprover:masterfrom
arthur-adjedj:eta-singleton-major

Conversation

@arthur-adjedj

@arthur-adjedj arthur-adjedj commented Sep 27, 2026 •
edited by nomeata
Loading

Copy link
Copy Markdown
Contributor

This PR expands the condition for which the major of a recursor can be eta-expanded. Namely, subsingleton structures such as And should be eta-expanded in this situation.

Remove the test kernel_is_prop_issue.lean as that test no longer reaches the code it used to test.

Related to #14977
Closes #3213

@arthur-adjedj arthur-adjedj mentioned this pull request Sep 27, 2026
Open
4 of 9 tasks
@github-actions github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Sep 27, 2026
@arthur-adjedj

arthur-adjedj commented Sep 28, 2026

Copy link
Copy Markdown
Contributor Author

downstream

@downstream-lean4 downstream-lean4 Bot added the downstream Request a downstream-lean4 adaptation PR. label Sep 28, 2026
@downstream-lean4 downstream-lean4 Bot mentioned this pull request Sep 28, 2026
Open
@arthur-adjedj

arthur-adjedj commented Oct 11, 2026

Copy link
Copy Markdown
Contributor Author

changelog-language

@github-actions github-actions Bot added the changelog-language Language features and metaprograms label Oct 11, 2026
@arthur-adjedj
arthur-adjedj marked this pull request as ready for review October 11, 2026 12:36
@nomeata nomeata mentioned this pull request Oct 11, 2026
Merged
nomeata added a commit to leanprover/lean-kernel-arena that referenced this pull request Oct 11, 2026
@nomeata @claude
Add corner cases for the planned eta changes to the official kernel (#…
76ddcf8 
…264)

Tests for the eta-related changes planned in leanprover/lean4#14977:

* corner-cases/eta-struct-major-no-whnf: structure eta on a recursor
major before reducing it (leanprover/lean4#15351)
* corner-cases/eta-struct-major-and: structure eta on a major in `Prop`,
like `And` (leanprover/lean4#15371, leanprover/lean4#3213)
* corner-cases/eta-struct-major-and-no-whnf: both together, with a
non-normalizing proof as major
* corner-cases/eta-unit-like-{pi,struct,proof-field,nested}: the
extended unit-like criterion (leanprover/lean4#15372,
leanprover/lean4#2258)
* corner-cases/eta-rec-struct: eta-expansion of a structure recursor
missing its major (leanprover/lean4#15374)
* bugs/eta-ctor-alias: a soundness bug in a draft of
leanprover/lean4#15373

and point the existing corner-cases/eta-ctor and corner-cases/eta-rule-k
at leanprover/lean4#15373 and leanprover/lean4#15374.

Co-authored-by: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
@arthur-adjedj arthur-adjedj mentioned this pull request Oct 12, 2026
Closed
@arthur-adjedj
test: add eta-before-whnf test
6f44930 
warning: this test leads to an infinite loop rather than a maxHeartBeats/maxRecDepth error in previous Lean versions
@arthur-adjedj
fix: eta-expand majors of subsingleton structures's recursors
1a3dbb4
@arthur-adjedj
cleanup and docs
777ec8f
@arthur-adjedj
delete kernel_is_prop_issue.lean.
7e2b336 
The test is not longer relevant, as the path the soundness bug originally took cannot be reached anymore with this PR, and is generally too sensitive to isDefEq bugs to be adapted reliably (eg leanprover#15103 also breaks it).
@arthur-adjedj arthur-adjedj mentioned this pull request Oct 12, 2026
Draft
@arthur-adjedj
arthur-adjedj marked this pull request as draft October 14, 2026 23:36
@downstream-lean4

downstream-lean4 Bot commented Oct 18, 2026

Copy link
Copy Markdown

The adaptation PR for this PR is leanprover/downstream-lean4#115.

@arthur-adjedj
arthur-adjedj marked this pull request as ready for review October 19, 2026 08:35
@arthur-adjedj

arthur-adjedj commented Oct 19, 2026

Copy link
Copy Markdown
Contributor Author

!bench

@leanprover-radar

leanprover-radar commented Oct 19, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for 98c6cf7 against 2c2bdd9 are in. There are significant results. @arthur-adjedj

  • 🟥 build//instructions: +16.0G (+0.15%)

Large changes (3🟥)

  • 🟥 elab/grind_ring_5//instructions: +246.8M (+3.00%)
  • 🟥 elab/sym_arith_norm//instructions: +469.2M (+3.02%)
  • 🟥 elab/whnfMatcherImplicitTransparencyCaching//instructions: +852.5M (+3.56%)

Medium changes (12🟥)

  • 🟥 build/module/Std.Data.HashMap.RawLemmas//instructions: +1.3G (+1.44%) (reduced significance based on absolute threshold)
  • 🟥 elab/cbv_system_f//instructions: +857.2M (+0.97%)
  • 🟥 elab/grind_bitvec2//instructions: +1.2G (+0.77%)
  • 🟥 elab/grind_list2//instructions: +162.3M (+0.43%)
  • 🟥 elab/realizations//instructions: +4.0G (+0.97%)
  • 🟥 elab/reduceMatch//instructions: +217.0M (+1.96%)
  • 🟥 elab/simp_arith1//instructions: +68.3M (+3.46%)
  • 🟥 elab/sym_arith_norm//task-clock: +82ms (+5.72%)
  • 🟥 elab/sym_arith_norm//wall-clock: +81ms (+5.61%)
  • 🟥 misc/import Init.Data.BitVec.Lemmas//instructions: +874.4M (+0.86%)
  • 🟥 misc/leanchecker --fresh Init//instructions: +4.1G (+1.35%)
  • 🟥 vcgen/GetThrowSetGrind/300/kernel//wall-clock: +10ms (+5.55%)

Small changes (2✅, 266🟥)

  • 🟥 build/module/Init.Control.Lawful.Instances//instructions: +14.8M (+0.24%)
  • 🟥 build/module/Init.Control.Lawful.MonadAttach.Instances//instructions: +3.7M (+0.24%)
  • 🟥 build/module/Init.Data.AC//instructions: +13.5M (+0.38%)
  • 🟥 build/module/Init.Data.Array.Basic//instructions: +17.6M (+0.17%)
  • 🟥 build/module/Init.Data.Array.BasicAux//instructions: +3.9M (+0.30%)
  • 🟥 build/module/Init.Data.Array.BinSearch//instructions: +64.2M (+1.13%) (reduced significance based on absolute threshold)
  • 🟥 build/module/Init.Data.Array.Bootstrap//instructions: +13.0M (+0.62%)
  • 🟥 build/module/Init.Data.Array.Erase//instructions: +21.5M (+0.32%)
  • 🟥 build/module/Init.Data.Array.Extract//instructions: +283.3M (+0.87%) (reduced significance based on absolute threshold)
  • 🟥 build/module/Init.Data.Array.FinRange//instructions: +3.8M (+0.34%)
  • 🟥 build/module/Init.Data.Array.InsertIdx//instructions: +16.2M (+0.65%) (reduced significance based on absolute threshold)
  • 🟥 build/module/Init.Data.Array.Lemmas//instructions: +158.7M (+0.32%)
  • 🟥 build/module/Init.Data.Array.Lex.Basic//instructions: +7.0M (+0.58%)
  • 🟥 build/module/Init.Data.Array.MapIdx//instructions: +17.4M (+0.21%)
  • 🟥 build/module/Init.Data.Array.QSort.Basic//instructions: +57.2M (+0.59%) (reduced significance based on absolute threshold)
  • 🟥 build/module/Init.Data.Array.Range//instructions: +9.3M (+0.26%)
  • 🟥 build/module/Init.Data.Array.Sort.Basic//instructions: +17.6M (+0.70%) (reduced significance based on absolute threshold)
  • 🟥 build/module/Init.Data.Array.Subarray.Split//instructions: +3.1M (+0.41%)
  • 🟥 build/module/Init.Data.BitVec.Bitblast//instructions: +422.6M (+0.89%) (reduced significance based on absolute threshold)
  • 🟥 build/module/Init.Data.BitVec.Bootstrap//instructions: +16.4M (+0.67%) (reduced significance based on absolute threshold)
  • and 248 more

nomeata
nomeata approved these changes Oct 20, 2026
View reviewed changes
Comment thread src/kernel/inductive.h Outdated
Comment thread src/kernel/inductive.h Outdated
Comment thread src/kernel/type_checker.cpp Outdated
@nomeata
nomeata enabled auto-merge October 20, 2026 12:40
@nomeata
nomeata added this pull request to the merge queue Oct 20, 2026
Merged via the queue into leanprover:master with commit a849eb9 Oct 20, 2026
17 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@nomeata nomeata nomeata approved these changes
@datokrat datokrat Awaiting requested review from datokrat
@TwoFX TwoFX Awaiting requested review from TwoFX
@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura is a code owner

Assignees

No one assigned

Labels

changelog-language Language features and metaprograms downstream Request a downstream-lean4 adaptation PR. toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Eta-expansion of Prop-structures

3 participants

@arthur-adjedj @leanprover-radar @nomeata