Ssreflect Users Discussion List

[Vincent Siles <>]

Hi everyone,
I'm currently working on a formalization with an abstract relation R :
A -> A -> Prop.
Most of the work doesn't need to know anything else about R, but
there is a special set of results when R is a decidable equality.

I currently the following:

Section Eqdec.
Variable eqA : A -> A -> Prop.
Variable eqA_dec : forall x y, {eqA x y}+{~eqA x y}.
Context `{Equivalence A eqA}.

(* code *)
End Eqdec.

Having to destruct eqA_dec is really annoying, so I was thinking that
the decidability
could be done using a boolean version of eqA, but I'm not sure what's
the right way
to do it.

I was thinking about the following solution:
Section Eqb.
Variable eqA : A -> A -> Prop.
Variable eqb : A -> A -> bool.
Hypothesis eqAP : forall x y, reflect (eqA x y) (eqb x y).
Context `{Equivalence A eqA}.

(* code *)
End Eqb.

Is this a reasonable solution ? Should I put all this in a Record ?
Any advices or remarks are very welcome.

Cheers,
Vincent