当我运行以下脚本时:
Definition inv (a: Prop): Prop :=
match a with
| False => True
| True => False
end.
Run Code Online (Sandbox Code Playgroud)
我得到"错误:这个条款是多余的." 知道为什么会这样吗?
谢谢,马库斯.
这有很多错误的事情.
False
不是数据构造函数,并且由于Coq中的数据构造函数和变量名之间没有语法差异,因此它将您理解| False =>
为匹配任何内容的模式False
,并以与您编写的相同的方式为其指定名称:
Definition inv (a: Prop): Prop :=
match a with
| x => True
| y => False
end.
Run Code Online (Sandbox Code Playgroud)
这就是为什么它告诉你第二个子句是多余的(因为第一个模式匹配所有东西).
现在你应该知道的另一件事是类型Prop
没有归纳定义,因此类型的值Prop
不能与任何东西匹配:事实上它没有意义,因为它是一个开放类型,你每次定义一个新的时候都会不断扩展归纳性.
所以没有办法inv
按照你编写的方式编写函数.