Option.decidableEqNone

Stream: lean4

[Aaron Liu]

Could we make docs#Option.decidableEqNone an instance? I know it makes a diamond with the current implementations, but

universe u

variable {α : Type u} (o : Option α)

example [DecidableEq α] : Option.instDecidableEq o none = @Option.decidableEqNone α o := by
  with_unfolding_all rfl -- fails :(

-- these are better

abbrev 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

abbrev instDecidableEqNone : Decidable (o = none) :=
  match o with
  | none => .isTrue rfl
  | some _ => .isFalse Option.noConfusion

abbrev instDecidableNoneEq : Decidable (none = o) :=
  match o with
  | none => .isTrue rfl
  | some _ => .isFalse Option.noConfusion

example [DecidableEq α] : instDecidableEq o none = instDecidableEqNone o := by
  with_reducible rfl
example [DecidableEq α] : instDecidableEq none o = instDecidableNoneEq o := by
  with_reducible rfl

that can be avoided.

[Eric Wieser]

I was not expecting

  match a, b with
  | none, none => .isTrue rfl
  | none, some _ => .isFalse Option.noConfusion
  | some _, none => .isFalse Option.noConfusion
  | some a, some b => decidable_of_decidable_of_eq (Option.some.injEq a b).symm

to have a different defeq

[Aaron Liu]

I was thinking about doing that but then I realized I don't know how the matches are compiled and better be safe than sorry

[Aaron Liu]

It turns out it is still defeq if you turn off smartUnfolding

[Eric Wieser]

Which I guess is something that forbids partially unfolding a match

[Eric Wieser]

How did you find smartUnfolding so fast?

[Aaron Liu]

prior experience

[Eric Wieser]

For reference, the docstring of that option is

when computing weak head normal form, use auxiliary definition created for functions defined by structural recursion

[Aaron Liu]

specifically, docs#Nat.repeatTR and docs#Nat.iterate are defeq but only if you turn off smartUnfolding

[Eric Wieser]

I guess there's an implicit "instead of actually unfolding"

[Aaron Liu]

I think Kyle said something about it before and I remembered

[Aaron Liu]

No one objected so I made a PR: lean4#9302

[Rob Simmons]

Just merged! Thanks for your patience everyone, I'm also working on a follow-up to get the same thing working for lists and maybe arrays.

[Aaron Liu]

I tried implementing it naively for lists (copy what I did for Option) but it didn't work because of the structural recursion

[Aaron Liu]

I think if it make it into two mutual definitions it might still be possible

[Rob Simmons]

@Aaron Liu I think the List instances in that PR works fine with defeq, you can check my work though! I basically just unfolded the definition by one step. It's only the array one that doesn't respect definitional equality right now.

[Rob Simmons]

(I'm still wrapping my head around lean-specific defeq nuances tbh)