The Coq standard library has two subsets of classes modules, one anchored in Coq.Classes.RelationClasses and the other in Coq.Classes.CRelationClasses. The latter seems to have been added more recently (2012).
I must be missing something obvious as they both look very similar to me.
What is the reason they exist?
2 Answers
The key difference is in the type of relations they support:
(* RelationClasses, actually defined in Relation_Definitions *)
Definition relation (A : Type) := A -> A -> Prop.
(* CRelationClasses *)
Definition crelation (A : Type) := A -> A -> Type.
In addition to crelation producing a Type instead of a Prop, another key difference is that crelation is universe polymorphic, but relation is not.
Require Import Relation_Definitions.
Require Import Coq.Classes.CRelationClasses.
Set Printing Universes.
Print relation.
(*
relation =
fun A : Type@{Coq.Relations.Relation_Definitions.1} => A -> A -> Prop
: Type@{Coq.Relations.Relation_Definitions.1} ->
Type@{max(Set+1,Coq.Relations.Relation_Definitions.1)}
*)
Print crelation.
(*
crelation@{u u0} =
fun A : Type@{u} => A -> A -> Type@{u0}
: Type@{u} -> Type@{max(u,u0+1)}
(* u u0 |= *)
*)
Check (fun (R: crelation (Type -> Type)) => R crelation).
Fail Check (fun (R: relation (Type -> Type)) => R relation).
(*
The command has indeed failed with message:
In environment
R : relation (Type@{test.7} -> Type@{test.8})
The term "relation" has type
"Type@{Coq.Relations.Relation_Definitions.1} ->
Type@{max(Set+1,Coq.Relations.Relation_Definitions.1)}"
while it is expected to have type "Type@{test.7} -> Type@{test.8}"
(universe inconsistency: Cannot enforce Coq.Relations.Relation_Definitions.1
<= test.8 because test.8 < Coq.Relations.Relation_Definitions.1).
*)
