Skip to content

feat: add simpDecideCbv simproc for cbv decide#12766

Merged
wkrozowski merged 8 commits intoleanprover:masterfrom
wkrozowski:wojciech/decide_simproc
Mar 3, 2026
Merged

feat: add simpDecideCbv simproc for cbv decide#12766
wkrozowski merged 8 commits intoleanprover:masterfrom
wkrozowski:wojciech/decide_simproc

Conversation

@wkrozowski
Copy link
Copy Markdown
Contributor

@wkrozowski wkrozowski commented Mar 2, 2026 •
edited
Loading

This PR adds a dedicated cbv simproc for Decidable.decide that directly matches on isTrue/isFalse instances, producing simpler proof terms and avoiding unnecessary unfolding through Decidable.rec.

wkrozowski and others added 4 commits February 24, 2026 18:18
@wkrozowski @claude
refactor: simplify cbv ite/dite simprocs by matching Decidable instan…
317a97c 
…ce directly

This PR replaces the `Decidable.decide` + `eq_true_of_decide`/`eq_false_of_decide`
approach in `simpIteCbv` and `simpDIteCbv` with direct pattern matching on the
`Decidable` instance for `isTrue`/`isFalse`. This produces simpler proof terms
and reduces code duplication by extracting shared helpers.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@wkrozowski
Merge branch 'master' into wojciech/cbv-ite-dite-decidable-simproc
108f4af
@wkrozowski
chore: update test
68bec6c
@wkrozowski @claude
feat: add simpDecideCbv simproc and simplify Decidable.rec handling
aeeee87 
Add a dedicated cbv simproc for `Decidable.decide` that directly matches
on `isTrue`/`isFalse` instances, avoiding unnecessary unfolding of the
`Decidable.rec` match. Also adjust the `Decidable.rec` simpInterlaced
flags to only force rewrite on the last argument.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@wkrozowski wkrozowski requested a review from leodemoura as a code owner March 2, 2026 18:59
@wkrozowski wkrozowski added the changelog-tactics User facing tactics label Mar 2, 2026
@wkrozowski
Copy link
Copy Markdown
Contributor Author

wkrozowski commented Mar 2, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Mar 2, 2026 •
edited
Loading

Benchmark results for aeeee87 against 6bebf9c are in! @wkrozowski

  • 🟥 build//instructions: +192.9M (+0.00%)

Large changes (2✅, 2🟥)

  • ✅ elab/cbv_decide//instructions: -24.5G (-32.01%)
  • 🟥 elab/cbv_divisors//instructions: +7.0G (+11.19%)
  • 🟥 elab/cbv_leroy//instructions: +833.1M (+1.71%)
  • ✅ elab/cbv_merge_sort//instructions: -13.0G (-37.70%)

Small changes (1✅, 1🟥)

  • 🟥 build/module/Init.Sym.Lemmas//instructions: +81.7M (+4.22%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Meta.Tactic.Cbv.ControlFlow//instructions: -481.7M (-7.09%) (reduced significance based on absolute threshold)

@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 Mar 2, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Mar 2, 2026 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6bebf9c529374bdb0736c3e1545dc563fafc3421 --onto 87ec768a509c45987a7d73258da0cc1ef047925c. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-02 19:58:56)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d66aaebca69ce116712f549fbeb310ce091fd48a --onto 87ec768a509c45987a7d73258da0cc1ef047925c. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-02 21:00:41)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d66aaebca69ce116712f549fbeb310ce091fd48a --onto cda84702e9b31165f1f83c657b532f36f34e0bd0. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-03 11:50:50)

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Mar 2, 2026 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 6bebf9c529374bdb0736c3e1545dc563fafc3421 --onto cda84702e9b31165f1f83c657b532f36f34e0bd0. You can force reference manual CI using the force-manual-ci label. (2026-03-02 19:58:58)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase d66aaebca69ce116712f549fbeb310ce091fd48a --onto cda84702e9b31165f1f83c657b532f36f34e0bd0. You can force reference manual CI using the force-manual-ci label. (2026-03-02 21:00:43)

@wkrozowski
Copy link
Copy Markdown
Contributor Author

wkrozowski commented Mar 2, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Mar 2, 2026 •
edited
Loading

Benchmark results for 45ec45e against d66aaeb are in! @wkrozowski

  • 🟥 build//instructions: +1.3G (+0.01%)

Large changes (1✅)

  • ✅ elab/cbv_divisors//instructions: -8.2G (-13.03%)

Small changes (2🟥)

  • 🟥 build/module/Init.Sym.Lemmas//instructions: +42.2M (+2.13%)
  • 🟥 build/module/Lean.Meta.Tactic.Cbv.ControlFlow//instructions: +962.0M (+19.19%) (reduced significance based on *//lines)

@wkrozowski
Copy link
Copy Markdown
Contributor Author

wkrozowski commented Mar 2, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Mar 2, 2026 •
edited
Loading

Benchmark results for f910f88 against d66aaeb are in! @wkrozowski

  • 🟥 build//instructions: +1.9G (+0.01%)

Large changes (1✅)

  • ✅ elab/cbv_divisors//instructions: -8.2G (-13.04%)

Medium changes (1✅)

  • ✅ elab/cbv_decide//instructions: -1.3G (-2.37%)

Small changes (2🟥)

  • 🟥 build/module/Init.Sym.Lemmas//instructions: +60.2M (+3.04%)
  • 🟥 build/module/Lean.Meta.Tactic.Cbv.ControlFlow//instructions: +1.6G (+31.33%) (reduced significance based on *//lines)

@wkrozowski
Copy link
Copy Markdown
Contributor Author

wkrozowski commented Mar 3, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Mar 3, 2026 •
edited
Loading

Benchmark results for e6b47ba against d66aaeb are in! @wkrozowski

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

  • Bench repo commit hashes for run other differ between commits.
  • 🟥 build//instructions: +1.9G (+0.02%)
  • 🟥 other exited with code 1

Small changes (2🟥)

  • 🟥 build/module/Init.Sym.Lemmas//instructions: +50.4M (+2.54%)
  • 🟥 build/module/Lean.Meta.Tactic.Cbv.ControlFlow//instructions: +1.6G (+31.32%) (reduced significance based on *//lines)

@wkrozowski
Copy link
Copy Markdown
Contributor Author

wkrozowski commented Mar 3, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Mar 3, 2026

Benchmark results for e6b47ba against d66aaeb are in! @wkrozowski

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

  • Bench repo commit hashes for run other differ between commits.
  • 🟥 build//instructions: +1.9G (+0.02%)
  • 🟥 other exited with code 1

Small changes (2🟥)

  • 🟥 build/module/Init.Sym.Lemmas//instructions: +50.4M (+2.54%)
  • 🟥 build/module/Lean.Meta.Tactic.Cbv.ControlFlow//instructions: +1.6G (+31.32%) (reduced significance based on *//lines)

@wkrozowski wkrozowski added this pull request to the merge queue Mar 3, 2026
Merged via the queue into leanprover:master with commit 1f04bf4 Mar 3, 2026
17 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura is a code owner

Assignees

No one assigned

Labels

changelog-tactics User facing tactics 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

@wkrozowski @leanprover-radar @leanprover-bot