Zulip Chat Archive

Stream: general

Topic: derive decidable_rel


Kevin Buzzard (Oct 03 2020 at 17:45):

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 (Oct 03 2020 at 17:51):

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

Last updated: Dec 20 2023 at 11:08 UTC