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