feat: proof of Myhill-Nerode theorem for DFAs by akhilesh-balaji · Pull Request #479 · leanprover/cslib

akhilesh-balaji · 2026-04-08T11:39:14Z

This PR adds a proof of the Myhill-Nerode theorem. It builds on the definition of right congruence (and associated definitions and theorems) in #278. These are the main results shown (the statement of the theorem has been taken from Wikipedia and amended slightly):

(1) L regular iff. ∼_L (distinguishability by L, also called the Nerode
congruence) has a finite number of equivalence classes N.
(2) N is the number of states in the minimal DFA accepting L.
(3) The minimal DFA is unique up to unique isomorphism. That is, for any
minimal DFA acceptor, there exists exactly one isomorphism from it to the
following one:

Let each equivalence class ⟦ x ⟧ correspond to a state, and let state
transitions be a : ⟦ x ⟧ → ⟦ x a ⟧ for each a ∈ Σ.
Let the starting state be ⟦ ϵ ⟧, and the accepting states be ⟦ x ⟧ where
x ∈ L.

ctchou

Very nice work! Please take a look my comments and make appropriate changes. I'll probably have more comments after those changes are made.

ctchou · 2026-04-08T18:06:44Z

@@ -0,0 +1,252 @@
+/-


Even though Automata.DA is used in the proofs, I think this file should be put in Cslib/Computability/Languages because it contains results about regular languages in general.

Also, please run lake exe mk_all --module, so that the new file can be added to Cslib.lean.

ctchou · 2026-04-08T18:08:36Z

+* [J. E. Hopcroft, R. Motwani, J. D. Ullman,
+  *Introduction to Automata Theory, Languages, and Computation*][Hopcroft2006]
+* [T. Malkin, *COMS W3261: Computer Science Theory, Handout 3: The Myhill-Nerode Theorem
+   and Implications*][Malkin2024]


Please add this reference to references.bib. Or perhaps the Wikipedia page suffices?
https://en.wikipedia.org/wiki/Myhill–Nerode_theorem

ctchou · 2026-04-08T18:12:40Z

+public import Cslib.Computability.Automata.DA.Basic
+public import Cslib.Computability.Automata.DA.Congr
+public import Cslib.Computability.Languages.RegularLanguage
+public import Cslib.Computability.Languages.Congruences.RightCongruence
+public import Mathlib.Computability.Language
+public import Mathlib.Data.Fintype.Card
+public import Mathlib.CategoryTheory.Iso


You only need:

public import Cslib.Computability.Languages.RegularLanguage

You can find this out by running #min_imports at the end of the file.

ctchou · 2026-04-08T18:18:08Z

+namespace Automata.DA
+open Acceptor
+
+variable {α : Type} {l m : Language α}


Replace Type by Type* for more generality.

ctchou · 2026-04-08T18:25:08Z

+equivalence class of the language under the Nerode congruence. Note that this is simply the DFA
+given rise to by the underlying right congruence with only the accept states specified here as
+`{⟦ x ⟧ | x ∈ l}`. -/
+def NerodeCongruence.toFinAcc (l : Language α) : 


Remove redundant space at the end of the line. You should be able to configure your editor to do that automatically.

ctchou · 2026-04-08T22:33:52Z

+
+/-- The DFA constructed from the Nerode congruence on `l` accepts `l`. -/
+@[simp, scoped grind =]
+theorem nerodecongruence_to_finacc_acc (l : Language α) :


The name of this theorem should probably be nerodeCongruence_language_eq, to be consistent with other similar theorems. Note that you should keep the camel case in nerodeCongruence in this all subsequent theorems.

ctchou · 2026-04-08T22:35:45Z

+
+/-- The Nerode congruence is the most coarse state congruence given a language. -/
+@[simp]
+theorem statecongruence_refines_nerodecongruence {M : DA.FinAcc States α} :


Camel case: stateCongruence, nerodeCongruence.

ctchou · 2026-04-08T22:45:03Z

+theorem nerodecongruence_eqv_cls_eq_union_statecongruence_eqv_clss
+    {M : DA.FinAcc States α} (Q : Quotient (NerodeCongruence (language M)).eq) :
+    {x : List α | (⟦ x ⟧ : Quotient (NerodeCongruence (language M)).eq) = Q} =
+      ⋃ (R : Quotient (StateCongruence M).eq)
+        (_ : (⟦ Quotient.out R ⟧ : Quotient (NerodeCongruence (language M)).eq) = Q),
+        {x | (⟦ x ⟧ : Quotient (StateCongruence M).eq) = R} := by


First, I find the statement of this theorem very hard to read. Can you find a better phrasing?

Second, this is really a general fact about Setoid, isn't it? If one Setoid is a refinement of another in the sense of the previous theorem, then their equivalence classes must be related in this manner. Can you find and prove a suitably general proposition in terms of Setoid? Perhaps there is something in mathlib already? Please pose this question on Zulip if you can't find anything on mathlib.

I had originally added this theorem thinking I would use it in the proof of unique_minimal_dfa, but I ended up not using it and did not remove it. Yes, this is a general statement about Setoids, and I will prove this generally.

But either way, I should probably remove this theorem from the file as it's not used anywhere and is unrelated to the proofs of Myhill-Nerode presented here.

I can't find anything similar in mathlib, so perhaps the general version of this belongs there.

You can put general definitions and results about Setoid in a file under the directory Cslib/Foundations/Data/Setoid. We have done similar things for Set.

ctchou · 2026-04-08T23:04:09Z

+--
+
+/-- The minimal DFA accepting `l` has `|l/c|` states. -/
+def IsMinimalAutomaton (M : DA.FinAcc States α)


I would add a second argument (l : Language α) so that M.IsMinimalAutomaton l means M is a minimal automaton accepting l. This would make the statement of the theorem unique_minimal_dfa below more natural. Also, instead of the finiteness assumption on the quotient type, you assume l is regular, from which it follows that the Nerode congruence of l has finite index.

ctchou · 2026-04-08T23:07:30Z

+theorem unique_minimal_dfa (M : DA.FinAcc States α) [Fintype States]
+    [Fintype (Quotient (NerodeCongruence (language M)).eq)] (hMin : IsMinimalAutomaton M) :
+    ∃! φ : States ≃ Quotient (NerodeCongruence (language M)).eq,
+      ∀ x, φ (M.mtr M.start x) = ⟦ x ⟧ := by


See my comment about IsMinimalAutomaton above. By replacing language M by l, you also make the formal statement closer to your informal comment above. Instead of the finiteness assumption on the quotient type, you assume l is regular.

akhilesh-balaji · 2026-04-13T11:06:46Z

Thank you for the review. I have addressed all of the comments, except the following one:

It seems to me that this theorem should follow from congr_language_eq, or at least makes use of it.

congr_language_eq seems to be only applicable to DAs with a single accepting state. Perhaps using this theorem would complicate the proof rather than making it simpler.

Also, I have tried to put [...] arguments closer to the beginning, but in arguments like [Finite (Quotient ((language M).NerodeCongruence).eq)], the argument (M : ...) needs to appear at the beginning. Should I refactor it slightly to make use of the regularity of the acceptance language rather than the finiteness of the quotient?

Please let me know what you think.

chenson2018 · 2026-04-13T22:11:52Z

@ctchou Did you mean to close this? Maybe an accidental force push?

ctchou · 2026-04-13T22:15:28Z

Sorry, I did something stupid and am trying to fix it now. Please stay tuned.

chenson2018 · 2026-04-13T22:20:21Z

This is part of why I pretty much never force-push, especially to a public branch involved in a PR. @akhilesh-balaji could maybe also just (force) push again or reopen themselves if need be.

ctchou · 2026-04-13T22:35:30Z

@akhilesh-balaji I'm very sorry for messing up your PR. I did some golfing for you, which you can find in the "myhill-nerode" branch of my cslib fork:
https://github.com/ctchou/cslib/tree/myhill-nerode
To fix this PR, you can fetch the above branch and then force-push it to this PR. My branch has just one commit above what you had, which contains my golfing.

In the future, please do not open a PR using the "main" branch. This is very error-prone and contributed to the mistake I made.

ctchou · 2026-04-13T22:56:54Z

@akhilesh-balaji If you have trouble re-opening this PR, just open a new one and we can proceed from there. Please do not use "main" again when you open a new PR.

chenson2018 · 2026-04-13T23:00:19Z

@akhilesh-balaji If you have trouble re-opening this PR, just open a new one and we can proceed from there. Please do not use "main" again when you open a new PR.

Yes, I'd normally be able to fix myself, but I think it is easiest to just reopen from a branch not named main. Sorry for the trouble, some of this was from our end!

akhilesh-balaji requested review from chenson2018 and fmontesi as code owners April 8, 2026 11:39

chenson2018 assigned ctchou Apr 8, 2026

ctchou requested changes Apr 8, 2026

View reviewed changes

ctchou closed this Apr 13, 2026

ctchou force-pushed the main branch from 59e6aaa to 615b6d3 Compare April 13, 2026 22:05

akhilesh-balaji mentioned this pull request Apr 14, 2026

feat: proof of Myhill-Nerode theorem for DFAs #491

Open

Conversation

akhilesh-balaji commented Apr 8, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ctchou left a comment

Choose a reason for hiding this comment

Uh oh!

ctchou Apr 8, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ctchou Apr 8, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

akhilesh-balaji commented Apr 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

chenson2018 commented Apr 13, 2026

Uh oh!

ctchou commented Apr 13, 2026

Uh oh!

chenson2018 commented Apr 13, 2026

Uh oh!

ctchou commented Apr 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ctchou commented Apr 13, 2026

Uh oh!

chenson2018 commented Apr 13, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

akhilesh-balaji commented Apr 8, 2026 •

edited

Loading

ctchou Apr 8, 2026 •

edited

Loading

ctchou Apr 8, 2026 •

edited

Loading

akhilesh-balaji commented Apr 13, 2026 •

edited

Loading

ctchou commented Apr 13, 2026 •

edited

Loading