Deterministic automaton corresponding to a right congruence.

def Cslib.RightCongruence.toDA {Symbol : Type u_1} [c : RightCongruence Symbol] : Automata.DA (Quotient c.eq) Symbol

Every right congruence gives rise to a DA whose states are the equivalence classes of the right congruence, whose start state is the empty word, and whose transition functiuon is concatenation on the right of the input symbol. Note that the transition function is well-defined only because c is a right congruence.

Equations

• Cslib.RightCongruence.toDA = { tr := fun (s : Quotient c.eq) (x : Symbol) => Quotient.lift (fun (u : List Symbol) => ⟦u ++ [x]⟧) ⋯ s, start := ⟦[]⟧ }

@[simp]

theorem Cslib.Automata.DA.congr_mtr_eq {Symbol : Type u_1} [c : RightCongruence Symbol] {xs : List Symbol} : RightCongruence.toDA.mtr RightCongruence.toDA.start xs = ⟦xs⟧

After consuming a finite word xs, c.toDA reaches the state ⟦ xs ⟧ which is the equivalence class of xs.

@[simp]

theorem Cslib.Automata.DA.FinAcc.congr_language_eq {Symbol : Type u_1} [c : RightCongruence Symbol] {a : Quotient c.eq} : Acceptor.language { toDA := RightCongruence.toDA, accept := {a} } = RightCongruence.eqvCls a

The language of c.toDA with a single accepting state s is exactly the equivalence class corresponding to s.