在Coq中,"if then else"允许非布尔第一个参数？

Question

我读了一些if a then b else c代表的教程match a with true => b | false => c end.然而前者非常奇怪地没有检查类型a,而后者当然确保它a是一个布尔值.例如,

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 ...允许它的第一个参数不是非布尔值？是否有一些超载正在进行？(Locate "if".没有结果.)

Answer 1

让我引用Coq参考手册,§2.2.2:

对于具有两个构造函数的归纳类型和不依赖于构造函数的参数的模式匹配表达式,可以使用if ... then ... else ...符号.更一般地,用于感应型与构造函数C1和C2,我们有以下等价:

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值.这是一个例子:

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