derive decidable_rel

Stream: general

[Kevin Buzzard]

import tactic

-- Let X be the set {A,B,C}
@[derive fintype] inductive X
|A : X
|B : X
|C : X

-- Define a relation by R(A,B) and R(A,C) both true, and everything else false.

open X

inductive R : X → X → Prop
| AB : R A B
| AC : R A C

instance : decidable_rel R :=
begin
  unfold decidable_rel,
  intros a b,
  cases a; cases b;
  [left, right, right, left, left, left, left, left, left];
  exact R.AB <|> exact R.AC <|> rintro (_ | _),
end

Am I missing a trick here? I couldn't derive decidable rel automatically. Or does my proof have too many ideas in?

[Bhavik Mehta]

You could do this

import tactic

-- Let X be the set {A,B,C}
@[derive [fintype, decidable_eq]] inductive X
|A : X
|B : X
|C : X

-- Define a relation by R(A,B) and R(A,C) both true, and everything else false.

open X

@[derive decidable_pred]
def R : X → X → Prop := λ x y, x = A ∧ (y = B ∨ y = C)

example : decidable_rel R := infer_instance