Right Congruence

This file contains basic definitions about right congruences on finite sequences.

NOTE: Left congruences and two-sided congruences can be similarly defined. But they are left to future work because they are not needed for now.

class Cslib.RightCongruence (α : Type u_1) extends Setoid (List α) : Type u_1

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 Cslib.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

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