Documentation

Mathlib.Computability.RegularExpressions

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 #

inductive RegularExpression (α : 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
    Equations
    • RegularExpression.instInhabited = { default := RegularExpression.zero }
    Equations
    • RegularExpression.instAdd = { add := RegularExpression.plus }
    Equations
    • RegularExpression.instMul = { mul := RegularExpression.comp }
    Equations
    • RegularExpression.instOne = { one := RegularExpression.epsilon }
    Equations
    • RegularExpression.instZero = { zero := RegularExpression.zero }
    Equations
    @[simp]
    theorem RegularExpression.zero_def {α : Type u_1} :
    RegularExpression.zero = 0
    @[simp]
    theorem RegularExpression.one_def {α : Type u_1} :
    RegularExpression.epsilon = 1
    @[simp]
    theorem RegularExpression.plus_def {α : Type u_1} (P : RegularExpression α) (Q : RegularExpression α) :
    P.plus Q = P + Q
    @[simp]
    theorem RegularExpression.comp_def {α : Type u_1} (P : RegularExpression α) (Q : RegularExpression α) :
    P.comp Q = P * Q

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

    Equations
    • RegularExpression.zero.matches' = 0
    • RegularExpression.epsilon.matches' = 1
    • (RegularExpression.char a).matches' = {[a]}
    • (P.plus Q).matches' = P.matches' + Q.matches'
    • (P.comp Q).matches' = P.matches' * Q.matches'
    • P.star.matches' = KStar.kstar P.matches'
    Instances For
      @[simp]
      theorem RegularExpression.matches'_char {α : Type u_1} (a : α) :
      (RegularExpression.char a).matches' = {[a]}
      @[simp]
      theorem RegularExpression.matches'_add {α : Type u_1} (P : RegularExpression α) (Q : RegularExpression α) :
      (P + Q).matches' = P.matches' + Q.matches'
      @[simp]
      theorem RegularExpression.matches'_mul {α : Type u_1} (P : RegularExpression α) (Q : RegularExpression α) :
      (P * Q).matches' = P.matches' * Q.matches'
      @[simp]
      theorem RegularExpression.matches'_pow {α : Type u_1} (P : RegularExpression α) (n : ) :
      (P ^ n).matches' = P.matches' ^ n
      @[simp]
      theorem RegularExpression.matches'_star {α : Type u_1} (P : RegularExpression α) :
      P.star.matches' = KStar.kstar P.matches'

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

      Equations
      • RegularExpression.zero.matchEpsilon = false
      • RegularExpression.epsilon.matchEpsilon = true
      • (RegularExpression.char a).matchEpsilon = false
      • (P.plus Q).matchEpsilon = (P.matchEpsilon || Q.matchEpsilon)
      • (P.comp Q).matchEpsilon = (P.matchEpsilon && Q.matchEpsilon)
      • P.star.matchEpsilon = true
      Instances For

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

        Equations
        • RegularExpression.zero.deriv x = 0
        • RegularExpression.epsilon.deriv x = 0
        • (RegularExpression.char a₁).deriv x = if a₁ = x then 1 else 0
        • (P.plus Q).deriv x = P.deriv x + Q.deriv x
        • (P.comp Q).deriv x = if P.matchEpsilon = true then P.deriv x * Q + Q.deriv x else P.deriv x * Q
        • P.star.deriv x = P.deriv x * P.star
        Instances For
          @[simp]
          @[simp]
          theorem RegularExpression.deriv_one {α : Type u_1} [DecidableEq α] (a : α) :
          @[simp]
          theorem RegularExpression.deriv_char_self {α : Type u_1} [DecidableEq α] (a : α) :
          @[simp]
          theorem RegularExpression.deriv_char_of_ne {α : Type u_1} {a : α} {b : α} [DecidableEq α] (h : a b) :
          @[simp]
          theorem RegularExpression.deriv_add {α : Type u_1} [DecidableEq α] (P : RegularExpression α) (Q : RegularExpression α) (a : α) :
          (P + Q).deriv a = P.deriv a + Q.deriv a
          @[simp]
          theorem RegularExpression.deriv_star {α : Type u_1} [DecidableEq α] (P : RegularExpression α) (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
          • x.rmatch [] = x.matchEpsilon
          • x.rmatch (a :: as) = (x.deriv a).rmatch as
          Instances For
            theorem RegularExpression.char_rmatch_iff {α : Type u_1} [DecidableEq α] (a : α) (x : List α) :
            (RegularExpression.char a).rmatch x = true x = [a]
            theorem RegularExpression.add_rmatch_iff {α : Type u_1} [DecidableEq α] (P : RegularExpression α) (Q : RegularExpression α) (x : List α) :
            (P + Q).rmatch x = true P.rmatch x = true Q.rmatch x = true
            theorem RegularExpression.mul_rmatch_iff {α : Type u_1} [DecidableEq α] (P : RegularExpression α) (Q : RegularExpression α) (x : List α) :
            (P * Q).rmatch x = true ∃ (t : List α) (u : List α), x = t ++ u P.rmatch t = true Q.rmatch u = true
            @[irreducible]
            theorem RegularExpression.star_rmatch_iff {α : Type u_1} [DecidableEq α] (P : RegularExpression α) (x : List α) :
            P.star.rmatch x = true ∃ (S : List (List α)), x = S.join tS, t [] P.rmatch t = true
            @[simp]
            theorem RegularExpression.rmatch_iff_matches' {α : Type u_1} [DecidableEq α] (P : RegularExpression α) (x : List α) :
            P.rmatch x = true x P.matches'
            Equations
            def RegularExpression.map {α : Type u_1} {β : Type u_2} (f : αβ) :

            Map the alphabet of a regular expression.

            Equations
            Instances For
              @[simp]
              theorem RegularExpression.map_pow {α : Type u_1} {β : Type u_2} (f : αβ) (P : RegularExpression α) (n : ) :
              @[simp]
              theorem RegularExpression.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : βγ) (f : αβ) (P : RegularExpression α) :
              @[simp]
              theorem RegularExpression.matches'_map {α : Type u_1} {β : Type u_2} (f : αβ) (P : RegularExpression α) :
              (RegularExpression.map f P).matches' = (Language.map f) P.matches'

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