From 5c8ebd886873c3c476a4a6729bb850d5f571b8d7 Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Wed, 19 Nov 2025 20:48:42 -0500 Subject: [PATCH] feat: make `Option.decidableEqNone` coherent with `Option.instDecidableEq` (#9302) 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](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Option.2EdecidableEqNone/near/527226250). --------- Co-authored-by: Eric Wieser Co-authored-by: Rob Simmons --- src/Init/Data/Option/Basic.lean | 34 ++++++++++++++++++++++++++++- src/Init/Data/Option/Instances.lean | 11 ---------- tests/lean/run/optionDecEq.lean | 11 ++++++++++ 3 files changed, 44 insertions(+), 12 deletions(-) create mode 100644 tests/lean/run/optionDecEq.lean diff --git a/src/Init/Data/Option/Basic.lean b/src/Init/Data/Option/Basic.lean index 36c855bf40..ee099c9e4b 100644 --- a/src/Init/Data/Option/Basic.lean +++ b/src/Init/Data/Option/Basic.lean @@ -15,7 +15,39 @@ public section namespace Option -deriving instance DecidableEq for Option +/- We write the instance manually so that it is coherent with `decidableEqNone` and +`decidableNoneEq`. + +TODO: adjust the `deriving instance DecidableEq` handler to generate something coherent. -/ +instance instDecidableEq {α} [DecidableEq α] : DecidableEq (Option α) := fun a b => + match a with + | none => match b with + | none => .isTrue rfl + | some _ => .isFalse Option.noConfusion + | some a => match b with + | none => .isFalse Option.noConfusion + | some b => decidable_of_decidable_of_eq (Option.some.injEq a b).symm + +/-- +Equality with `none` is decidable even if the wrapped type does not have decidable equality. +-/ +instance decidableEqNone (o : Option α) : Decidable (o = none) := + /- We use a `match` instead of transferring from `isNone_iff_eq_none` for + compatibility with the `DecidableEq` instance. -/ + match o with + | none => .isTrue rfl + | some _ => .isFalse Option.noConfusion + +/-- +Equality with `none` is decidable even if the wrapped type does not have decidable equality. +-/ +instance decidableNoneEq (o : Option α) : Decidable (none = o) := + /- We use a `match` instead of transferring from `isNone_iff_eq_none` for + compatibility with the `DecidableEq` instance. -/ + match o with + | none => .isTrue rfl + | some _ => .isFalse Option.noConfusion + deriving instance BEq for Option @[simp, grind =] theorem getD_none : getD none a = a := rfl diff --git a/src/Init/Data/Option/Instances.lean b/src/Init/Data/Option/Instances.lean index 5f28a958a2..0dbbaa1420 100644 --- a/src/Init/Data/Option/Instances.lean +++ b/src/Init/Data/Option/Instances.lean @@ -35,17 +35,6 @@ instance [DecidableEq α] (j : α) (o : Option α) : Decidable (j ∈ o) := theorem some_inj {a b : α} : some a = some b ↔ a = b := by simp; rfl -/-- -Equality with `none` is decidable even if the wrapped type does not have decidable equality. - -This is not an instance because it is not definitionally equal to the standard instance of -`DecidableEq (Option α)`, which can cause problems. It can be locally bound if needed. - -Try to use the Boolean comparisons `Option.isNone` or `Option.isSome` instead. --/ -@[inline] def decidableEqNone {o : Option α} : Decidable (o = none) := - decidable_of_decidable_of_iff isNone_iff_eq_none - instance decidableForallMem {p : α → Prop} [DecidablePred p] : ∀ o : Option α, Decidable (∀ a, a ∈ o → p a) | none => isTrue nofun diff --git a/tests/lean/run/optionDecEq.lean b/tests/lean/run/optionDecEq.lean new file mode 100644 index 0000000000..ddafc80ae5 --- /dev/null +++ b/tests/lean/run/optionDecEq.lean @@ -0,0 +1,11 @@ +variable {α : Type u} [DecidableEq α] + +-- test for instance diamonds + +example (x : Option α) : + Option.instDecidableEq x none = Option.decidableEqNone x := by + with_reducible_and_instances rfl + +example (x : Option α) : + Option.instDecidableEq none x = Option.decidableNoneEq x := by + with_reducible_and_instances rfl