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 인용 보자 : 정확히 두 개의 생성자와 생성자의 인자에 의존하지 않는 패턴 matchings 표현을위한 유도 유형의

을 표기법은 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.