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.

source

inductive regular_expression (α : Type u) :

Type u

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

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

source

@[protected, instance]

def regular_expression.inhabited {α : Type u_1} :

inhabited (regular_expression α)

Equations

regular_expression.inhabited = {default := regular_expression.zero α}

source

@[protected, instance]

def regular_expression.has_add {α : Type u_1} :

has_add (regular_expression α)

Equations

regular_expression.has_add = {add := regular_expression.plus α}

source

@[protected, instance]

def regular_expression.has_mul {α : Type u_1} :

has_mul (regular_expression α)

Equations

regular_expression.has_mul = {mul := regular_expression.comp α}

source

@[protected, instance]

def regular_expression.has_one {α : Type u_1} :

has_one (regular_expression α)

Equations

regular_expression.has_one = {one := regular_expression.epsilon α}

source

@[protected, instance]

def regular_expression.has_zero {α : Type u_1} :

has_zero (regular_expression α)

Equations

regular_expression.has_zero = {zero := regular_expression.zero α}

source

@[protected, instance]

def regular_expression.nat.has_pow {α : Type u_1} :

has_pow (regular_expression α) ℕ

Equations

regular_expression.nat.has_pow = {pow := λ (n : regular_expression α) (r : ℕ), npow_rec r n}

source

@[simp]

theorem regular_expression.zero_def {α : Type u_1} :

regular_expression.zero = 0

source

@[simp]

theorem regular_expression.one_def {α : Type u_1} :

regular_expression.epsilon = 1

source

@[simp]

theorem regular_expression.plus_def {α : Type u_1} (P Q : regular_expression α) :

P.plus Q = P + Q

source

@[simp]

theorem regular_expression.comp_def {α : Type u_1} (P Q : regular_expression α) :

P.comp Q = P * Q

source

@[simp]

def regular_expression.matches {α : Type u_1} :

regular_expression α → language α

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

Equations

P.star.matches = has_kstar.kstar P.matches
(P * Q).matches = P.matches * Q.matches
(P + Q).matches = P.matches + Q.matches
(regular_expression.char a).matches = {[a]}
1.matches = 1
0.matches = 0

Instances for regular_expression.matches

regular_expression.matches.decidable_pred

source

@[simp]

theorem regular_expression.matches_zero {α : Type u_1} :

0.matches = 0

source

@[simp]

theorem regular_expression.matches_epsilon {α : Type u_1} :

1.matches = 1

source

@[simp]

theorem regular_expression.matches_char {α : Type u_1} (a : α) :

(regular_expression.char a).matches = {[a]}

source

@[simp]

theorem regular_expression.matches_add {α : Type u_1} (P Q : regular_expression α) :

(P + Q).matches = P.matches + Q.matches

source

@[simp]

theorem regular_expression.matches_mul {α : Type u_1} (P Q : regular_expression α) :

(P * Q).matches = P.matches * Q.matches

source

@[simp]

theorem regular_expression.matches_pow {α : Type u_1} (P : regular_expression α) (n : ℕ) :

(P ^ n).matches = P.matches ^ n

source

@[simp]

theorem regular_expression.matches_star {α : Type u_1} (P : regular_expression α) :

P.star.matches = has_kstar.kstar P.matches

source

def regular_expression.match_epsilon {α : Type u_1} :

regular_expression α → bool

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

Equations

P.star.match_epsilon = bool.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 = bool.ff
1.match_epsilon = bool.tt
0.match_epsilon = bool.ff

source

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

regular_expression α → α → regular_expression α

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

Equations

P.star.deriv a = P.deriv a * P.star
(P * Q).deriv a = ite ↥(P.match_epsilon) (P.deriv a * Q + Q.deriv a) (P.deriv a * Q)
(P + Q).deriv a = P.deriv a + Q.deriv a
(regular_expression.char a₁).deriv a₂ = ite (a₁ = a₂) 1 0
1.deriv _x = 0
0.deriv _x = 0

source

@[simp]

theorem regular_expression.deriv_zero {α : Type u_1} [dec : decidable_eq α] (a : α) :

0.deriv a = 0

source

@[simp]

theorem regular_expression.deriv_one {α : Type u_1} [dec : decidable_eq α] (a : α) :

1.deriv a = 0

source

@[simp]

theorem regular_expression.deriv_char_self {α : Type u_1} [dec : decidable_eq α] (a : α) :

(regular_expression.char a).deriv a = 1

source

@[simp]

theorem regular_expression.deriv_char_of_ne {α : Type u_1} [dec : decidable_eq α] {a b : α} (h : a ≠ b) :

(regular_expression.char a).deriv b = 0

source

@[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

source

@[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

source

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

regular_expression α → list α → bool

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

Equations

P.rmatch (a :: as) = (P.deriv a).rmatch as
P.rmatch list.nil = P.match_epsilon

source

@[simp]

theorem regular_expression.zero_rmatch {α : Type u_1} [dec : decidable_eq α] (x : list α) :

0.rmatch x = bool.ff

source

theorem regular_expression.one_rmatch_iff {α : Type u_1} [dec : decidable_eq α] (x : list α) :

↥(1.rmatch x) ↔ x = list.nil

source

theorem regular_expression.char_rmatch_iff {α : Type u_1} [dec : decidable_eq α] (a : α) (x : list α) :

↥((regular_expression.char a).rmatch x) ↔ x = [a]

source

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)

source

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)

source

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 → t ≠ list.nil ∧ ↥(P.rmatch t)

source

@[simp]

theorem regular_expression.rmatch_iff_matches {α : Type u_1} [dec : decidable_eq α] (P : regular_expression α) (x : list α) :

↥(P.rmatch x) ↔ x ∈ P.matches

source

@[protected, instance]

def regular_expression.matches.decidable_pred {α : Type u_1} [dec : decidable_eq α] (P : regular_expression α) :

decidable_pred P.matches

Equations

regular_expression.matches.decidable_pred P = id (λ (x : list α), id (_.mpr (eq.decidable (P.rmatch x) bool.tt)))

source

@[simp]

def regular_expression.map {α : Type u_1} {β : Type u_2} (f : α → β) :

regular_expression α → regular_expression β

Map the alphabet of a regular expression.

Equations

regular_expression.map f R.star = (regular_expression.map f R).star
regular_expression.map f (R * S) = regular_expression.map f R * regular_expression.map f S
regular_expression.map f (R + S) = regular_expression.map f R + regular_expression.map f S
regular_expression.map f (regular_expression.char a) = regular_expression.char (f a)
regular_expression.map f 1 = 1
regular_expression.map f 0 = 0

source

@[protected, simp]

theorem regular_expression.map_pow {α : Type u_1} {β : Type u_2} (f : α → β) (P : regular_expression α) (n : ℕ) :

regular_expression.map f (P ^ n) = regular_expression.map f P ^ n

source

@[simp]

theorem regular_expression.map_id {α : Type u_1} (P : regular_expression α) :

regular_expression.map id P = P

source

@[simp]

theorem regular_expression.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β → γ) (f : α → β) (P : regular_expression α) :

regular_expression.map g (regular_expression.map f P) = regular_expression.map (g ∘ f) P

source

@[simp]

theorem regular_expression.matches_map {α : Type u_1} {β : Type u_2} (f : α → β) (P : regular_expression α) :

(regular_expression.map f P).matches = ⇑(language.map f) P.matches

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