2
$\begingroup$

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?

$\endgroup$
2

1 Answer 1

1
$\begingroup$

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.
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.