在Coq中，“如果是，则为其他”允许非布尔值的第一个参数？ [英] In Coq, "if then else" allows non-boolean first argument?

问题描述

我在一些教程中读到如果a然后b则c 表示 match a with true => b |假=> c end 。但是前者很奇怪地没有检查 a 的类型，而后者当然确保 a 是一个布尔值。例如，

I read in a few tutorials that if a then b else c stands for match a with true => b | false => c end. However the former very strangely does not check the type of a, while the latter of course makes sure that a is a boolean. For instance,

Coq < Check if nil then 1 else 2.
if nil then 1 else 2
     : nat
where
?A : [ |- Type] 


Coq < Check match nil with true => 1 | false => 2 end.
Toplevel input, characters 33-38:
> Check match nil with true => 1 | false => 2 end.
>                                  ^^^^^
Error: Found a constructor of inductive type bool while
a constructor of list is expected.

为什么 if ... then ... else ... 允许其第一个参数不是非布尔值？是否发生了一些超载？ （找到如果。不给出结果。）

Why is if ... then ... else ... allowing its first argument to be anything else than a non-boolean? Is there some overloading going on? (Locate "if". gives no result.)

推荐答案

让我引用 Coq参考手册：

对于正好具有两个构造函数的归纳类型以及不依赖于构造函数参数的模式匹配表达式，可以使用 if ... then ... else ... 表示法。更一般而言，对于具有构造函数 C1 和 C2 的归纳类型，我们具有以下等效项：

For inductive types with exactly two constructors and for pattern-matchings expressions which do not depend on the arguments of the constructors, it is possible to use a if ... then ... else ... notation. More generally, for an inductive type with constructors C1 and C2, we have the following equivalence:

if term [dep_ret_type] then term1 else term2 

等于

match term [dep_ret_type] with
| C1 _ ... _ => term1              (* we cannot bind the arguments *)
| C2 _ ... _ => term2
end

如您所见，第一个构造函数被视为 true 值。下面是一个示例：

As you can see, the first constructor is treated as true value. Here is an example:

Definition is_empty {A : Type} (xs : list A) : bool :=
  if xs then true else false.

这篇关于在Coq中，“如果是，则为其他”允许非布尔值的第一个参数？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！