Library Coq.Relations.Relation_Operators
Some operators on relations
Initial authors: Bruno Barras, Cristina Cornes
Some of the initial definitions were taken from :
Constructing Recursion Operators in Type Theory
L. Paulson JSC (1986) 2, 325-355
Further extensions by Pierre Castéran
Definition by direct transitive closure
Alternative definition by transitive extension on the left
Alternative definition by transitive extension on the right
Definition by direct transitive closure
Reflexive-transitive closure
Definition by direct reflexive-transitive closure
Alternative definition by transitive extension on the left
Alternative definition by transitive extension on the right
Reflexive-symmetric-transitive closure
Definition by direct reflexive-symmetric-transitive closure
Alternative definition by symmetric-transitive extension on the left
Alternative definition by symmetric-transitive extension on the right
Disjoint union of relations
Lexicographic order on dependent pairs
Multiset of two relations