匹配中的冗余子句 [英] Redundant clause in match

问题描述

当我运行以下脚本时:

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

我得到错误:此子句是多余的".知道为什么会这样吗?

I get "Error: This clause is redundant." Any idea why this happens?

谢谢，马库斯.

推荐答案

与此有关的事情很多.

False 不是数据构造函数，并且由于Coq中的数据构造函数和变量名称之间在语法上没有区别，因此它可以理解您的 |.False => 作为匹配任何内容并为其命名为 False 的模式，其方式与您编写代码的方式相同:

False is not a data constructor, and since there is no syntactic difference between data constructors and variable names in Coq, it understands your | False => as a pattern matching anything and giving it the name False, in the same way as you could have written:

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

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

This is why it tells you that the second clause is redundant (since the first pattern matches everything).

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

Now another thing you should know is that the type Prop is not inductively-defined, and therefore values of type Prop cannot be matched against anything: in fact it would not make sense, since it is an open type that you keep expanding everytime you define a new inductive property.

因此无法以编写函数的方式编写函数 inv .

So there is no way to write a function inv the way you write it.

这篇关于匹配中的冗余子句的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！