feat: make `Option.decidableEqNone` coherent with `Option.instDecidableEq` #9302

plp127 · 2025-07-10T16:48:35Z

This PR modifies Option.instDecidableEq and Option.decidableEqNone so that the latter can be made into a global instance without causing diamonds. It also adds Option.decidabeNoneEq.

See Zulip.

eric-wieser · 2025-07-10T16:51:59Z

src/Init/Data/Option/Basic.lean


 namespace Option

-deriving instance DecidableEq for Option


Maybe this is a signal that we should be fixing the derive handler instead?

I'm not so sure; the current variant uses a single match which is usually sufficient. Doing double-match in general would probably just add unneeded complexity.

Besides, the internals of DecidableEq is probably not something that should be relied upon.

src/Init/Data/Option/Basic.lean

tests/lean/run/optionDecEq.lean

TwoFX · 2025-07-21T08:53:08Z

Happy to merge this once the tests are green and we have a building mathlib.

plp127 · 2025-07-21T20:49:15Z

I have no idea why the build is failing, so I don't know how to continue here.

eric-wieser · 2025-07-21T23:17:01Z

Presumably you found it, but the relevant part of the log is

optionDecEq.lean:7:31: error: tactic 'rfl' failed, the left-hand side
  x.instDecidableEq none
is not definitionally equal to the right-hand side
  x.decidableEqNone
α : Type u
inst✝ : DecidableEq α
x : Option α
⊢ x.instDecidableEq none = x.decidableEqNone
optionDecEq.lean:11:31: error: tactic 'rfl' failed, the left-hand side
  none.instDecidableEq x
is not definitionally equal to the right-hand side
  x.decidableNoneEq
α : Type u
inst✝ : DecidableEq α
x : Option α
⊢ none.instDecidableEq x = x.decidableNoneEq

Rob23oba · 2025-07-22T06:52:26Z

Well, it's not actually equal under with_reducible or with_reducible_and_instances, probably because these are different match constants; maybe putting them in the same file would help?

leanprover-community-bot · 2025-07-22T22:13:55Z

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 338456e765807b088f44b1205a7743a215e331a1 --onto cdab726e3d289b80860ae9f5a7de21d990c8b95f. You can force Mathlib CI using the force-mathlib-ci label. (2025-07-22 22:13:55)
💥 Mathlib branch lean-pr-testing-9302 build failed against this PR. (2025-07-24 10:04:26) View Log
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5c2ae7b414fdf7181118d67050d5436b180948cb --onto 6ae31ea2d6e9d6d30c0e2bedac166377a15d07ef. You can force Mathlib CI using the force-mathlib-ci label. (2025-07-29 14:35:54)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5cc0a103468a8da333f1f07781e5b83799582f6f --onto 5a4226f2bdcc6299df76285b1d30f238546c09fe. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-19 17:49:03)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 126fca1ec89b929b0cd73022ff0d444beea82685 --onto 5a4226f2bdcc6299df76285b1d30f238546c09fe. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-19 20:36:24)
✅ Mathlib branch lean-pr-testing-9302 has successfully built against this PR. (2025-11-19 22:56:47) View Log

leanprover-bot · 2025-07-22T22:13:57Z

Reference manual CI status:

❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 338456e765807b088f44b1205a7743a215e331a1 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-07-22 22:13:56)
❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-07-23 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-07-24 09:21:04)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 5c2ae7b414fdf7181118d67050d5436b180948cb --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-07-29 14:35:55)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 5cc0a103468a8da333f1f07781e5b83799582f6f --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-11-19 17:49:05)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 126fca1ec89b929b0cd73022ff0d444beea82685 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-11-19 20:36:26)
❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-11-18 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-11-19 21:59:14)

Rob23oba · 2025-07-24T08:27:38Z

Could you git pull --ff upstream nightly-with-mathlib?

robsimmons · 2025-11-19T19:04:46Z

!bench

leanprover-radar · 2025-11-19T19:05:05Z

Benchmark results for 8f37814 against 5cc0a10 are in! @robsimmons

Runs (1)

other exited with code -1 (🟥)

Co-authored-by: Eric Wieser <[email protected]>

robsimmons · 2025-11-19T20:48:06Z

!bench

leanprover-radar · 2025-11-19T20:48:23Z

Benchmark results for e9a9ee1 against 5a4226f are in! @robsimmons

Runs (2)

other exited with code 2 (🟥)
stdlib exited with code 2 (🟥)

robsimmons · 2025-11-19T20:58:10Z

!bench

leanprover-radar · 2025-11-19T20:58:19Z

Benchmark results for 94a8559 against 5a4226f are in! @plp127 @robsimmons

Major changes (1)

stdlib//instructions changed by +7.3% (🟥).

This PR adds support for decidable equality of empty lists and empty arrays. Decidable equality for lists and arrays is suitably modified so that all diamonds are definitionally equal. Following #9302, the strong condition of definitionally equal under `with_reducible_and_instances` is tested. This also moves some of the comments added in #9302 out of docstrings. --------- Co-authored-by: Aaron Liu <[email protected]> Co-authored-by: Eric Wieser <[email protected]>

plp127 requested a review from kim-em as a code owner July 10, 2025 16:48

eric-wieser reviewed Jul 10, 2025

View reviewed changes

src/Init/Data/Option/Basic.lean Outdated Show resolved Hide resolved

eric-wieser approved these changes Jul 10, 2025

View reviewed changes

Rob23oba reviewed Jul 10, 2025

View reviewed changes

tests/lean/run/optionDecEq.lean Outdated Show resolved Hide resolved

Rob23oba reviewed Jul 10, 2025

View reviewed changes

tests/lean/run/optionDecEq.lean Outdated Show resolved Hide resolved

TwoFX added changelog-library Library awaiting-author Waiting for PR author to address issues labels Jul 21, 2025

TwoFX self-assigned this Jul 21, 2025

leanprover-bot added the P-high We will work on this issue label Jul 21, 2025

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jul 22, 2025

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jul 24, 2025

Update lean-toolchain for testing leanprover/lean4#9302

9a81a9b

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jul 24, 2025

Update lean-toolchain for testing leanprover/lean4#9302

e11aeb1

leanprover-community-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Jul 24, 2025

github-actions bot added the stale label Sep 25, 2025

robsimmons force-pushed the aliu/option branch from 8f37814 to f48675b Compare November 19, 2025 19:45

plp127 and others added 5 commits November 19, 2025 15:45

modify instances

7b24f4f

add tests

75b3832

rename test

f6d84fc

Update src/Init/Data/Option/Basic.lean

b3cd033

Co-authored-by: Eric Wieser <[email protected]>

try to fix tests

4c71a3b

move instances

e9a9ee1

robsimmons force-pushed the aliu/option branch from 002c50e to e9a9ee1 Compare November 19, 2025 20:47

Remove duplication from merge

94a8559

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 19, 2025

Update lean-toolchain for leanprover/lean4#9302

54cc073

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Nov 19, 2025

Update lean-toolchain for leanprover/lean4#9302

c36a932

robsimmons mentioned this pull request Nov 19, 2025

feat: allow decidable equality for empty lists and empty arrays #11269

Merged

leanprover-community-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Nov 19, 2025

robsimmons added this pull request to the merge queue Nov 20, 2025

github-actions bot removed the stale label Nov 20, 2025

Merged via the queue into leanprover:master with commit 5c8ebd8 Nov 20, 2025
25 checks passed

plp127 deleted the aliu/option branch November 20, 2025 02:54

feat: make Option.decidableEqNone coherent with Option.instDecidableEq #9302

feat: make Option.decidableEqNone coherent with Option.instDecidableEq #9302

Uh oh!

Conversation

plp127 commented Jul 10, 2025

Uh oh!

eric-wieser Jul 10, 2025

Choose a reason for hiding this comment

Uh oh!

Rob23oba Jul 10, 2025

Choose a reason for hiding this comment

Uh oh!

Rob23oba Jul 10, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

TwoFX commented Jul 21, 2025

Uh oh!

plp127 commented Jul 21, 2025

Uh oh!

eric-wieser commented Jul 21, 2025

Uh oh!

Rob23oba commented Jul 22, 2025

Uh oh!

leanprover-community-bot commented Jul 22, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-bot commented Jul 22, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Rob23oba commented Jul 24, 2025

Uh oh!

robsimmons commented Nov 19, 2025

Uh oh!

leanprover-radar commented Nov 19, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

robsimmons commented Nov 19, 2025

Uh oh!

leanprover-radar commented Nov 19, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

robsimmons commented Nov 19, 2025

Uh oh!

leanprover-radar commented Nov 19, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

8 participants

feat: make `Option.decidableEqNone` coherent with `Option.instDecidableEq` #9302

feat: make `Option.decidableEqNone` coherent with `Option.instDecidableEq` #9302

leanprover-community-bot commented Jul 22, 2025 •

edited

Loading

leanprover-bot commented Jul 22, 2025 •

edited

Loading

leanprover-radar commented Nov 19, 2025 •

edited

Loading

leanprover-radar commented Nov 19, 2025 •

edited

Loading

leanprover-radar commented Nov 19, 2025 •

edited

Loading