Right Congruence

This file contains basic definitions about left, right, and (two-sided) congruences on finite sequences.

class Language.RightCongruence (α : Type u_2) extends Setoid (List α) : Type u_2

A right congruence is an equivalence relation on finite sequences (represented by lists) that is preserved by concatenation on the right. The equivalence relation is represented by a setoid to to enable ready access to the quotient construction.

• r : List α → List α → Prop
• iseqv : Equivalence ⇑self.eq
• right_cov : CovariantClass (List α) (List α) (fun (x y : List α) => y ++ x) ⇑self.eq

@[reducible, inline]

abbrev Language.RightCongruence.eqvCls {α : Type u_1} [c : RightCongruence α] (a : Quotient c.eq) : Language α

The equivalence class (as a language) corresponding to an element of the quotient type.

Equations

• Language.RightCongruence.eqvCls a = Quotient.mk c.eq ⁻¹' {a}

class Language.LeftCongruence (α : Type u_2) extends Setoid (List α) : Type u_2

A left congruence is an equivalence relation on finite sequences (represented by lists) that is preserved by concatenation on the left. The equivalence relation is represented by a setoid to to enable ready access to the quotient construction.

• r : List α → List α → Prop
• iseqv : Equivalence ⇑self.eq
• left_cov : CovariantClass (List α) (List α) (fun (x y : List α) => x ++ y) ⇑self.eq

@[reducible, inline]

abbrev Language.LeftCongruence.eqvCls {α : Type u_1} [c : LeftCongruence α] (a : Quotient c.eq) : Language α

The equivalence class (as a language) corresponding to an element of the quotient type.

Equations

• Language.LeftCongruence.eqvCls a = Quotient.mk c.eq ⁻¹' {a}

class Language.Congruence (α : Type u_2) extends Language.LeftCongruence α, Language.RightCongruence α : Type u_2

A (two-sided) congruence is an equivalence relation on finite sequences (represented by lists) that is both a left-congruence and a right-congruence.

• r : List α → List α → Prop
• iseqv : Equivalence ⇑self.eq
• left_cov : CovariantClass (List α) (List α) (fun (x y : List α) => x ++ y) ⇑self.eq
• right_cov : CovariantClass (List α) (List α) (fun (x y : List α) => y ++ x) ⇑self.eq

@[reducible, inline]

abbrev Language.Congruence.eqvCls {α : Type u_1} [c : Congruence α] (a : Quotient c.eq) : Language α

The equivalence class (as a language) corresponding to an element of the quotient type.

Equations

• Language.Congruence.eqvCls a = Quotient.mk c.eq ⁻¹' {a}