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.
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.)
Let me quote the Coq Reference manual:
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 constructorsC1
andC2
, we have the following equivalence:if term [dep_ret_type] then term1 else term2
is equivalent to
match term [dep_ret_type] with | C1 _ ... _ => term1 (* we cannot bind the arguments *) | C2 _ ... _ => term2 end
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.