How to assume an identifier bound to a type with decidable equality using Coq.Structures.Equalities?

Using Coq
1

Hi. Within a section I can use

Parameter A : Type.

to assume A to be a type. I would like to constrain A so that it is any type with decidable equality. I found Coq.Structures.Equalities.HasEqDec but don’t know how to use it.

2

If you really want to use Structures.Equalities, then just start your script with

Module Foo (Import M:MiniDecidableType).

You will then be in a context where there is a type t with a decidable equality.

Goal forall x y:t, x = y \/ x <> y.
Proof.
intros x y.
destruct (eq_dec x y).
now left.
now right.
Qed.

But this is kind of overengineered. If you do not care about modules, just start your script with

Parameter t:Type.
Parameter eq_dec: forall x y:t, {x = y} + {x <> y}.

This has the exact same effect as before.

3

Thanks. I was also advised to assume more axioms and, more importantly, according to the advisor, to avoid using modules at all costs. I am going to learn more about the reason. For now this problem has a good enough solution.