# mathlib3documentation

computability.regular_expressions

# Regular Expressions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.
inductive regular_expression (α : Type u) :

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).

• 0 (zero) matches nothing
• 1 (epsilon) matches only the empty string
• char a matches only the string 'a'
• star P matches any finite concatenation of strings which match P
• P + Q (plus P Q) matches anything which match P or Q
• P * Q (comp P Q) matches x ++ y if x matches P and y matches Q
Instances for regular_expression
@[protected, instance]
Equations
@[protected, instance]
def regular_expression.has_add {α : Type u_1} :
Equations
@[protected, instance]
def regular_expression.has_mul {α : Type u_1} :
Equations
@[protected, instance]
def regular_expression.has_one {α : Type u_1} :
Equations
@[protected, instance]
def regular_expression.has_zero {α : Type u_1} :
Equations
@[protected, instance]
Equations
@[simp]
theorem regular_expression.zero_def {α : Type u_1} :
@[simp]
theorem regular_expression.one_def {α : Type u_1} :
@[simp]
theorem regular_expression.plus_def {α : Type u_1} (P Q : regular_expression α) :
P.plus Q = P + Q
@[simp]
theorem regular_expression.comp_def {α : Type u_1} (P Q : regular_expression α) :
P.comp Q = P * Q
@[simp]
def regular_expression.matches {α : Type u_1} :

matches P provides a language which contains all strings that P matches

Equations
Instances for regular_expression.matches
@[simp]
theorem regular_expression.matches_zero {α : Type u_1} :
@[simp]
theorem regular_expression.matches_epsilon {α : Type u_1} :
@[simp]
theorem regular_expression.matches_char {α : Type u_1} (a : α) :
= {[a]}
@[simp]
theorem regular_expression.matches_add {α : Type u_1} (P Q : regular_expression α) :
@[simp]
theorem regular_expression.matches_mul {α : Type u_1} (P Q : regular_expression α) :
@[simp]
theorem regular_expression.matches_pow {α : Type u_1} (P : regular_expression α) (n : ) :
(P ^ n).matches = P.matches ^ n
@[simp]

match_epsilon P is true if and only if P matches the empty string

Equations
def regular_expression.deriv {α : Type u_1} [dec : decidable_eq α] :

P.deriv a matches x if P matches a :: x, the Brzozowski derivative of P with respect to a

Equations
@[simp]
theorem regular_expression.deriv_zero {α : Type u_1} [dec : decidable_eq α] (a : α) :
0.deriv a = 0
@[simp]
theorem regular_expression.deriv_one {α : Type u_1} [dec : decidable_eq α] (a : α) :
1.deriv a = 0
@[simp]
theorem regular_expression.deriv_char_self {α : Type u_1} [dec : decidable_eq α] (a : α) :
= 1
@[simp]
theorem regular_expression.deriv_char_of_ne {α : Type u_1} [dec : decidable_eq α] {a b : α} (h : a b) :
= 0
@[simp]
theorem regular_expression.deriv_add {α : Type u_1} [dec : decidable_eq α] (P Q : regular_expression α) (a : α) :
(P + Q).deriv a = P.deriv a + Q.deriv a
@[simp]
theorem regular_expression.deriv_star {α : Type u_1} [dec : decidable_eq α] (P : regular_expression α) (a : α) :
P.star.deriv a = P.deriv a * P.star
def regular_expression.rmatch {α : Type u_1} [dec : decidable_eq α] :

P.rmatch x is true if and only if P matches x. This is a computable definition equivalent to matches.

Equations
@[simp]
theorem regular_expression.zero_rmatch {α : Type u_1} [dec : decidable_eq α] (x : list α) :
theorem regular_expression.one_rmatch_iff {α : Type u_1} [dec : decidable_eq α] (x : list α) :
(1.rmatch x)
theorem regular_expression.char_rmatch_iff {α : Type u_1} [dec : decidable_eq α] (a : α) (x : list α) :
x) x = [a]
theorem regular_expression.add_rmatch_iff {α : Type u_1} [dec : decidable_eq α] (P Q : regular_expression α) (x : list α) :
((P + Q).rmatch x) (P.rmatch x) (Q.rmatch x)
theorem regular_expression.mul_rmatch_iff {α : Type u_1} [dec : decidable_eq α] (P Q : regular_expression α) (x : list α) :
((P * Q).rmatch x) (t u : list α), x = t ++ u (P.rmatch t) (Q.rmatch u)
theorem regular_expression.star_rmatch_iff {α : Type u_1} [dec : decidable_eq α] (P : regular_expression α) (x : list α) :
(P.star.rmatch x) (S : list (list α)), x = S.join (t : list α), t S (P.rmatch t)
@[simp]
theorem regular_expression.rmatch_iff_matches {α : Type u_1} [dec : decidable_eq α] (P : regular_expression α) (x : list α) :
@[protected, instance]
Equations
@[simp]
def regular_expression.map {α : Type u_1} {β : Type u_2} (f : α β) :

Map the alphabet of a regular expression.

Equations
• (R * S) =
• (R + S) =
@[protected, simp]
theorem regular_expression.map_pow {α : Type u_1} {β : Type u_2} (f : α β) (P : regular_expression α) (n : ) :
(P ^ n) =
@[simp]
theorem regular_expression.map_id {α : Type u_1} (P : regular_expression α) :
@[simp]
theorem regular_expression.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β γ) (f : α β) (P : regular_expression α) :
@[simp]
theorem regular_expression.matches_map {α : Type u_1} {β : Type u_2} (f : α β) (P : regular_expression α) :

The language of the map is the map of the language.