mathlib documentation

computability.regular_expressions

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.

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

@[protected, instance]

def regular_expression.inhabited {α : Type u} :

inhabited (regular_expression α)

Equations

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

@[protected, instance]

def regular_expression.has_add {α : Type u} :

has_add (regular_expression α)

Equations

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

@[protected, instance]

def regular_expression.has_mul {α : Type u} :

has_mul (regular_expression α)

Equations

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

@[protected, instance]

def regular_expression.has_one {α : Type u} :

has_one (regular_expression α)

Equations

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

@[protected, instance]

def regular_expression.has_zero {α : Type u} :

has_zero (regular_expression α)

Equations

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

@[simp]

theorem regular_expression.zero_def {α : Type u} :

regular_expression.zero = 0

@[simp]

theorem regular_expression.one_def {α : Type u} :

regular_expression.epsilon = 1

@[simp]

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

P.plus Q = P + Q

@[simp]

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

P.comp Q = P * Q

def regular_expression.matches {α : Type u} :

regular_expression α → language α

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

Equations

P.star.matches = P.matches.star
(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

@[simp]

theorem regular_expression.matches_zero_def {α : Type u} :

@[simp]

theorem regular_expression.matches_epsilon_def {α : Type u} :

@[simp]

theorem regular_expression.matches_add_def {α : Type u} (P Q : regular_expression α) :

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

@[simp]

theorem regular_expression.matches_mul_def {α : Type u} (P Q : regular_expression α) :

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

@[simp]

theorem regular_expression.matches_star_def {α : Type u} (P : regular_expression α) :

P.star.matches = P.matches.star

def regular_expression.match_epsilon {α : Type u} :

regular_expression α → bool

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

def regular_expression.deriv {α : Type u} [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

def regular_expression.rmatch {α : Type u} [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

@[simp]

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

0.rmatch x = ff

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

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

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

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

theorem regular_expression.add_rmatch_iff {α : Type u} [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} [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} [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)

@[simp]

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

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

@[protected, instance]

def regular_expression.matches.decidable_pred {α : Type u} [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) tt)))