syntax - 使用 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 时，出现错误。如果我理解正确的话，这应该只是因为我不知道正确的语法，但我越来越沮丧，因为我无法找到我可以理解的文档。 (尽管我已经花了好几个月的时间来证明有关常规语言的东西。)

感谢任何帮助，谢谢。

Answer 1

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

1. 当你写下reglang_eq时，你定义了一个命题，但没有给出任何证明。您想要做的是将 := 替换为冒号 (:)，这样您就可以进入证明模式并证明您的主张。一旦你这样做并完成了证明，你就可以应用它。但如果你尝试这样做，你就会遇到第二个问题......

2. 在 Coq 中，构造函数总是不相交的。这意味着您的方程成立的唯一方法是当 r = EmptyStr A 时(假设后者也是构造函数)。您在这里可能想要的是为常规语言定义不同的表示，以便串联和空语言成为定义的操作(即逻辑内部定义的函数)。