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 #
relation.refl_gen: Reflexive closure.refl_gen rrelates everythingrrelated, plus for allait relatesawith itself. Sorefl_gen r a b ↔ r a b ∨ a = b.relation.trans_gen: Transitive closure.trans_gen rrelates everythingrrelated transitively. Sotrans_gen r a b ↔ ∃ x₀ ... xₙ, r a x₀ ∧ r x₀ x₁ ∧ ... ∧ r xₙ b.relation.refl_trans_gen: Reflexive transitive closure.refl_trans_gen rrelates everythingrrelated transitively, plus for allait relatesawith itself. Sorefl_trans_gen 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 thatacan be rewritten tobin a number of rewrites.relation.comp: Relation composition. We provide notation∘r. Forr : α → β → Propands : β → γ → Prop,r ∘r srelatesa : αandc : γiff there existsb : βthat's related to both.relation.map: Image of a relation under a pair of maps. Forr : α → β → Prop,f : α → γ,g : β → δ,map r f gis the relationγ → δ → Proprelatingf aandg bfor alla,brelated byr.relation.join: Join of a relation. Forr : α → α → Prop,join r a b ↔ ∃ c, r a c ∧ r b c. In terms of rewriting systems, this means thataandbcan be rewritten to the same term.
theorem
reflexive.rel_of_ne_imp
{α : Type u_1}
{r : α → α → Prop}
(h : reflexive r)
{x y : α}
(hr : x ≠ y → r 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.
If a reflexive relation r : α → α → Prop holds over x y : α,
then it holds whether or not 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
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 : α → β) :
transitive (r on f)
theorem
equivalence.comap
{α : Type u_1}
{β : Type u_2}
{r : β → β → Prop}
(h : equivalence r)
(f : α → β) :
equivalence (r on 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
- relation.comp r p a c = ∃ (b : β), r a b ∧ p b c
theorem
relation.comp_assoc
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{r : α → β → Prop}
{p : β → γ → Prop}
{q : γ → δ → Prop} :
relation.comp (relation.comp r p) q = relation.comp r (relation.comp p q)
theorem
relation.flip_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{r : α → β → Prop}
{p : β → γ → Prop} :
flip (relation.comp r p) = relation.comp (flip p) (flip r)
@[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.
- 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
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 ᾰ
- 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
theorem
relation.refl_gen_iff
{α : Type u_1}
(r : α → α → Prop)
(a ᾰ : α) :
relation.refl_gen r a ᾰ ↔ ᾰ = a ∨ r a ᾰ
- 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
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 : α} :
relation.refl_gen r a b → relation.refl_trans_gen r 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) :
relation.refl_trans_gen r a c
theorem
relation.refl_trans_gen.single
{α : Type u_1}
{r : α → α → Prop}
{a b : α}
(hab : r a b) :
relation.refl_trans_gen 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) :
relation.refl_trans_gen r a c
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 h → P 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) :
relation.refl_trans_gen r b c ∨ relation.refl_trans_gen r c b
theorem
relation.trans_gen.to_refl
{α : Type u_1}
{r : α → α → Prop}
{a b : α}
(h : relation.trans_gen r a b) :
relation.refl_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) :
relation.trans_gen r a 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) :
relation.trans_gen r a 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) :
relation.trans_gen r a 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) :
relation.trans_gen r a 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) :
relation.trans_gen r a 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 h → P 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) :
relation.trans_gen r a 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) :
relation.trans_gen r = r
theorem
relation.trans_gen.lift
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{p : β → β → Prop}
{a b : α}
(f : α → β)
(h : ∀ (a b : α), r a b → p (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 b → relation.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 b → relation.trans_gen p a b) → relation.trans_gen r a b → relation.trans_gen p a b
theorem
relation.refl_trans_gen_iff_eq
{α : Type u_1}
{r : α → α → Prop}
{a b : α}
(h : ∀ (b : α), ¬r a b) :
relation.refl_trans_gen r a b ↔ b = a
theorem
relation.refl_trans_gen_iff_eq_or_trans_gen
{α : Type u_1}
{r : α → α → Prop}
{a b : α} :
relation.refl_trans_gen r a b ↔ b = a ∨ relation.trans_gen r 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 b → p (f a) (f b))
(hab : relation.refl_trans_gen r a b) :
relation.refl_trans_gen p (f a) (f b)
theorem
relation.refl_trans_gen.mono
{α : Type u_1}
{r : α → α → Prop}
{a b : α}
{p : α → α → Prop} :
(∀ (a b : α), r a b → p a b) → relation.refl_trans_gen r a b → relation.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.refl_trans_gen.lift'
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{p : β → β → Prop}
{a b : α}
(f : α → β)
(h : ∀ (a b : α), r a b → relation.refl_trans_gen p (f a) (f b))
(hab : relation.refl_trans_gen r a b) :
relation.refl_trans_gen p (f a) (f b)
theorem
relation.refl_trans_gen_closed
{α : Type u_1}
{r : α → α → Prop}
{a b : α}
{p : α → α → Prop} :
(∀ (a b : α), r a b → relation.refl_trans_gen p a b) → relation.refl_trans_gen r a b → relation.refl_trans_gen p a b
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
theorem
relation.church_rosser
{α : Type u_1}
{r : α → α → Prop}
{a b c : α}
(h : ∀ (a b c : α), r a b → r 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) :
relation.join (relation.refl_trans_gen r) b 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) :
relation.join r a b
theorem
relation.transitive_join
{α : Type u_1}
{r : α → α → Prop}
(ht : transitive r)
(h : ∀ (a b c : α), r a b → r a c → relation.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 b → r a c → relation.join r b c) :
theorem
relation.equivalence_join_refl_trans_gen
{α : Type u_1}
{r : α → α → Prop}
(h : ∀ (a b c : α), r a b → r 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 b → r a b) :
relation.join r' a b → r 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 b → r 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 b → r a b) → relation.refl_trans_gen r' a b → r a b
theorem
eqv_gen.mono
{α : Type u_1}
{a b : α}
{r p : α → α → Prop}
(hrp : ∀ (a b : α), r a b → p a b)
(h : eqv_gen r a b) :
eqv_gen p a b