The Coq mailing list

["Mark Dickinson" <dickinsm AT gmail.com>]

I'm having some trouble understanding how implicit coercion to Funclass
interacts with definitions.

Here's a small example to illustrate the problem: the aim is to define
the type of equivalence relations on a given type A, in such a way that
if R is an equivalence relation on A and x and y are terms of type A then
R x y is a valid term.

(* Begin script *)

Section Relations.

Definition relation A : Type := A -> A -> Prop.
Definition reflexive A (R : relation A) := forall x, R x x.
Definition symmetric A (R : relation A) := forall x y, R x y -> R y x.
Definition transitive A (R : relation A) := forall x y z, R y z -> R x
y -> R x z.

Record equivalence_relation (A : Type) : Type := {
  equivalent :> relation A;
  reflexive_prf : reflexive A equivalent;
  symmetric_prf : symmetric A equivalent;
  transitive_prf : transitive A equivalent
}.

Variable A : Type.
Variable R : equivalence_relation A.
Variables x y : A.
Check R x y.

End Relations.

(* End script *)

Running this under coq version 8.1, the line "Check R x y." fails,
giving the error message:

Toplevel input, characters 22-25
Error: Illegal application (Non-functional construction):
The expression "R" of type "equivalence_relation A"
cannot be applied to the term
 "x" : "A"

However, if I replace the line "equivalent :> relation A;" by
"equivalent :> A -> A -> Prop;" then all is well.

The problem seems to be that the definition of equivalence_relation
provides an implicit coercion from equivalence_relation to relation,
but there's no coercion path from relation to Funclass.

How do I declare the coercion from relation to Funclass so that
"Check R x y." typechecks?  As a newcomer to Coq, I'm sure
I'm missing something obvious; any pointers would be appreciated.

Mark Dickinson