The composition of two relations, yielding a new relation. The result
relates a term of α
and a term of γ
if there is an intermediate
term of β
related to both.
Equations
- relation.comp r p a c = ∃ (b : β), r a b ∧ p b c
The map of a relation r
through a pair of functions pushes the
relation to the codomains of the functions. The resulting relation is
defined by having pairs of terms related if they have preimages
related by r
.
- refl : ∀ {α : Type u_1} (r : α → α → Prop) (a : α), relation.refl_trans_gen r a a
- tail : ∀ {α : Type u_1} (r : α → α → Prop) (a : α) {b c : α}, relation.refl_trans_gen r a b → r b c → relation.refl_trans_gen r a c
refl_trans_gen r
: reflexive transitive closure of r
- refl : ∀ {α : Type u_1} (r : α → α → Prop) (a : α), relation.refl_gen r a a
- single : ∀ {α : Type u_1} (r : α → α → Prop) (a : α) {b : α}, r a b → relation.refl_gen r a b
refl_gen r
: reflexive closure of r
- single : ∀ {α : Type u_1} (r : α → α → Prop) (a : α) {b : α}, r a b → relation.trans_gen r a b
- tail : ∀ {α : Type u_1} (r : α → α → Prop) (a : α) {b c : α}, relation.trans_gen r a b → r b c → relation.trans_gen r a c
trans_gen r
: transitive closure of r
The join of a relation on a single type is a new relation for which
pairs of terms are related if there is a third term they are both
related to. For example, if r
is a relation representing rewrites
in a term rewriting system, then confluence is the property that if
a
rewrites to both b
and c
, then join r
relates b
and c
(see relation.church_rosser
).
Equations
- relation.join r = λ (a b : α), ∃ (c : α), r a c ∧ r b c