In Coq, "wenn dann else" nicht booleschen ersten Argument erlaubt?

Question

Ich lese in ein paar Tutorials, dass if a then b else c für match a with true => b | false => c end steht. Allerdings überprüft das erste sehr merkwürdig nicht den Typ a, während letzteres natürlich sicherstellt, dass a ein boolescher ist. Zum Beispiel

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. 

Warum ist erlaubt if ... then ... else ... erstes Argument nichts anderes als ein nicht-boolean zu sein? Gibt es eine Überlastung? (Locate "if". gibt kein Ergebnis.)

Answer 1

Lassen Sie mich das Coq Referenzhandbuch zitieren, §2.2.2:

Für induktive Typen mit genau zwei Konstrukteuren und für muster passende Ausdrücke, die auf die Argumente der Konstrukteure hängen nicht Es ist möglich, eine if ... then ... else ... Notation zu verwenden. Allgemeiner C1 und C2 für einen induktiven Typ mit Konstrukteuren, wir die folgende Äquivalenz haben:

if term [dep_ret_type] then term1 else term2 

entspricht

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

Wie Sie sehen können, ist der erste Konstruktor als true behandelt Wert. Hier ein Beispiel:

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