The Coq mailing list

[Damien Pous <Damien.Pous AT inria.fr>]

Sebastien Briais also used the following trick:

Assume an arbitrary set and a list over that set, and consider the set
of elements of that list.

Variable U: Set.
Variable X: list U.
Goal forall x, In x U -> x = x.
...

Depending on what you want to do, this might do the job.

Damien


2011/5/6 Vincent 
<vincent.siles AT gmail.com>:
> Hi Gyesik,
> I think the two usual ways to do this in Coq is to use the Finite
> predicate (Finite_sets.v),
> or to use the FSet Module interface.
>
> There are some new attempts to define Finite sets with Co-Inductive or
> Accessibility-like
> predicates, but they are still under investigation, and they are not
> in the stdlib.
>
> Cheers,
> Vincent
>
>
> 2011/5/6 Gyesik Lee 
> <leegys AT gmail.com>:
>> Hi,
>>
>> many languages are based on a finite set of symbols.
>> I am wondering how to represent phrases such as "Let L be a finite set
>> of constants".
>> On paper, we usually say, L is indexed by numbers less than a natural 
>> number.
>> Is there a simple, intuitive way to do the same thing in Coq?
>> Any help will be appreciated.
>>
>> Gyesik
>>
>