regexp_coq 源码

Coq中的正则表达式 作为一个大学项目开始,此项目尝试在Coq中定义正则表达式并证明相关的引理和性质。 单词和语言的定义如下: Notation word := (list A). Notation language := (word -> Prop). 并被用来开发更复杂的术语。 引理 langKleenKleen :一种语言的Kleen闭包等同于该语言的Kleen闭包。 regular_regexp :正则表达式表示的语言是正则语言。 regexp_regular :任何正则语言都可以用正则表达式表示。 rmatch_correct :Brzozowski的派生词可用于检查单词