how to derive decidable_rel easily?

Stream: general

[Eric Rodriguez]

say that I have these definitions:

inductive sign_type
| zero | neg | pos

def le : sign_type → sign_type → Prop
| neg _     := true
| zero neg  := false
| zero zero := true
| zero pos  := true
| pos neg   := false
| pos zero  := false
| pos pos   := true

clearly, this is a decidable_rel. I don't particularly want to list out all 9 cases again though, to do of_true .../of_false .... is there some automatic way to generate decidable_rel for these sorts of declarations?

[Yaël Dillies]

Your MWE doesn't compile but does @[derive decidable] work?

[Eric Wieser]

open sign_type makes it work

[Eric Rodriguez]

oops, sorry

[Eric Rodriguez]

neither @[derive decidable] nor @[derive decidable_rel] work

[Eric Wieser]

What's the import for the decidable derive handler?

[Yaël Dillies]

Probably import tactic is enough

[Eric Wieser]

You might also want:

inductive le : sign_type → sign_type → Prop
| of_neg (a) : le neg a
| zero : le zero zero
| of_pos (a) : le a pos

[Eric Wieser]

Followed by

instance : decidable_rel le
| neg a := is_true (le.of_neg a)
| zero zero := is_true le.zero
| a pos := is_true (le.of_pos a)
| zero neg := is_false (λ h, by cases h)
| pos zero := is_false (λ h, by cases h)
| pos neg := is_false (λ h, by cases h)

[Eric Wieser]

Or

instance : decidable_rel le :=
λ a b, by cases a; cases b; {apply is_true, constructor} <|> {apply is_false, intro h, cases h}

[Eric Wieser]

That last proof works for both definitions of le

[Eric Wieser]

How does @[derive decidable_eq] work today? Which derive handler is it using? (edit: ah, docs#tactic.decidable_eq_derive_handler)

[Eric Rodriguez]

I ended up going with the inductive approach and λ a b, by cases a; cases b; exact is_false (by rintro ⟨⟩) <|> exact is_true (by constructor), but it would be nice if there was some other way to do this! I assume the metaprogramming thread is debugging this?

[Damiano Testa]

Honestly, I do not understand much of decidable, but I am always very fond of Johan's suggestion in one of the counterexamples. Is what below useful?

/--  The three element monoid. -/
@[derive [decidable_eq]]
inductive sign_type
| zero
| pos
| neg

namespace sign_type

instance inhabited : inhabited sign_type := ⟨zero⟩

instance : has_zero sign_type := ⟨zero⟩
instance : has_one sign_type := ⟨pos⟩
notation `-1` := neg

/-- The order on `sign_type` is the one induced by the natural order on the image of `aux1`. -/
def aux1 : sign_type → ℕ
| -1 := 0
|  0 := 1
|  1 := 2

/-- A tactic to prove facts by cases. -/
meta def boom : tactic unit :=
`[repeat {rintro ⟨⟩}; dec_trivial]

lemma aux1_inj : function.injective aux1 :=
by boom

instance : linear_order sign_type :=
linear_order.lift aux1 $ aux1_inj

instance : decidable_rel (has_le.le : sign_type → sign_type → Prop) :=
by apply_instance

[Damiano Testa]

(Although I realize that the choice of -1 as notation for neg means that -1 : ℤ will not work, but - 1 : ℤ does! :upside_down: )

[Eric Rodriguez]

I just gave it a has_neg instance, that worked better I think! This is a neat idea, too

[Damiano Testa]

Slowly, this is crawling to become zmod 3...

[Yaël Dillies]

Probably closer to fin' 3

[Damiano Testa]

Sure, although, unless addition starts playing a role, it will be difficult to tell!

[Eric Rodriguez]

I mean, it is, it was just suggested in #12835 to make it a separate type

[Eric Rodriguez]

because sign : \a \to fin 3 is weird