使用 Coq 等式定义

Question

我有一个等式定义：

Definition reglang_eq :=
  forall (A : Set)
  (r1 r2 : RegularLanguage A),
  (forall xs : List A,
    EvalInRegLang A r1 xs <-> EvalInRegLang A r2 xs)
  -> r1 = r2
.

和一个子目标：

Concat A (EmptyStr A) r = Concat A r (EmptyStr A)
(* note: Concat is a RegularLanguage constructor *)

当我尝试应用或重写 reglang_eq 时，出现错误。如果我理解正确，这应该只是因为我不知道正确的语法，但我越来越沮丧，因为我一直无法找到我能理解的文档。（尽管几个月来我一直在通过证明有关 RegularLanguages 的东西跌跌撞撞。）

感谢任何帮助，谢谢。

Answer 1

如果Concat确实是一个正则语言构造函数，你将无法证明你的目标。这里有两个问题：

当你写下reglang_eq时，你定义了一个命题，但没有给出任何证明。您要做的是仅用冒号 (:) 替换 :=，这样您就可以进入证明模式并证明您的主张。一旦你这样做并完成了你的证明，你就可以应用它了。但是如果你试图这样做，你会遇到第二个问题...
在 Coq 中，构造函数总是不相交的。这意味着你的等式唯一可以成立的方法是当 r = EmptyStr A （假设后者也是一个构造函数）。您在这里可能想要的是为常规语言定义不同的表示形式，以便连接和空语言成为定义的操作（即在逻辑内部定义的函数）。

使用 Coq 等式定义

Using Coq Equality Definition

syntax

coq