Lean Formalization of the Lookaround Normal Form (LNF)

This repo contains the Lean formalization files for the paper "Regex Decision Procedures in Extended RE#".

Quick start

1. Install VS Code and then install the lean4 extension.
2. Open this folder in VS Code.
3. Open the Regex.lean file, which collects all modules of the formalization.

Brief file overview

Listed below is a brief description of each file of the formalization.

This folder contains the formalization of the RESharp fragment, which extends EREa with a restricted subset of lookarounds.

EREa/ – Extended Regular Expressions with Anchors

This folder contains formalization results for the EREa class of regular expressions, which includes intersection, complement and start/end anchors.

• EREa : main definitions for the class EREa.
• Metrics : metrics on regular expressions to show termination of theorems/definitions.
• Semantics : classical matching semantics, defined on locations and spans.
• Derivatives : main definitions for derivative-based matching (includes both symbolic derivatives and classical).
• Equivalence : proof of equivalence between the symbolic and classical derivative-based matching.
• Correctness : contains the equivalence theorem between the language-based semantics and the derivative-based matching.

The rest of the development is for the RESharp fragment.

• Definitions : main definitions for the class RESharp.
• TTerm: main definitions and lemmas about transition terms.
• Metrics : metrics on regular expressions to show termination of theorems/definitions.
• Semantics: classical matching semantics, defined on locations and spans.
• Conversions: contains the conversion theorems between match semantics of the three classes of regexes EREa, RESharp and RE.
• LookaroundNormalForm: contains the main correctness theorem lnf_correct for the lookaround normal form.

Dependencies

The project dependencies are listed in lakefile.toml.

• Lean v4.23.0-rc2

The Lean version manager elan and the build tool lake will automatically download these dependency versions when you run lake build.

Lean has minimal platform requirements. The instructions provided above will work on Ubuntu 24.04 (x86-64) with git and curl installed. Other platforms, including Windows and macOS, are supported by Lean as well. Please see the Lean documentation for more details on platform support.

List of claims

• RESharp.LookaroundNormalForm.lean contains the main lnf_correct theorem which corresponds to Theorem 2 from Section 3.3 of the paper.