Skip to content

feat(Computability/Languages): regular languages have matching regular expressions through Kleene’s Algorithm - #887

Open
chiyunhsu wants to merge 124 commits into
leanprover:mainfrom
chiyunhsu:IsRegularIffRegex
Open

feat(Computability/Languages): regular languages have matching regular expressions through Kleene’s Algorithm#887
chiyunhsu wants to merge 124 commits into
leanprover:mainfrom
chiyunhsu:IsRegularIffRegex

Conversation

@chiyunhsu

@chiyunhsu chiyunhsu commented Sep 8, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

We introduce IsRegular.iff_regex, a language is regular if and only if it matches a regular expression. It is a combination of the existing IsRegular.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 on Fin n with 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

chiyunhsu and others added 30 commits July 14, 2026 18:16
@chiyunhsu
add regex_of_dfa, matches'_sum_map, IsRegular.regex
f569711
@chiyunhsu
Add language_sum
1152ce8
@chiyunhsu
Merge branch 'main' into IsRegularIffRegex
66dddab
@chiyunhsu
Changes union to sum to preserve Language API
ff56e6a
@brooke-gill
Initial progress
9fce529
@chiyunhsu
Merge branch 'main' into IsRegularIffRegex
d9315b4
@chiyunhsu
Added regex_of_dfa' to avoid equiv with Fin n
bdaac4a
@chiyunhsu
Merge pull request #3 from chiyunhsu/Chiyun_IsRegularIffRegex
52f25eb 
Added regex_of_dfa' to avoid equiv with Fin n
@brooke-gill
Added regex_of_dfa'
1dd27bf
@brooke-gill
Finished iff_dfa'
f141577
@brooke-gill
Finished language_sum
1234567
@chiyunhsu
minimum golf
c1fcd5b
@chiyunhsu
Trial statement relating regex_of_dfa with path
31decc2
@chiyunhsu
Added assignments for next week
47a454a
@brooke-gill
Finished aux
0000000
@chiyunhsu
Change the assumption of regex_of_dfa to depend only on da
1aa5732
@chiyunhsu
Some progress on main thm; add lemmas on matches
3ca35a8
@chiyunhsu
golf on main thm
fd72bc3
@brooke-gill
Worked on empty_or_char_of_path_supp_empty
479fd18
@chiyunhsu
Small change
b513f77
@chiyunhsu
Merge branch 'IsRegularIffRegex' of https://github.com/chiyunhsu/cslib …
a328ab9 
…into IsRegularIffRegex
@chiyunhsu
Comment out unnecessary assumptions
3ef773d
@brooke-gill
Added backwards direction
f7a69bf
@chiyunhsu
Code suggestion and some progress
b424913
@chiyunhsu
Change regex_of_da' to regex_of_flts
f2cd0f9
@chiyunhsu
Add new lemmas
172b6d4
@chiyunhsu
Deleted unnecessary info
36527ad
@brooke-gill
Finished set_aux
62d5507
@chiyunhsu
Major revision
719d5d7
@chiyunhsu
Update
1eb056b
@chiyunhsu
chiyunhsu requested a review from ctchou October 13, 2026 02:31
ctchou
ctchou requested changes Oct 13, 2026
View reviewed changes

@ctchou ctchou left a comment •
edited
Loading

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The new code looks good. I just pushed a commit containing some additional golfing. Some general remarks:

  • We prefer lia over grind over omega
  • Please always put the proof on a new line, even if it is short.
  • Instead of writing (by lia : <some proposition>), write show <some proposition> by lia.
  • A lot of the proofs can probably be simplified using grind, but I didn't attempt any of that.

Comment thread Cslib/Computability/Languages/RegularLanguage.lean Outdated
@iosephusferrum iosephusferrum mentioned this pull request Oct 19, 2026
Open
@chiyunhsu
chiyunhsu requested a review from ctchou October 20, 2026 04:28
ctchou
ctchou requested changes Oct 21, 2026
View reviewed changes

@ctchou ctchou left a comment •
edited
Loading

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is probably the last batch of my comments.

Note that I pushed a commit to lowercase some identifier names.

Comment thread Cslib/Computability/Languages/KleeneAlgorithm.lean Outdated
Comment thread Cslib/Computability/Languages/KleeneAlgorithm.lean Outdated
ctchou
ctchou requested changes Oct 21, 2026
View reviewed changes
Comment thread Cslib/Computability/Languages/KleeneAlgorithm.lean Outdated
@chiyunhsu

chiyunhsu commented Oct 22, 2026

Copy link
Copy Markdown
Contributor Author

I have two last questions for the structure of the code:

  • Should the theorems in section reindex remain in KleeneAlgorithm.lean, or should they be moved to for example LTS/Basic.lean or other suitable files.
  • Should language_nfa_eq_regex_of_singleton_start_accept also have namespace NA.FinAcc? On the other hand, I think bddLang_eq_language_nfa should indeed stay in the namespace LTS.

@ctchou

ctchou commented Oct 22, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

I've moved the reindexing stuff to LTS/Bisimulation.lean, got rid of all Fintype, and did some other cleanups.

@ctchou

ctchou commented Oct 22, 2026

Copy link
Copy Markdown
Collaborator

@chiyunhsu I did some further golfing. I'm now satisfied with it. Do you have any more changes you want to do?

ctchou and others added 3 commits October 21, 2026 21:09
@ctchou
add an unsaved change
d4e1b10
@chiyunhsu
some rename
dacc736 
- AllButFirstLast is Prop, so revert allButFirstLast back to AllButFirstLast
- rename `bddLang_eq_language_nfa` as `bddLang_eq_nfa`
- syntax change for NA.FinAcc.mk in nfa’ so that it is consistent with others
@ctchou
fix the last NA.FinAcc.mk
168060e
ctchou
ctchou approved these changes Oct 22, 2026
View reviewed changes

@ctchou ctchou left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm satisfied with the code now.

@ctchou

ctchou commented Oct 22, 2026

Copy link
Copy Markdown
Collaborator

CC @fmontesi

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@ctchou ctchou ctchou approved these changes
@fmontesi fmontesi Awaiting requested review from fmontesi fmontesi is a code owner
@chenson2018 chenson2018 Awaiting requested review from chenson2018 chenson2018 is a code owner
@kim-em kim-em Awaiting requested review from kim-em
@arademaker arademaker Awaiting requested review from arademaker arademaker is a code owner
@sorrachai sorrachai Awaiting requested review from sorrachai sorrachai is a code owner
@SamuelSchlesinger SamuelSchlesinger Awaiting requested review from SamuelSchlesinger SamuelSchlesinger is a code owner
@crei crei Awaiting requested review from crei crei is a code owner

At least 1 approving review is required to merge this pull request.

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@chiyunhsu @ctchou @brooke-gill