Library Coq.Classes.SetoidDec
Decidable setoid equality theory.
Author: Matthieu Sozeau
Institution: LRI, CNRS UMR 8623 - University Paris Sud
Set Implicit Arguments.
Export notations.
The DecidableSetoid class asserts decidability of a Setoid.
It can be useful in proofs to reason more classically.
The EqDec class gives a decision procedure for a particular setoid
equality.
We define the == overloaded notation for deciding equality. It does not
take precedence of == defined in the type scope, hence we can have both
at the same time.
Invert the branches.
Overloaded notation for inequality.
Infix "=/=" :=
nequiv_dec (
no associativity,
at level 70).
Define boolean versions, losing the logical information.
Decidable leibniz equality instances.
The equiv is burried inside the setoid, but we can recover
it by specifying which setoid we're talking about.
Objects of function spaces with countable domains like bool
have decidable equality.