The Coq mailing list

[Georges Gonthier <gonthier AT microsoft.com>]

If you have trouble understanding coercions, use the
   Print Graph.
command to display the entire coercion DAG. In this case it will tell you 
that 'equivalent' is a coercion to relation, not to Funclass. Adding the 
declaration
  Identity Coercion fun_of_relation : relation >-> Funclass.
will sort the problem out (it tells the coercion system that relation is an 
alias for a function type).

Cheers,

Georges Gonthier

-----Original Message-----
From: 
coq-club-admin AT pauillac.inria.fr
 
[mailto:coq-club-admin AT pauillac.inria.fr]
 On Behalf Of Mark Dickinson
Sent: 23 October 2008 12:05
To: 
coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Interaction of coercions and definitions

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