The Coq mailing list

[Nuno Gaspar <nmpgaspar AT gmail.com>]

Hello fellas,

I've a question about what looks like (to me at least :)) a weird behavior from string_dec.

Let's see, as expected the following typechecks properly: 

(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}".

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? :))

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.*)

I would appreciate some lights in this subject please!

Just to give some context: I have the following hypothesis in my context, and I would expect that the tactic congruence would solve my goal, but no luck. I just assumed that I needed a simple simpl in H, but nope...I then started a few experiments with string_dec and got stuck.

H: (if string_dec s0 s0 then true else false) = false

Thank you.

--
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.