The Coq mailing list

[Daniil Frumin <difrumin AT gmail.com>]

Thanks everyone for the replies!

On Wed, Jul 9, 2014 at 3:37 PM, Guillaume Melquiond
<guillaume.melquiond AT inria.fr>
 wrote:
> On 09/07/2014 15:11, Daniil Frumin wrote:
>>
>> Hi, all
>>
>> I was just curious about lack of facts for the Ensembles:
>> http://coq.inria.fr/stdlib/Coq.Sets.Ensembles.html
>>
>> Surely, there are a lot of small (but useful) theorems to state about
>> sets.
>
>
> Two disclaimers:
>
> 1. The theories from Sets were written almost twenty years ago, and they
> have not seen much love since then. So do not expect too much from them.
>
> 2. The Ensembles.v file only gives the basic definitions. See the other
> files of the Sets directory for the theorems.
>

Thanks! It was stupid of me not to look at other files, and it seems that
Constructive_sets provides at least some of the theorems I needed.


>
>> Another thing I was actually wondering about, is the possibility of
>> having rewrites using the Same_set as justifications.
>> I mean going from
>>
>> Г, Same_set A B, In A x |- _
>>
>> to
>>
>> Г, Same_set A B, In B x |- _
>>
>>
>> I am not very familiar with Ltac to write it myself, but it does make
>> sense to me.
>
>
> This kind of transformation is pointless. Because of the axiom
> Extensionality_Ensembles, you have A = B as soon as you have Same_set A B.
>
> So just forget about Same_set and always use plain equality instead. That
> way you will not have to learn about setoid rewriting (which is the modern
> way of dealing with the kind of rewriting you expect).
>

I know about setoids, but I didn't find a setoid typeclass instance :(

> Best regards,
>
> Guillaume



-- 
Sincerely yours,
-- Daniil