Skip to content

feat: keep haves above a split match in equation lemmas - #16235

Open
leodemoura wants to merge 15 commits into
masterfrom
eqns-keep-have-match
Open

feat: keep haves above a split match in equation lemmas#16235
leodemoura wants to merge 15 commits into
masterfrom
eqns-keep-have-match

Conversation

@leodemoura

@leodemoura leodemoura commented Nov 3, 2026

Copy link
Copy Markdown
Member

This PR makes the equation lemmas f.eq_<i> keep the haves and lets of the right-hand side when they split a match below them, instead of inlining their values into each equation. Inlining duplicated the values, exponentially for nested haves, and lost the sharing of the join points that do notation introduces, which vcgen +jp [f] needs (#16122). The generated equations are otherwise the same: inlining the haves gives back the previous equations.

mkEqnTypes now introduces the root haves as let-declarations, and commits a step only if it simplifies or splits a match. A match in the value of a have is reduced or split in place, and the have is inlined only where splitting requires it, for example when its value depends on a split variable and the match elaborator made it a discriminant. saveEqn puts the used declarations back into the right-hand side.

Breaking change: after rw [f], the goal can contain haves above a split match. Use dsimp only after rw [f], or simp only [f] instead of rw [f].

🤖 Generated with Claude Code

@leodemoura leodemoura added the changelog-language Language features and metaprograms label Nov 3, 2026
@leodemoura @claude
feat: keep haves above a split match in equation lemmas
a1e65b3 
This PR makes the equation lemmas `f.eq_<i>` keep the `have`s and `let`s of the right-hand side when they split a `match` below them, instead of inlining their values into each equation. Inlining duplicated the values, exponentially for nested `have`s, and lost the sharing of the join points that `do` notation introduces, which `vcgen +jp [f]` needs (#16122). The generated equations are otherwise the same: inlining the `have`s gives back the previous equations.

`mkEqnTypes` now introduces the root `have`s as let-declarations, and commits a step only if it simplifies or splits a `match`. A `match` in the value of a `have` is reduced or split in place, and the `have` is inlined only where splitting requires it, for example when its value depends on a split variable and the `match` elaborator made it a discriminant. `saveEqn` puts the used declarations back into the right-hand side.

Breaking change: after `rw [f]`, the goal can contain `have`s above a split `match`. Use `dsimp only` after `rw [f]`, or `simp only [f]` instead of `rw [f]`.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@leodemoura
leodemoura force-pushed the eqns-keep-have-match branch from e3265a2 to a1e65b3 Compare November 3, 2026 21:37
@leodemoura
leodemoura added this pull request to the merge queue Nov 3, 2026
@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 Nov 3, 2026
@leodemoura
leodemoura removed this pull request from the merge queue due to a manual request Nov 3, 2026
leodemoura and others added 8 commits November 3, 2026 22:06
@leodemoura @claude
fix: drop unused root haves in equation lemmas
4d39918 
Unused `have`s at the root of the right-hand side are now dropped from the equation lemmas, also when no `match` is split below them.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@leodemoura @claude
fix: split a match in a have value in the right-hand side
05b1825 
A `have` whose value has a `match` to split or simplify is moved back into the right-hand side, where `Split.splitMatch` and `simpMatch?` rewrite its value, also with the hypotheses of overlapping patterns. The `have` is kept instead of inlined.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@leodemoura @claude
fix: split other matches before zeta-reducing in equation lemmas
56829eb 
When splitting a `match` fails, `splitMatch?` first tries the other `match`es, and only then zeta-reduces let-variables. This keeps the `have`s that the `match` elaborator generalizes as discriminants of an outer `match`.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@leodemoura
Checkpoint
84ca713
@leodemoura
refactor: preserve binding scopes in equation generation
2f34ed4 
Keep let/have bindings in their lexical scopes while generating equations. Separate matcher case refinement from RHS normalization and construct equality proofs for scoped telescope rewrites.

Isolate simplifier caches when entering local scopes. Add regression coverage for nested bindings, dependent values, computed discriminants, and normalization proofs.
@leodemoura
fix: preserve have invariants during equation normalization
abd904c 
This PR fixes generated equations whose have bindings become invalid after reducing dependent matches.

Track the definitions unfolded while typechecking normalized telescopes, then substitute the corresponding have values throughout their scopes. Apply the pass after simp and dsimp, and add regressions for dependent types, named-match proof arguments, and fixed binding values.
@leodemoura
chore: checkpoint equation normalization (wip)
06c7186
@leodemoura
refactor: reuse letToHave in equation normalization
d3dee0b 
Rebuild changed binding bodies with let and run letToHave before revisiting the result. Preserve sharing for dependent bindings, and cover conversion of existing lets and nested shared values in the tests and benchmarks.
@leodemoura leodemoura added the downstream Request a downstream-lean4 adaptation PR. label Nov 4, 2026
@leodemoura
fix: discard impossible branches when generating equations
876b91e 
This PR avoids duplicate equation theorems by eliminating contradictory branches after matcher refinement.

Use the existing contradiction checker in Split.refineMatch to close branches whose discriminant equalities or overlap exclusions become contradictory after substitution. Add regressions for dependent bindings, constant discriminants, and quantified overlap exclusions, and update the expected trace names after removing an impossible equation.
@leodemoura
test: remove equation have-chain benchmark
354bae1
@leodemoura

leodemoura commented Nov 4, 2026

Copy link
Copy Markdown
Member Author

!bench

@leanprover-radar

leanprover-radar commented Nov 4, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for 354bae1 against aab5551 are in. There are significant results. @leodemoura

  • 🟥 build//instructions: +17.6G (+0.19%)

Large changes (3✅, 4🟥)

  • 🟥 elab/cbv_arm_ldst//instructions: +2.4G (+6.89%)
  • 🟥 elab/cbv_dedup//instructions: +107.8M (+4.51%)
  • ✅ elab/cbv_merge_sort//instructions: -1.2G (-7.67%)
  • ✅ elab/cbv_merge_sort//task-clock: -152ms (-11.12%)
  • ✅ elab/cbv_merge_sort//wall-clock: -153ms (-11.26%)
  • 🟥 elab/realizations//instructions: +17.5G (+4.75%)
  • and 1 hidden

Medium changes (1✅, 1🟥)

  • 🟥 build/module/Std.Data.DTreeMap.Internal.Model//instructions: +2.2G (+4.98%) (reduced significance based on absolute threshold)
  • ✅ elab/bv_stress_replicate//wall-clock: -66ms (-5.79%)

Small changes (8✅, 207🟥)

  • ✅ compiled/async/http_server//task-clock: -19s (-33.81%)
  • ✅ compiled/async/http_server//wall-clock: -10s (-42.31%)
  • ✅ elab/cbv_aes//instructions: -204.6M (-1.15%)
  • 🟥 elab/cbv_leroy//instructions: +93.3M (+0.27%)
  • ✅ elab/grind_field_kernel_cancel//instructions: -47.6M (-0.14%)
  • 🟥 elab/partial_fixpoint_mutual_eqns//instructions: +319.0M (+1.25%)
  • 🟥 lake/inundation/env//instructions: +2.8M (+0.32%)
  • 🟥 misc/import Init.Data.BitVec.Lemmas//instructions: +106.2M (+0.13%)
  • 🟥 misc/import Init.Data.List.Sublist//instructions: +30.0M (+0.38%)
  • 🟥 misc/import Std.Data.Internal.List.Associative//instructions: +187.4M (+0.37%)
  • 🟥 misc/re-elab Init.Data.List.Basic//instructions: +2.4G (+2.31%)
  • and 204 hidden

@downstream-lean4 downstream-lean4 Bot mentioned this pull request Nov 4, 2026
Open
@downstream-lean4

downstream-lean4 Bot commented Nov 4, 2026

Copy link
Copy Markdown

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

@sgraf812 @claude
fix: rewrite over-applied matchers in rwMatcher
a224596 
`rwMatcher` instantiated the matcher congruence equation with all
arguments of the matcher application. If the matcher is applied to more
arguments than its arity, the extra arguments land on the pattern
variables of the equation, and the overlap hypotheses cannot be
discharged. Equation generation then keeps the `match` unsplit, for
example in the `@[to_dual]` translation `WithInitial.comp` of Mathlib's
`WithTerminal.comp`.

`rwMatcher` now rewrites the matcher application and reapplies the extra
arguments.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01D74FF1zb7wKmojVzQB51CA
@leodemoura
leodemoura added this pull request to the merge queue Nov 4, 2026
@github-merge-queue
github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Nov 4, 2026
@leodemoura leodemoura mentioned this pull request Nov 4, 2026
Closed
@sgraf812 @claude
fix: prove equations with matcher congruence equations
fb93fa8 
`mkEqnTypes` computes an equation statement by rewriting a matcher with
its congruence equation, also when the discriminants of that alternative
are not constructor applications. `mkEqnProof` then cannot reduce the
matcher on the left-hand side if the compiled matcher cases on such a
discriminant, for example `AugmentedSimplexCategory.tensorHom` in
Mathlib. `mkEqnProof` now tries the same rewrite on the left-hand side
before it fails.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01D74FF1zb7wKmojVzQB51CA
@leodemoura
leodemoura added this pull request to the merge queue Nov 4, 2026
@github-merge-queue
github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Nov 4, 2026

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

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.

3 participants

@leodemoura @leanprover-radar @sgraf812