小编use*_*685的帖子

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

常规语言是一组字符串,但我不知道怎么说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吗？

感谢您的帮助.