在Coq中制作和比较集合

Question

我无法理解是否有可能证明两套(在这种情况下是常规语言)是相同的,因此是可以互换的.根据我的理解,即使它们不是建设性地相等,也可以是等价的.

常规语言是一组字符串,但我不知道怎么说r1 = r2这样就可以在证明中使用像对称这样的东西.

这是我的RegularLanguage声明:

Inductive RegularLanguage (A : Set) : Set :=
  | EmptyLang : RegularLanguage A
  | EmptyStr : RegularLanguage A
  | Unit : A -> RegularLanguage A
  | Union :
    RegularLanguage A
    -> RegularLanguage A
    -> RegularLanguage A
  | Concat :
    RegularLanguage A
    -> RegularLanguage A
    -> RegularLanguage A
  | KleeneStar : RegularLanguage A -> RegularLanguage A
.

即使我说类型是Set,但据我所知,这并不会创建一组字符串.我需要一些类型的功能RegularLanguage -> Set of strings吗？

感谢您的帮助.

Answer 1

关于一些Coq概念存在一些误解,我将试图澄清.

首先,在Coq中,你不应该把它Set看作我们在传统数学中所谓的"集合".相反,您应该将其视为一种类型.Coq也有Type,但为了这篇文章的目的,你可以查看两者Set,Type也可以互换.为了避免混淆,从现在起,我将使用"组"是指在传统数学组的通常概念,和"类型"指的元件Set和Type在Coq的.

那么,集合和类型之间究竟有什么区别？那么,在正常的数学中,问问自己是否有任何东西是任何给定集合的成员是有道理的.因此,如果我们要在正常数学中发展正则表达式理论,并且每个正则表达式被视为一个集合,那么提出问题是有意义的0 \in EmptyLang,因为,即使它0是一个自然数,它也可能是元素任何先验集合.作为一个不太习惯的例子,空字符串既是完整语言的成员(即包含所有字符串的成员),也是任何基本语言的Kleene闭包.

另一方面,在Coq中,语言的每个有效元素只有一种类型.例如,空字符串具有list A某些类型A,即写入的类型[] : list A.如果我们尝试[]使用"has type"语法询问是否属于某种常规语言,则会出现错误; 尝试输入例如

Check ([] : EmptyLang). 

两个集合和类型都可以看作是元素的集合,但是类型在某种意义上更具限制性:例如,一个可以采用两个集合的交集,但是没有办法采用两种类型的交集.

第二,当你写作

Inductive RegularLanguage (A : Set) : Set := (* ... *)

但这并不意味着你列出的标题下的元素定义设置,也不类型.这意味着,对于每种类型A((A : Set)部分),您要定义一个标注的新类型RegularLanguage A(RegularLanguage (A : Set) : Set部分),其元素由给定的构造函数列表自由生成.因此,我们有

EmptyLang : RegularLanguage nat

RegularLanguage nat : Set

但我们不具备

EmptyLang : Set

(再一次,您可以尝试将所有上述判断键入Coq,以查看哪些被接受,哪些不被接受).

"自由生成"特别意味着你列出的构造函数是单射的和不相交的.正如先前提到的那样,特别是情况并非如此Union l1 l2 = Union l2 l1; 事实上,你通常可以证明Union l1 l2 <> Union l2 l1.问题在于,您在Coq(您无法更改)中的归纳定义类型与您对常规语言的平等概念的相同概念之间存在不匹配.

虽然有几种解决方法,但我认为最简单的方法是使用setoid重写功能.这将涉及首先定义函数或谓词(例如,作为larsr建议的布尔函数regexp_match : RegularLanguage A -> list A -> bool)以确定常规语言何时包含某些字符串.然后,您可以在语言上定义等价关系:

Definition regexp_equiv A (l1 l2 : RegularLanguage A) : Prop :=
  forall s, regexp_match l1 s = regexp_match l2 s.

并使用setoid rewrite来重写这种等价关系.然而,有一个小警告,即你只能在与这种等价关系兼容的上下文中用等价关系重写,并且你需要明确地证明lemmas这样做.您可以在参考手册中找到更多详细信息.