# Documentation

Mathlib.Logic.Relation

# Relation closures #

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

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

## Definitions #

• Relation.ReflGen: Reflexive closure. ReflGen r relates everything r related, plus for all a it relates a with itself. So ReflGen r a b ↔ r a b ∨ a = b.
• Relation.TransGen: Transitive closure. TransGen r relates everything r related transitively. So TransGen r a b ↔ ∃ x₀ ... xₙ, r a x₀ ∧ r x₀ x₁ ∧ ... ∧ r xₙ b.
• Relation.ReflTransGen: Reflexive transitive closure. ReflTransGen r relates everything r related transitively, plus for all a it relates a with itself. So ReflTransGen r a b ↔ (∃ x₀ ... xₙ, r a x₀ ∧ r x₀ x₁ ∧ ... ∧ r xₙ b) ∨ a = b. It is the same as the reflexive closure of the transitive closure, or the transitive closure of the reflexive closure. In terms of rewriting systems, this means that a can be rewritten to b in a number of rewrites.
• Relation.Comp: Relation composition. We provide notation ∘r. For r : α → β → Prop and s : β → γ → Prop, r ∘r srelates a : α and c : γ iff there exists b : β that's related to both.
• Relation.Map: Image of a relation under a pair of maps. For r : α → β → Prop, f : α → γ, g : β → δ, Map r f g is the relation γ → δ → Prop relating f a and g b for all a, b related by r.
• Relation.Join: Join of a relation. For r : α → α → Prop, Join r a b ↔ ∃ c, r a c ∧ r b c. In terms of rewriting systems, this means that a and b can be rewritten to the same term.
theorem IsRefl.reflexive {α : Type u_1} {r : ααProp} [IsRefl α r] :
theorem Reflexive.rel_of_ne_imp {α : Type u_1} {r : ααProp} (h : ) {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 : ) {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} [IsRefl α 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 [IsRefl α r].

theorem Symmetric.iff {α : Type u_1} {r : ααProp} (H : ) (x : α) (y : α) :
r x y r y x
theorem Symmetric.flip_eq {α : Type u_1} {r : ααProp} (h : ) :
flip r = r
theorem Symmetric.swap_eq {α : Type u_1} {r : ααProp} :
theorem flip_eq_iff {α : Type u_1} {r : ααProp} :
flip r = r
theorem swap_eq_iff {α : Type u_1} {r : ααProp} :
theorem Reflexive.comap {α : Type u_1} {β : Type u_2} {r : ββProp} (h : ) (f : αβ) :
theorem Symmetric.comap {α : Type u_1} {β : Type u_2} {r : ββProp} (h : ) (f : αβ) :
theorem Transitive.comap {α : Type u_1} {β : Type u_2} {r : ββProp} (h : ) (f : αβ) :
theorem Equivalence.comap {α : Type u_1} {β : Type u_2} {r : ββProp} (h : ) (f : αβ) :
def Relation.Comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (r : αβProp) (p : βγProp) (a : α) (c : γ) :

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.

Instances For
theorem Relation.comp_eq {α : Type u_1} {β : Type u_2} {r : αβProp} :
(Relation.Comp r fun x x_1 => x = x_1) = r
theorem Relation.eq_comp {α : Type u_1} {β : Type u_2} {r : αβProp} :
Relation.Comp (fun x x_1 => x = x_1) r = r
theorem Relation.iff_comp {α : Type u_1} {r : PropαProp} :
Relation.Comp (fun x x_1 => x x_1) r = r
theorem Relation.comp_iff {α : Type u_1} {r : α} :
(Relation.Comp r fun x x_1 => x x_1) = r
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} :
def Relation.Fibration {α : Type u_1} {β : Type u_2} (rα : ααProp) (rβ : ββProp) (f : αβ) :

A function f : α → β is a fibration between the relation rα and rβ if for all a : α and b : β, whenever b : β and f a are related by rβ, b is the image of some a' : α under f, and a' and a are related by rα.

Instances For
theorem Acc.of_fibration {α : Type u_1} {β : Type u_2} {rα : ααProp} {rβ : ββProp} (f : αβ) (fib : Relation.Fibration f) {a : α} (ha : Acc a) :
Acc (f a)

If f : α → β is a fibration between relations rα and rβ, and a : α is accessible under rα, then f a is accessible under rβ.

theorem Acc.of_downward_closed {α : Type u_1} {β : Type u_2} {rβ : ββProp} (f : αβ) (dc : ∀ {a : α} {b : β}, b (f a)c, f c = b) (a : α) (ha : Acc (InvImage f) a) :
Acc (f a)
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.

Instances For
theorem Relation.ReflTransGen.cases_tail_iff {α : Type u_1} (r : ααProp) (a : α) :
∀ (a : α), a = a b, r b a
inductive Relation.ReflTransGen {α : Type u_1} (r : ααProp) (a : α) :
αProp
• refl: ∀ {α : Type u_1} {r : ααProp} {a : α},
• tail: ∀ {α : Type u_1} {r : ααProp} {a b c : α}, r b c

ReflTransGen r: reflexive transitive closure of r

Instances For
theorem Relation.reflGen_iff {α : Type u_1} (r : ααProp) (a : α) :
∀ (a : α), a = a r a a
inductive Relation.ReflGen {α : Type u_1} (r : ααProp) (a : α) :
αProp
• refl: ∀ {α : Type u_1} {r : ααProp} {a : α},
• single: ∀ {α : Type u_1} {r : ααProp} {a b : α}, r a b

ReflGen r: reflexive closure of r

Instances For
theorem Relation.transGen_iff {α : Type u_1} (r : ααProp) (a : α) :
∀ (a : α), r a a b, r b a
inductive Relation.TransGen {α : Type u_1} (r : ααProp) (a : α) :
αProp
• single: ∀ {α : Type u_1} {r : ααProp} {a b : α}, r a b
• tail: ∀ {α : Type u_1} {r : ααProp} {a b c : α}, r b c

TransGen r: transitive closure of r

Instances For
theorem Relation.ReflGen.to_reflTransGen {α : Type u_1} {r : ααProp} {a : α} {b : α} :
theorem Relation.ReflGen.mono {α : Type u_1} {r : ααProp} {p : ααProp} (hp : (a b : α) → r a bp a b) {a : α} {b : α} :
instance Relation.ReflGen.instIsReflReflGen {α : Type u_1} {r : ααProp} :
theorem Relation.ReflTransGen.trans {α : Type u_1} {r : ααProp} {a : α} {b : α} {c : α} (hab : ) (hbc : ) :
theorem Relation.ReflTransGen.single {α : Type u_1} {r : ααProp} {a : α} {b : α} (hab : r a b) :
theorem Relation.ReflTransGen.head {α : Type u_1} {r : ααProp} {a : α} {b : α} {c : α} (hab : r a b) (hbc : ) :
theorem Relation.ReflTransGen.symmetric {α : Type u_1} {r : ααProp} (h : ) :
theorem Relation.ReflTransGen.cases_tail {α : Type u_1} {r : ααProp} {a : α} {b : α} :
b = a c, r c b
theorem Relation.ReflTransGen.head_induction_on {α : Type u_1} {r : ααProp} {b : α} {P : (a : α) → Prop} {a : α} (h : ) (refl : P b (_ : )) (head : {a c : α} → (h' : r a c) → (h : ) → P c hP a (_ : )) :
P a h
theorem Relation.ReflTransGen.trans_induction_on {α : Type u_1} {r : ααProp} {P : {a b : α} → Prop} {a : α} {b : α} (h : ) (ih₁ : (a : α) → P a a (_ : )) (ih₂ : {a b : α} → (h : r a b) → P a b (_ : )) (ih₃ : {a b c : α} → (h₁ : ) → (h₂ : ) → P a b h₁P b c h₂P a c (_ : )) :
P a b h
theorem Relation.ReflTransGen.cases_head {α : Type u_1} {r : ααProp} {a : α} {b : α} (h : ) :
a = b c, r a c
theorem Relation.ReflTransGen.cases_head_iff {α : Type u_1} {r : ααProp} {a : α} {b : α} :
a = b c, r a c
theorem Relation.ReflTransGen.total_of_right_unique {α : Type u_1} {r : ααProp} {a : α} {b : α} {c : α} (U : ) (ab : ) (ac : ) :
theorem Relation.TransGen.to_reflTransGen {α : Type u_1} {r : ααProp} {a : α} {b : α} (h : ) :
theorem Relation.TransGen.trans_left {α : Type u_1} {r : ααProp} {a : α} {b : α} {c : α} (hab : ) (hbc : ) :
instance Relation.TransGen.instTransTransGenReflTransGen {α : Type u_1} {r : ααProp} :
theorem Relation.TransGen.trans {α : Type u_1} {r : ααProp} {a : α} {b : α} {c : α} (hab : ) (hbc : ) :
instance Relation.TransGen.instTransTransGen {α : Type u_1} {r : ααProp} :
Trans () () ()
theorem Relation.TransGen.head' {α : Type u_1} {r : ααProp} {a : α} {b : α} {c : α} (hab : r a b) (hbc : ) :
theorem Relation.TransGen.tail' {α : Type u_1} {r : ααProp} {a : α} {b : α} {c : α} (hab : ) (hbc : r b c) :
theorem Relation.TransGen.head {α : Type u_1} {r : ααProp} {a : α} {b : α} {c : α} (hab : r a b) (hbc : ) :
theorem Relation.TransGen.head_induction_on {α : Type u_1} {r : ααProp} {b : α} {P : (a : α) → Prop} {a : α} (h : ) (base : {a : α} → (h : r a b) → P a (_ : )) (ih : {a c : α} → (h' : r a c) → (h : ) → P c hP a (_ : )) :
P a h
theorem Relation.TransGen.trans_induction_on {α : Type u_1} {r : ααProp} {P : {a b : α} → Prop} {a : α} {b : α} (h : ) (base : {a b : α} → (h : r a b) → P a b (_ : )) (ih : {a b c : α} → (h₁ : ) → (h₂ : ) → P a b h₁P b c h₂P a c (_ : )) :
P a b h
theorem Relation.TransGen.trans_right {α : Type u_1} {r : ααProp} {a : α} {b : α} {c : α} (hab : ) (hbc : ) :
instance Relation.TransGen.instTransReflTransGenTransGen {α : Type u_1} {r : ααProp} :
theorem Relation.TransGen.tail'_iff {α : Type u_1} {r : ααProp} {a : α} {c : α} :
b, r b c
theorem Relation.TransGen.head'_iff {α : Type u_1} {r : ααProp} {a : α} {c : α} :
b, r a b
theorem Acc.TransGen {α : Type u_1} {r : ααProp} {a : α} (h : Acc r a) :
Acc () a
theorem acc_transGen_iff {α : Type u_1} {r : ααProp} {a : α} :
Acc () a Acc r a
theorem WellFounded.transGen {α : Type u_1} {r : ααProp} (h : ) :
theorem Relation.reflGen_eq_self {α : Type u_1} {r : ααProp} (hr : ) :
theorem Relation.reflexive_reflGen {α : Type u_1} {r : ααProp} :
theorem Relation.reflGen_minimal {α : Type u_1} {r : ααProp} {r' : ααProp} (hr' : ) (h : (x y : α) → r x yr' x y) {x : α} {y : α} (hxy : ) :
r' x y
theorem Relation.transGen_eq_self {α : Type u_1} {r : ααProp} (trans : ) :
theorem Relation.transitive_transGen {α : Type u_1} {r : ααProp} :
instance Relation.instIsTransTransGen {α : Type u_1} {r : ααProp} :
theorem Relation.transGen_idem {α : Type u_1} {r : ααProp} :
theorem Relation.TransGen.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.TransGen p (f a) (f b)
theorem Relation.TransGen.lift' {α : Type u_1} {β : Type u_2} {r : ααProp} {p : ββProp} {a : α} {b : α} (f : αβ) (h : ∀ (a b : α), r a bRelation.TransGen p (f a) (f b)) (hab : ) :
Relation.TransGen p (f a) (f b)
theorem Relation.TransGen.closed {α : Type u_1} {r : ααProp} {a : α} {b : α} {p : ααProp} :
(∀ (a b : α), r a b) →
theorem Relation.TransGen.mono {α : Type u_1} {r : ααProp} {a : α} {b : α} {p : ααProp} :
((a b : α) → r a bp a b) →
theorem Relation.transGen_minimal {α : Type u_1} {r : ααProp} {r' : ααProp} (hr' : ) (h : (x y : α) → r x yr' x y) {x : α} {y : α} (hxy : ) :
r' x y
theorem Relation.TransGen.swap {α : Type u_1} {r : ααProp} {a : α} {b : α} (h : ) :
theorem Relation.transGen_swap {α : Type u_1} {r : ααProp} {a : α} {b : α} :
theorem Relation.reflTransGen_iff_eq {α : Type u_1} {r : ααProp} {a : α} {b : α} (h : ∀ (b : α), ¬r a b) :
b = a
theorem Relation.reflTransGen_iff_eq_or_transGen {α : Type u_1} {r : ααProp} {a : α} {b : α} :
b = a
theorem Relation.ReflTransGen.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.ReflTransGen p (f a) (f b)
theorem Relation.ReflTransGen.mono {α : Type u_1} {r : ααProp} {a : α} {b : α} {p : ααProp} :
((a b : α) → r a bp a b) →
theorem Relation.reflTransGen_eq_self {α : Type u_1} {r : ααProp} (refl : ) (trans : ) :
theorem Relation.reflTransGen_minimal {α : Type u_1} {r : ααProp} {r' : ααProp} (hr₁ : ) (hr₂ : ) (h : (x y : α) → r x yr' x y) {x : α} {y : α} (hxy : ) :
r' x y
theorem Relation.reflexive_reflTransGen {α : Type u_1} {r : ααProp} :
theorem Relation.transitive_reflTransGen {α : Type u_1} {r : ααProp} :
instance Relation.instIsReflReflTransGen {α : Type u_1} {r : ααProp} :
instance Relation.instIsTransReflTransGen {α : Type u_1} {r : ααProp} :
theorem Relation.reflTransGen_idem {α : Type u_1} {r : ααProp} :
theorem Relation.ReflTransGen.lift' {α : Type u_1} {β : Type u_2} {r : ααProp} {p : ββProp} {a : α} {b : α} (f : αβ) (h : ∀ (a b : α), r a bRelation.ReflTransGen p (f a) (f b)) (hab : ) :
Relation.ReflTransGen p (f a) (f b)
theorem Relation.reflTransGen_closed {α : Type u_1} {r : ααProp} {a : α} {b : α} {p : ααProp} :
(∀ (a b : α), r a b) →
theorem Relation.ReflTransGen.swap {α : Type u_1} {r : ααProp} {a : α} {b : α} (h : ) :
theorem Relation.reflTransGen_swap {α : Type u_1} {r : ααProp} {a : α} {b : α} :
@[simp]
theorem Relation.reflGen_transGen {α : Type u_1} {r : ααProp} :
@[simp]
theorem Relation.transGen_reflGen {α : Type u_1} {r : ααProp} :
@[simp]
theorem Relation.reflTransGen_reflGen {α : Type u_1} {r : ααProp} :
@[simp]
theorem Relation.reflTransGen_transGen {α : Type u_1} {r : ααProp} :
theorem Relation.reflTransGen_eq_transGen {α : Type u_1} {r : ααProp} (hr : ) :
theorem Relation.reflTransGen_eq_reflGen {α : Type u_1} {r : ααProp} (hr : ) :
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).

Instances For
theorem Relation.church_rosser {α : Type u_1} {r : ααProp} {a : α} {b : α} {c : α} (h : ∀ (a b c : α), r a br a cd, ) (hab : ) (hac : ) :

A sufficient condition for the Church-Rosser property.

theorem Relation.join_of_single {α : Type u_1} {r : ααProp} {a : α} {b : α} (h : ) (hab : r a b) :
theorem Relation.symmetric_join {α : Type u_1} {r : ααProp} :
theorem Relation.reflexive_join {α : Type u_1} {r : ααProp} (h : ) :
theorem Relation.transitive_join {α : Type u_1} {r : ααProp} (ht : ) (h : ∀ (a b c : α), r a br a c) :
theorem Relation.equivalence_join {α : Type u_1} {r : ααProp} (hr : ) (ht : ) (h : ∀ (a b c : α), r a br a c) :
theorem Relation.equivalence_join_reflTransGen {α : Type u_1} {r : ααProp} (h : ∀ (a b c : α), r a br a cd, ) :
theorem Relation.join_of_equivalence {α : Type u_1} {r : ααProp} {a : α} {b : α} {r' : ααProp} (hr : ) (h : (a b : α) → r' a br a b) :
Relation.Join r' a br a b
theorem Relation.reflTransGen_of_transitive_reflexive {α : Type u_1} {r : ααProp} {a : α} {b : α} {r' : ααProp} (hr : ) (ht : ) (h : (a b : α) → r' a br a b) (h' : ) :
r a b
theorem Relation.reflTransGen_of_equivalence {α : Type u_1} {r : ααProp} {a : α} {b : α} {r' : ααProp} (hr : ) :
((a b : α) → r' a br a b) → r a b
theorem Equivalence.eqvGen_iff {α : Type u_1} {r : ααProp} {a : α} {b : α} (h : ) :
EqvGen r a b r a b
theorem Equivalence.eqvGen_eq {α : Type u_1} {r : ααProp} (h : ) :
= r
theorem EqvGen.mono {α : Type u_1} {a : α} {b : α} {r : ααProp} {p : ααProp} (hrp : (a b : α) → r a bp a b) (h : EqvGen r a b) :
EqvGen p a b