The Coq mailing list

[Andrew McCreight <andrew.mccreight AT yale.edu>]

What you want can't be done in the logic (CiC).  You could probably write 
a tactic to do that, but you can't reason about tactics, so that probably 
isn't useful.

In the metalogic of Twelf you can pattern match against variables, but 
that's fairly unusual.

-Andrew

On Wed, 16 Jan 2008, Theodoros G. Tsokos wrote:

> 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