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)
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.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.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.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.trans_gen_eq_self
{α : Type u_1}
{r : α → α → Prop}
(trans : transitive r) :
relation.trans_gen r = r
theorem
relation.trans_gen.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.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.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
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
relation.eqv_gen_iff_of_equivalence
{α : Type u_1}
{r : α → α → Prop}
{a b : α}
(h : equivalence r) :
theorem
relation.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