About

This project contains a model for regular expressions and matching regexes to strings. It is based on the use of the Brzozowski derivative, which provides a method to convert regular expressions into DFAs by finding different expressions and deciding whether a certain expression contains the empty string.

The most important parts of the project are...

• The Regex type in in Regex/Defs.lean,
• The Matches proposition in Regex/Matches.lean.
• The function Regex.derivative in Regex/Basic.lean

Running

To run this project first install Lean 4, then run lake -q exe regex in the terminal.
It will first ask you for a regular expression, input whatever kind of regular expression you want. Then it will repeatedly ask you for strings to match this regular expression against. Keep going as you see fit, and then just use ^C to exit.

> lake exe regex
-- (ignore these warnings)

Input regex: How (have|has) your (days?|nights?) been\?
Now matching strings against the regex: how (have|has) your (day(ε|s)|night(ε|s)) been?
how has your day been?
String matches!
Derivative: ε
blah
String doesn't match :(
derivative: ∅
^C

Alternatively, you could use Lean's powerful LSP and define a regex r in Main.lean, and then do #eval r.match_full "[example string]" to see if it matches or not.

-- in Main.lean:
def r: Regex := (parseRegex "court|cat?|kit").get!

#eval r.match_full "court" -- true
#eval r.match_full "ca"    -- true
#eval r.match_full "long"  -- false
#eval r.match_full "kite"  -- false

Syntax

The syntax for regular expressions is basically what you expect. The expressions contain syntax for union |, brackets [abc], kleene star *, optional ?, and nonempty kleene star +. Parentheses also group characters together, and one can use \ before any special character to escape it. All of the following are all examples of valid regexes:

[abc]*d   -- matches "abbabacd" and "caaacbad"
eenie|meenie|miny|moe 
code?    -- matches "code" and "cod"
(kitty)+ -- matches "kitty", "kittykitty", "kittykittykitty", but not "".

I still have more to work on

This is still somewhat work in progress right now. The main hurdle I need to deal with right now is that Regex.simp is coded in a way that makes it very difficult to prove that it does not modify the regular language in any way when simplifying. Once I refactor that it will be fairly simple to fully verify that this is a correct program.

In the future this could be expanded to add a model of deterministic finite automata, and I could add some better pretty printing for regular expressions, and better error handling for parsing expressions. I could also possibly create two separate regular expression types, one for formal verification and another for a smaller memory footprint.