DecidableEq for Tree

Stream: general

[Asei Inoue]

why this raise an error?

variable {α : Type} [DecidableEq α]

inductive Tree (α : Type) where
  | empty
  | node (v : α) (children : List (Tree α))
/- None of the deriving handlers for class `DecidableEq` applied to Tree -/
deriving DecidableEq, BEq

[Henrik Böving]

Because Tree is a nested inductive type so it's quite a bit more complicated to automatically derive a DecidableEq (or anything that recurses over it for that matter)

[Asei Inoue]

but we can derive BEq. why?

[Henrik Böving]

Most likely because BEq is not proof carrying so getting it done is quite a lot easier. It's most likely not the case that deriving DecidableEq is actually impossible, it's just hard.

[Joachim Breitner]

The derived BEq uses partial here. That would be silly for DecidableEq.

[Eric Wieser]

Would it? DecidableEq is for more than just decide

[Aaron Liu]

I feel like it should still be possible to systematically derive a DecidableEq here

[Aaron Liu]

how does it work normally?

[Joachim Breitner]

Hmm, ok, maybe silly is a strong word. So you say a partial definition that doesn't work with by decide or with kernel reduction of if would still be more useful than unhelpful?

[Joachim Breitner]

(it is maybe unfortunate that the same type class is used both for kernel reduction and compiled code)

[Eric Wieser]

I would argue that decidable instances are still sometimes a good idea even if they are neither reducible nor executable!

[Joachim Breitner]

If you want something that's neither reducible nor executable, wouldn't then Classical.propDecidable serve your purpose?

[Edward van de Meent]

having an instance makes lean not complain about failure to synthesize. However, if you use open Classical, the instance synthesis might not give you the decidability instance you want in unrelated cases (possibly in the same declaration, making open in not a feasible alternative). Therefore there is benefit, however small

[Edward van de Meent]

that aside, maybe this just means that someone needs to look into/spend time writing a non-partial deriver for DecidableEq for mutual/nested inductives...

[Aaron Liu]

Edward van de Meent said:

having an instance makes lean not complain about failure to synthesize. However, if you use open Classical, the instance synthesis might not give you the decidability instance you want in unrelated cases (possibly in the same declaration, making open in not a feasible alternative). Therefore there is benefit, however small

but if that's the case then you can just register the instance but make the implementation be Classical.propDecidable, right? (mathlib does this for docs#Real.decidableEq)

[Eric Wieser]

I guess I should clarify that while registering the instance is a good idea in that case, indeed there would be little value in deriving it