Library Coq.Classes.EquivDec
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.
Notation " x == y " := (
equiv_dec (
x :>) (
y :>)) (
no associativity,
at level 70) :
equiv_scope.
Definition swap_sumbool {
A B} (
x : {
A } + {
B }) : {
B } + {
A } :=
match x with
|
left H => @
right _ _ H
|
right H => @
left _ _ H
end.
Require Import Coq.Program.Program.
Open Local Scope program_scope.
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 burried inside the setoid, but we can recover it by specifying which setoid we're talking about.
Program Instance nat_eq_eqdec :
EqDec nat eq :=
eq_nat_dec.
Require Import Coq.Bool.Bool.
Program Instance bool_eqdec :
EqDec bool eq :=
bool_dec.
Program Instance unit_eqdec :
EqDec unit eq :=
λ x y,
in_left.
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 }.
Solve Obligations using unfold complement,
equiv ;
program_simpl.
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 }.
Solve Obligations using unfold complement,
equiv ;
program_simpl.
Objects of function spaces with countable domains like bool have decidable equality.
Proving the reflection requires functional extensionality though.