coq - 匹配中的冗余子句

当我运行以下脚本时:

Definition inv (a: Prop): Prop :=
match a with
| False => True
| True => False
end.

我收到“错误:此条款是多余的。”知道为什么会这样吗？

谢谢，
马库斯。

最佳答案

这有很多错误的地方。
False 不是数据构造函数，并且由于 Coq 中的数据构造函数和变量名称之间没有语法差异，因此它将您的 | False => 理解为匹配任何内容的模式，并将其命名为 False ，就像您可以编写的那样:

Definition inv (a: Prop): Prop :=
  match a with
  | x => True
  | y => False
  end.

这就是为什么它告诉您第二个子句是多余的(因为第一个模式匹配所有内容)。

现在你应该知道的另一件事是 Prop 类型不是归纳定义的，因此 Prop 类型的值不能与任何东西匹配:实际上它没有意义，因为它是一个开放类型，你每次定义时都会不断扩展一种新的归纳性质。

所以没有办法像你写的那样写一个函数 inv 。

关于coq - 匹配中的冗余子句，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/27028360/