Metatheory about term-rewriting systems

This is an adaptation of Mathlib.Logic.Relation for Type-valued relations (contrary to Prop)

def Reflexive {α : Type u} {r : α → α → Type u} : Type u

Property of being reflexive

Equations

• Reflexive = ((x : α) → r x x)

def Transitive {α : Type u} {r : α → α → Type u} : Type u

Property of being transitive

Equations

• Transitive = ((x y z : α) → r x y → r y z → r x z)

inductive ReflTransGen {α : Type u} (r : α → α → Type u) : α → α → Type u

Reflexive transitive closure

• refl {α : Type u} {r : α → α → Type u} {a : α} : ReflTransGen r a a
• head {α : Type u} {r : α → α → Type u} {a b c : α} : r a b → ReflTransGen r b c → ReflTransGen r a c

def ReflTransGen.trans {α : Type u} {r : α → α → Type u} {a b c : α} (hab : ReflTransGen r a b) (hbc : ReflTransGen r b c) : ReflTransGen r a c

Rt-closure is transitive

Equations

• ReflTransGen.refl.trans hbc_2 = hbc_2
• (ReflTransGen.head x tail).trans hbc = ReflTransGen.head x (tail.trans hbc)

def ReflTransGen.size {α : Type u} {r : α → α → Type u} {a b : α} (hab : ReflTransGen r a b) : Nat

Equations

• ReflTransGen.refl.size = 0
• (ReflTransGen.head a_1 tail).size = 1 + tail.size

def Join {α : Type u} (r : α → α → Type u) (a b : α) : Type u

Two elements can be joined if there exists an element to which both are related

Equations

• Join r a b = ((w : α) × r a w × r b w)

def DiamondProperty {α : Type u} (r : α → α → Type u) : Type u

Property that if diverged in 1 step, the results can be joined in 1 step

Equations

• DiamondProperty r = ((a b c : α) → r a b → r a c → Join r b c)

def Confluence {α : Type u} (r : α → α → Type u) : Type u

Property that if diverged in any number of steps, the results can be joined in any number of steps

Equations

• Confluence r = ((a b c : α) → ReflTransGen r a b → ReflTransGen r a c → Join (ReflTransGen r) b c)

def Takahashi {α : Type u} (r : α → α → Type u) : Type u

Equations

• Takahashi r = ((complete_development : α → α) × ({s u : α} → r s u → r u (complete_development s)))

def takahashi_implies_diamond {α : Type u} {r : α → α → Type u} (tak : Takahashi r) : DiamondProperty r

Equations

• takahashi_implies_diamond ⟨cd, joins⟩ a _b _c rab rac = ⟨cd a, (joins rab, joins rac)⟩

def diamond_implies_confluence' {α : Type u} {r : α → α → Type u} (h : (a b c : α) → r a b → r a c → Join r b c) (a b c : α) (hab : ReflTransGen r a b) (hac : ReflTransGen r a c) : Join (ReflTransGen r) b c

Diamond property implies Church-Rosser (in the form in which Lean recognizes termination)

Equations

• One or more equations did not get rendered due to their size.
• diamond_implies_confluence' h a a c ReflTransGen.refl hac = ⟨c, (hac, ReflTransGen.refl)⟩

def diamond_implies_confluence'.step {α : Type u} {r : α → α → Type u} {a b c : α} (h : (a b c : α) → r a b → r a c → Join r b c) (hab : r a b) (hac : ReflTransGen r a c) : (d : α) × ReflTransGen r b d × r c d

Equations

• One or more equations did not get rendered due to their size.
• diamond_implies_confluence'.step h hab ReflTransGen.refl = ⟨b, (ReflTransGen.refl, hab)⟩

def diamond_implies_confluence {α : Type u} {r : α → α → Type u} : DiamondProperty r → Confluence r

Diamond property implies Church-Rosser

Equations

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

def Equivalece {α : Type u} (r1 r2 : α → α → Type u) : Type u

Equations

• Equivalece r1 r2 = (({a b : α} → r1 a b → r2 a b) × ({a b : α} → r2 a b → r1 a b))

def WeakEquivalence {α : Type u} (r1 r2 : α → α → Type u) : Type u

Equations

• WeakEquivalence r1 r2 = (({a b : α} → ReflTransGen r1 a b → ReflTransGen r2 a b) × ({a b : α} → ReflTransGen r2 a b → ReflTransGen r1 a b))

def weak_equiv_keeps_confluence {α : Type u} {r1 r2 : α → α → Type u} (weakEquiv : WeakEquivalence r1 r2) (conf : Confluence r1) : Confluence r2

Equations

• weak_equiv_keeps_confluence (r1_to_r2, r2_to_r1) conf a b c r2ab r2ac = match conf a b c (r2_to_r1 r2ab) (r2_to_r1 r2ac) with | ⟨w, (r1bw, r1cw)⟩ => ⟨w, (r1_to_r2 r1bw, r1_to_r2 r1cw)⟩

def ZProperty {α : Type u} (r : α → α → Type u) : Type u

Equations

• ZProperty r = ((f : α → α) × ({a b : α} → r a b → ReflTransGen r b (f a) × ReflTransGen r (f a) (f b)))

def lift_f {α : Type u} {r : α → α → Type u} {a b : α} (ab : ReflTransGen r a b) (z : ZProperty r) : ReflTransGen r (z.fst a) (z.fst b)

Equations

• lift_f ReflTransGen.refl z = ReflTransGen.refl
• lift_f (ReflTransGen.head a_1 tail) z = match z.snd a_1 with | (fst, fa_fu) => let fu_fb := lift_f tail z; fa_fu.trans fu_fb

def aux {α : Type u} {r : α → α → Type u} {a b u : α} (au : r a u) (u_b : ReflTransGen r u b) (z : ZProperty r) : ReflTransGen r b (z.fst b)

Equations

• aux au ReflTransGen.refl z = match z.snd au with | (u_fa, fa_fu) => u_fa.trans fa_fu
• aux au (ReflTransGen.head a_1 tail) z = aux a_1 tail z

def step {α : Type u} {r : α → α → Type u} {a b c : α} (ab : r a b) (ac : ReflTransGen r a c) (z : ZProperty r) : ReflTransGen r b (z.fst c)

Equations

• step ab ac z = (z.snd ab).fst.trans (lift_f ac z)

theorem decr {α : Type u} {r : α → α → Type u} {a b c : α} (ab : r a b) (b_c : ReflTransGen r b c) : b_c.size < (ReflTransGen.head ab b_c).size

@[irreducible]

def z_confluence {α : Type u} {r : α → α → Type u} (z : ZProperty r) {a b c : α} (a_b : ReflTransGen r a b) (a_c : ReflTransGen r a c) : Join (ReflTransGen r) b c

Equations

• One or more equations did not get rendered due to their size.
• z_confluence z ReflTransGen.refl a_c = ⟨c, (a_c, ReflTransGen.refl)⟩
• z_confluence z (ReflTransGen.head as s_c) ReflTransGen.refl = ⟨b, (ReflTransGen.refl, ⋯ ▸ ReflTransGen.head as s_c)⟩

def z_implies_confluence {α : Type u} {r : α → α → Type u} (z : ZProperty r) : Confluence r

Equations

• z_implies_confluence z x✝² x✝¹ x✝ ab ac = z_confluence z ab ac