Decidable (none ∈ L)

Stream: Is there code for X?

[Scott Morrison]

Do we have

import Mathlib

set_option autoImplicit true

example (L : List (Option α)) : Decidable (none ∈ L) := inferInstance -- failed to synthesize instance

hiding somewhere?

[Mario Carneiro]

I don't think so

[Mario Carneiro]

it should be a one liner since \exists x \in L, x = none is decidable

[Scott Morrison]

9-liner?

instance (x : Option α) : Decidable (x = none) := by
  cases x <;> (simp; infer_instance)

example (L : List (Option α)) : Decidable (∃ x ∈ L, x = none) := inferInstance

theorem List.mem_iff_exists_mem_eq {a : α} {L : List α} : a ∈ L ↔ ∃ x ∈ L, x = a := by
  simp

instance (L : List (Option α)) : Decidable (none ∈ L) := by
  rw [List.mem_iff_exists_mem_eq]
  infer_instance

[Scott Morrison]

Even that first instance seems to be missing.

[Yaël Dillies]

Yes, because it conflicts with docs#instDecidableEqOption, but we do have it as a definition. In fact, we have it twice! docs#Option.decidable_eq_none, docs#Option.decidableEqNone.

[Scott Morrison]

Ugh, Decidable conflicts are lame.

[Eric Wieser]

I think the conflict is solvable?

attribute [-instance] instDecidableEqOption

instance eqNone (x : Option α) : Decidable (x = none) := match x with
  | none => .isTrue rfl
  | some x => .isFalse <| by simp

instance noneEq (x : Option α) : Decidable (none = x) := match x with
  | none => .isTrue rfl
  | some x => .isFalse <| by simp

instance eq [DecidableEq α] : DecidableEq (Option α) := fun x y => match x with
  | none => inferInstance
  | some x => match y with
    | none => .isFalse <| by simp
    | some y => if h : x = y then .isTrue <| by simp [h] else .isFalse <| by simp [h]

example [DecidableEq α] (x : Option α) : eq x none = eqNone x := rfl
example [DecidableEq α] (x : Option α) : eq none x = noneEq x := rfl

[Eric Wieser]

This would have to go in core, since that's where the offending instDecidableEqOption is

[Yaël Dillies]

Nicely done!

[Scott Morrison]

Nice. If you make a PR please assign it to me, and include a comment explaining why it needs to be done in core.

[Eric Wieser]

What's not entirely clear to me is why the above is necessary; it looks like the obvious way to implement the decidability

[Eric Wieser]

Perhaps we should actually be changing the DecidableEq derive handler to produce something analogous to the instance eq above

[Schrodinger ZHU Yifan]

Eric Wieser said:

I think the conflict is solvable?

attribute [-instance] instDecidableEqOption

instance eqNone (x : Option α) : Decidable (x = none) := match x with
  | none => .isTrue rfl
  | some x => .isFalse <| by simp

instance noneEq (x : Option α) : Decidable (none = x) := match x with
  | none => .isTrue rfl
  | some x => .isFalse <| by simp

instance eq [DecidableEq α] : DecidableEq (Option α) := fun x y => match x with
  | none => inferInstance
  | some x => match y with
    | none => .isFalse <| by simp
    | some y => if h : x = y then .isTrue <| by simp [h] else .isFalse <| by simp [h]

example [DecidableEq α] (x : Option α) : eq x none = eqNone x := rfl
example [DecidableEq α] (x : Option α) : eq none x = noneEq x := rfl

what does “attribute -instance” do here

[Yaël Dillies]

It locally makes instDecidableEqOption a non-instance