The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

Hi,


> (if string_dec s0 s0 then true else false) = false
>
> So I would expect that,
>
> assert (string_dec s0 s0 = true)
>
> also would. However it yields: The term "true" has type "bool" while it is
> expected to have type "{s0 = s0} + {s0 <> s0}".

string_dec a b indeed has type {a = b} + {a <> b} (called sumbool
iirc), which is an inductive with two constructors. Since if .. then
... else ... seems to work with any type with two constructors (check
the result of if 0 then true else false) your expression reduces to
false. However, you cannot assert string_dec s0 s0 = true, because of
the type mismatch. You have to use a coercion from the sumbool type to
bool.

> Furthermore, it looks like Coq is not able to compute the result of
> "string_dec s0 s0", to the fairly obvious answer true. (it's obvious...
> right? :))

In this case s0 is a variable, and Coq cannot reduce string_dec s0 s0
to "true" (the left-constructor of {a=b}+{a<>b}) by computation. You
have to prove that forall s, string_dec x x = "true".

> This is surprising to me since I've been using the following function for
> quite a while now, and I never stumbled across such thing.
>
> Definition beq_ident id1 id2 : bool :=
>   match id1, id2 with
>     | Ident str1, Ident str2    => match string_dec str1 str2 with
>                                       | left _ => true
>                                       | right _ => false
>                                    end
>   end.
>
> Evaluating it, gives what one would expect....
>
> Definition X := Ident "foo".
> Definition Y := Ident "bar".
> Definition f x y : bool := beq_ident x y.
> Eval compute in f X Y.   (*yields false, as expected.*)

In this case, X and Y are closed terms, not variables, so the
reduction may proceed. But for your particular goal, you need to use a
theorem, since you are dealing with abstract variables.

With best regards,
Thomas