mathlib3 documentation

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 #

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

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 : α) :
@[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

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 : α) :
@[simp]
theorem regular_expression.deriv_char_of_ne {α : Type u_1} [dec : decidable_eq α] {a b : α} (h : a b) :
@[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

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 α) :
theorem regular_expression.char_rmatch_iff {α : Type u_1} [dec : decidable_eq α] (a : α) (x : list α) :
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 t list.nil (P.rmatch t)
@[simp]
theorem regular_expression.rmatch_iff_matches {α : Type u_1} [dec : decidable_eq α] (P : regular_expression α) (x : list α) :
@[protected, simp]
theorem regular_expression.map_pow {α : Type u_1} {β : Type u_2} (f : α β) (P : regular_expression α) (n : ) :
@[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.