Library Coq.Classes.EquivDec
Decidable equivalences.
Author: Matthieu Sozeau
Institution: LRI, CNRS UMR 8623 - University Paris Sud
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) :
equiv_scope.
Define boolean versions, losing the logical information.
Decidable leibniz equality instances.
The equiv is buried inside the setoid, but we can recover it by specifying
which setoid we're talking about.
#[
global]
Program Instance nat_eq_eqdec :
EqDec nat eq :=
eq_nat_dec.
#[
global]
Program Instance bool_eqdec :
EqDec bool eq :=
bool_dec.
#[
global]
Program Instance unit_eqdec :
EqDec unit eq :=
fun x y =>
in_left.
Obligation Tactic :=
unfold complement,
equiv ;
program_simpl.
#[
global]
Program Instance prod_eqdec `(
EqDec A eq,
EqDec B eq) :
EqDec (
prod A B)
eq :=
{
equiv_dec x y :=
let '
(x1, x2) :=
x in
let '
(y1, y2) :=
y in
if x1 == y1 then
if x2 == y2 then in_left
else in_right
else in_right }.
#[
global]
Program Instance sum_eqdec `(
EqDec A eq,
EqDec B eq) :
EqDec (
sum A B)
eq := {
equiv_dec x y :=
match x,
y with
|
inl a,
inl b =>
if a == b then in_left else in_right
|
inr a,
inr b =>
if a == b then in_left else in_right
|
inl _,
inr _ |
inr _,
inl _ =>
in_right
end }.
Objects of function spaces with countable domains like bool have decidable
equality. Proving the reflection requires functional extensionality though.