The Coq mailing list

[Benjamin Werner <benjamin.werner AT inria.fr>]

Hi,

I am not totally sure of what you want to do.

Indeed, you need to know somehow that equality on strings is
decidable, as explained in other responses.

But also, in this example, the equality test can return false for x  
and y *only*
if you are sure x and y are different, which is not specified here.

In particular, you cannot, in the logic, talk about the identifiers of  
Coq
itself (if that was what you had in mind). Nor can you prove:

forall x y : string, x<>y

(fortunately, since this would immediately lead to an inconsistency).

Cheers,


Benjamin


Le 16 janv. 08 à 20:18, Theodoros G. Tsokos a écrit :

> Dear all,
>
> I'm having the following definition (representing identifiers of a  
> language)
>
> Variable string : Type.
> Variables x y z : string.
>
> I'm trying to find a way to compare the above strings, that is the  
> identifiers themselves, not their values, and get a boolean number  
> as an output. That is, something like:
>
> Variables A B : string.
> if (A=B) then true else false.
>
> where :
> for A= x and B=x it'll give me true, but for A=x and B=y it'll give  
> me false.
>
> I tried to use sumbool, like implemented in Yves Bertot's Semantics  
> Survey [1] :
> Variable string_dec : forall a b:string, {a=b}+{a<>b}
>
> but I got really confused.
>
> Thank you very much in advance for your time and help. It's probably  
> a trivial solution so apologize for using the list for something  
> like that.
>
> Regards,
> Theo.
>
> [1] http://coq.inria.fr/contribs/Semantics_survey.html
>
> --
> | Theodoros G. Tsokos                                      |
> | http://www.cs.bham.ac.uk/~txt                            ;|
> | School of Computer Science, The University of Birmingham |
> | Edgbaston, Birmingham, B15 2TT, United Kingdom           |
> | -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- |
> | "The freedom of speech includes the freedom to shut up"  |
> | -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- |
> | "Democracy: the freedom to say whatever one wants and    |
> | the capital to implement whatever it wants"              |
> --
>
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>         http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club