Reversal of nondeterministic automata

This file defines Cslib.Automata.NA.FinAcc.reverse, which reverses every transition of a nondeterministic automaton and swaps its start and accept states. Its underlying transition system is Cslib.LTS.reverse, so the transition results are inherited from Cslib/Foundations/Semantics/LTS/Reverse.lean.

The main result is FinAcc.reverse_language_eq: the language accepted by na.reverse is the Language.reverse of the language accepted by na. It follows from FinAcc.accepts_reverse, the statement that na.reverse accepts xs iff na accepts xs.reverse.

def Cslib.Automata.NA.FinAcc.reverse {State : Type u_1} {Symbol : Type u_2} (na : FinAcc State Symbol) : FinAcc State Symbol

na.reverse reverses every transition of na and swaps its start and accept states, so that it accepts exactly the reversals of the words accepted by na.

Equations

• na.reverse = { toLTS := na.reverse, start := na.accept, accept := na.start }

@[simp]

theorem Cslib.Automata.NA.FinAcc.reverse_reverse {State : Type u_1} {Symbol : Type u_2} (na : FinAcc State Symbol) : na.reverse.reverse = na

Reversing an automaton twice gives back the original automaton.

theorem Cslib.Automata.NA.FinAcc.reverse_involutive {State : Type u_1} {Symbol : Type u_2} : Function.Involutive reverse

Reversal of an automaton is an involution.

@[simp]

theorem Cslib.Automata.NA.FinAcc.reverse_start {State : Type u_1} {Symbol : Type u_2} (na : FinAcc State Symbol) : na.reverse.start = na.accept

The start states of na.reverse are the accept states of na.

@[simp]

theorem Cslib.Automata.NA.FinAcc.reverse_accept {State : Type u_1} {Symbol : Type u_2} (na : FinAcc State Symbol) : na.reverse.accept = na.start

The accept states of na.reverse are the start states of na.

@[simp]

theorem Cslib.Automata.NA.FinAcc.reverse_mTr {State : Type u_1} {Symbol : Type u_2} (na : FinAcc State Symbol) {xs : List Symbol} {s s' : State} : na.reverse.MTr s' xs s ↔ na.MTr s xs.reverse s'

The multistep transitions of na.reverse are exactly the reversed multistep transitions of na.

@[simp]

theorem Cslib.Automata.NA.FinAcc.accepts_reverse {State : Type u_1} {Symbol : Type u_2} {na : FinAcc State Symbol} {xs : List Symbol} : Acceptor.Accepts na.reverse xs ↔ Acceptor.Accepts na xs.reverse

na.reverse accepts a word iff na accepts its reversal.

@[simp]

theorem Cslib.Automata.NA.FinAcc.reverse_language_eq {State : Type u_1} {Symbol : Type u_2} (na : FinAcc State Symbol) : Acceptor.language na.reverse = (Acceptor.language na).reverse

na.reverse accepts exactly the reversals of the words accepted by na.