remora

Regex matcher in lean 4 via brzozowski derivatives, with correctness established against an inductive match relation

The alphabet α needs DecidableEq for the executable pieces whereas the Matches relation itself doesn't

Example

import Regex
open RegexMatcher Regex

-- a(b|c)*
def r : Regex Char :=
  .cat (.char 'a') (.star (.plus (.char 'b') (.char 'c')))

#eval match_ r "abcbc".toList   -- true
#eval match_ r "a".toList        -- true
#eval match_ r "".toList         -- false

example : Matches r ['a', 'b', 'c'] := by decide

RegexTest.lean has a handful of #guard assertions you can use as a sanity check