The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Fri, 31 Aug 2012 01:11:29 -0700,
Ed Morehouse 
<emorehouse AT wesleyan.edu>
 a écrit :

> Hi Coq Clubbers,
> 
> I have been trying to gain proficiency with type classes and instance 
> resolution in Coq and have been fairly successful, that is, until I 
> started to try to use notations with my type classes via the 
> "operational type class" technique as described, for example, in
> Pierre Castéran and Matthieu Sozeau's recent tutorial.
> 
> Below is a small example illustrating the kind of problems I've been 
> having.  I would be grateful if someone could explain to me why the 
> tactic in the last line doesn't succeed.  I'm sure it's something
> silly that I'm misunderstanding but, well, I couldn't figure it out.
> 
> 
> ----------8<----------
> 
> ...
> 
> (* since it's a preorder it should be reflexive too, right? *)
> Goal Reflexive le .
> Proof .
> unfold Reflexive .
> apply reflexivity .

It works if you declare [le] as an instance of a binary relation :

Instance le_bin_rel : Binary_Relation nat := le.

Goal Reflexive le_bin_rel.
Proof .
unfold Reflexive .
apply reflexivity.


> 
> (* Error:
>   * Could not find an instance for "Reflexive le".
>   *
>   * but why not? (Reflexive le) should be satisfied by (Preorder le),
>   * which Coq figured out all by itself, so why can't it infer 
> (Reflexive le)?
>   *)
> 
> 
> ---------->8----------
> 
> I thought that maybe it wasn't getting that le is a binary relation
> on nat, but adding the line:
> 
> Instance le_relation : Binary_Relation nat  :=  le .
> 
> doesn't help either.
> 
> 
> 
> thanks in advance for any help,
> 
> -Ed
>