匹配中的冗余子句

Mar*_*cus 2 coq

当我运行以下脚本时:

Definition inv (a: Prop): Prop :=
match a with
| False => True
| True => False
end.
Run Code Online (Sandbox Code Playgroud)

我得到"错误:这个条款是多余的." 知道为什么会这样吗?

谢谢,马库斯.

Pti*_*val 6

这有很多错误的事情.

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按照你编写的方式编写函数.

  • 但是,您可以编写"定义inv(a:Prop):Prop:= a - > False",它具有相似的含义. (3认同)