The Coq mailing list

[<michael.soegtrop AT intel.com>]

Dear Coq Users,

I have a question on Type Class Substructures as descibed in the reference
manual section 19.5.2. I tried the example given in the manual:

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

Definition NatLERefl : Reflexive nat le.
Proof. unfold Reflexive. apply le_n. Qed.

Definition NatLETrans : Transitive nat le.
Proof. unfold Transitive. apply le_trans. Qed.

Definition NatLEPreOrder : PreOrder nat le.
Proof. constructor. apply NatLERefl. apply NatLETrans. Qed.

(* The manual claims that in this situation any PreOrder can be used when a
reflexive or transitive relation is expected, so I assume they type check as
such. But when I try the below assignment, it doesn't type check: *)

Definition testPreorderIsRefl : Reflexive nat le := NatLEPreOrder.

(* A side note: the same does work using a record with implicit coercion *)

Record PreOrder' (A : Type) (R : relation A) := {
  PreOrder_Reflexive' :> Reflexive A R ;
  PreOrder_Transitive' :> Transitive A R
}.

Definition NatLEPreOrder' : PreOrder' nat le.
Proof. constructor. apply NatLERefl. apply NatLETrans. Qed.

Definition testPreorderIsRefl : Reflexive nat le := NatLEPreOrder'.

Does somehone have an example on Type Class Substructures, which illustrates
the concept?

Thanks & best regards,

Michael