computability.regular_expressions

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

mathlib documentation

Regular Expressions #

TODO #