# Library CoqEqDec

A type class-based library for working with decidable equality.

Require Import Coq.Classes.Equivalence.

Require Import Coq.Classes.EquivDec.

Require Import Coq.Logic.Decidable.

Hint Extern 0 (?x === ?x) => reflexivity.

Hint Extern 1 (_ === _) => (symmetry; trivial; fail).

Hint Extern 1 (_ =/= _) => (symmetry; trivial; fail).

The EqDec class is defined in Coq's standard library.

Lemma equiv_reflexive' : forall `{EqDec A} (x : A),

x === x.

Lemma equiv_symmetric' : forall `{EqDec A} (x y : A),

x === y ->

y === x.

Lemma equiv_transitive' : forall `{EqDec A} (x y z : A),

x === y ->

y === z ->

x === z.

Lemma equiv_decidable : forall `{EqDec A} (x y : A),

decidable (x === y).

It is convenient to be able to use a single notation for decidable
equality on types. This can naturally be done using a type class.
However, the definition of EqDec in the EquivDec library is
overly general for cases where the equality is eq: the extra
layer of abstraction provided by abstracting over the equivalence
relation gets in the way of smooth reasoning. To get around this,
we define a version of that class where the equivalence relation
is hard-coded to be eq.

Implementation note: One should not declare an instance for EqDec_eq A directly. First, declare an instance for @EqDec A eq eq_equivalence. Second, let class inference build an instance for EqDec_eq A using the instance declaration below.

Implementation note (BEA): Specifying eq_equivalence explicitly is important. Following Murphy's Law, if type class inference can find multiple ways of inferring the @Equivalence A eq argument, it will do so in the most inconvenient way possible. Additionally, I choose to infer EqDec_eq instances from EqDec instances because the standard library already defines instances for EqDec.

Implementation note: One should not declare an instance for EqDec_eq A directly. First, declare an instance for @EqDec A eq eq_equivalence. Second, let class inference build an instance for EqDec_eq A using the instance declaration below.

Implementation note (BEA): Specifying eq_equivalence explicitly is important. Following Murphy's Law, if type class inference can find multiple ways of inferring the @Equivalence A eq argument, it will do so in the most inconvenient way possible. Additionally, I choose to infer EqDec_eq instances from EqDec instances because the standard library already defines instances for EqDec.

Class EqDec_eq (A : Type) :=

eq_dec : forall (x y : A), {x = y} + {x <> y}.

Instance EqDec_eq_of_EqDec `(@EqDec A eq eq_equivalence) : EqDec_eq A.

This page has been generated by coqdoc