The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Michael,

  there is no type class instance needed here, and actually you have
not declared
any instance (using keyword Instance instead of Definition), apart
from the ones declared
with :> (beware that this syntax has a slightly different meaning in
Class declarations and
Record declarations).

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.

Instance 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 := _. (* This uses
NatLEPreOrder and the PreOrder_Reflexive sub-instance* )

Best,
-- Matthieu

2014-12-10 17:30 GMT+01:00  
<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



-- 
-- Matthieu