Library coqrel.RelClasses

Require Export Coq.Classes.RelationClasses.
Require Export RelDefinitions.

More classes for relation properties

In the following we introduce more typeclasses for characterizing properties of relations, in the spirit of the RelationClasses standard library.

Coreflexive relations


Class Coreflexive {A} (R: relation A) :=
  coreflexivity: x y, R x y x = y.

Global Instance eq_corefl {A}:
  Coreflexive (@eq A).
Proof.
  firstorder.
Qed.

Global Instance subrel_eq {A} (R: relation A):
  Coreflexive R
  Related R eq subrel.
Proof.
  firstorder.
Qed.