The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Dear Michael,

  the problem here is that your last definition does not generate any
type class constraint but a conversion problem  PreOrder nat le =
Reflexive nat le which fails. If you put _ instead, then there is a
typeclasss constraint ? : Reflexive nat le that is generated and can
be filled using the instances. The point of type classes is usually to
let the system infer the instances, not write them explicitely like
NatLEPreOrder here. Also, type class substructures/subinstances are
not coercions (as in your example PreOrder'). You can however declare
them after the fact to be coercions using, e.g : Coercion
PreOrder_Reflexive : PreOrder >-> Reflexive.

  You might be interested in reading this introduction in addition to
the reference manual:
http://www.labri.fr/perso/casteran/CoqArt/TypeClassesTut/typeclassestut.pdf

Hope this helps,
-- Matthieu

2014-12-11 13:16 GMT+01:00 Soegtrop, Michael 
<michael.soegtrop AT intel.com>:
> Dear Matthieu,
>
> I replaced the "Definition" with "Instance" and the "Qed" with "Defined" as 
> below, but I still can't get it to work so far that I can experiment with 
> it and understand the semantics of a type class substructure. I also read 
> your paper "First-Class Type Classes", but it doesn't explain this in much 
> more detail than the reference manual. I would really appreciate a simple 
> example, which demonstrates the semantics of type class substructures.
>
> Best regards,
>
> Michael
>
>
> Require Import Arith.
>
> Definition relation (A : Type) := A->A->Prop.
>
> Class Reflexive (A : Type) (R : relation A) := reflexivity : forall x, R x 
> x.
>
> Class Transitive (A : Type) (R : relation A) := transitivity : forall x y 
> z, R x y -> R y z -> R x z.
>
> Class PreOrder (A : Type) (R : relation A) := {
>   PreOrder_Reflexive :> Reflexive A R ;
>   PreOrder_Transitive :> Transitive A R
> }.
>
> Instance NatLERefl : Reflexive nat le.
> Proof. unfold Reflexive. apply le_n. Defined.
>
> Instance NatLETrans : Transitive nat le.
> Proof. unfold Transitive. apply le_trans. Defined.
>
> Instance NatLEPreOrder : PreOrder nat le.
> Proof. constructor. apply NatLERefl. apply NatLETrans. Defined.
>
> (*Does not work - type checking error *)
> Definition testPreorderIsRefl : Reflexive nat le := NatLEPreOrder.
>



-- 
-- Matthieu