The Coq mailing list

["Vladimir Komendantsky" <komendantsky AT gmail.com>]

For instance, this definition for relation is compatible with your script:

Record relation (A:Type) := mk_relation {
  fun_of_rel :> A -> A -> Prop
}.

It defines the required coercion from relation to Funclass.

V


2008/10/23 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
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>