def Thesis.locally_decreasing {α I : Type} [LT I] [WellFoundedLT I] (B : Thesis.ARS α I) : Prop

An ARS B is locally trace-decreasing (LTD) if it is indexed by a well-founded partial order (I, <) such that every peak c <-β a ->α b can be joined by reductions of the form

• b ->>_<α · ->⁼_β · ->>_{<α ∪ <β} d
• c ->>_<β · ->⁼_α · ->>_{<α ∪ <β} d

Equations

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

def Thesis.stronger_decreasing {α J : Type} [LinearOrder J] (B : Thesis.ARS α J) : Prop

Equations

• Thesis.stronger_decreasing B = ∀ (a b c : α) (i j : J), B.rel i a b ∧ B.rel j a c → ∃ (d : α), (B.union_lt (i ⊔ j))∗ b d ∧ (B.union_lt (i ⊔ j))∗ c d

theorem Thesis.stronger_decreasing_imp_locally_decreasing {α J : Type} [LinearOrder J] [WellFoundedLT J] {B : Thesis.ARS α J} : Thesis.stronger_decreasing B → Thesis.locally_decreasing B

def Thesis.DCR {α I : Type} (A : Thesis.ARS α I) : Prop

An ARS A is called Decreasing Church-Rosser (DCR) if there exists a reduction- equivalent ARS B which is locally decreasing.

Equations

• Thesis.DCR A = ∃ (I_1 : Type) (x : LT I_1) (x_1 : WellFoundedLT I_1) (B : Thesis.ARS α I_1), A.union_rel = B.union_rel ∧ Thesis.locally_decreasing B

def Thesis.DCRn {α I : Type} (n : ℕ) (A : Thesis.ARS α I) : Prop

An ARS A is DCR with n labels if there exists a reduction-equivalent ARS B which is indexed by { i | i < n } which is locally decreasing.

Equations

• Thesis.DCRn n A = ∃ (B : Thesis.ARS α (Fin n)), A.union_rel = B.union_rel ∧ Thesis.locally_decreasing B

theorem Thesis.DCRn_imp_DCR {α I : Type} {n : ℕ} {A : Thesis.ARS α I} : Thesis.DCRn n A → Thesis.DCR A

If an ARS is DCRn, it is DCR.

It is somewhat unclear to me why we need these explicit universe annotations, and Lean can't just figure it out on its own, but I suppose it doesn't matter.

theorem Thesis.locally_decreasing_components {α : Type} (n : ℕ) (B : Thesis.ARS α ↑{i : ℕ | i < n}) : (∀ (b : α), Thesis.locally_decreasing (B.component b).ars) → Thesis.locally_decreasing B

If all components of an ARS are locally decreasing, the whole ARS is locally decreasing.

def Thesis.example_ars : Thesis.ARS ℕ Unit

Equations

• Thesis.example_ars = { rel := fun (x : Unit) (x y : ℕ) => x < y }

theorem Thesis.MainRoad.exists_dcr_main_road {α I : Type} {A : Thesis.ARS α I} (C : Thesis.Component A) (hcp : Thesis.cofinality_property_conv A) : ∃ (N : ℕ∞) (f : ℕ → { b : α // C.p b }) (hseq : Thesis.reduction_seq C.ars.union_rel N f), Thesis.cofinal_reduction hseq ∧ hseq.acyclic

def Thesis.MainRoad.seq {α I : Type} {A : Thesis.ARS α I} (C : Thesis.Component A) (hcp : Thesis.cofinality_property_conv A) : Thesis.reduction_seq C.ars.union_rel ⋯.choose ⋯.choose

Equations

• ⋯ = ⋯

def Thesis.MainRoad.is_cr {α I : Type} {A : Thesis.ARS α I} (C : Thesis.Component A) (hcp : Thesis.cofinality_property_conv A) : Thesis.cofinal_reduction ⋯

Equations

• ⋯ = ⋯

noncomputable def Thesis.MainRoad.len {α I : Type} {A : Thesis.ARS α I} (C : Thesis.Component A) (hcp : Thesis.cofinality_property_conv A) : ℕ∞

Equations

• Thesis.MainRoad.len C hcp = ⋯.choose

noncomputable def Thesis.MainRoad.f {α I : Type} {A : Thesis.ARS α I} (C : Thesis.Component A) (hcp : Thesis.cofinality_property_conv A) : ℕ → { b : α // C.p b }

Equations

• Thesis.MainRoad.f C hcp = ⋯.choose

def Thesis.MainRoad.is_acyclic {α I : Type} {A : Thesis.ARS α I} (C : Thesis.Component A) (hcp : Thesis.cofinality_property_conv A) : ⋯.acyclic

Equations

• ⋯ = ⋯

def Thesis.RewriteDistance.is_reduction_seq_from {α : Type} (r : Rel α α) (a b : α) (f : ℕ → α) (N : ℕ) : Prop

Equations

• Thesis.RewriteDistance.is_reduction_seq_from r a b f N = (f 0 = a ∧ f N = b ∧ Thesis.reduction_seq r (↑N) f)

theorem Thesis.RewriteDistance.exists_red_seq_set {α : Type} {r : Rel α α} {a : α} (X : Set α) (hX : ∃ x ∈ X, r∗ a x) : ∃ (N : ℕ) (f : ℕ → α), ∃ x ∈ X, Thesis.RewriteDistance.is_reduction_seq_from r a x f N

If some element in X is a reduct of a, there must be a reduction sequence from a to some x in X.

noncomputable def Thesis.RewriteDistance.dX {α : Type} {r : Rel α α} (a : α) (X : Set α) (hX : ∃ x ∈ X, r∗ a x) : { n : ℕ // (∃ (f : ℕ → α), ∃ x ∈ X, Thesis.RewriteDistance.is_reduction_seq_from r a x f n) ∧ ∀ m < n, ¬∃ (f : ℕ → α), ∃ x ∈ X, Thesis.RewriteDistance.is_reduction_seq_from r a x f m }

Equations

• Thesis.RewriteDistance.dX a X hX = Nat.findX ⋯

theorem Thesis.RewriteDistance.dX.spec {α : Type} {r : Rel α α} {a : α} (X : Set α) (hX : ∃ x ∈ X, r∗ a x) : ∃ (f : ℕ → α), ∃ x ∈ X, Thesis.RewriteDistance.is_reduction_seq_from r a x f ↑(Thesis.RewriteDistance.dX a X hX)

theorem Thesis.RewriteDistance.dX.min {α : Type} {r : Rel α α} {a : α} (X : Set α) (hX : ∃ x ∈ X, r∗ a x) (m : ℕ) : m < ↑(Thesis.RewriteDistance.dX a X hX) → ¬∃ (f : ℕ → α), ∃ x ∈ X, Thesis.RewriteDistance.is_reduction_seq_from r a x f m

theorem Thesis.RewriteDistance.dX_step_ge {α : Type} {r : Rel α α} (a b : α) {X : Set α} (ha : ∃ x ∈ X, r∗ a x) (hb : ∃ x ∈ X, r∗ b x) (hrel : r a b) {n : ℕ} (hdX : ↑(Thesis.RewriteDistance.dX a X ha) = n + 1) : ↑(Thesis.RewriteDistance.dX b X hb) ≥ n

If a -> b and the minimal distance from a to X is n + 1, the distance from b to X must be at least n. (If not, a could go via b and arrive at the main road earlier.)

theorem Thesis.RewriteDistance.dX_step_le {α : Type} {r : Rel α α} (a x : α) {X : Set α} (hx : x ∈ X) (hX : ∃ x ∈ X, r∗ a x) {f : ℕ → α} {n : ℕ} (hrel : Thesis.RewriteDistance.is_reduction_seq_from r a x f n) : ↑(Thesis.RewriteDistance.dX a X hX) ≤ n

If there is a path of length n from a to some x ∈ X, then the distance dX(a, X) is at most n.

def Thesis.DCRComplete.SingleComponent.C' {α I : Type} {A : Thesis.ARS α I} {C : Thesis.Component A} {N : ℕ∞} {f : ℕ → C.Subtype} (main_road : Thesis.reduction_seq C.ars.union_rel N f) (hcr : Thesis.cofinal_reduction main_road) : Thesis.ARS C.Subtype ℕ

Equations

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

theorem Thesis.DCRComplete.SingleComponent.steps_along_hseq {α I : Type} {A : Thesis.ARS α I} {C : Thesis.Component A} {N : ℕ∞} {f : ℕ → C.Subtype} (main_road : Thesis.reduction_seq C.ars.union_rel N f) (hcr : Thesis.cofinal_reduction main_road) {n k : ℕ} (hk : ↑n + ↑k < N + 1) : ((Thesis.DCRComplete.SingleComponent.C' main_road hcr).rel 0)∗ (f n) (f (n + k))

If f (n + k) is within our sequence, we can take k 0-steps from f n to f (n + k).

theorem Thesis.DCRComplete.SingleComponent.C'.reduction_equivalent {α I : Type} {A : Thesis.ARS α I} {C : Thesis.Component A} {N : ℕ∞} {f : ℕ → C.Subtype} (main_road : Thesis.reduction_seq C.ars.union_rel N f) (hcr : Thesis.cofinal_reduction main_road) (b c : C.Subtype) : C.ars.union_rel b c ↔ (Thesis.DCRComplete.SingleComponent.C' main_road hcr).union_rel b c

C' is reduction-equivalent to the component of A it stems from.

theorem Thesis.DCRComplete.SingleComponent.dX_imp_red_seq {α I : Type} {A : Thesis.ARS α I} {C : Thesis.Component A} {N : ℕ∞} {f : ℕ → C.Subtype} (main_road : Thesis.reduction_seq C.ars.union_rel N f) (hcr : Thesis.cofinal_reduction main_road) (n : ℕ) (b : C.Subtype) : ↑(Thesis.RewriteDistance.dX b main_road.elems ⋯) = n → ∃ (x : { b : α // C.p b }) (f_1 : ℕ → C.Subtype), x ∈ main_road.elems ∧ f_1 0 = b ∧ f_1 n = x ∧ Thesis.reduction_seq ((Thesis.DCRComplete.SingleComponent.C' main_road hcr).union_lt (n + 1)) (↑n) f_1

One of the main parts of the proof for 14.2.30: if the distance from b to some x ∈ X is n, there is a reduction sequence from b to x using steps with indices smaller than n + 1.

theorem Thesis.DCRComplete.SingleComponent.C'.is_stronger_decreasing {α I : Type} {A : Thesis.ARS α I} {C : Thesis.Component A} {N : ℕ∞} {f : ℕ → C.Subtype} (main_road : Thesis.reduction_seq C.ars.union_rel N f) {hacyclic : main_road.acyclic} (hcr : Thesis.cofinal_reduction main_road) : Thesis.stronger_decreasing (Thesis.DCRComplete.SingleComponent.C' main_road hcr)

theorem Thesis.DCRComplete.SingleComponent.C'.is_ld {α I : Type} {A : Thesis.ARS α I} {C : Thesis.Component A} {N : ℕ∞} {f : ℕ → C.Subtype} (main_road : Thesis.reduction_seq C.ars.union_rel N f) {hacyclic : main_road.acyclic} (hcr : Thesis.cofinal_reduction main_road) : Thesis.locally_decreasing (Thesis.DCRComplete.SingleComponent.C' main_road hcr)

C' is locally decreasing.

theorem Thesis.DCRComplete.dcr_component {α I : Type} (A : Thesis.ARS α I) (hcp : Thesis.cofinality_property A) (C : Thesis.Component A) : Thesis.DCR C.ars

If A has the cofinality property, any component of A is DCR.

def Thesis.DCRComplete.dcr_total_ars {α I : Type} (A : Thesis.ARS α I) (hcp' : Thesis.cofinality_property_conv A) : Thesis.ARS α ℕ

Equations

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

def Thesis.DCRComplete.dcr_total.reduction_equivalent {α I : Type} (A : Thesis.ARS α I) (hcp' : Thesis.cofinality_property_conv A) : A.union_rel = (Thesis.DCRComplete.dcr_total_ars A hcp').union_rel

Equations

• ⋯ = ⋯

def Thesis.DCRComplete.dcr_total.is_ld {α I : Type} (A : Thesis.ARS α I) (hcp' : Thesis.cofinality_property_conv A) : Thesis.locally_decreasing (Thesis.DCRComplete.dcr_total_ars A hcp')

The dcr_total_ars is locally decreasing. This follows from the fact that each component is locally decreasing, any diverging steps z <-j x i-> y must be within one component, and thus have a decreasing diagram from z ->> d <<- y.

Equations

• ⋯ = ⋯

def Thesis.DCRComplete.dcr_of_cp {α I : Type} (A : Thesis.ARS α I) (hcp : Thesis.cofinality_property A) : Thesis.DCR A

Proposition 14.2.30: Any ARS with the cofinality property is DCR.

Equations

• ⋯ = ⋯

def Thesis.NewmanDCR.A' {α I : Type} (A : Thesis.ARS α I) : Thesis.ARS α α

Equations

• Thesis.NewmanDCR.A' A = { rel := fun (i a b : α) => i = a ∧ A.union_rel a b }

def Thesis.NewmanDCR.my_lt {α I : Type} (A : Thesis.ARS α I) : LT α

Equations

• Thesis.NewmanDCR.my_lt A = { lt := fun (a b : α) => A.union_rel⁺ b a }

def Thesis.NewmanDCR.my_wf {α I : Type} (A : Thesis.ARS α I) (hsn : Thesis.strongly_normalizing A.union_rel) : WellFoundedLT α

Equations

• ⋯ = ⋯

def Thesis.NewmanDCR.A'_locally_decreasing {α I : Type} (A : Thesis.ARS α I) (hwc : Thesis.weakly_confluent A.union_rel) (hsn : Thesis.strongly_normalizing A.union_rel) : Thesis.locally_decreasing (Thesis.NewmanDCR.A' A)

Equations

• ⋯ = ⋯

theorem Thesis.NewmanDCR.newman_dcr {α I : Type} (A : Thesis.ARS α I) (hwc : Thesis.weakly_confluent A.union_rel) (hsn : Thesis.strongly_normalizing A.union_rel) : Thesis.DCR A