The Coq mailing list

[Ed Morehouse <emorehouse AT wesleyan.edu>]

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<----------

Require Import Utf8 ZArith .

Generalizable All Variables .

Obligation Tactic  :=  eauto 10 with arith .

(* an "operational type class" for binary relations to support infix 
notation *)
Class Binary_Relation (A : Type) : Type  :=
  binary_relation : A → A → Prop .
Hint Unfold Binary_Relation .
Hint Unfold binary_relation .

Infix "∙"  :=  binary_relation  (at level 61 , left associativity) .

Instance relations_are_relations `(R : A → A → Prop) : Binary_Relation A :=
{
  binary_relation  :=  R
} .

Print Instances Binary_Relation .

(* some properties that binary relations could have *)

Class Reflexive `(R : Binary_Relation A) : Prop  :=
  reflexivity  :  ∀ (x : A) , x ∙ x .
Hint Unfold Reflexive .

Class Transitive `(R : Binary_Relation A) : Prop  :=
  transitivity  :  ∀ (x y z : A) , x ∙ y → y ∙ z → x ∙ z .
Hint Unfold Transitive .

(* etc. *)

(* a preorder is a reflexive and transitive relation *)
Class Preorder `(R : Binary_Relation A) : Prop  :=
{
  preorder_reflexivity  :>  Reflexive R
  ;
  preorder_transitivity  :>  Transitive R
} .
Hint Constructors Preorder .

(* test out the notation: *)
Goal  ∀ `(P : Preorder A) (x y z : A ) , x ∙ y →  y ∙ z → x ∙ z .
Proof .
intros .
eapply transitivity.
- eassumption .
- assumption .
Qed .
(* so far, so good *)

(* notice that ≤ is a preorder on nat: *)
Program Instance le_preorder : Preorder le .
Obligations (* seems okay *) .


(* since it's a preorder it should be reflexive too, right? *)
Goal Reflexive le .
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