Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Facts about Ensembles

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Facts about Ensembles


Chronological Thread 
  • From: Guillaume Melquiond <guillaume.melquiond AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Facts about Ensembles
  • Date: Wed, 09 Jul 2014 15:37:02 +0200

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.

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

Best regards,

Guillaume



Archive powered by MHonArc 2.6.18.

Top of Page