feat(Automata): Regular languages are closed under reversal. - #775

Open

Lsonic233 wants to merge 12 commits into

leanprover:mainfrom

Lsonic233:na-reverse

Commits on Aug 4, 2026

feat(Automata): reversal of NFA
Lsonic233
committed
559a00e
feat(Automata): theorems in FinAcc namespace, closure iff for regular languages
Lsonic233
committed
44c23e7

Commits on Aug 5, 2026

feat(Automata): small changes
Lsonic233
committed
7fd28b3
feat(Automata): define lts reversal and make NA inherit it
Lsonic233
committed
76b5448
fix(Automata): register LTS.Reverse in the library root
Lsonic233
committed
4ca749d

Commits on Aug 6, 2026

feat(LTS): reversal lemmas for defs in LTS/Basic.lean
Lsonic233
committed
4af0820
remove simp tag
Lsonic233
committed
c402e40
removed redundant import
Lsonic233
committed
4960db0

Commits on Aug 7, 2026

reverse involutive, shorter proof for canReach
Lsonic233
committed
5312810

Commits on Aug 8, 2026

grind proof of Execution.reverse
Lsonic233
committed
8f97c0b
improve the proof of Execution.reverse
ctchou
committed
45e5959

Commits on Aug 9, 2026

aesop to grind
Lsonic233
committed
6541abd