The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Short answer:

If you don't want to use sumbool, you can.  You just have to assume that 
there
exists a function string_eq_bool with the type:

string -> string -> bool

and a theorem that says:

string_eq_bool_reflect : string_eq_bool x y <-> x = y

Then if-then-else constructions must have the following shape:

if string_eq_bool x y then ... else ...

When you do proofs about such a construction, you need to use the 
case_eq tactic.

for instance if you have  a goal of the form

====
P (if string_eq_bool (f a) (g b) then A else B)

entering the tactic

case_eq (string_eq_bool (f a) (g b)

leads you to two goals:

====
string_eq_bool (f a) (g b) = true -> P A

and

====
string_eq_bool (f a) (g b) = false -> P B

and it requires a little more work with string_eq_bool_reflect to get to 
equalities.

But in any case, you cannot use "if E then...else..." if E is an element 
of Prop, because
Prop is not a datatype (rather, it is a type of types).

Long answer:

In general, in our mind, we think that every proposition is either true 
or false.  However,
in Coq, the tradition has long been to work in a slightly different 
frame of mind
(what is called a logic), where you don't allow yourself to assume that 
a proposition
is either True or False, unless you have proved otherwise.  For some 
types and some
elements A and B in on of those types, you can still prove "A=B" when you
have good reasons to assert that they are equal (for instance, if you know
that A and B come from the same initial computation through different 
paths, or
they were constructed in the same fashion, etc...) or you can prove 
"A<>B" when you
can prove that in some context they can really be distinguished, but in 
general
given an A and a B, you may have no certain way to assert whether they 
are the same
or different.  In this case, the sentence "if A=B then ... else ..." 
would make no sense.

In Coq, you want to avoid having sentences that make no sense.

So "A=B" makes sense, it means "A" and "B" are the same, there is no context
that can distinguish between them.  The sentence "C<>D" makes sense, it 
means
we can find a context where these two values provoke a different 
behavior.   These
sentences can make sense, but in general, you cannot write a program 
that says

if A = B ....

because in general, you have no way (based on a function that will 
terminate) to
assert that A=B or A <> B holds.

This is to say, that in this point of view the type "A = B" is really 
different from
a boolean value.

Now, there are types, like nat, Z, or string, where you can provide a 
function of
type nat -> nat -> bool so that this function returns "true" exactly 
when the two arguments
are equal.  But given a function f of type nat -> nat -> bool how do you 
know what
it computes?

In Coq, you also find dependent types.  With dependent types, you
can enforce the discipline that some function can be called only when some
property holds.  For instance we could write a function that can be 
called with
two numbers x and y only when x <> y.  The type of this function would be:

g : forall x y, x <> y -> T

Such a function actually takes three arguments: x, y, and a proof that x 
<> y.

Now if you write

if f x y then ... else g x y ??

You have two problems.
First, you need to trust that f really is the function that computes 
equality (not the
function that checks whether x < y), and you don't know what to put 
instead of ??.

These problems can be solved with "certified booleans": the sumbool type.

When you write that f : forall x y:nat, {x=y}+{x<>y} **

you actually say that f will return values of the form "left ..."  
"right ...", which
almost the same, except for the names, as returning values of the form 
"true" or "false".
But you say more: you actually say that f x y may be of the form "left 
h", in in
this case h is a certificate that "x=y" really holds (it is an 
inhabitant of the type "x=y"),
or it may be of the form "right h", and in this case h is a certificate 
that "x<>y" holds.

So when you write **, you actually say that nat is one of those types 
for which there exists
an equality tests.

More over, you can now write pattern matching constructs on the value of f:

match f x y with
 left h => ...
| right h' => g x y h'
end

So the certificate h' can be passed on to g, thus making sure that g is 
only used when allowed.

So, the gain is that you can now program even more safely than in 
conventional typed functional
programming languages.  The price to pay is that you have to make a 
distinction in you head
between "Properties-as-types" which may hold or not, but can't be tested 
in a conditional statement,
and things that you can really compute, like the equality test between 
natural numbers, or
strings.  In your case, you can't write "if A=B then ... else ..." but 
you can write
"if string_eq_dec A B then ... else ..." if string_eq_dec has the type 
forall x y:string,{x=y}+{x<>y}

Now, with the help of Coq notations, you can also choose to attach the 
notation "A ?= B" to
"string_eq_dec A B" and get to write "if A ?= B then ... else ...", 
which get closer to your
intuition.

It seems more complicated to use string_eq_dec instead of a function of type
string -> string -> bool
but in the long run, there are benefits to the former, which makes 
proofs easier.

In the "ssreflect" style, as proposed by Georges Gonthier, functions of 
boolean type
are more convenient to use that functions of sumbool type, but you need 
to use
the ssreflect infrastructure, which also requires some explaining.

I hope this helps,

Yves