The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 03.06.2013 18:25, schrieb Kevin Sullivan:
> Hi folks, sorry for a newbie question. I've started playing around 
> with types as values, but I'm not sure how to do simple computations 
> with such values. One such computation would be comparison for 
> equality. I'm obviously missing some basic knowlege. Here's a simple 
> but broken program that should make my intent clear. What do I need to 
> go read to make this work? Thanks!
>
> Definition teq (t1 t2: Set) : bool :=
>   if (t1 = t2) then true else false.
>
> Kevin

Hi Kevin,
since you consider yourself a beginner (considering Coq) I'd like to 
mention the following:

Recall that "if (a : A) then x else y" is basically equal to "match a 
with first constructor of A  => x | second constructor of A => y end"; 
there is no magic in your if that could decide anything about the "truth 
value" or something like that of the proposition (t1 = t2). Prop is not 
inductive and doesn't have constructors in this sense, and especially 
not two - so it isn't very surprising that the if doesn't work.

Recall that if you assume classical logic, you get something like: (xm : 
(forall p : Prop, p \/ ~p)). Note that (xm (t1 = t2)) has type (t1 = t2 
\/ t1 <> t2).  Recall that (t1 = t2 \/ t1 <> t2) is an inductive type 
with two constructors. Therefore, (if xm (t1 = t2) then true else false) 
would work the way you imagine.

I believe that there was a level-mismatch between what you plugged into 
the if (a proposition) and what should be in the if (something that 
decides whether that proposition holds or not). I also fell for this 
when I first came into contact with Coq and I think it stems from the 
syntax "if a == b then ..." common in other programming languages.
Note that if you would give the type of the expression (a == b) in Coq, 
it would not be Prop; it could be, among other things, bool or {x=y} \/ 
{x<>y} (and both of these types have two constructors).

To sum it up, the proposition (a=b) and the decision procedure "a == b" 
are very different and live on different levels. Recall that you can 
give a procedure like "==" for elements of nat and many other types. "if 
1 = 3 then x else y" is not meaningful in Coq, while if 1 == 3 then x 
else y is (when x == y is a notation for, e.g., eq_nat_dec x y).

Kind regards and hoping that this helped, Jonas