Regular languages in Lean

Stream: general

[Noam Atar]

Hey! I formulated regular languages and proved the Myhill-Nerode theorem in Lean. The code is right here:
https://github.com/atarnoam/lean-automata

If you want to read it and have suggestions, I'd love to hear them!
I'd also like to upload this to mathlib. Can I have permissions to do pull requests to mathlib? (My github username is atarnoam)

[Bryan Gin-ge Chen]

@Noam Atar Invite sent! https://github.com/leanprover-community/mathlib/invitations

I haven't looked at your code yet, but there's a PR in progress on regular languages by @Fox Thomson at #6225.

[Noam Atar]

Oh, interesting! I see he decided to wait for the definition of regularity. I'll wait too then

[Bryan Gin-ge Chen]

I don't know of anyone other than Fox that is working on regular automata and languages for mathlib right now (please correct me if I'm wrong!), so it would probably make sense for you two to coordinate your efforts.

[Fox Thomson]

Yes sorry I forgot to close that PR, I think it makes more sence to state regular languages in terms of regular expressions, once we have this then we can state things like M-N and the pumping lemma with it but for now I'd say to get it into mathlib without the is_regular

[Alexandre Rademaker]

Hi @Noam Atar, nice work, do you have any documentation or paper explaining details? I would be very interested in the learnings during the experiment. For instance, when I see https://github.com/atarnoam/lean-automata/blob/main/src/regular_languages.lean#L124-L140 I am puzzled if that was the only way to make it. Yes, I know https://en.wikipedia.org/wiki/Curry–Howard_correspondence, but yet, some decisions probably have reasons behind them.

[Noam Atar]

@Fox Thomson What part do you mean?

[Noam Atar]

@Alexandre Rademaker Hey, I just wrote it for fun and to learn lean. What you asked about is the standard way to build a DFA out of a regular language, as in the proof of M.N. You can read about it here: https://en.wikipedia.org/wiki/Myhill%E2%80%93Nerode_theorem

[Fox Thomson]

@Noam Atar Stating things like instance fintype_language_space_of_regular (l : language α) (M : DFA α σ) [fintype σ] (h : M.accepts = l) : fintype (space l) which should be easily refactorable when we have a flexible is_regular

[Alexandre Rademaker]

Hi @Noam Atar, what is unusual for me is the definition with a tactic mode proof.

[Noam Atar]

@Alexandre Rademaker tactic mode is just a nice way to work to get a term of some type. It doesn't care if that term is a definition or a proof!

[Kevin Buzzard]

It matters if you make a definition using a complicated tactic and it turns out to be a completely unwieldy term that you can't reason about easily

[Noam Atar]

Of course

[Bjørn Kjos-Hanssen]

It's a bit awkward how lists are (by their inductive definition) extended on the left and consequently DFAs work that way too. So a word like lean is processed by the DFA in the order n,a,e,l. Any easy way around that?

[Mario Carneiro]

@Bjørn Kjos-Hanssen you could redefine what "process" means to process the characters from the front and work your way down the list; this makes more sense to me anyway

[Mario Carneiro]

i.e. a DFA processes a :: l if s steps via a to s' and s' processes l

[Bjørn Kjos-Hanssen]

@Mario Carneiro well, it's just the opposite convention from most treatments of automata. But yeah, in a way it doesn't matter.

[Mario Carneiro]

@Bjørn Kjos-Hanssen I think you misunderstood me. I mean that "lean" should be written as [l, e, a, n] and it should be processed in the order l,e,a,n

[Mario Carneiro]

and this should be ensured by writing the "DFA processes l" definition so that elements are pulled from the front of the list instead of the back

[Matt Diamond]

since DFA.eval_from uses foldl, isn't it already pulling elements from the "front"?

[Matt Diamond]

oh I guess you mean that the input list has to be constructed via prepends... but the folding itself works left-to-right

[Bjørn Kjos-Hanssen]

@Matt Diamond Anyway there is eval_from_append_singleton which lets you work in the expected direction