Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
chiyunhsu wants to merge 95 commits into
base: main
Choose a base branch
from
Open

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
95 commits
Select commit Hold shift + click to select a range
f569711
add regex_of_dfa, matches'_sum_map, IsRegular.regex
chiyunhsu Jul 15, 2026
1152ce8
Add language_sum
chiyunhsu Jul 15, 2026
66dddab
Merge branch 'main' into IsRegularIffRegex
chiyunhsu Jul 16, 2026
ff56e6a
Changes union to sum to preserve Language API
chiyunhsu Jul 17, 2026
9fce529
Initial progress
brooke-gill Jul 21, 2026
d9315b4
Merge branch 'main' into IsRegularIffRegex
chiyunhsu Jul 21, 2026
bdaac4a
Added regex_of_dfa' to avoid equiv with Fin n
chiyunhsu Jul 21, 2026
52f25eb
Merge pull request #3 from chiyunhsu/Chiyun_IsRegularIffRegex
chiyunhsu Jul 21, 2026
1dd27bf
Added regex_of_dfa'
brooke-gill Jul 23, 2026
f141577
Finished iff_dfa'
brooke-gill Jul 26, 2026
1234567
Finished language_sum
brooke-gill Jul 27, 2026
c1fcd5b
minimum golf
chiyunhsu Jul 28, 2026
31decc2
Trial statement relating regex_of_dfa with path
chiyunhsu Jul 28, 2026
47a454a
Added assignments for next week
chiyunhsu Jul 28, 2026
0000000
Finished aux
brooke-gill Jul 31, 2026
1aa5732
Change the assumption of regex_of_dfa to depend only on da
chiyunhsu Aug 2, 2026
3ca35a8
Some progress on main thm; add lemmas on matches
chiyunhsu Aug 3, 2026
fd72bc3
golf on main thm
chiyunhsu Aug 3, 2026
479fd18
Worked on empty_or_char_of_path_supp_empty
brooke-gill Aug 3, 2026
b513f77
Small change
chiyunhsu Aug 4, 2026
a328ab9
Merge branch 'IsRegularIffRegex' of https://github.com/chiyunhsu/csli…
chiyunhsu Aug 4, 2026
3ef773d
Comment out unnecessary assumptions
chiyunhsu Aug 4, 2026
f7a69bf
Added backwards direction
brooke-gill Aug 4, 2026
b424913
Code suggestion and some progress
chiyunhsu Aug 4, 2026
f2cd0f9
Change regex_of_da' to regex_of_flts
chiyunhsu Aug 4, 2026
172b6d4
Add new lemmas
chiyunhsu Aug 4, 2026
36527ad
Deleted unnecessary info
chiyunhsu Aug 4, 2026
62d5507
Finished set_aux
brooke-gill Aug 5, 2026
719d5d7
Major revision
chiyunhsu Aug 7, 2026
1eb056b
Update
chiyunhsu Aug 7, 2026
2c2b450
Finished mem_sum_matches'_iff
brooke-gill Aug 9, 2026
10c728f
Finished isPrefix_splitFirst
brooke-gill Aug 11, 2026
90c9ccc
Finished isSuffix_splitLast
chiyunhsu Aug 11, 2026
2d76705
Added proofs for isSuffix_splitLast, splitLastCompl, splitLast_append
brooke-gill Aug 11, 2026
c5b4be8
Added defs for splitLast_mem, splitLastCompl_mem
brooke-gill Aug 11, 2026
e4f35c8
Assign new tasks
chiyunhsu Aug 11, 2026
751d198
Proved splitFirstCompl_mem
chiyunhsu Aug 11, 2026
147606e
Proved path3
chiyunhsu Aug 17, 2026
02219ae
Finished pathSupp_append
brooke-gill Aug 17, 2026
48af610
Golfed pathSupp_append
brooke-gill Aug 17, 2026
3eb5173
Finished hole #1 of splitLast_mem
brooke-gill Aug 18, 2026
5912e0d
Finished a hole in splitLast_mem
brooke-gill Aug 18, 2026
0dec154
Finished path1 hole
brooke-gill Aug 18, 2026
9d6e458
Finished path1
brooke-gill Aug 18, 2026
2f591f9
Slight golf
chiyunhsu Aug 18, 2026
38a1fc1
Finished part of splitLast_mem
brooke-gill Aug 18, 2026
8337681
Task assigned
chiyunhsu Aug 18, 2026
27af11b
Update
chiyunhsu Aug 18, 2026
f43a101
Proved the harder part of splitLast_mem
chiyunhsu Aug 19, 2026
e88753a
Proved splitLastCompl_mem
chiyunhsu Aug 20, 2026
b550ea1
Merge branch 'main' into IsRegularIffRegex
chiyunhsu Aug 22, 2026
d32d270
Finished first hole
brooke-gill Aug 24, 2026
48c65d1
Finished second hole in splitLast_mem
brooke-gill Aug 24, 2026
458c9bf
Golfing
brooke-gill Aug 24, 2026
efe6912
Assign tasks
chiyunhsu Aug 26, 2026
d80c574
Removed leftover code
brooke-gill Aug 26, 2026
19abbc3
Finished hole 3
brooke-gill Aug 28, 2026
efd54e5
Golfed hole 3
brooke-gill Aug 28, 2026
70fe2a9
One line!!
brooke-gill Aug 28, 2026
301d35d
Finished hole 2
brooke-gill Aug 29, 2026
416bfc1
Finished IsRegular.iff_regex
brooke-gill Aug 30, 2026
0ac954c
Golf a hole
chiyunhsu Aug 31, 2026
c132ee1
golf another hole; please continue to golf it
chiyunhsu Aug 31, 2026
d5eb931
Deleting old codes
chiyunhsu Aug 31, 2026
c80620c
Golfed hole 2 to remove `have`
brooke-gill Sep 1, 2026
08514f4
Golfed hole 2
brooke-gill Sep 1, 2026
5f53ce5
Folded rw statement into simp_all
brooke-gill Sep 1, 2026
43ba335
Restructuring files until before mtr_head_eq
chiyunhsu Sep 1, 2026
7daf804
Discard use of mtr lemmas
chiyunhsu Sep 1, 2026
1ad979d
Finished splitLast section
chiyunhsu Sep 2, 2026
f371d09
Finished kstar section. Regex is WIP
chiyunhsu Sep 2, 2026
d506784
Finish first round of proofreading
chiyunhsu Sep 2, 2026
50bcb62
Minor notational changes
chiyunhsu Sep 2, 2026
25d5608
Typo
chiyunhsu Sep 2, 2026
111ea1f
Fold "rw/grind" into grind
brooke-gill Sep 3, 2026
ed34707
Fold "have"s into grind
brooke-gill Sep 3, 2026
bbe821f
Free golfs
brooke-gill Sep 3, 2026
1ca1b2f
More free golfs
brooke-gill Sep 3, 2026
8c00c42
Rewind some golf
chiyunhsu Sep 3, 2026
3dfe1fb
Added docstring and modified comments
brooke-gill Sep 8, 2026
67b35f8
Small change in comment; delete RegularExpresions.lean
chiyunhsu Sep 8, 2026
60caa7a
Switched the role of splitLast and splitLastCompl
chiyunhsu Sep 8, 2026
ff12620
Delete a commented proof
chiyunhsu Sep 8, 2026
b64f539
Added docstrings to important theorems
brooke-gill Sep 8, 2026
8d895c8
Added docstrings to slightly less important theorems
brooke-gill Sep 8, 2026
0d274b3
Fixed double newlines
brooke-gill Sep 8, 2026
d8cc3ad
Notational Cleanups
chiyunhsu Sep 8, 2026
743492f
Merge branch 'main' into IsRegularIffRegex
chiyunhsu Sep 8, 2026
b717135
Delete one import
chiyunhsu Sep 8, 2026
27204ad
Run lake exe mk_all
chiyunhsu Sep 8, 2026
1c0a2d5
Delete accidental added blank line
chiyunhsu Sep 8, 2026
5ab53cd
Update authors
chiyunhsu Sep 8, 2026
064d881
Added missing docstring
chiyunhsu Sep 8, 2026
a8c7125
Minor
chiyunhsu Sep 9, 2026
7423fca
Change BddPath to BddPathFLTS
chiyunhsu Sep 9, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Cslib.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,7 @@ public import Cslib.Computability.Distributed.FLP.ZeroConsensus
public import Cslib.Computability.Languages.Congruences.BuchiCongruence
public import Cslib.Computability.Languages.Congruences.RightCongruence
public import Cslib.Computability.Languages.ExampleEventuallyZero
public import Cslib.Computability.Languages.KleeneAlgorithm
public import Cslib.Computability.Languages.Language
public import Cslib.Computability.Languages.LanguageHom
public import Cslib.Computability.Languages.MyhillNerode
Expand Down
Loading
Loading