Relations: Confluence

This module proves some properties regarding confluence that are used for both lambda calculi and combinatory logic. Some notable theorems:

• Diamond.to_confluent: the diamond property implies confluence
• LocallyConfluent.terminating_toConfluent: Newman's lemma

We prove most results first for two relations, where Confluent r becomes Commute r₁ r₂, then specialize to the classical case where r₁ = r₂.

References

• Term Rewriting and All That

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

@[deprecated Relation.Commute.to_confluent (since := "2026-09-03")]

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

Alias of Relation.Commute.to_confluent.

@[simp]

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

@[deprecated Relation.StronglyCommute.to_stronglyConfluent (since := "2026-09-03")]

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

Alias of Relation.StronglyCommute.to_stronglyConfluent.

@[simp]

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

@[deprecated Relation.DiamondCommute.to_diamond (since := "2026-09-03")]

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

Alias of Relation.DiamondCommute.to_diamond.

@[simp]

theorem Relation.SemiCommute.to_semiConfluent {α : Type u_1} {r : α → α → Prop} : SemiCommute r r = SemiConfluent r

@[simp]

theorem Relation.LocallyCommute.to_locallyConfluent {α : Type u_1} {r : α → α → Prop} : LocallyCommute r r = LocallyConfluent r

instance Relation.instSymmForallForallPropDiamondCommute {α : Type u_1} : Std.Symm DiamondCommute

instance Relation.instSymmForallForallPropLocallyCommute {α : Type u_1} : Std.Symm LocallyCommute

theorem Relation.DiamondCommute.diamond_commute_reflTransGen_right {α : Type u_1} {r₁ r₂ : α → α → Prop} (h : DiamondCommute r₁ r₂) : DiamondCommute r₁ (ReflTransGen r₂)

theorem Relation.DiamondCommute.diamond_commute_reflTransGen_left {α : Type u_1} {r₁ r₂ : α → α → Prop} (h : DiamondCommute r₁ r₂) : DiamondCommute (ReflTransGen r₁) r₂

theorem Relation.DiamondCommute.to_semiCommute {α : Type u_1} {r₁ r₂ : α → α → Prop} (h : DiamondCommute r₁ r₂) : SemiCommute r₁ r₂

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

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

@[deprecated Relation.Diamond.to_semiConfluent (since := "2026-09-12")]

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

Alias of Relation.Diamond.to_semiConfluent.

---

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

theorem Relation.Commute.isTrans_join₂_reflTransGen {α : Type u_1} {r₁ r₂ : α → α → Prop} (h : Commute r₁ r₂) : IsTrans α (Join₂ (ReflTransGen r₁) (ReflTransGen r₂))

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

theorem Relation.SemiCommute.to_commute {α : Type u_1} {r₁ r₂ : α → α → Prop} (h : SemiCommute r₁ r₂) : Commute r₁ r₂

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

@[deprecated Relation.SemiConfluent.to_confluent (since := "2026-09-03")]

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

Alias of Relation.SemiConfluent.to_confluent.

theorem Relation.commute_equivalents {α : Type u_1} {r₁ r₂ : α → α → Prop} : [SemiCommute r₁ r₂, Commute r₁ r₂, IsTrans α (Join₂ (ReflTransGen r₁) (ReflTransGen r₂)), ReflTransGen (r₁ ⊔ Function.swap r₂) ≤ Join₂ (ReflTransGen r₁) (ReflTransGen r₂), ReflTransGen (r₁ ⊔ Function.swap r₂) = Join₂ (ReflTransGen r₁) (ReflTransGen r₂)].TFAE

theorem Relation.semiCommute_iff_commute {α : Type u_1} {r₁ r₂ : α → α → Prop} : SemiCommute r₁ r₂ ↔ Commute r₁ r₂

theorem Relation.DiamondCommute.to_commute {α : Type u_1} {r₁ r₂ : α → α → Prop} (h : DiamondCommute r₁ r₂) : Commute r₁ r₂

instance Relation.instSymmForallForallPropSemiCommute {α : Type u_1} : Std.Symm SemiCommute

theorem Relation.churchRosser_iff_eqvGen_le_join_reflTransGen {α : Type u_1} {r : α → α → Prop} : ChurchRosser r ↔ EqvGen r ≤ Join (ReflTransGen r)

theorem Relation.confluent_equivalents {α : Type u_1} {r : α → α → Prop} : [ChurchRosser r, SemiConfluent r, Confluent r, IsTrans α (Join (ReflTransGen r)), EqvGen r ≤ Join (ReflTransGen r), EqvGen r = Join (ReflTransGen r)].TFAE

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

@[deprecated Relation.semiConfluent_iff_churchRosser (since := "2026-09-03")]

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

Alias of Relation.semiConfluent_iff_churchRosser.

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

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

Alias of the forward direction of Relation.confluent_iff_churchRosser.

@[deprecated Relation.confluent_iff_churchRosser (since := "2026-09-03")]

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

Alias of Relation.confluent_iff_churchRosser.

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

@[deprecated Relation.confluent_iff_semiConfluent (since := "2026-09-03")]

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

Alias of Relation.confluent_iff_semiConfluent.

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

@[deprecated Relation.Diamond.to_confluent (since := "2026-09-03")]

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

Alias of Relation.Diamond.to_confluent.

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

@[deprecated Relation.confluent_of_unique_end (since := "2026-09-03")]

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

Alias of Relation.confluent_of_unique_end.

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.

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.

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

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

@[deprecated Relation.Terminating.confluent_iff_forall_unique_normal (since := "2026-09-03")]

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

Alias of Relation.Terminating.confluent_iff_forall_unique_normal.

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

@[deprecated Relation.Convergent.to_terminating (since := "2026-09-03")]

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

Alias of Relation.Convergent.to_terminating.

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

@[deprecated Relation.Convergent.to_confluent (since := "2026-09-03")]

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

Alias of Relation.Convergent.to_confluent.

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

@[deprecated Relation.Convergent.to_normalizing (since := "2026-09-03")]

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

Alias of Relation.Convergent.to_normalizing.

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

@[deprecated Relation.Convergent.unique_normal (since := "2026-09-03")]

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

Alias of Relation.Convergent.unique_normal.

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

@[deprecated Relation.Confluent.to_locallyConfluent (since := "2026-09-03")]

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

Alias of Relation.Confluent.to_locallyConfluent.

theorem Relation.LocallyCommute.commute_of_terminating_sup {α : Type u_1} {r₁ r₂ : α → α → Prop} (hlc : LocallyCommute r₁ r₂) (ht : Terminating (r₁ ⊔ r₂)) : Commute r₁ 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.

@[deprecated Relation.LocallyConfluent.terminating_toConfluent (since := "2026-09-03")]

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

Alias of Relation.LocallyConfluent.terminating_toConfluent.

---

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

theorem Relation.StronglyCommute.extend {α : Type u_1} {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.to_commute {α : Type u_1} {r₁ r₂ : α → α → Prop} (h : StronglyCommute r₁ r₂) : Commute r₁ r₂

@[deprecated Relation.StronglyCommute.to_commute (since := "2026-09-03")]

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

Alias of Relation.StronglyCommute.to_commute.

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

@[deprecated Relation.StronglyConfluent.to_confluent (since := "2026-09-03")]

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

Alias of Relation.StronglyConfluent.to_confluent.

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.RightUnique.to_confluent {α : 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.)

@[deprecated Relation.RightUnique.to_confluent (since := "2026-09-03")]

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

Alias of Relation.RightUnique.to_confluent.

---

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.)

theorem Relation.Reducible.sup_iff {α : Type u_1} {r₁ r₂ : α → α → Prop} (x : α) : Reducible (r₁ ⊔ r₂) x ↔ Reducible r₁ x ∨ Reducible r₂ x

theorem Relation.Normal.sup_iff {α : Type u_1} {r₁ r₂ : α → α → Prop} (x : α) : Normal (r₁ ⊔ r₂) x ↔ Normal r₁ x ∧ Normal r₂ x