# Proving that equality is decidable on an Inductive Set

I've managed to prove that equality within a type is indeed decidable.

  Require Import Coq.Logic.Decidable.

Inductive Person : Set :=
alice
|bob
|charlie.

Print Person_rec.

Inductive Role : Set :=
truth_teller
|spy
|liar.

Definition eq_def (S:Set) :Prop := forall p0 p1:S, decidable (p0 = p1).

Lemma person_eq_def : eq_def Person.
Proof.
unfold eq_def.
intros.
unfold decidable.
destruct p0; destruct p1;
auto || (right; discriminate).
Qed.

Lemma role_eq_def : eq_def Role.
Proof.
unfold eq_def.
intros.
unfold decidable.
destruct p0; destruct p1;
auto || (right; discriminate).
Qed.


What disturbs me a bit is two aspects.

1. The demonstrations for person_eq_def and role_eq_def are the same. There must be a way to prevent this type of repetition, but I failed to find it.

2. Is there an advanced tactic that I missed to prove these?

As JojoModding pointed out in his comment , the tactic decide equality works.

https://coq.inria.fr/doc/v8.19/refman/proofs/writing-proofs/reasoning-inductives.html#coq:tacn.decide-equality

Thus

  Lemma person_eq_def : eq_def Person.
Proof.
unfold eq_def.
unfold decidable.
decide equality.
Qed.

Lemma role_eq_def : eq_def Role.
Proof.
unfold eq_def.
unfold decidable.
decide equality.
Qed.