A formalization of DFAs, NFAs and their equivalence.
- Lib.v
Tactics definitions and some used notations.
- DFA.v
Formalization of DFAs along with proof of complement, intersection and union constructions.
- NFA.v
Formalization of NFAs along with proof of equivalence between NFAs and DFAs.
This project is developed with Coq version 8.15.2. Run make
to build to project.