Conversation
Added regex_of_dfa' to avoid equiv with Fin n
…into IsRegularIffRegex
I personally prefer to have the list of lemmas given to grind in order of application. I have not seen adding a whole by tactic into grind before. I think it might be too much golfing
RegularExpresions.lean has been saved in SummerResearch2026
ctchou
requested changes
Sep 9, 2026
ctchou
left a comment
ctchou
left a comment
Collaborator
There was a problem hiding this comment.
This is the first batch of my comments. I will have more in the future.
My general point is that by defining FLTS.execution, you can express directly the concepts in the textbook proof, rather than using bespoke recursive definitions. This allows you to leverage the large number of results about lists in mathlib.
ctchou
requested changes
Sep 9, 2026
chiyunhsu
requested review from
arademaker,
kim-em and
sorrachai
as code owners
September 9, 2026 20:51
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
We introduce
IsRegular.iff_regex, a language is regular if and only if it matches a regular expression. It is a combination of the existingIsRegular.regex, a language matching a regular expression is regular and our new direction. The new direction is proven through Kleene’s algorithm.It is the result that was anticipated in PR#846 by @ctchou.
The pull request introduces a new file,
KleeneAlgorithm.lean. In it, we proved a language defined by a DFA onFin nwith one accepting state has a matching regular expression. The algorithm applies induction on a bound which restricts which interior states that a run may pass through.Implemented collaboratively by Brooke Gill and Chi-Yun Hsu