Proving that equality is decidable on an ``Inductive Set``

Question

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?

Answer 1

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.