decidable equality over inductive types

Stream: Is there code for X?

[Jared green]

it there a way to automatically infer decidable equality over an inductive type built only from a base with decidable equality?

[Matt Diamond]

does deriving DecidableEq work?

[Jared green]

can i see an example of how that would look:

[Matt Diamond]

sure!

inductive Foo where
  | one
  | two
deriving DecidableEq

#eval Foo.one = Foo.two -- false
#eval Foo.one = Foo.one -- true

[Jared green]

it doesnt work.

[Matt Diamond]

ah okay... could you post a #mwe of what you're trying to do?

[Jared green]

open Classical

variable {α : Type}[h : DecidableEq α]
inductive normalizable α (pred : α -> Prop)
  where
  | atom : α -> (normalizable α pred)
  | And : (normalizable α pred) -> (normalizable α pred) -> normalizable α pred
  | Or : (normalizable α pred) -> (normalizable α pred) -> normalizable α pred
  | Not : normalizable α pred -> normalizable α pred

[Jared green]

im getting an error further down the line and im not sure whether this is responsible

[Matt Diamond]

I see... well, I'm not sure either since I don't know what error you're getting, but in theory adding deriving DecidableEq should derive decidable equality for a type

[Jared green]

how can we know that?

[Matt Diamond]

import Mathlib

variable {α : Type}[h : DecidableEq α]
inductive normalizable α (pred : α -> Prop)
  where
  | atom : α -> (normalizable α pred)
  | And : (normalizable α pred) -> (normalizable α pred) -> normalizable α pred
  | Or : (normalizable α pred) -> (normalizable α pred) -> normalizable α pred
  | Not : normalizable α pred -> normalizable α pred
deriving DecidableEq

example : ∀ (pred : α -> Prop), Nonempty (DecidableEq (normalizable α pred)) := fun p => ⟨by infer_instance⟩

[Matt Diamond]

of course, if you have open Classical then everything is decidable and you don't need to derive it in the first place

[Matt Diamond]

well, unless you're trying to avoid noncomputable defs

[Arthur Adjedj]

Matt Diamond said:

I see... well, I'm not sure either since I don't know what error you're getting, but in theory adding deriving DecidableEq should derive decidable equality for a type

Note that deriving DecidableEq does not always work. In particular, it doesn't handle:

• Indexed inductive types (I'm not sure DecidableEq is provable for indexed inductives in general)
• Nested inductive types (doable, should be handled soon™)
• Inductives types with recursive occurences inside dependent families such as:

inductive Foo where
  | foo : (Nat → Foo) → Foo
deriving DecidableEq --fails