Regular Expressions #
This file contains the formal definition for regular expressions and basic lemmas. Note these are regular expressions in terms of formal language theory. Note this is different to regex's used in computer science such as the POSIX standard.
- Show that this regular expressions and DFA/NFA's are equivalent.
attribute [pattern] has_mul.mulhas been added into this file, it could be moved.
- zero : Π (α : Type u), regular_expression α
- epsilon : Π (α : Type u), regular_expression α
- char : Π (α : Type u), α → regular_expression α
- plus : Π (α : Type u), regular_expression α → regular_expression α → regular_expression α
- comp : Π (α : Type u), regular_expression α → regular_expression α → regular_expression α
- star : Π (α : Type u), regular_expression α → regular_expression α
This is the definition of regular expressions. The names used here is to mirror the definition of a Kleene algebra (https://en.wikipedia.org/wiki/Kleene_algebra).
matches P provides a language which contains all strings that
match_epsilon P is true if and only if
P matches the empty string
P.deriv a matches
a :: x, the Brzozowski derivative of
P with respect