Formalizzazione dei Linguaggi Regolari in Agda

We use the proof assistant Agda to prove properties on Regular Expressions and Finite State Automata. Initially, we prove the correctness of two ways to decide whether or not a string belongs to the language of a regular expression. The first one uses Brzozowski's Derivatives and the second one transforms regular expressions into Non-deterministic Finite State Automata. Finally, we show the pumping lemma for regular languages and conclude with the non-regularity of an example language.