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.
TODO
- Show that this regular expressions and DFA/NFA's are equivalent.
attribute [pattern] has_mul.mul
has 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).
Equations
Equations
Equations
Equations
Equations
matches P
provides a language which contains all strings that P
matches
match_epsilon P
is true if and only if P
matches the empty string
Equations
- P.star.match_epsilon = tt
- (P * Q).match_epsilon = P.match_epsilon && Q.match_epsilon
- (P + Q).match_epsilon = P.match_epsilon || Q.match_epsilon
- (regular_expression.char _x).match_epsilon = ff
- 1.match_epsilon = tt
- 0.match_epsilon = ff
P.deriv a
matches x
if P
matches a :: x
, the Brzozowski derivative of P
with respect
to a
P.rmatch x
is true if and only if P
matches x
. This is a computable definition equivalent
to matches
.
Equations
- regular_expression.matches.decidable_pred P = id (λ (x : list α), id (_.mpr (eq.decidable (P.rmatch x) tt)))