defining computable Epsilon NFAs for regular expressions

Stream: general

[Paige Thomas]

I was wondering if anyone might have a suggestion for this. I am attempting to define the construction of nondeterministic finite automata with epsilon translations for regular expressions, and I am creating unique states for combining these automata by using the EpsilonNFA.wrapLeft and EpsilonNFA.wrapRight functions that I have defined. However, proving anything about using these functions seems to turn into a mess. For example, I can't seem to prove the properties of the NFA for the regular expression union operator. Is there maybe a trick to this that I am missing? Was this the wrong approach?

[pandaman]

I'm glad to see more people are working on Regex! I would begin with proving properties of simpler constructs like these theorems and then use them to prove the desired one.

example : state ∈ e.epsilon_closure states ↔ (Or.inl state) ∈ (e.wrapLeft σ_r).epsilon_closure (state.map Or.inl)
example : state ∈ e.eval_one states symbol ↔ (Or.inl state) ∈ (e.wrapLeft σ_r).eval_one (state.map Or.inl) symbol

[Paige Thomas]

I have made some progress with help since I posted this. Sorry. Thank you though!