feat(computability): prove equivalence of NFAs and regular expressions #14250
Conversation
This adds a working proof that NFAs are equivalent to regular expressions. This is *not* meant to be committed into the actual library yet, rather just so people can see my work so far. I will soon fix style things and add comments on parts that I'm unsure about.
Add documentation, TODOs, and questions about my proof. Still a WIP.
Use standard brace placement in tactic mode. Replace intermediate simp with rw and simp only.
Fix all style issues
RussellEmerine
added
the
awaiting-review
src/computability/GNFA.lean
Outdated
| Given an equivalence between `σ` and `τ`, convert an NFA with state type `σ` into the corresponding | ||
| NFA with state type `τ`. | ||
|
|
||
| TODO: possibly move to computability/NFA |
There was a problem hiding this comment.
Since this is your first PR and it's rather large; I recommend you split this definition and the lemma below into a second PR (adding it to the NFA file), and then come back to this one once that's merged.
| * probably move this into computability/regular_expression | ||
| * maybe change the order to `pow n * r`? | ||
| -/ | ||
| def pow (r : regular_expression α) : ℕ → regular_expression α |
There was a problem hiding this comment.
Is monoid (regular_expression a) true?
There was a problem hiding this comment.
Ah no, because regexes have no useful meaning of equality.
There was a problem hiding this comment.
I've moved this definition to #14261 and added a lemma.
eric-wieser
added
awaiting-author
| end | ||
|
|
||
| theorem star_iff_pow {r : regular_expression α} {x} : | ||
| x ∈ r.star.matches ↔ (∃ (n : ℕ), x ∈ (r ^ n).matches) := |
There was a problem hiding this comment.
I think this follows trivially from language.star_eq_supr_pow
There was a problem hiding this comment.
Thank you for all your feedback, Eric. I will be making changes and keeping an eye on #14261 .
Merge updates to master, including a regular expression power operator that will be used in the proof of correctness for the star case of regular expression to NFA
Refactored GNFA proofs to use fintype.induction_empty_option instead of fin.
semorrison
added
the
too-late
Provide a way to convert NFAs to regular expressions and vice versa, and prove that the conversions accept the same language.
TODO: statement of some theorems, style, adding @[simp] annotations appropriately, conversions between DFAs and regular expressions