# Zulip Chat Archive

## Stream: maths

### Topic: The Myhill-Nerode theorem, proved using regular expressions

#### Chris Wong (Jul 12 2020 at 12:00):

Found this interesting paper. This might give us a way to formalize regular languages without depending on automata (and graphs).

https://nms.kcl.ac.uk/christian.urban/Publications/rexp.pdf

#### Scott Morrison (Jul 12 2020 at 12:06):

The two sentences

Unfortunately, automata are not so straightforward to

formalise in theorem provers. The reason is that natural representations for automata are

graphs, matrices or functions, none of which are inductive datatypes.

sounds very strange relative to mathlib! :-)

#### Scott Morrison (Jul 12 2020 at 12:06):

And a little bit later:

Systems such as Coq permit quantification over

types and thus can state such a definition. This has been recently exploited in an elegant and

short formalisation of the Myhill-Nerode theorem in Coq by Doczkal et al. (2013), but as

said this is not available to us working in Isabelle/HOL.

suggests that this approach is not going to be a natural one for Lean.

#### Chris Wong (Jul 12 2020 at 12:31):

Yeah, I can see how we're not constrained in the same way Isabelle/HOL folks are :P

What do you mean by it being unnatural?

#### Chris Wong (Jul 12 2020 at 12:49):

(I guess since Myhill-Nerode is so easy to prove in terms of automata, any other approach will feel unnatural in comparison? :shrug: )

#### Scott Morrison (Jul 12 2020 at 12:57):

No -- I just meant that they are essentially complaining about the lack of dependent types, and point out that it was straightforward to formalise in Coq, and presumably for this problem Coq and Lean will be pretty equivalent.

#### Chris Wong (Jul 12 2020 at 13:27):

Yeah, I found this repo soon afterward (along with a bunch of papers):

https://github.com/coq-community/reglang

I guess a Lean translation of this would be quite doable, but not very interesting (in terms of research value)

#### Alex J. Best (Jul 12 2020 at 14:05):

There seem to be quite a few different implementations in coq with different aims. The connection with decision procedures for presburger arithmetic (aka `omega`

in lean) sounds really cool though to me.

Last updated: May 12 2021 at 08:14 UTC