Abstract Rewriting Systems

Here, we define the basic structure of an abstract rewriting system. We also define some derived structures, namely that of a sub-ARS and a component.

structure Thesis.ARS (α : Type u_1) (I : Type u_2) : Type (max u_1 u_2)

An Abstract Rewriting System (ARS), consisting of a set α, index type I and an indexed set of rewrite relations on α over I (ARS.rel).

• rel : I → Rel α α

  The rewrite relations for this ARS.

theorem Thesis.ARS.ext {α : Type u_1} {I : Type u_2} {x y : Thesis.ARS α I} (rel : x.rel = y.rel) : x = y

@[reducible, inline]

abbrev Thesis.ARS.union_rel {α : Type u_1} {I : Type u_2} (A : Thesis.ARS α I) : Rel α α

The union of the indexed relations of an ARS.

Equations

• A.union_rel x y = ∃ (i : I), A.rel i x y

@[reducible, inline]

abbrev Thesis.ARS.union_lt {α : Type u_1} {I : Type u_2} [LT I] (A : Thesis.ARS α I) : I → Rel α α

The union of reduction relations with an index smaller than i.

Equations

• A.union_lt i x y = ∃ j < i, A.rel j x y

theorem Thesis.ARS.union_lt_max {α : Type u_2} {I : Type u_1} [LinearOrder I] {i j : I} (A : Thesis.ARS α I) (a b : α) : A.union_lt i a b → A.union_lt (i ⊔ j) a b

If a -> b with an index smaller than i, then certainly a -> b with an index smaller than (max i j).

theorem Thesis.ARS.union_lt_trans {α : Type u_2} {I : Type u_1} [LinearOrder I] (A : Thesis.ARS α I) (a b : α) {i j : I} (hij : i ≤ j) : A.union_lt i a b → A.union_lt j a b

If i ≤ j, then A.union_lt i is a subset of A.union_lt j.

@[reducible, inline]

abbrev Thesis.ARS.conv {α : Type u_1} {I : Type u_2} (A : Thesis.ARS α I) : Rel α α

The convertability relation ≡ generated from the union of ARS relations. Note that this is denoted using = in TeReSe, which we use for equality.

Equations

• A.conv = A.union_rel≡

structure Thesis.SubARS {β : Type u_1} {I : Type u_2} (B : Thesis.ARS β I) : Type (max u_1 u_2)

SubARS B is a sub-ARS of B.

• p : β → Prop

  This SubARS contains the elements in the subtype {b // p b}.

• ars : Thesis.ARS { b : β // self.p b } I

  The underlying ARS of this SubARS.

• restrict : ∀ (i : I) (a b : { b : β // self.p b }), self.ars.rel i a b ↔ B.rel i ↑a ↑b

  SubARS.ars.rel i is the restriction of B.rel i to the subtype.

• closed : ∀ (i : I) (a b : β), self.p a ∧ B.rel i a b → self.p b

  {b // p b} is closed under B.rel i

theorem Thesis.SubARS.ext {β : Type u_1} {I : Type u_2} {B : Thesis.ARS β I} {x y : Thesis.SubARS B} (p : x.p = y.p) (ars : HEq x.ars y.ars) : x = y

@[reducible, inline]

abbrev Thesis.SubARS.Subtype {β : Type u_1} {I : Type u_2} {A : Thesis.ARS β I} (S : Thesis.SubARS A) : Type u_1

The subtype of this SubARS.

Equations

• S.Subtype = { b : β // S.p b }

@[simp]

theorem Thesis.SubARS.restrict_union {α : Type u_1} {I : Type u_2} {A : Thesis.ARS α I} (S : Thesis.SubARS A) (a b : { b : α // S.p b }) : S.ars.union_rel a b ↔ A.union_rel ↑a ↑b

The restriction property of a SubARS extends to the union of rewrite relations.

theorem Thesis.SubARS.closed_union {α : Type u_1} {I : Type u_2} {A : Thesis.ARS α I} (S : Thesis.SubARS A) (a b : α) : S.p a ∧ A.union_rel a b → S.p b

The closure property of a SubARS extends to the union of rewrite relations.

theorem Thesis.SubARS.restrict_union_lt {α : Type u_1} {I : Type u_2} {A : Thesis.ARS α I} [PartialOrder I] (S : Thesis.SubARS A) (i : I) (a b : { b : α // S.p b }) : S.ars.union_lt i a b ↔ A.union_lt i ↑a ↑b

The restriction property of a SubARS extends to the (partial) union of rewrite relations.

theorem Thesis.SubARS.closed_union_lt {α : Type u_1} {I : Type u_2} {A : Thesis.ARS α I} [PartialOrder I] (S : Thesis.SubARS A) (i : I) (a b : α) : S.p a ∧ A.union_lt i a b → S.p b

The closure property of a SubARS extends to the (partial) union of rewrite relations.

def Thesis.SubARS.generate {β : Type u_1} {I : Type u_2} (B : Thesis.ARS β I) (s : Set β) : Thesis.SubARS B

The sub-ARS generated by a subset of β

Equations

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

def Thesis.ARS.reduction_graph {β : Type u_1} {I : Type u_2} (B : Thesis.ARS β I) (b : β) : Thesis.SubARS B

The reduction graph of an element b in an ARS B is the sub-ARS containing all reducts of b.

Equations

• B.reduction_graph b = Thesis.SubARS.generate B {b}

@[simp]

theorem Thesis.ARS.reduction_graph_p {α : Type u_1} {I : Type u_2} (A : Thesis.ARS α I) {a : α} : (A.reduction_graph a).p = fun (x : α) => A.union_rel∗ a x

structure Thesis.Component {α : Type u_1} {I : Type u_2} (A : Thesis.ARS α I) extends Thesis.SubARS A : Type (max u_1 u_2)

A component of A is a sub-ARS of A containing elements that are convertible to one another.

• p : α → Prop
• ars : Thesis.ARS { b : α // self.p b } I
• restrict : ∀ (i : I) (a b : { b : α // self.p b }), self.ars.rel i a b ↔ A.rel i ↑a ↑b
• closed : ∀ (i : I) (a b : α), self.p a ∧ A.rel i a b → self.p b
• component_restrict : ∀ {a b : α}, self.p a → self.p b → A.conv a b
• component_closed : ∀ {a b : α}, self.p a → A.conv a b → self.p b
• component_nonempty : ∃ (a : α), self.p a

theorem Thesis.Component.ext {α : Type u_1} {I : Type u_2} {A : Thesis.ARS α I} {x y : Thesis.Component A} (p : x.p = y.p) (ars : HEq x.ars y.ars) : x = y

def Thesis.ARS.component {α : Type u_1} {I : Type u_2} (A : Thesis.ARS α I) (a : α) : Thesis.Component A

The component of a ∈ α w.r.t. conversion is the sub-ARS component a with set of elements { a' | a ≡ a' } and the reduction relation restricted to this convertability class.

Equations

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

def Thesis.ARS.components {α : Type u_1} {I : Type u_2} (A : Thesis.ARS α I) : Set (Thesis.Component A)

The set of components of this ARS.

Equations

• A.components = A.component '' Set.univ

theorem Thesis.component_unique {α : Type u_1} {I : Type u_2} {A : Thesis.ARS α I} {c₁ c₂ : Thesis.Component A} (a : α) : c₁.p a → c₂.p a → c₁ = c₂

A component is unique; that is to say, if any element appears in two components, the components must be the equal to one another.

theorem Thesis.ARS.component_root_mem {α : Type u_1} {I : Type u_2} {A : Thesis.ARS α I} {a : α} : (A.component a).p a

The element from which a component is derived is trivially a member of that component.

theorem Thesis.component_mem_eq {α : Type u_1} {I : Type u_2} {A : Thesis.ARS α I} {x : Thesis.Component A} {b : α} (helem : x.p b) : A.component b = x

@[simp]

theorem Thesis.ARS.component_p {α : Type u_1} {I : Type u_2} (A : Thesis.ARS α I) {a : α} : (A.component a).p = fun (x : α) => A.conv a x

@[simp]

theorem Thesis.SubARS.star_restrict {α : Type u_1} {I : Type u_2} {A : Thesis.ARS α I} (S : Thesis.SubARS A) (i : I) (a b : { b : α // S.p b }) : (S.ars.rel i)∗ a b ↔ (A.rel i)∗ ↑a ↑b

The restriction property of a sub-ARS extends to the reflexive-transitive closure of its reduction relations.

@[simp]

theorem Thesis.SubARS.star_restrict_union {α : Type u_1} {I : Type u_2} {A : Thesis.ARS α I} (S : Thesis.SubARS A) (a b : { b : α // S.p b }) : S.ars.union_rel∗ a b ↔ A.union_rel∗ ↑a ↑b

The restriction property of a sub-ARS extends to the reflexive-transitive closure of the union of its reduction relations.

@[simp]

theorem Thesis.SubARS.star_restrict_union_lt {α : Type u_1} {I : Type u_2} {A : Thesis.ARS α I} [PartialOrder I] (S : Thesis.SubARS A) (i : I) (a b : { b : α // S.p b }) : (S.ars.union_lt i)∗ a b ↔ (A.union_lt i)∗ ↑a ↑b

The restriction property of a sub-ARS extends to the reflexive-transitive closure of the (partial) union of its reduction relations.

theorem Thesis.SubARS.star_closed {α : Type u_1} {I : Type u_2} {A : Thesis.ARS α I} (S : Thesis.SubARS A) (i : I) (a b : α) : S.p a ∧ (A.rel i)∗ a b → S.p b

The closure property of a sub-ARS extends to the reflexive-transitive closure of its reduction relations.

theorem Thesis.SubARS.star_closed_union {α : Type u_1} {I : Type u_2} {A : Thesis.ARS α I} (S : Thesis.SubARS A) (a b : α) : S.p a ∧ A.union_rel∗ a b → S.p b

The closure property of a sub-ARS extends to the reflexive-transitive closure of the union of its reduction relations.

theorem Thesis.SubARS.star_closed_union_lt {α : Type u_1} {I : Type u_2} {A : Thesis.ARS α I} [PartialOrder I] (S : Thesis.SubARS A) (i : I) (a b : α) : S.p a ∧ (A.union_lt i)∗ a b → S.p b

The closure property of a sub-ARS extends to the reflexive-transitive closure of the (partial) union of its reduction relations.

theorem Thesis.SubARS.down_confluent {α : Type u_1} {I : Type u_2} (A : Thesis.ARS α I) (S : Thesis.SubARS A) (i : I) : Thesis.confluent (A.rel i) → Thesis.confluent (S.ars.rel i)

A sub-ARS of a confluent ARS is confluent.

theorem Thesis.SubARS.down_confluent_union {α : Type u_1} {I : Type u_2} (A : Thesis.ARS α I) (S : Thesis.SubARS A) : Thesis.confluent A.union_rel → Thesis.confluent S.ars.union_rel

theorem Thesis.SubARS.down_sn {α : Type u_1} {I : Type u_2} (A : Thesis.ARS α I) (S : Thesis.SubARS A) (i : I) : Thesis.strongly_normalizing (A.rel i) → Thesis.strongly_normalizing (S.ars.rel i)

A sub-ARS of a strongly normalizing ARS is strongly normalizing.

theorem Thesis.SubARS.down_wcr_union {α : Type u_1} {I : Type u_2} (A : Thesis.ARS α I) (S : Thesis.SubARS A) : Thesis.weakly_confluent A.union_rel → Thesis.weakly_confluent S.ars.union_rel

A sub-ARS of a weakly confluent ARS is weakly confluent.