Relations

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)

@[reducible, inline]

abbrev Diamond {α : Sort u_1} (R : α → α → Prop) : Prop

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

Equations

• Diamond R = ∀ {A B C : α}, R A B → R A C → ∃ (D : α), R B D ∧ R C D

@[reducible, inline]

abbrev Confluence {α : Type u_1} (R : α → α → Prop) : Prop

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

Equations

• Confluence R = Diamond (Relation.ReflTransGen R)

theorem Relation.ReflTransGen.diamond_extend {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {A B C : α✝} (h : Diamond R) : ReflTransGen R A B → R A C → ∃ (D : α✝), ReflTransGen R B D ∧ ReflTransGen R C D

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

theorem Relation.ReflTransGen.diamond_confluence {α✝ : Type u_1} {R : α✝ → α✝ → Prop} (h : Diamond R) : Confluence R

The diamond property implies confluence.

def trans_of_subrelation {α : Type u_1} (s s' r : α → α → Prop) (hr : Transitive r) (h : ∀ (a b : α), s a b → r a b) (h' : ∀ (a b : α), s' a b → r a b) : Trans s s' r

Equations

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

def trans_of_subrelation_left {α : Type u_1} (s r : α → α → Prop) (hr : Transitive r) (h : ∀ (a b : α), s a b → r a b) : Trans s r r

Equations

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

def trans_of_subrelation_right {α : Type u_1} (s r : α → α → Prop) (hr : Transitive r) (h : ∀ (a b : α), s a b → r a b) : Trans r s r

Equations

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

theorem church_rosser_of_diamond {α : Type u_1} {r : α → α → Prop} (h : ∀ (a b c : α), r a b → r a c → Relation.Join r b c) : Equivalence (Relation.Join (Relation.ReflTransGen r))

This is a straightforward but useful specialisation of a more general result in Mathlib.Logic.Relation.