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 #

source
inductive regular_expression (α : Type u) :
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
source
@[protected, instance]
def regular_expression.inhabited {α : Type u_1} :
inhabited (regular_expression α)
Equations
source
@[protected, instance]
def regular_expression.has_add {α : Type u_1} :
has_add (regular_expression α)
Equations
source
@[protected, instance]
def regular_expression.has_mul {α : Type u_1} :
has_mul (regular_expression α)
Equations
source
@[protected, instance]
def regular_expression.has_one {α : Type u_1} :
has_one (regular_expression α)
Equations
source
@[protected, instance]
def regular_expression.has_zero {α : Type u_1} :
has_zero (regular_expression α)
Equations
source
@[protected, instance]
def regular_expression.nat.has_pow {α : Type u_1} :
has_pow (regular_expression α) ℕ
Equations
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
Instances for regular_expression.matches
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 = P.matches.star
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
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
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
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
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
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.