Relations

References

• Term Rewriting and All That

theorem WellFounded.ofTransGen {α : Type u_1} {r : α → α → Prop} (trans_wf : WellFounded (Relation.TransGen r)) : WellFounded r

@[simp]

theorem WellFounded.iff_transGen {α : Type u_1} {r : α → α → Prop} : WellFounded (Relation.TransGen r) ↔ WellFounded r

def Relation.emptyHRelation {α : Sort u} {β : Sort v} : α → β → Prop

The empty (heterogeneous) relation, which always returns False.

Equations

• Relation.emptyHRelation x✝¹ x✝ = False

theorem Relation.ReflGen.to_eqvGen {α : Type u_1} {r : α → α → Prop} {a b : α} (h : ReflGen r a b) : EqvGen r a b

theorem Relation.TransGen.to_eqvGen {α : Type u_1} {r : α → α → Prop} {a b : α} (h : TransGen r a b) : EqvGen r a b

theorem Relation.ReflTransGen.to_eqvGen {α : Type u_1} {r : α → α → Prop} {a b : α} (h : ReflTransGen r a b) : EqvGen r a b

theorem Relation.SymmGen.to_eqvGen {α : Type u_1} {r : α → α → Prop} {a b : α} (h : SymmGen r a b) : EqvGen r a b

@[reducible, inline]

abbrev Relation.MJoin {α : Type u_1} (r : α → α → Prop) : α → α → Prop

The join of the reflexive transitive closure. This is not named in Mathlib, but see #loogle Relation.Join (Relation.ReflTransGen ?r)

Equations

• Relation.MJoin r = Relation.Join (Relation.ReflTransGen r)

theorem Relation.MJoin.refl {α : Type u_1} {r : α → α → Prop} (a : α) : MJoin r a a

theorem Relation.MJoin.symm {α : Type u_1} {r : α → α → Prop} : Symmetric (MJoin r)

theorem Relation.MJoin.single {α : Type u_1} {r : α → α → Prop} {a b : α} (h : ReflTransGen r a b) : MJoin r a b

def Relation.UpTo {α : Type u_1} (r s : α → α → Prop) : α → α → Prop

The relation r 'up to' the relation s.

Equations

• Relation.UpTo r s = Relation.Comp s (Relation.Comp r s)

class Relation.RightEuclidean {α : Type u_1} (r : α → α → Prop) : Prop

A relation r is (right) Euclidean if r a b and r a c guarantee r b c.

• rightEuclidean {a b c : α} : r a b → r a c → r b c

class Relation.LeftEuclidean {α : Type u_1} (r : α → α → Prop) : Prop

A relation r is (left) Euclidean if r a c and r b c guarantee r a b.

• leftEuclidean {a b c : α} : r a c → r b c → r a b

theorem Relation.RightEuclidean.refl_range {α : Type u_1} {r : α → α → Prop} [RightEuclidean r] {a b : α} (ab : r a b) : r b b

A RightEuclidean relation is reflexive on its range

theorem Relation.RightEuclidean.leftEuclidean_swap {α : Type u_1} {r : α → α → Prop} [RightEuclidean r] : LeftEuclidean fun (a b : α) => r b a

The converse of a RightEuclidean relation is LeftEuclidean

instance Relation.RightEuclidean.instSymmOfRefl {α : Type u_1} {r : α → α → Prop} [RightEuclidean r] [Std.Refl r] : Std.Symm r

theorem Relation.RightEuclidean.trichotomous_trans {α : Type u_1} {r : α → α → Prop} [RightEuclidean r] [Std.Trichotomous r] : IsTrans α r

theorem Relation.RightEuclidean.antisymm_rightUnique {α : Type u_1} {r : α → α → Prop} [RightEuclidean r] [Std.Antisymm r] : Relator.RightUnique r

theorem Relation.RightEuclidean.rightUnique_antisymm {α : Type u_1} {r : α → α → Prop} [RightEuclidean r] (h : Relator.RightUnique r) : Std.Antisymm r

theorem Relation.LeftEuclidean.refl_dom {α : Type u_1} {r : α → α → Prop} [LeftEuclidean r] {a b : α} (ab : r a b) : r a a

A LeftEuclidean relation is reflexive on its domain

theorem Relation.LeftEuclidean.rightEuclidean_swap {α : Type u_1} {r : α → α → Prop} [LeftEuclidean r] : RightEuclidean fun (a b : α) => r b a

The converse of a LeftEuclidean relation is RightEuclidean

instance Relation.LeftEuclidean.instSymmOfRefl {α : Type u_1} {r : α → α → Prop} [LeftEuclidean r] [Std.Refl r] : Std.Symm r

theorem Relation.LeftEuclidean.trichotomous_trans {α : Type u_1} {r : α → α → Prop} [LeftEuclidean r] [Std.Trichotomous r] : IsTrans α r

theorem Relation.LeftEuclidean.antisymm_leftUnique {α : Type u_1} {r : α → α → Prop} [LeftEuclidean r] [Std.Antisymm r] : Relator.LeftUnique r

theorem Relation.LeftEuclidean.leftUnique_antisymm {α : Type u_1} {r : α → α → Prop} [LeftEuclidean r] (h : Relator.LeftUnique r) : Std.Antisymm r

theorem Relation.symm_leftEuclidean_iff_rightEuclidean {α : Type u_1} {r : α → α → Prop} [Std.Symm r] : LeftEuclidean r ↔ RightEuclidean r

For a symmetric relation, LeftEuclidean and RightEuclidean are equivalent.

theorem Relation.symm_leftEuclidean_iff_trans {α : Type u_1} {r : α → α → Prop} [Std.Symm r] : LeftEuclidean r ↔ IsTrans α r

For a symmetric relation, LeftEuclidean and transitivity are equivalent.

theorem Relation.symm_rightEuclidean_iff_trans {α : Type u_1} {r : α → α → Prop} [Std.Symm r] : RightEuclidean r ↔ IsTrans α r

For a symmetric relation, RightEuclidean and transitivity are equivalent.

@[reducible, inline]

abbrev Relation.Diamond {α : Type u_1} (r : α → α → Prop) : Prop

A relation has the diamond property when all reductions with a common origin are joinable

Equations

• Relation.Diamond r = ∀ {a b c : α}, r a b → r a c → Relation.Join r b c

@[reducible, inline]

abbrev Relation.Confluent {α : Type u_1} (r : α → α → Prop) : Prop

A relation is confluent when its reflexive transitive closure has the diamond property.

Equations

• Relation.Confluent r = Relation.Diamond (Relation.ReflTransGen r)

@[reducible, inline]

abbrev Relation.SemiConfluent {α : Type u_1} (r : α → α → Prop) : Prop

A relation is semi-confluent when single and multiple steps with common origin are multi-joinable.

Equations

• Relation.SemiConfluent r = ∀ {x y₁ y₂ : α}, Relation.ReflTransGen r x y₂ → r x y₁ → Relation.Join (Relation.ReflTransGen r) y₁ y₂

@[reducible, inline]

abbrev Relation.ChurchRosser {α : Type u_1} (r : α → α → Prop) : Prop

A relation has the Church Rosser property when equivalence implies multi-joinability.

Equations

• Relation.ChurchRosser r = ∀ {x y : α}, Relation.EqvGen r x y → Relation.Join (Relation.ReflTransGen r) x y

theorem Relation.Diamond.extend {α : Type u_1} {r : α → α → Prop} {a b c : α} (h : Diamond r) : ReflTransGen r a b → r a c → Join (ReflTransGen r) b c

Extending a multistep reduction by a single step preserves multi-joinability.

theorem Relation.Diamond.toConfluent {α : Type u_1} {r : α → α → Prop} (h : Diamond r) : Confluent r

The diamond property implies confluence.

theorem Relation.Confluent.toChurchRosser {α : Type u_1} {r : α → α → Prop} (h : Confluent r) : ChurchRosser r

theorem Relation.SemiConfluent.toConfluent {α : Type u_1} {r : α → α → Prop} (h : SemiConfluent r) : Confluent r

theorem Relation.SemiConfluent_iff_ChurchRosser {α : Type u_1} {r : α → α → Prop} : SemiConfluent r ↔ ChurchRosser r

theorem Relation.Confluent_iff_ChurchRosser {α : Type u_1} {r : α → α → Prop} : Confluent r ↔ ChurchRosser r

theorem Relation.Confluent_iff_SemiConfluent {α : Type u_1} {r : α → α → Prop} : Confluent r ↔ SemiConfluent r

theorem Relation.Confluent_of_unique_end {α : Type u_1} {r : α → α → Prop} {x : α} (h : ∀ (y : α), ReflTransGen r y x) : Confluent r

@[reducible, inline]

abbrev Relation.Reducible {α : Type u_1} (r : α → α → Prop) (x : α) : Prop

An element is reducible with respect to a relation if there is a value it is related to.

Equations

• Relation.Reducible r x = ∃ (y : α), r x y

class Relation.Serial {α : Type u_1} (r : α → α → Prop) : Prop

A relation r is serial if every element is Reducible.

• serial (a : α) : Reducible r a

theorem Relation.refl_serial {α : Type u_1} (r : α → α → Prop) (h : Std.Refl r) : Serial r

instance Relation.instSerialOfRefl {α : Type u_1} {r : α → α → Prop} [instRefl : Std.Refl r] : Serial r

@[reducible, inline]

abbrev Relation.Normal {α : Type u_1} (r : α → α → Prop) (x : α) : Prop

An element is normal if it is not reducible.

Equations

• Relation.Normal r x = ¬Relation.Reducible r x

theorem Relation.Normal_iff {α : Type u_1} (r : α → α → Prop) (x : α) : Normal r x ↔ ∀ (y : α), ¬r x y

@[reducible, inline]

abbrev Relation.Normalizable {α : Type u_1} (r : α → α → Prop) (x : α) : Prop

An element is normalizable if it is related to a normal element.

Equations

• Relation.Normalizable r x = ∃ (n : α), Relation.ReflTransGen r x n ∧ Relation.Normal r n

@[reducible, inline]

abbrev Relation.Normalizing {α : Type u_1} (r : α → α → Prop) : Prop

A relation is normalizing when every element is normalizable.

Equations

• Relation.Normalizing r = ∀ (x : α), Relation.Normalizable r x

theorem Relation.Normal.reflTransGen_eq {α : Type u_1} {r : α → α → Prop} {x y : α} (h : Normal r x) (xy : ReflTransGen r x y) : x = y

A multi-step from a normal form must be reflexive.

theorem Relation.ChurchRosser.normal_eqvGen_reflTransGen {α : Type u_1} {r : α → α → Prop} {x y : α} (cr : ChurchRosser r) (norm : Normal r x) (xy : EqvGen r y x) : ReflTransGen r y x

For a Church-Rosser relation, elements in an equivalence class must be multi-step related.

theorem Relation.ChurchRosser.normal_eq {α : Type u_1} {r : α → α → Prop} {x y : α} (cr : ChurchRosser r) (nx : Normal r x) (ny : Normal r y) (xy : EqvGen r x y) : x = y

For a Church-Rosser relation there is one normal form in each equivalence class.

@[implicit_reducible]

def Relation.trans_of_subrelation {α : Type u_1} (s s' r : α → α → Prop) (hr : IsTrans α r) (h : Subrelation s r) (h' : Subrelation s' r) : Trans s s' r

A pair of subrelations lifts to transitivity on the relation.

Equations

• Relation.trans_of_subrelation s s' r hr h h' = { trans := ⋯ }

@[implicit_reducible]

def Relation.trans_of_subrelation_left {α : Type u_1} (s r : α → α → Prop) (hr : IsTrans α r) (h : Subrelation s r) : Trans s r r

A subrelation lifts to transitivity on the left of the relation.

Equations

• Relation.trans_of_subrelation_left s r hr h = { trans := ⋯ }

@[implicit_reducible]

def Relation.trans_of_subrelation_right {α : Type u_1} (s r : α → α → Prop) (hr : IsTrans α r) (h : Subrelation s r) : Trans r s r

A subrelation lifts to transitivity on the right of the relation.

Equations

• Relation.trans_of_subrelation_right s r hr h = { trans := ⋯ }

theorem Relation.Confluent.equivalence_join_reflTransGen {α : Type u_1} {r : α → α → Prop} (h : Confluent r) : Equivalence (Join (ReflTransGen r))

Confluence implies that multi-step joinability is an equivalence.

@[reducible, inline]

abbrev Relation.SN {α : Type u_1} (r : α → α → Prop) : α → Prop

An element x is SN (for strongly-normalising) for a relation r if it is accesible under the inverse of r.

Equations

• Relation.SN r = Acc fun (a b : α) => r b a

theorem Relation.SN_iff_SN_of_rel {α : Type u_1} {r : α → α → Prop} (x : α) : SN r x ↔ ∀ (y : α), r x y → SN r y

theorem Relation.SN.intro {α : Type u_1} {r : α → α → Prop} {x : α} (h : ∀ (y : α), r x y → SN r y) : SN r x

theorem Relation.SN.of_rel {α : Type u_1} {r : α → α → Prop} {x y : α} (hx : SN r x) (h : r x y) : SN r y

theorem Relation.SN.of_rel_reflTransGen {α : Type u_1} {r : α → α → Prop} {x y : α} (hx : SN r x) (h : ReflTransGen r x y) : SN r y

theorem Relation.SN.transGen {α : Type u_1} {r : α → α → Prop} {x : α} (hx : SN r x) : SN (TransGen r) x

theorem Relation.SN.of_le {α : Type u_1} {r : α → α → Prop} {x : α} {r' : α → α → Prop} (hx : SN r x) (h : r' ≤ r) : SN r' x

@[simp]

theorem Relation.SN.iff_transGen {α : Type u_1} {r : α → α → Prop} (x : α) : SN (TransGen r) x ↔ SN r x

theorem Relation.SN.iff_isEmpty_chain {α : Type u_1} {r : α → α → Prop} {x : α} : SN r x ↔ IsEmpty ↑{f : ℕ → α | f 0 = x ∧ ∀ (n : ℕ), r (f n) (f (n + 1))}

SN r x is equivalent to the more elementary definition, that there is no infinite sequence of reductions starting with x.

theorem Relation.SN.onFun_of_image {α : Type u_1} {β : Type u_2} {x : α} {r : β → β → Prop} {f : α → β} (hx : SN r (f x)) : SN (Function.onFun r f) x

theorem Relation.SN.of_normal {α : Type u_1} {r : α → α → Prop} {x : α} (hx : Normal r x) : SN r x

@[reducible, inline]

abbrev Relation.Terminating {α : Type u_1} (r : α → α → Prop) : Prop

A relation is terminating when the inverse of its transitive closure is well-founded. Note that this is also called Noetherian or strongly normalizing in the literature.

Equations

• Relation.Terminating r = WellFounded fun (a b : α) => r b a

theorem Relation.Terminating.apply {α : Type u_1} {r : α → α → Prop} (hr : Terminating r) (x : α) : SN r x

theorem Relation.Terminating.iff_forall_sn {α : Type u_1} {r : α → α → Prop} : Terminating r ↔ ∀ (x : α), SN r x

theorem Relation.Terminating.toTransGen {α : Type u_1} {r : α → α → Prop} (ht : Terminating r) : Terminating (TransGen r)

theorem Relation.Terminating.ofTransGen {α : Type u_1} {r : α → α → Prop} : Terminating (TransGen r) → Terminating r

theorem Relation.Terminating.iff_transGen {α : Type u_1} {r : α → α → Prop} : Terminating (TransGen r) ↔ Terminating r

theorem Relation.Terminating.iff_isEmpty_chain {α : Type u_1} {r : α → α → Prop} : Terminating r ↔ IsEmpty { f : ℕ → α // ∀ (n : ℕ), r (f n) (f (n + 1)) }

theorem Relation.Terminating.of_le {α : Type u_1} {r r' : α → α → Prop} (hr : Terminating r) (h : r' ≤ r) : Terminating r'

theorem Relation.Terminating.subtype_sn {α : Type u_1} (r : α → α → Prop) : Terminating fun (a b : { x : α // SN r x }) => r ↑a ↑b

theorem Relation.SN.isNormalizable {α : Type u_1} {r : α → α → Prop} {x : α} (hx : SN r x) : Normalizable r x

theorem Relation.Terminating.isNormalizing {α : Type u_1} {r : α → α → Prop} (hr : Terminating r) : Normalizing r

theorem Relation.Terminating.isConfluent_iff_all_unique_Normal {α : Type u_1} {r : α → α → Prop} (ht : Terminating r) : Confluent r ↔ ∀ (a : α), ∃! n : α, ReflTransGen r a n ∧ Normal r n

@[reducible, inline]

abbrev Relation.Convergent {α : Type u_1} (r : α → α → Prop) : Prop

A relation is convergent when it is both confluent and terminating.

Equations

• Relation.Convergent r = (Relation.Confluent r ∧ Relation.Terminating r)

theorem Relation.Convergent.isTerminating {α : Type u_1} {r : α → α → Prop} (h : Convergent r) : Terminating r

theorem Relation.Convergent.isConfluent {α : Type u_1} {r : α → α → Prop} (h : Convergent r) : Confluent r

theorem Relation.Convergent.isNormalizing {α : Type u_1} {r : α → α → Prop} (h : Convergent r) : Normalizing r

theorem Relation.Convergent.unique_Normal {α : Type u_1} {r : α → α → Prop} (h : Convergent r) (a : α) : ∃! n : α, ReflTransGen r a n ∧ Normal r n

@[reducible, inline]

abbrev Relation.LocallyConfluent {α : Type u_1} (r : α → α → Prop) : Prop

A relation is locally confluent when all reductions with a common origin are multi-joinable

Equations

• Relation.LocallyConfluent r = ∀ {a b c : α}, r a b → r a c → Relation.Join (Relation.ReflTransGen r) b c

theorem Relation.Confluent.toLocallyConfluent {α : Type u_1} {r : α → α → Prop} (h : Confluent r) : LocallyConfluent r

theorem Relation.LocallyConfluent.Terminating_toConfluent {α : Type u_1} {r : α → α → Prop} (hlc : LocallyConfluent r) (ht : Terminating r) : Confluent r

Newman's lemma: a terminating, locally confluent relation is confluent.

@[reducible, inline]

abbrev Relation.StronglyConfluent {α : Type u_1} (r : α → α → Prop) : Prop

A relation is strongly confluent when single steps are reflexive- and multi-joinable.

Equations

• Relation.StronglyConfluent r = ∀ {x y₁ y₂ : α}, r x y₁ → r x y₂ → ∃ (z : α), Relation.ReflGen r y₁ z ∧ Relation.ReflTransGen r y₂ z

def Relation.Commute {α : Type u_1} (r₁ r₂ : α → α → Prop) : Prop

Generalization of Confluent to two relations.

Equations

• Relation.Commute r₁ r₂ = ∀ {x y₁ y₂ : α}, Relation.ReflTransGen r₁ x y₁ → Relation.ReflTransGen r₂ x y₂ → ∃ (z : α), Relation.ReflTransGen r₂ y₁ z ∧ Relation.ReflTransGen r₁ y₂ z

theorem Relation.Commute.symmetric {α : Type u_1} : Symmetric Commute

theorem Relation.Commute.toConfluent {α : Type u_1} {r : α → α → Prop} : Commute r r = Confluent r

def Relation.StronglyCommute {α : Type u_1} (r₁ r₂ : α → α → Prop) : Prop

Generalization of StronglyConfluent to two relations.

Equations

• Relation.StronglyCommute r₁ r₂ = ∀ {x y₁ y₂ : α}, r₁ x y₁ → r₂ x y₂ → ∃ (z : α), Relation.ReflGen r₂ y₁ z ∧ Relation.ReflTransGen r₁ y₂ z

theorem Relation.StronglyCommute.toStronglyConfluent {α : Type u_1} {r : α → α → Prop} : StronglyCommute r r = StronglyConfluent r

def Relation.DiamondCommute {α : Type u_1} (r₁ r₂ : α → α → Prop) : Prop

Generalization of Diamond to two relations.

Equations

• Relation.DiamondCommute r₁ r₂ = ∀ {x y₁ y₂ : α}, r₁ x y₁ → r₂ x y₂ → ∃ (z : α), r₂ y₁ z ∧ r₁ y₂ z

theorem Relation.DiamondCommute.toDiamond {α : Type u_1} {r : α → α → Prop} : DiamondCommute r r = Diamond r

theorem Relation.StronglyCommute.extend {α✝ : Type u_2} {r₁ r₂ : α✝ → α✝ → Prop} {x y z : α✝} (h : StronglyCommute r₁ r₂) (xy : ReflTransGen r₁ x y) (xz : r₂ x z) : ∃ (w : α✝), ReflGen r₂ y w ∧ ReflTransGen r₁ z w

theorem Relation.StronglyCommute.toCommute {α✝ : Type u_2} {r₁ r₂ : α✝ → α✝ → Prop} (h : StronglyCommute r₁ r₂) : Commute r₁ r₂

theorem Relation.StronglyConfluent.toConfluent {α : Type u_1} {r : α → α → Prop} (h : StronglyConfluent r) : Confluent r

theorem Relation.join_inl {α : Type u_1} {r₁ r₂ : α → α → Prop} {a b : α} (r₁_ab : r₁ a b) : (r₁ ⊔ r₂) a b

theorem Relation.join_inr {α : Type u_1} {r₁ r₂ : α → α → Prop} {a b : α} (r₂_ab : r₂ a b) : (r₁ ⊔ r₂) a b

theorem Relation.join_inl_reflTransGen {α : Type u_1} {r₁ r₂ : α → α → Prop} {a b : α} (r₁_ab : ReflTransGen r₁ a b) : ReflTransGen (r₁ ⊔ r₂) a b

theorem Relation.join_inr_reflTransGen {α : Type u_1} {r₁ r₂ : α → α → Prop} {a b : α} (r₂_ab : ReflTransGen r₂ a b) : ReflTransGen (r₁ ⊔ r₂) a b

theorem Relation.Commute.join_left {α : Type u_1} {r₁ r₂ r₃ : α → α → Prop} (c₁ : Commute r₁ r₃) (c₂ : Commute r₂ r₃) : Commute (r₁ ⊔ r₂) r₃

theorem Relation.Commute.join_confluent {α : Type u_1} {r₁ r₂ : α → α → Prop} (c₁ : Confluent r₁) (c₂ : Confluent r₂) (comm : Commute r₁ r₂) : Confluent (r₁ ⊔ r₂)

theorem Relation.reflTransGen_mono_closed {α : Type u_1} {r₁ r₂ : α → α → Prop} (h₁ : Subrelation r₁ r₂) (h₂ : Subrelation r₂ (ReflTransGen r₁)) : ReflTransGen r₁ = ReflTransGen r₂

If a relation is squeezed by a relation and its multi-step closure, they are multi-step equal

theorem Relation.ReflGen.compRel_symm {α : Type u_1} {r : α → α → Prop} {a b : α} : ReflGen (SymmGen r) a b → ReflGen (SymmGen r) b a

@[simp]

theorem Relation.reflTransGen_compRel {α : Type u_1} {r : α → α → Prop} : ReflTransGen (SymmGen r) = EqvGen r

theorem Relation.RightUnique.toConfluent {α : Type u_1} {r : α → α → Prop} (hr : Relator.RightUnique r) : Confluent r

Relator.RightUnique corresponds to deterministic reductions, which are confluent, as all multi-reductions with a common origin start the same (this fact is Relation.ReflTransGen.total_of_right_unique.)

def Relation.command_Reduction_notation__ : Lean.ParserDescr

This command adds notations for relations. This should not usually be called directly, but from the reduction_sys attribute.

As an example reduction_notation foo "β" will add the notations "⭢β" and "↠β".

Note that the string used will afterwards be registered as a notation. This means that if you have also used this as a constructor name, you will need quotes to access corresponding cases, e.g. «β» in the above example.

Equations

• One or more equations did not get rendered due to their size.

def Relation.reduction_sys : Lean.ParserDescr

This attribute calls the reduction_notation command for the annotated declaration, such as in:

@[reduction_sys "ₙ", simp]
def PredReduction (a b : ℕ) : Prop := a = b + 1

Equations

• One or more equations did not get rendered due to their size.