coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Facts about Ensembles, Daniil Frumin, 07/09/2014
- Re: [Coq-Club] Facts about Ensembles, Amin Timany, 07/09/2014
- Re: [Coq-Club] Facts about Ensembles, Guillaume Melquiond, 07/09/2014
- Re: [Coq-Club] Facts about Ensembles, Robbert Krebbers, 07/09/2014
- Re: [Coq-Club] Facts about Ensembles, Daniil Frumin, 07/10/2014
Archive powered by MHonArc 2.6.18.