Skip to content

fix: cbv handling of ite/dite/decide#12816

Merged
wkrozowski merged 10 commits intoleanprover:masterfrom
wkrozowski:wojciech/cbv-classical-draft
Mar 6, 2026
Merged

fix: cbv handling of ite/dite/decide#12816
wkrozowski merged 10 commits intoleanprover:masterfrom
wkrozowski:wojciech/cbv-classical-draft

Conversation

@wkrozowski
Copy link
Contributor

@wkrozowski wkrozowski commented Mar 5, 2026 •
edited
Loading

This PR solves three distinct issues with the handling of ite/dite,decide.

  1. We prevent the simprocs from picking up noncomputable, Classical instances, such as Classical.propDecidable, when simplifying the proposition in ite/dite/decide.

  2. We fix a type mismatch occurring when the condition/proposition is unchanged but the Decidable instance is simplified.

  3. If we rewrite the proposition from c to c' and the evaluation of the original instance Decidable c gets stuck we try fallback path of of obtaining Decidable c' instance and evaluating it. This matters when the instance is evaluated via cbv_eval lemmas.

@wkrozowski @claude
fix: prevent cbv from picking up classical Decidable instances
15c333b 
This PR adds a test documenting the issue where `cbv` picks up
`Classical.propDecidable` when re-synthesizing `Decidable` instances
after unfolding propositions, and sketches approaches for fixing it.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@wkrozowski wkrozowski added the changelog-tactics User facing tactics label Mar 5, 2026
@wkrozowski
Copy link
Contributor Author

wkrozowski commented Mar 5, 2026

!bench

@leanprover-radar
Copy link

leanprover-radar commented Mar 5, 2026 •
edited
Loading

Benchmark results for 15c333b against fe1ad52 are in! @wkrozowski

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

No significant changes detected.

@wkrozowski
Copy link
Contributor Author

wkrozowski commented Mar 5, 2026

!bench

@leanprover-radar
Copy link

leanprover-radar commented Mar 5, 2026 •
edited
Loading

Benchmark results for 95146e1 against fe1ad52 are in! @wkrozowski

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

Large changes (2🟥)

  • 🟥 elab/cbv_aes//instructions: +53.3G (+113.73%)
  • 🟥 elab/cbv_arm_ldst//instructions: +1.7G (+2.24%)

Small changes (1✅)

  • ✅ build/module/Lean.Meta.Tactic.Cbv.ControlFlow//instructions: -146.4M (-2.22%) (reduced significance based on absolute threshold)

@wkrozowski
Copy link
Contributor Author

wkrozowski commented Mar 5, 2026

!bench

@leanprover-radar
Copy link

leanprover-radar commented Mar 5, 2026 •
edited
Loading

Benchmark results for a3adbf7 against fe1ad52 are in! @wkrozowski

  • 🟥 build//instructions: +922.7M (+0.01%)

Small changes (1🟥)

  • 🟥 build/module/Lean.Meta.Tactic.Cbv.ControlFlow//instructions: +131.7M (+2.00%) (reduced significance based on *//lines)

@wkrozowski
Copy link
Contributor Author

wkrozowski commented Mar 5, 2026

!bench

@leanprover-radar
Copy link

leanprover-radar commented Mar 5, 2026 •
edited
Loading

Benchmark results for a0efe1a against fe1ad52 are in! @wkrozowski

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

Small changes (1🟥)

  • 🟥 build/module/Lean.Meta.Tactic.Cbv.ControlFlow//instructions: +255.3M (+3.88%) (reduced significance based on *//lines)

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

mathlib-lean-pr-testing bot commented Mar 5, 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 fe1ad52f88a2b72913f9cb5f218146cb5a0c584f --onto 333ab1c6f0ce11f33551d6a736054cb72812cad9. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-05 22:41:26)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a165292462a973c20d3cc8c8b23a3ac2334a2a4a --onto 333ab1c6f0ce11f33551d6a736054cb72812cad9. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-06 13:06:32)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Mar 5, 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 fe1ad52f88a2b72913f9cb5f218146cb5a0c584f --onto cda84702e9b31165f1f83c657b532f36f34e0bd0. You can force reference manual CI using the force-manual-ci label. (2026-03-05 22:41:27)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase a165292462a973c20d3cc8c8b23a3ac2334a2a4a --onto cda84702e9b31165f1f83c657b532f36f34e0bd0. You can force reference manual CI using the force-manual-ci label. (2026-03-06 13:06:34)

@wkrozowski
Copy link
Contributor Author

wkrozowski commented Mar 6, 2026

!bench

@leanprover-radar
Copy link

leanprover-radar commented Mar 6, 2026 •
edited
Loading

Benchmark results for 314bfad against a165292 are in! @wkrozowski

  • ✅ build//instructions: -286.3M (-0.00%)

Small changes (1🟥)

  • 🟥 build/module/Lean.Meta.Tactic.Cbv.ControlFlow//instructions: +259.8M (+3.95%) (reduced significance based on *//lines)

@wkrozowski
Copy link
Contributor Author

wkrozowski commented Mar 6, 2026

!bench

@leanprover-radar
Copy link

leanprover-radar commented Mar 6, 2026 •
edited
Loading

Benchmark results for f9418ee against a165292 are in! @wkrozowski

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

Small changes (2✅, 1🟥)

  • 🟥 build/module/Lean.Meta.Tactic.Cbv.ControlFlow//instructions: +380.6M (+5.78%) (reduced significance based on *//lines)
  • ✅ elab/cbv_arm_ldst//instructions: -331.1M (-0.43%)
  • ✅ elab/cbv_merge_sort//instructions: -261.2M (-1.22%)

@wkrozowski
Copy link
Contributor Author

wkrozowski commented Mar 6, 2026

!bench

@leanprover-radar
Copy link

leanprover-radar commented Mar 6, 2026 •
edited
Loading

Benchmark results for c46d6cc against a165292 are in! @wkrozowski

  • ✅ build//instructions: -750.8M (-0.01%)

Small changes (2✅, 1🟥)

  • 🟥 build/module/Lean.Meta.Tactic.Cbv.ControlFlow//instructions: +381.6M (+5.80%) (reduced significance based on *//lines)
  • ✅ elab/cbv_arm_ldst//instructions: -340.4M (-0.44%)
  • ✅ elab/cbv_merge_sort//instructions: -271.5M (-1.26%)

@wkrozowski
Copy link
Contributor Author

wkrozowski commented Mar 6, 2026

!bench

@leanprover-radar
Copy link

leanprover-radar commented Mar 6, 2026 •
edited
Loading

Benchmark results for 3f831d2 against a165292 are in! @wkrozowski

  • ✅ build//instructions: -348.1M (-0.00%)

Small changes (2✅, 1🟥)

  • 🟥 build/module/Lean.Meta.Tactic.Cbv.ControlFlow//instructions: +235.4M (+3.58%) (reduced significance based on *//lines)
  • ✅ elab/cbv_arm_ldst//instructions: -343.0M (-0.44%)
  • ✅ elab/cbv_merge_sort//instructions: -260.7M (-1.21%)

@wkrozowski
Copy link
Contributor Author

wkrozowski commented Mar 6, 2026

!bench

@leanprover-radar
Copy link

leanprover-radar commented Mar 6, 2026 •
edited
Loading

Benchmark results for 3a5f5a0 against a165292 are in! @wkrozowski

  • 🟥 build//instructions: +697.3M (+0.01%)

Large changes (1🟥)

  • 🟥 lake/inundation/build no-op//instructions: +619.1M (+10.59%)

Small changes (2✅, 2🟥)

  • 🟥 build/module/Init.Sym.Lemmas//instructions: +56.4M (+2.77%)
  • 🟥 build/module/Lean.Meta.Tactic.Cbv.ControlFlow//instructions: +945.2M (+14.36%) (reduced significance based on *//lines)
  • ✅ elab/cbv_arm_ldst//instructions: -361.1M (-0.46%)
  • ✅ elab/cbv_merge_sort//instructions: -274.4M (-1.28%)

@wkrozowski wkrozowski changed the title fix: prevent cbv from picking up classical Decidable instances fix: cbv handling of ite/dite/decide Mar 6, 2026
@wkrozowski wkrozowski mentioned this pull request Mar 6, 2026
Closed
@wkrozowski
Copy link
Contributor Author

wkrozowski commented Mar 6, 2026

!bench

@leanprover-radar
Copy link

leanprover-radar commented Mar 6, 2026 •
edited
Loading

Benchmark results for 699fa8e against a165292 are in! @wkrozowski

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

Small changes (2✅, 2🟥)

  • 🟥 build/module/Init.Sym.Lemmas//instructions: +56.9M (+2.80%)
  • 🟥 build/module/Lean.Meta.Tactic.Cbv.ControlFlow//instructions: +1.1G (+16.68%) (reduced significance based on *//lines)
  • ✅ elab/cbv_arm_ldst//instructions: -347.8M (-0.45%)
  • ✅ elab/cbv_merge_sort//instructions: -263.1M (-1.23%)

@wkrozowski wkrozowski force-pushed the wojciech/cbv-classical-draft branch from 699fa8e to 3a5f5a0 Compare March 6, 2026 15:35
@wkrozowski wkrozowski marked this pull request as ready for review March 6, 2026 15:37
@wkrozowski wkrozowski requested a review from leodemoura as a code owner March 6, 2026 15:37
@wkrozowski
Copy link
Contributor Author

wkrozowski commented Mar 6, 2026

!bench

@leanprover-radar
Copy link

leanprover-radar commented Mar 6, 2026

Benchmark results for 3a5f5a0 against a165292 are in! @wkrozowski

  • 🟥 build//instructions: +697.3M (+0.01%)

Large changes (1🟥)

  • 🟥 lake/inundation/build no-op//instructions: +619.1M (+10.59%)

Small changes (2✅, 2🟥)

  • 🟥 build/module/Init.Sym.Lemmas//instructions: +56.4M (+2.77%)
  • 🟥 build/module/Lean.Meta.Tactic.Cbv.ControlFlow//instructions: +945.2M (+14.36%) (reduced significance based on *//lines)
  • ✅ elab/cbv_arm_ldst//instructions: -361.1M (-0.46%)
  • ✅ elab/cbv_merge_sort//instructions: -274.4M (-1.28%)

@wkrozowski wkrozowski added this pull request to the merge queue Mar 6, 2026
Merged via the queue into leanprover:master with commit 54f1881 Mar 6, 2026
33 of 35 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