Proofs for derivatives of regular expressions in Lean4.

This derivatives for regular expressions is used as the foundation for the katydid validation algorithm. Understanding how derivatives work for regular expressions is important before trying to understand the katydid validation algorithm.

This repo contains:

• Correctness and decidability proof for the derivative algorithm
• Correct by construction proof for the derivative algorithm
• Proofs for simplification rules
• Implementation of capturing using derivatives
• Implementation of modified capturing using derivatives
• Lean4 learnings we had while recreating algorithms and proofs in Lean.

A lot of work was done by building on our previous work in Coq and our attempt at Reproving Agda in Lean

The contributing guidelines are short and shouldn't be surprising. Please read the contributing guidelines.

Contributing to this repo requires an understanding the underlying algorithm that is the subject of the proofs in this repo:

• Derivatives of Regular Expressions explained
• Derivatives of Context-Free Grammars explained (only the simplification rules, smart constructors and memoization are important)
• Derivatives of Symbolic Automata explained

This repo also requires an understanding of proof assistants, since all the proofs in this repo are done using LeanProver:

• Knowledge of dependent types, induction and understanding the difference between a property True and a boolean true. We recommend reading The Little Typer to gain an understanding of the basics.
• Experience with an Interactive Theorem Prover, like Coq or Lean, including using tactics and Inductive Predicates. If you are unfamiliar with interactive theorem provers you can watch our talk for a taste. We recommend reading Coq in a Hurry as a quick overview and Coq Art up to Chapter 8: Inductive Predicates for a proper understanding.

Optionally the following will also be helpful, but this is not required:

• Experience with Lean4, since this project is written in Lean4. We recommend reading:
  • Lean4 Learning Resources to close the gap between Coq and Lean.
  • Lean Manual for programming in Lean and Monads.
  • Coq Lean Tactic Cheat Sheet
  • Lean Standard Libary Documentation
  • Lean4 Meta Programming Book
  • Lean Tactics File
  • Tactic List

Questions about Lean4 can be asked on proofassistants.stackexchange by tagging questions with lean and lean4 or in the Zulip Chat.

• Lean4 has exceptional instructions for installing Lean4 in VS Code.
• Remember to also add lake (the build system for lean) to your PATH. You can do this on mac by adding export PATH=~/.elan/bin/:${PATH} to your ~/.zshrc file
• Use mathlib's cache to speed up building time by running: $ lake exe cache get