mathlib documentation

logic.relation

Relation closures #

This file defines the reflexive, transitive, and reflexive transitive closures of relations. It also proves some basic results on definitions in core, such as eqv_gen.

Note that this is about unbundled relations, that is terms of types of the form α → β → Prop. For the bundled version, see rel.

Definitions #

theorem is_refl.reflexive {α : Type u_1} {r : α → α → Prop} [is_refl α r] :
theorem reflexive.rel_of_ne_imp {α : Type u_1} {r : α → α → Prop} (h : reflexive r) {x y : α} (hr : x yr x y) :
r x y

To show a reflexive relation r : α → α → Prop holds over x y : α, it suffices to show it holds when x ≠ y.

theorem reflexive.ne_imp_iff {α : Type u_1} {r : α → α → Prop} (h : reflexive r) {x y : α} :
x yr x y r x y

If a reflexive relation r : α → α → Prop holds over x y : α, then it holds whether or not x ≠ y.

theorem reflexive_ne_imp_iff {α : Type u_1} {r : α → α → Prop} [is_refl α r] {x y : α} :
x yr x y r x y

If a reflexive relation r : α → α → Prop holds over x y : α, then it holds whether or not x ≠ y. Unlike reflexive.ne_imp_iff, this uses [is_refl α r].

@[protected]
theorem symmetric.iff {α : Type u_1} {r : α → α → Prop} (H : symmetric r) (x y : α) :
r x y r y x
theorem reflexive.comap {α : Type u_1} {β : Type u_2} {r : β → β → Prop} (h : reflexive r) (f : α → β) :
theorem symmetric.comap {α : Type u_1} {β : Type u_2} {r : β → β → Prop} (h : symmetric r) (f : α → β) :
theorem transitive.comap {α : Type u_1} {β : Type u_2} {r : β → β → Prop} (h : transitive r) (f : α → β) :
theorem equivalence.comap {α : Type u_1} {β : Type u_2} {r : β → β → Prop} (h : equivalence r) (f : α → β) :
def relation.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (r : α → β → Prop) (p : β → γ → Prop) (a : α) (c : γ) :
Prop

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
theorem relation.comp_eq {α : Type u_1} {β : Type u_2} {r : α → β → Prop} :
theorem relation.eq_comp {α : Type u_1} {β : Type u_2} {r : α → β → Prop} :
theorem relation.iff_comp {α : Type u_1} {r : Prop → α → Prop} :
theorem relation.comp_iff {α : Type u_1} {r : α → Prop → Prop} :
theorem relation.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : α → β → Prop} {p : β → γ → Prop} {q : γ → δ → Prop} :
theorem relation.flip_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → β → Prop} {p : β → γ → Prop} :
@[protected]
def relation.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (r : α → β → Prop) (f : α → γ) (g : β → δ) :
γ → δ → Prop

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.

Equations
inductive relation.refl_trans_gen {α : Type u_1} (r : α → α → Prop) (a : α) :
α → Prop

refl_trans_gen r: reflexive transitive closure of r

theorem relation.refl_trans_gen.cases_tail_iff {α : Type u_1} (r : α → α → Prop) (a ᾰ : α) :
relation.refl_trans_gen r a = a ∃ {b : α}, relation.refl_trans_gen r a b r b
inductive relation.refl_gen {α : Type u_1} (r : α → α → Prop) (a : α) :
α → Prop
  • refl : ∀ {α : Type u_1} (r : α → α → Prop) (a : α), relation.refl_gen r a a
  • single : ∀ {α : Type u_1} (r : α → α → Prop) (a : α) {b : α}, r a brelation.refl_gen r a b

refl_gen r: reflexive closure of r

theorem relation.refl_gen_iff {α : Type u_1} (r : α → α → Prop) (a ᾰ : α) :
relation.refl_gen r a = a r a
inductive relation.trans_gen {α : Type u_1} (r : α → α → Prop) (a : α) :
α → Prop

trans_gen r: transitive closure of r

theorem relation.trans_gen_iff {α : Type u_1} (r : α → α → Prop) (a ᾰ : α) :
relation.trans_gen r a r a ∃ {b : α}, relation.trans_gen r a b r b
theorem relation.refl_gen.to_refl_trans_gen {α : Type u_1} {r : α → α → Prop} {a b : α} :
theorem relation.refl_trans_gen.trans {α : Type u_1} {r : α → α → Prop} {a b c : α} (hab : relation.refl_trans_gen r a b) (hbc : relation.refl_trans_gen r b c) :
theorem relation.refl_trans_gen.single {α : Type u_1} {r : α → α → Prop} {a b : α} (hab : r a b) :
theorem relation.refl_trans_gen.head {α : Type u_1} {r : α → α → Prop} {a b c : α} (hab : r a b) (hbc : relation.refl_trans_gen r b c) :
theorem relation.refl_trans_gen.symmetric {α : Type u_1} {r : α → α → Prop} (h : symmetric r) :
theorem relation.refl_trans_gen.cases_tail {α : Type u_1} {r : α → α → Prop} {a b : α} :
relation.refl_trans_gen r a b(b = a ∃ (c : α), relation.refl_trans_gen r a c r c b)
theorem relation.refl_trans_gen.head_induction_on {α : Type u_1} {r : α → α → Prop} {b : α} {P : Π (a : α), relation.refl_trans_gen r a b → Prop} {a : α} (h : relation.refl_trans_gen r a b) (refl : P b relation.refl_trans_gen.refl) (head : ∀ {a c : α} (h' : r a c) (h : relation.refl_trans_gen r c b), P c hP a _) :
P a h
theorem relation.refl_trans_gen.trans_induction_on {α : Type u_1} {r : α → α → Prop} {P : Π {a b : α}, relation.refl_trans_gen r a b → Prop} {a b : α} (h : relation.refl_trans_gen r a b) (ih₁ : ∀ (a : α), P relation.refl_trans_gen.refl) (ih₂ : ∀ {a b : α} (h : r a b), P _) (ih₃ : ∀ {a b c : α} (h₁ : relation.refl_trans_gen r a b) (h₂ : relation.refl_trans_gen r b c), P h₁P h₂P _) :
P h
theorem relation.refl_trans_gen.cases_head {α : Type u_1} {r : α → α → Prop} {a b : α} (h : relation.refl_trans_gen r a b) :
a = b ∃ (c : α), r a c relation.refl_trans_gen r c b
theorem relation.refl_trans_gen.cases_head_iff {α : Type u_1} {r : α → α → Prop} {a b : α} :
relation.refl_trans_gen r a b a = b ∃ (c : α), r a c relation.refl_trans_gen r c b
theorem relation.refl_trans_gen.total_of_right_unique {α : Type u_1} {r : α → α → Prop} {a b c : α} (U : relator.right_unique r) (ab : relation.refl_trans_gen r a b) (ac : relation.refl_trans_gen r a c) :
theorem relation.trans_gen.to_refl {α : Type u_1} {r : α → α → Prop} {a b : α} (h : relation.trans_gen r a b) :
theorem relation.trans_gen.trans_left {α : Type u_1} {r : α → α → Prop} {a b c : α} (hab : relation.trans_gen r a b) (hbc : relation.refl_trans_gen r b c) :
theorem relation.trans_gen.trans {α : Type u_1} {r : α → α → Prop} {a b c : α} (hab : relation.trans_gen r a b) (hbc : relation.trans_gen r b c) :
theorem relation.trans_gen.head' {α : Type u_1} {r : α → α → Prop} {a b c : α} (hab : r a b) (hbc : relation.refl_trans_gen r b c) :
theorem relation.trans_gen.tail' {α : Type u_1} {r : α → α → Prop} {a b c : α} (hab : relation.refl_trans_gen r a b) (hbc : r b c) :
theorem relation.trans_gen.head {α : Type u_1} {r : α → α → Prop} {a b c : α} (hab : r a b) (hbc : relation.trans_gen r b c) :
theorem relation.trans_gen.head_induction_on {α : Type u_1} {r : α → α → Prop} {b : α} {P : Π (a : α), relation.trans_gen r a b → Prop} {a : α} (h : relation.trans_gen r a b) (base : ∀ {a : α} (h : r a b), P a _) (ih : ∀ {a c : α} (h' : r a c) (h : relation.trans_gen r c b), P c hP a _) :
P a h
theorem relation.trans_gen.trans_induction_on {α : Type u_1} {r : α → α → Prop} {P : Π {a b : α}, relation.trans_gen r a b → Prop} {a b : α} (h : relation.trans_gen r a b) (base : ∀ {a b : α} (h : r a b), P _) (ih : ∀ {a b c : α} (h₁ : relation.trans_gen r a b) (h₂ : relation.trans_gen r b c), P h₁P h₂P _) :
P h
theorem relation.trans_gen.trans_right {α : Type u_1} {r : α → α → Prop} {a b c : α} (hab : relation.refl_trans_gen r a b) (hbc : relation.trans_gen r b c) :
theorem relation.trans_gen.tail'_iff {α : Type u_1} {r : α → α → Prop} {a c : α} :
relation.trans_gen r a c ∃ (b : α), relation.refl_trans_gen r a b r b c
theorem relation.trans_gen.head'_iff {α : Type u_1} {r : α → α → Prop} {a c : α} :
relation.trans_gen r a c ∃ (b : α), r a b relation.refl_trans_gen r b c
theorem relation.trans_gen_eq_self {α : Type u_1} {r : α → α → Prop} (trans : transitive r) :
theorem relation.transitive_trans_gen {α : Type u_1} {r : α → α → Prop} :
theorem relation.trans_gen_idem {α : Type u_1} {r : α → α → Prop} :
theorem relation.trans_gen.lift {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {p : β → β → Prop} {a b : α} (f : α → β) (h : ∀ (a b : α), r a bp (f a) (f b)) (hab : relation.trans_gen r a b) :
relation.trans_gen p (f a) (f b)
theorem relation.trans_gen.lift' {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {p : β → β → Prop} {a b : α} (f : α → β) (h : ∀ (a b : α), r a brelation.trans_gen p (f a) (f b)) (hab : relation.trans_gen r a b) :
relation.trans_gen p (f a) (f b)
theorem relation.trans_gen.closed {α : Type u_1} {r : α → α → Prop} {a b : α} {p : α → α → Prop} :
(∀ (a b : α), r a brelation.trans_gen p a b)relation.trans_gen r a brelation.trans_gen p a b
theorem relation.refl_trans_gen_iff_eq {α : Type u_1} {r : α → α → Prop} {a b : α} (h : ∀ (b : α), ¬r a b) :
theorem relation.refl_trans_gen_iff_eq_or_trans_gen {α : Type u_1} {r : α → α → Prop} {a b : α} :
theorem relation.refl_trans_gen.lift {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {p : β → β → Prop} {a b : α} (f : α → β) (h : ∀ (a b : α), r a bp (f a) (f b)) (hab : relation.refl_trans_gen r a b) :
theorem relation.refl_trans_gen.mono {α : Type u_1} {r : α → α → Prop} {a b : α} {p : α → α → Prop} :
(∀ (a b : α), r a bp a b)relation.refl_trans_gen r a brelation.refl_trans_gen p a b
theorem relation.refl_trans_gen_eq_self {α : Type u_1} {r : α → α → Prop} (refl : reflexive r) (trans : transitive r) :
theorem relation.reflexive_refl_trans_gen {α : Type u_1} {r : α → α → Prop} :
theorem relation.transitive_refl_trans_gen {α : Type u_1} {r : α → α → Prop} :
theorem relation.refl_trans_gen.lift' {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {p : β → β → Prop} {a b : α} (f : α → β) (h : ∀ (a b : α), r a brelation.refl_trans_gen p (f a) (f b)) (hab : relation.refl_trans_gen r a b) :
theorem relation.refl_trans_gen_closed {α : Type u_1} {r : α → α → Prop} {a b : α} {p : α → α → Prop} :
(∀ (a b : α), r a brelation.refl_trans_gen p a b)relation.refl_trans_gen r a brelation.refl_trans_gen p a b
def relation.join {α : Type u_1} (r : α → α → Prop) :
α → α → Prop

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
theorem relation.church_rosser {α : Type u_1} {r : α → α → Prop} {a b c : α} (h : ∀ (a b c : α), r a br a c(∃ (d : α), relation.refl_gen r b d relation.refl_trans_gen r c d)) (hab : relation.refl_trans_gen r a b) (hac : relation.refl_trans_gen r a c) :

A sufficient condition for the Church-Rosser property.

theorem relation.join_of_single {α : Type u_1} {r : α → α → Prop} {a b : α} (h : reflexive r) (hab : r a b) :
theorem relation.symmetric_join {α : Type u_1} {r : α → α → Prop} :
theorem relation.reflexive_join {α : Type u_1} {r : α → α → Prop} (h : reflexive r) :
theorem relation.transitive_join {α : Type u_1} {r : α → α → Prop} (ht : transitive r) (h : ∀ (a b c : α), r a br a crelation.join r b c) :
theorem relation.equivalence_join {α : Type u_1} {r : α → α → Prop} (hr : reflexive r) (ht : transitive r) (h : ∀ (a b c : α), r a br a crelation.join r b c) :
theorem relation.equivalence_join_refl_trans_gen {α : Type u_1} {r : α → α → Prop} (h : ∀ (a b c : α), r a br a c(∃ (d : α), relation.refl_gen r b d relation.refl_trans_gen r c d)) :
theorem relation.join_of_equivalence {α : Type u_1} {r : α → α → Prop} {a b : α} {r' : α → α → Prop} (hr : equivalence r) (h : ∀ (a b : α), r' a br a b) :
relation.join r' a br a b
theorem relation.refl_trans_gen_of_transitive_reflexive {α : Type u_1} {r : α → α → Prop} {a b : α} {r' : α → α → Prop} (hr : reflexive r) (ht : transitive r) (h : ∀ (a b : α), r' a br a b) (h' : relation.refl_trans_gen r' a b) :
r a b
theorem relation.refl_trans_gen_of_equivalence {α : Type u_1} {r : α → α → Prop} {a b : α} {r' : α → α → Prop} (hr : equivalence r) :
(∀ (a b : α), r' a br a b)relation.refl_trans_gen r' a br a b
theorem equivalence.eqv_gen_iff {α : Type u_1} {r : α → α → Prop} {a b : α} (h : equivalence r) :
eqv_gen r a b r a b
theorem equivalence.eqv_gen_eq {α : Type u_1} {r : α → α → Prop} (h : equivalence r) :
theorem eqv_gen.mono {α : Type u_1} {a b : α} {r p : α → α → Prop} (hrp : ∀ (a b : α), r a bp a b) (h : eqv_gen r a b) :
eqv_gen p a b